awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Reflection
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
F : Dual R M
hF : MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ
y : M
hy : Membership.mem (γ := Submodule R M) (span R Φ) y
hy' :
  Membership.mem (γ := Set ↥(span R Φ)) (range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯))
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy)
⊢ Membership.mem (γ := Set ↥(span R Φ)) {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy)

Tactic:
rw [range_inclusion] at hy'

Premises used: Set.range_inclusion
-- Module: Mathlib.LinearAlgebra.Reflection
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
F : Dual R M
hF : MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ
y : M
hy : Membership.mem (γ := Submodule R M) (span R Φ) y
hy' : y ∈ Φ
rw :
  Membership.mem (α := ↥(span R Φ)) (γ := Set ↥(span R Φ)) {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}
    ((preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F) :
          (a : ↥(span R Φ)) → ↥(span R Φ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy) :
      ↥(span R Φ))
⊢ Membership.mem (α := ↥(span R Φ)) (γ := Set ↥(span R Φ)) (range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯))
    ((preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F) :
          (a : ↥(span R Φ)) → ↥(span R Φ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy) :
      ↥(span R Φ))

Tactic:
rw [range_inclusion]

Premises used: Set.range_inclusion
-- Module: Mathlib.LinearAlgebra.Reflection
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
F : Dual R M
hF : MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ
y : M
hy : Membership.mem (γ := Submodule R M) (span R Φ) y
hy' : y ∈ Φ
⊢ Membership.mem (α := ↥(span R Φ)) (γ := Set ↥(span R Φ)) {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}
    ((preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F) :
          (a : ↥(span R Φ)) → ↥(span R Φ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy) :
      ↥(span R Φ))

Tactic:
hF hy'

Premises used: Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.Reflection
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
F : Dual R M
hF : MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ
y : M
hy : Membership.mem (γ := Submodule R M) (span R Φ) y
hy' : y ∈ Φ
⊢ Membership.mem (α := ↥(span R Φ)) (γ := Set ↥(span R Φ)) {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}
    ((preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F) :
          (a : ↥(span R Φ)) → ↥(span R Φ))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy) :
      ↥(span R Φ))

Tactic:
exact hF hy'
-- Module: Mathlib.LinearAlgebra.Reflection
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
⊢ ∀ {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'
-- Module: Mathlib.LinearAlgebra.Reflection
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
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 Φ))
        Φ' Φ'
⊢ 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 Φ))

Tactic:
eq_of_preReflection_mapsTo hΦ'₁ hΦ'₂ hf₁ (this hf₂) hg₁ (this hg₂)

Premises used: Module.Dual.eq_of_preReflection_mapsTo
-- Module: Mathlib.LinearAlgebra.Reflection
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
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 Φ))
        Φ' Φ'
⊢ 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 Φ))

Tactic:
exact eq_of_preReflection_mapsTo hΦ'₁ hΦ'₂ hf₁ (this hf₂) hg₁ (this hg₂)

Premises used: Module.Dual.eq_of_preReflection_mapsTo
-- Module: Mathlib.LinearAlgebra.Reflection
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
⊢ (⇑(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:
simp
-- Module: Mathlib.LinearAlgebra.Reflection
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
rw₅ rw₆ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 z = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 4 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)

Tactic:
rw [smul_smul, hgxfy, smul_smul, ← Nat.cast_smul_eq_nsmul R (2 * 2), show 2 * 2 = 4 from rfl,
        Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, HMul.hMul, smul_smul, Nat.cast_smul_eq_nsmul, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Reflection
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)

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]
-- Module: Mathlib.LinearAlgebra.Reflection
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)
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)))
⊢ (⇑(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:
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]

Premises used: neg_sub, map_sub, Module.reflection_apply_self, Function.iterate_succ', two_smul, map_add, LinearEquiv.trans_apply, smul_neg, map_neg, smul_sub, add_smul, Function.comp_apply, Module.reflection_apply, map_nsmul, smul_add, map_smul
-- Module: Mathlib.LinearAlgebra.Reflection
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)
⊢ 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:
abel
-- Module: Mathlib.LinearAlgebra.Reflection
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)
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)
⊢ (⇑(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)

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

Premises used: neg_sub, map_sub, Module.reflection_apply_self, Function.iterate_succ', two_smul, map_add, LinearEquiv.trans_apply, smul_neg, map_neg, smul_sub, add_smul, Function.comp_apply, Module.reflection_apply, map_nsmul, smul_add, map_smul
-- Module: Mathlib.LinearAlgebra.Reflection
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
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
⊢ Set.Infinite.{u_2} (α := M) (range fun (n : ℕ) ↦ (⇑(reflection hgy ≪≫ₗ reflection hfx) : (a : M) → M)^[n] 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

Tactic:
simp only [reflection_reflection_iterate hfx hgy hgxfy, infinite_range_add_nsmul_iff, sub_ne_zero]

Premises used: sub_ne_zero, Module.reflection_reflection_iterate, infinite_range_add_nsmul_iff
-- Module: Mathlib.LinearAlgebra.Reflection
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
⊢ 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

Premises used: two_smul, two_zsmul
-- Module: Mathlib.LinearAlgebra.Reflection
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 (α := ℤ) 2 x = HSMul.hSMul (α := ℤ) 2 y
⊢ x = y

Tactic:
smul_right_injective _ two_ne_zero h

Premises used: smul_right_injective, two_ne_zero
-- Module: Mathlib.LinearAlgebra.Reflection
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 (α := ℤ) 2 x = HSMul.hSMul (α := ℤ) 2 y
⊢ x = y

Tactic:
exact smul_right_injective _ two_ne_zero h

Premises used: smul_right_injective, two_ne_zero
-- Module: Mathlib.LinearAlgebra.Reflection
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 ∈ Φ
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
⊢ x = 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