bump to nightly-2023-02-28-03

mathlib commit leanprover-community/mathlib@9da1b35

Mathbin/Algebra/Module/Equiv.lean

@@ -5,7 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
   Frédéric Dupuis, Heather Macbeth
 
 ! This file was ported from Lean 3 source module algebra.module.equiv
-! leanprover-community/mathlib commit fac369018417f980cec5fcdafc766a69f88d8cfe
+! leanprover-community/mathlib commit ea94d7cd54ad9ca6b7710032868abb7c6a104c9c
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -451,7 +451,8 @@ variable (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ
 include σ₃₁
 
 #print LinearEquiv.trans /-
--- Note: The linter thinks the `ring_hom_comp_triple` argument is doubled -- it is not.
+-- Note: the `ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁` is unused, but is convenient to carry around
+-- implicitly for lemmas like `linear_equiv.self_trans_symm`.
 /-- Linear equivalences are transitive. -/
 @[trans, nolint unused_arguments]
 def trans : M₁ ≃ₛₗ[σ₁₃] M₃ :=

Mathbin/Algebra/Order/Ring/Canonical.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.order.ring.canonical
-! leanprover-community/mathlib commit a1b3559280c8e09220759127b400d1b02d7ac071
+! leanprover-community/mathlib commit 824f9ae93a4f5174d2ea948e2d75843dd83447bb
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -145,6 +145,11 @@ instance (priority := 100) toCovariantClassMulLE : CovariantClass α α (· * ·
   apply self_le_add_right
 #align canonically_ordered_comm_semiring.to_covariant_mul_le CanonicallyOrderedCommSemiring.toCovariantClassMulLE
 
+-- see Note [lower instance priority]
+instance (priority := 100) toOrderedCommMonoid : OrderedCommMonoid α :=
+  { ‹CanonicallyOrderedCommSemiring α› with mul_le_mul_left := fun _ _ => mul_le_mul_left' }
+#align canonically_ordered_comm_semiring.to_ordered_comm_monoid CanonicallyOrderedCommSemiring.toOrderedCommMonoid
+
 #print CanonicallyOrderedCommSemiring.toOrderedCommSemiring /-
 -- see Note [lower instance priority]
 instance (priority := 100) toOrderedCommSemiring : OrderedCommSemiring α :=

Mathbin/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, David Kurniadi Angdinata
 
 ! This file was ported from Lean 3 source module algebraic_geometry.elliptic_curve.weierstrass
-! leanprover-community/mathlib commit 67f92b6f60865717e0811128b77d49ab4c07f7f1
+! leanprover-community/mathlib commit 03994e05d8bfc59a41d2ec99523d6553d21848ac
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -97,7 +97,7 @@ private unsafe def C_simp : tactic Unit :=
   sorry
 #align C_simp C_simp
 
-universe u v
+universe u v w
 
 variable {R : Type u}
 
@@ -256,13 +256,14 @@ theorem variableChange_Δ : (W.variableChange u r s t).Δ = ↑u⁻¹ ^ 12 * W.
 
 end VariableChange
 
+variable (A : Type v) [CommRing A] [Algebra R A] (B : Type w) [CommRing B] [Algebra R B]
+  [Algebra A B] [IsScalarTower R A B]
+
 section BaseChange
 
 /-! ### Base changes -/
 
 
-variable (A : Type v) [CommRing A] [Algebra R A]
-
 /-- The Weierstrass curve over `R` base changed to `A`. -/
 @[simps]
 def baseChange : WeierstrassCurve A :=
@@ -333,6 +334,13 @@ theorem baseChange_Δ : (W.base_change A).Δ = algebraMap R A W.Δ :=
     map_simp
 #align weierstrass_curve.base_change_Δ WeierstrassCurve.baseChange_Δ
 
+theorem baseChange_self : W.base_change R = W := by ext <;> rfl
+#align weierstrass_curve.base_change_self WeierstrassCurve.baseChange_self
+
+theorem baseChange_baseChange : (W.base_change A).base_change B = W.base_change B := by
+  ext <;> exact (IsScalarTower.algebraMap_apply R A B _).symm
+#align weierstrass_curve.base_change_base_change WeierstrassCurve.baseChange_baseChange
+
 end BaseChange
 
 section TorsionPolynomial
@@ -491,6 +499,30 @@ theorem equation_iff_variableChange (x y : R) :
   ring1
 #align weierstrass_curve.equation_iff_variable_change WeierstrassCurve.equation_iff_variableChange
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported non-interactive tactic _private.272596109.map_simp -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported non-interactive tactic _private.272596109.map_simp -/
+theorem equation_iff_baseChange [Nontrivial A] [NoZeroSMulDivisors R A] (x y : R) :
+    W.Equation x y ↔ (W.base_change A).Equation (algebraMap R A x) (algebraMap R A y) :=
+  by
+  simp only [equation_iff]
+  refine' ⟨fun h => _, fun h => _⟩
+  ·
+    convert congr_arg (algebraMap R A) h <;>
+      · run_tac
+          map_simp
+        rfl
+  · apply NoZeroSMulDivisors.algebraMap_injective R A
+    run_tac
+      map_simp
+    exact h
+#align weierstrass_curve.equation_iff_base_change WeierstrassCurve.equation_iff_baseChange
+
+theorem equation_iff_baseChange_of_baseChange [Nontrivial B] [NoZeroSMulDivisors A B] (x y : A) :
+    (W.base_change A).Equation x y ↔
+      (W.base_change B).Equation (algebraMap A B x) (algebraMap A B y) :=
+  by rw [equation_iff_base_change (W.base_change A) B, base_change_base_change]
+#align weierstrass_curve.equation_iff_base_change_of_base_change WeierstrassCurve.equation_iff_baseChange_of_baseChange
+
 /-! ### Nonsingularity of Weierstrass curves -/
 
 
@@ -574,6 +606,32 @@ theorem nonsingular_iff_variableChange (x y : R) :
   congr 4 <;> ring1
 #align weierstrass_curve.nonsingular_iff_variable_change WeierstrassCurve.nonsingular_iff_variableChange
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported non-interactive tactic _private.272596109.map_simp -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported non-interactive tactic _private.272596109.map_simp -/
+theorem nonsingular_iff_baseChange [Nontrivial A] [NoZeroSMulDivisors R A] (x y : R) :
+    W.Nonsingular x y ↔ (W.base_change A).Nonsingular (algebraMap R A x) (algebraMap R A y) :=
+  by
+  rw [nonsingular_iff, nonsingular_iff, and_congr <| W.equation_iff_base_change A x y]
+  refine'
+    ⟨Or.imp (not_imp_not.mpr fun h => _) (not_imp_not.mpr fun h => _),
+      Or.imp (not_imp_not.mpr fun h => _) (not_imp_not.mpr fun h => _)⟩
+  any_goals apply NoZeroSMulDivisors.algebraMap_injective R A;
+    run_tac
+      map_simp;
+    exact h
+  any_goals
+    convert congr_arg (algebraMap R A) h <;>
+      · run_tac
+          map_simp
+        rfl
+#align weierstrass_curve.nonsingular_iff_base_change WeierstrassCurve.nonsingular_iff_baseChange
+
+theorem nonsingular_iff_baseChange_of_baseChange [Nontrivial B] [NoZeroSMulDivisors A B] (x y : A) :
+    (W.base_change A).Nonsingular x y ↔
+      (W.base_change B).Nonsingular (algebraMap A B x) (algebraMap A B y) :=
+  by rw [nonsingular_iff_base_change (W.base_change A) B, base_change_base_change]
+#align weierstrass_curve.nonsingular_iff_base_change_of_base_change WeierstrassCurve.nonsingular_iff_baseChange_of_baseChange
+
 theorem nonsingular_zero_of_Δ_ne_zero (h : W.Equation 0 0) (hΔ : W.Δ ≠ 0) : W.Nonsingular 0 0 :=
   by
   simp only [equation_zero, nonsingular_zero] at *

Mathbin/All.lean

@@ -1901,6 +1901,7 @@ import Mathbin.LinearAlgebra.Basic
 import Mathbin.LinearAlgebra.Basis
 import Mathbin.LinearAlgebra.Basis.Bilinear
 import Mathbin.LinearAlgebra.BilinearForm
+import Mathbin.LinearAlgebra.BilinearForm.TensorProduct
 import Mathbin.LinearAlgebra.BilinearMap
 import Mathbin.LinearAlgebra.Charpoly.Basic
 import Mathbin.LinearAlgebra.Charpoly.ToMatrix

Mathbin/Analysis/Analytic/Composition.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johan Commelin
 
 ! This file was ported from Lean 3 source module analysis.analytic.composition
-! leanprover-community/mathlib commit b2ff9a3d7a15fd5b0f060b135421d6a89a999c2f
+! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -497,8 +497,8 @@ theorem comp_summable_nNReal (q : FormalMultilinearSeries 𝕜 F G) (p : FormalM
   /- This follows from the fact that the growth rate of `‖qₙ‖` and `‖pₙ‖` is at most geometric,
     giving a geometric bound on each `‖q.comp_along_composition p op‖`, together with the
     fact that there are `2^(n-1)` compositions of `n`, giving at most a geometric loss. -/
-  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min ENNReal.zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩
-  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min ENNReal.zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩
+  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hq) with ⟨rq, rq_pos, hrq⟩
+  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 (lt_min zero_lt_one hp) with ⟨rp, rp_pos, hrp⟩
   simp only [lt_min_iff, ENNReal.coe_lt_one_iff, ENNReal.coe_pos] at hrp hrq rp_pos rq_pos
   obtain ⟨Cq, hCq0, hCq⟩ : ∃ Cq > 0, ∀ n, ‖q n‖₊ * rq ^ n ≤ Cq :=
     q.nnnorm_mul_pow_le_of_lt_radius hrq.2

Mathbin/Analysis/NormedSpace/Enorm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.normed_space.enorm
-! leanprover-community/mathlib commit 17ef379e997badd73e5eabb4d38f11919ab3c4b3
+! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -85,7 +85,7 @@ theorem map_smul (c : 𝕜) (x : V) : e (c • x) = ‖c‖₊ * e x :=
       _ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) := _
       _ = e (c • x) := _
 
-    · exact ENNReal.mul_le_mul le_rfl (e.map_smul_le' _ _)
+    · exact mul_le_mul_left' (e.map_smul_le' _ _) _
     ·
       rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top,
           one_mul] <;>

Mathbin/Analysis/NormedSpace/LpSpace.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 
 ! This file was ported from Lean 3 source module analysis.normed_space.lp_space
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -679,7 +679,7 @@ theorem norm_const_smul (hp : p ≠ 0) {c : 𝕜} (f : lp E p) : ‖c • f‖ =
 instance [Fact (1 ≤ p)] : NormedSpace 𝕜 (lp E p)
     where norm_smul_le c f :=
     by
-    have hp : 0 < p := ennreal.zero_lt_one.trans_le (Fact.out _)
+    have hp : 0 < p := zero_lt_one.trans_le (Fact.out _)
     simp [norm_const_smul hp.ne']
 
 variable {𝕜' : Type _} [NormedField 𝕜']
@@ -1072,7 +1072,7 @@ protected theorem norm_compl_sum_single (hp : 0 < p.toReal) (f : lp E p) (s : Fi
 protected theorem hasSum_single [Fact (1 ≤ p)] (hp : p ≠ ⊤) (f : lp E p) :
     HasSum (fun i : α => lp.single p i (f i : E i)) f :=
   by
-  have hp₀ : 0 < p := ennreal.zero_lt_one.trans_le (Fact.out _)
+  have hp₀ : 0 < p := zero_lt_one.trans_le (Fact.out _)
   have hp' : 0 < p.to_real := ENNReal.toReal_pos hp₀.ne' hp
   have := lp.hasSum_norm hp' f
   rw [HasSum, Metric.tendsto_nhds] at this⊢
@@ -1107,7 +1107,7 @@ open Topology uniformity
 /-- The coercion from `lp E p` to `Π i, E i` is uniformly continuous. -/
 theorem uniformContinuous_coe [_i : Fact (1 ≤ p)] : UniformContinuous (coe : lp E p → ∀ i, E i) :=
   by
-  have hp : p ≠ 0 := (ennreal.zero_lt_one.trans_le _i.elim).ne'
+  have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
   rw [uniformContinuous_pi]
   intro i
   rw [normed_add_comm_group.uniformity_basis_dist.uniform_continuous_iff
@@ -1139,7 +1139,7 @@ theorem sum_rpow_le_of_tendsto (hp : p ≠ ∞) {C : ℝ} {F : ι → lp E p} (h
     {f : ∀ a, E a} (hf : Tendsto (id fun i => F i : ι → ∀ a, E a) l (𝓝 f)) (s : Finset α) :
     (∑ i : α in s, ‖f i‖ ^ p.toReal) ≤ C ^ p.toReal :=
   by
-  have hp' : p ≠ 0 := (ennreal.zero_lt_one.trans_le _i.elim).ne'
+  have hp' : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
   have hp'' : 0 < p.to_real := ENNReal.toReal_pos hp' hp
   let G : (∀ a, E a) → ℝ := fun f => ∑ a in s, ‖f a‖ ^ p.to_real
   have hG : Continuous G := by
@@ -1164,7 +1164,7 @@ theorem norm_le_of_tendsto {C : ℝ} {F : ι → lp E p} (hCF : ∀ᶠ k in l, 
   rcases eq_top_or_lt_top p with (rfl | hp)
   · apply norm_le_of_forall_le hC
     exact norm_apply_le_of_tendsto hCF hf
-  · have : 0 < p := ennreal.zero_lt_one.trans_le _i.elim
+  · have : 0 < p := zero_lt_one.trans_le _i.elim
     have hp' : 0 < p.to_real := ENNReal.toReal_pos this.ne' hp.ne
     apply norm_le_of_forall_sum_le hp' hC
     exact sum_rpow_le_of_tendsto hp.ne hCF hf

Mathbin/Analysis/SpecialFunctions/Pow.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Sébasti
   Rémy Degenne, David Loeffler
 
 ! This file was ported from Lean 3 source module analysis.special_functions.pow
-! leanprover-community/mathlib commit 92ca63f0fb391a9ca5f22d2409a6080e786d99f7
+! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -2295,7 +2295,7 @@ theorem le_rpow_self_of_one_le {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (h_one_
 theorem rpow_pos_of_nonneg {p : ℝ} {x : ℝ≥0∞} (hx_pos : 0 < x) (hp_nonneg : 0 ≤ p) : 0 < x ^ p :=
   by
   by_cases hp_zero : p = 0
-  · simp [hp_zero, ENNReal.zero_lt_one]
+  · simp [hp_zero, zero_lt_one]
   · rw [← Ne.def] at hp_zero
     have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
     rw [← zero_rpow_of_pos hp_pos]
@@ -2327,7 +2327,7 @@ theorem rpow_le_one {x : ℝ≥0∞} {z : ℝ} (hx : x ≤ 1) (hz : 0 ≤ z) : x
 theorem rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz : z < 0) : x ^ z < 1 :=
   by
   cases x
-  · simp [top_rpow_of_neg hz, ENNReal.zero_lt_one]
+  · simp [top_rpow_of_neg hz, zero_lt_one]
   · simp only [some_eq_coe, one_lt_coe_iff] at hx
     simp [coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
       NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]
@@ -2336,7 +2336,7 @@ theorem rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz
 theorem rpow_le_one_of_one_le_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (hz : z < 0) : x ^ z ≤ 1 :=
   by
   cases x
-  · simp [top_rpow_of_neg hz, ENNReal.zero_lt_one]
+  · simp [top_rpow_of_neg hz, zero_lt_one]
   · simp only [one_le_coe_iff, some_eq_coe] at hx
     simp [coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
       NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]

Mathbin/Analysis/SpecificLimits/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johannes Hölzl, Yury G. Kudryashov, Patrick Massot
 
 ! This file was ported from Lean 3 source module analysis.specific_limits.basic
-! leanprover-community/mathlib commit b2ff9a3d7a15fd5b0f060b135421d6a89a999c2f
+! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -561,7 +561,7 @@ theorem exists_pos_tsum_mul_lt_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) {
   refine' ⟨fun i => δ' i / max 1 (w i), fun i => div_pos (Hpos _) (this i), _⟩
   refine' lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i => _) Hsum
   rw [coe_div (this i).ne']
-  refine' mul_le_of_le_div' (ENNReal.mul_le_mul le_rfl <| ENNReal.inv_le_inv.2 _)
+  refine' mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 _) _)
   exact coe_le_coe.2 (le_max_right _ _)
 #align ennreal.exists_pos_tsum_mul_lt_of_countable ENNReal.exists_pos_tsum_mul_lt_of_countable
 

Mathbin/Data/Finmap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sean Leather, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.finmap
-! leanprover-community/mathlib commit 4c19a16e4b705bf135cf9a80ac18fcc99c438514
+! leanprover-community/mathlib commit c3fc15b26b3ff8958ec3e5711177a9ae3d5c45b7
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -456,22 +456,22 @@ def foldl {δ : Type w} (f : δ → ∀ a, β a → δ)
 #print Finmap.any /-
 /-- `any f s` returns `tt` iff there exists a value `v` in `s` such that `f v = tt`. -/
 def any (f : ∀ x, β x → Bool) (s : Finmap β) : Bool :=
-  s.foldl (fun x y z => x ∨ f y z)
+  s.foldl (fun x y z => x || f y z)
     (by
       intros
-      simp [or_right_comm])
+      simp_rw [Bool.or_assoc, Bool.or_comm])
     false
 #align finmap.any Finmap.any
 -/
 
 #print Finmap.all /-
 /-- `all f s` returns `tt` iff `f v = tt` for all values `v` in `s`. -/
 def all (f : ∀ x, β x → Bool) (s : Finmap β) : Bool :=
-  s.foldl (fun x y z => x ∧ f y z)
+  s.foldl (fun x y z => x && f y z)
     (by
       intros
-      simp [and_right_comm])
-    false
+      simp_rw [Bool.and_assoc, Bool.and_comm])
+    true
 #align finmap.all Finmap.all
 -/
 

Mathbin/Data/Int/Units.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.int.units
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit 45a1ada01ed893722d0f8d15b9e44270996515d5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -103,6 +103,11 @@ theorem eq_one_or_neg_one_of_mul_eq_one' {z w : ℤ} (h : z * w = 1) :
 #align int.eq_one_or_neg_one_of_mul_eq_one' Int.eq_one_or_neg_one_of_mul_eq_one'
 -/
 
+theorem eq_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = w :=
+  (eq_one_or_neg_one_of_mul_eq_one' h).elim (fun h => h.1.trans h.2.symm) fun h =>
+    h.1.trans h.2.symm
+#align int.eq_of_mul_eq_one Int.eq_of_mul_eq_one
+
 #print Int.mul_eq_one_iff_eq_one_or_neg_one /-
 theorem mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 :=
   by