awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Finite.{u_2 + 1} (↑Φ : Type u_2)
hx : Membership.mem (γ := Submodule R M) (span R Φ) x
f g : Dual R M
hf₁ : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hf₂ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hg₁ : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hg₂ : MapsTo (⇑(preReflection x g) : (a : M) → M) Φ Φ
Φ' : Set ↥(span R Φ) := range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯)
hΦ'₁ : Φ'.Finite
hΦ'₂ : Eq (α := Submodule R ↥(span R Φ)) (span R Φ') ⊤
x' : ↥(span R Φ) := Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) x hx
⊢ Eq (α := Dual.{u_1, u_2} R ↥(span R Φ))
    ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) f :
      Dual.{u_1, u_2} R ↥(span R Φ))
    ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) g :
      Dual.{u_1, u_2} R ↥(span R Φ))
have this : ∀ {F : Dual R M},
  MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ →
    MapsTo
      (⇑(preReflection x'
            ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F)) :
        (a : ↥(span R Φ)) → ↥(span R Φ))
      Φ' Φ'
Tactic: have this : ∀ {F : Dual R M}, MapsTo (preReflection x F) Φ Φ →
      MapsTo (preReflection x' ((span R Φ).subtype.dualMap F)) Φ' Φ' := by
    intro F hF ⟨y, hy⟩ hy'
    simp only [Φ'] at hy' ⊢
    rw [range_inclusion] at hy'
    simp only [SetLike.coe_sort_coe, mem_setOf_eq] at hy' ⊢
    rw [range_inclusion]
    exact hF hy'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
z : M
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
have rw : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) • z =
  HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
Tactic: rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
z : M
rw :
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) • z =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
Tactic: rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
z : M
rw :
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) • z =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HMul.hMul (α := ℕ) 2 2 • z
Tactic: rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
z : M
rw :
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) • z =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HMul.hMul (α := ℕ) 2 2 • z
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(HMul.hMul (α := ℕ) 2 2) : R) z
Tactic: rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
z : M
rw :
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) • z =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HMul.hMul (α := ℕ) 2 2 • z
rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(HMul.hMul (α := ℕ) 2 2) : R) z
rw₄ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑4 : R) z
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
have rw₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z
Tactic: rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n + 1] y =
    y +
      (n + 1) •
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
have hz : ∀ (z : M),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
Tactic: have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
      intro z
      rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
ih :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
hz :
  ∀ (z : M),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : M) → R) x : R) z) =
      HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := ℕ) 2 z)
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n + 1] y =
    y +
      (n + 1) •
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
have succ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - y +
    (-(n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x) -
        (n • y + n • y + (n • y + n • y) -
          (n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x +
              n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x +
            (n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x +
              n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x))) -
      (n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - n • y +
        (n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - n • y))) =
  y +
    (n • HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x +
        HSMul.hSMul (α := ℕ) 1 (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x) -
      (n • y + HSMul.hSMul (α := ℕ) 1 y + (n • y + HSMul.hSMul (α := ℕ) 1 y)))
Tactic: simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
      LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
      map_nsmul, map_smul, smul_neg, hz, add_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
have zero : (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[0] y =
  y +
    HSMul.hSMul (α := ℕ) 0
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
      intro z
      rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
    simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
      LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
      map_nsmul, map_smul, smul_neg, hz, add_smul]
    abel
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgxfy : HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
n : ℕ
zero :
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[0] y =
    y +
      HSMul.hSMul (α := ℕ) 0
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
    y +
      n • (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
have succ : ∀ (n : ℕ)
  (ih :
    (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y =
      y +
        n •
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x -
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)),
  (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n + 1] y =
    y +
      (n + 1) •
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    have hz : ∀ z : M, f y • g x • z = 2 • 2 • z := by
      intro z
      rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]
    simp only [iterate_succ', comp_apply, ih, two_smul, smul_sub, smul_add, map_add,
      LinearEquiv.trans_apply, reflection_apply_self, map_neg, reflection_apply, neg_sub, map_sub,
      map_nsmul, map_smul, smul_neg, hz, add_smul]
    abel
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
h : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
⊢ x = y
have h₁ : HSMul.hSMul (α := ℤ) 2 x = HSMul.hSMul (α := ℤ) 2 y
Tactic: rw [hfy, two_smul R x, two_smul R y, ← two_zsmul, ← two_zsmul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
⊢ x = y
have suffices : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
Tactic: suffices h : f y • x = (2 : R) • y by
    rw [hfy, two_smul R x, two_smul R y, ← two_zsmul, ← two_zsmul] at h
    exact smul_right_injective _ two_ne_zero h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hΦ : Φ.Finite
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
have contrapose! : ∀ (hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y),
  Φ.Infinite
Tactic: contrapose! hΦ
Cleared hypotheses: hΦ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
⊢ HMul.hMul (α := R) (β := R) ((f : (a : M) → R) y : R) ((g : (a : M) → R) x : R) = 4
have rw : HMul.hMul (α := R) 2 2 = 4
Tactic: rw [hfy, hgx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
⊢ HMul.hMul (α := R) 2 2 = 4
have norm_cast : Eq.{u_1 + 1} (α := R) (↑(HMul.hMul (α := ℕ) 2 2) : R) 4
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
⊢ Φ.Infinite
have apply : (range fun (n : ℕ) ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y) ⊆ Φ
Tactic: apply ((infinite_range_reflection_reflection_iterate_iff hfx hgy
    (by rw [hfy, hgx]; norm_cast)).mpr hΦ).mono
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
⊢ (range fun (n : ℕ) ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y) ⊆ Φ
have rw : ∀ (y_1 : ℕ), (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[y_1] y ∈ Φ
Tactic: rw [range_subset_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst_3 : IsAddTorsionFree M
Φ : Set M
hfx : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) x : R) (2 : R)
hgy : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) y : R) (2 : R)
hgx : Eq.{u_1 + 1} (α := R) ((g : (a : M) → R) x : R) (2 : R)
hfy : Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) y : R) (2 : R)
hxfΦ : MapsTo (⇑(preReflection x f) : (a : M) → M) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g) : (a : M) → M) Φ Φ
hyΦ : y ∈ Φ
hΦ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((f : (a : M) → R) y : R) x ≠ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 y
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈ Φ
have rw : (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] y ∈
  (comp (β := M) (⇑(reflection hfx) : (a : M) → M) (⇑(reflection hgy) : (a : M) → M))^[n] '' Φ
Tactic: rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo hfx hxfΦ).comp
    (bijOn_reflection_of_mapsTo hgy hygΦ)).image_eq n]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
⊢ c i = c j
have e_a : i = j
Tactic: congr