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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
h :
  ∀ (x_1 : M),
    Eq (α := M)
      ((LinearMap.smulRight (f - g) x ∘ₗ
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) :
            (a : M) → M)
          x_1 :
        M)
      ((0 : (a : M) → M) x_1 : M)
⊢ Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0

Tactic:
ext
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
x_1 : M
⊢ Eq (α := M)
    ((LinearMap.smulRight (f - g) x ∘ₗ
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) :
          (a : M) → M)
        x_1 :
      M)
    ((0 : (a : M) → M) x_1 : M)

Tactic:
simp [hf₁, hg₁]
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
⊢ Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0

Tactic:
have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
        ext; simp [hf₁, hg₁]
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
ih :
  (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this :
  Eq (α := M →ₗ[R] M)
    (LinearMap.smulRight (f - g) x ∘ₗ
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x))
    0
succ :
  HMul.hMul (α := M →ₗ[R] M) LinearMap.id LinearMap.id +
        LinearMap.id * HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      (LinearMap.smulRight (f - g) x * LinearMap.id +
        LinearMap.smulRight (f - g) x *
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
⊢ (↑(u ^ (n + 1)) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)

Tactic:
rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]

Premises used: add_mul, LinearEquiv.coe_toLinearMap_mul, mul_add, pow_succ'
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
n : ℕ
zero :
  (↑(HPow.hPow (β := ℕ) u 0) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑0 : R) (LinearMap.smulRight (f - g) x)
succ :
  ∀ (n : ℕ)
    (ih :
      (↑(u ^ n) : M →ₗ[R] M) =
        LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)),
    (↑(u ^ (n + 1)) : M →ₗ[R] M) =
      LinearMap.id +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑(n + 1) : R) (LinearMap.smulRight (f - g) x)
⊢ (↑(u ^ n) : M →ₗ[R] M) =
    LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)

Tactic:
induction n with
    | zero => simp
    | succ n ih =>
      have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
        ext; simp [hf₁, hg₁]
      rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
      simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
        add_assoc, Nat.cast_succ, add_smul, one_smul]

Premises used: add_mul, Nat.cast_succ, Module.End.mul_eq_comp, LinearEquiv.coe_toLinearMap_mul, add_assoc, one_smul, add_smul, LinearMap.comp_id, mul_add, LinearMap.id_comp, add_zero, pow_succ'
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu : (↑u : M →ₗ[R] M) = LinearMap.id + LinearMap.smulRight (f - g) x
⊢ ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)

Tactic:
replace hu : ∀ (n : ℕ),
      ↑(u ^ n) = LinearMap.id (R := R) (M := M) + (n : R) • (f - g).smulRight x := by
    intro n
    induction n with
    | zero => simp
    | succ n ih =>
      have : ((f - g).smulRight x).comp ((n : R) • (f - g).smulRight x) = 0 := by
        ext; simp [hf₁, hg₁]
      rw [pow_succ', LinearEquiv.coe_toLinearMap_mul, ih, hu, add_mul, mul_add, mul_add]
      simp_rw [Module.End.mul_eq_comp, LinearMap.comp_id, LinearMap.id_comp, this, add_zero,
        add_assoc, Nat.cast_succ, add_smul, one_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
inst_3 : CharZero R
inst_4 : IsDomain R
inst_5 : IsTorsionFree R M
x : M
Φ : Set M
hΦ₁ : Φ.Finite
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this : IsOfFinOrder u
obtain : ∀ (n : ℕ) (hn₀ : 0 < n) (hn₁ : u ^ n = 1), f = g
⊢ f = g

Tactic:
obtain ⟨n, hn₀, hn₁⟩ := isOfFinOrder_iff_pow_eq_one.mp this

Premises used: Iff.mp, isOfFinOrder_iff_pow_eq_one
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : u ^ n = 1
⊢ (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id

Tactic:
replace hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id := LinearEquiv.toLinearMap_inj.mpr hn₁
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
this : IsOfFinOrder u
n : ℕ
hn₀ : 0 < n
hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id
⊢ f = g

Tactic:
simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n

Premises used: sub_eq_zero, LT.lt.ne'
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
suffices : IsOfFinOrder u
⊢ f = g

Tactic:
suffices IsOfFinOrder u by
    obtain ⟨n, hn₀, hn₁⟩ := isOfFinOrder_iff_pow_eq_one.mp this
    replace hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id := LinearEquiv.toLinearMap_inj.mpr hn₁
    simpa [hn₁, hn₀.ne', hx, sub_eq_zero] using hu n
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
⊢ IsOfFinOrder u

Tactic:
u.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo hΦ₁ hΦ₂ (hg₂.comp hf₂)

Premises used: LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo, Set.MapsTo.comp
-- 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
hΦ₂ : Eq (α := Submodule R M) (span R Φ) ⊤
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) Φ Φ
hx : x ≠ 0
u : M ≃ₗ[R] M := reflection hg₁ * reflection hf₁
hu :
  ∀ (n : ℕ),
    (↑(u ^ n) : M →ₗ[R] M) =
      LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x)
⊢ IsOfFinOrder u

Tactic:
exact u.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo hΦ₁ hΦ₂ (hg₂.comp hf₂)

Premises used: LinearEquiv.isOfFinOrder_of_finite_of_span_eq_top_of_mapsTo, Set.MapsTo.comp
-- 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
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)) ⋯)
rw :
  ∀ (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) Φ Φ),
    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 Φ))
⊢ 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:
rw [← finite_coe_iff] at hΦ₁

Premises used: Set.finite_coe_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
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)) ⋯)
⊢ Φ'.Finite

Tactic:
have hΦ'₁ : Φ'.Finite := finite_range (inclusion Submodule.subset_span)
-- 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
simp :
  Eq.{u_2 + 1} (α := Submodule R ↥(span R Φ)) (span R (range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯))) ⊤
⊢ Eq (α := Submodule R ↥(span R Φ)) (span R Φ') ⊤

Tactic:
simp only [Φ']
-- 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
rw : Eq.{u_2 + 1} (α := Submodule R ↥(span R Φ)) (span R {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(span R Φ)) (span R (range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯))) ⊤

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
⊢ Eq.{u_2 + 1} (α := Submodule R ↥(span R Φ)) (span R {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}) ⊤

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
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
⊢ Eq (α := Submodule R ↥(span R Φ)) (span R Φ') ⊤

Tactic:
have hΦ'₂ : span R Φ' = ⊤ := by
    simp only [Φ']
    rw [range_inclusion]
    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
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) Φ Φ
this :
  ∀ (y : M) (hy : Membership.mem (γ := Submodule R M) (span R Φ) y),
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy ∈ Φ' →
      Membership.mem (α := ↥(span R Φ)) Φ'
        ((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 Φ))
⊢ MapsTo
    (⇑(preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F)) :
      (a : ↥(span R Φ)) → ↥(span R Φ))
    Φ' Φ'

Tactic:
⟨y, 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
hF : MapsTo (⇑(preReflection x F) : (a : M) → M) Φ Φ
y : M
hy : Membership.mem (γ := Submodule R M) (span R Φ) y
hy' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R Φ) x) y hy ∈ Φ'
simp :
  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 Φ))
⊢ Membership.mem (α := ↥(span R Φ)) Φ'
    ((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:
simp only [Φ'] at hy' ⊢