awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 :
  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) +
      HAdd.hAdd (α := M →ₗ[R] M) (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)
⊢ 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)
have succ₁ : LinearMap.id +
      LinearMap.id ∘ₗ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
    HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x)
      (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)
Tactic: 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]
-- 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
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 :
  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) +
      HAdd.hAdd (α := M →ₗ[R] M) (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)
succ₁ :
  LinearMap.id +
        LinearMap.id ∘ₗ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
      HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x)
        (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)
⊢ 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)
have succ₂ : LinearMap.id + HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) (LinearMap.smulRight (f - g) x) +
    HAdd.hAdd (α := M →ₗ[R] M) (LinearMap.smulRight (f - g) x)
      (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)
Tactic: 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]
-- 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
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)
have 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)
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]
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
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)
⊢ (↑(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)
have 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)
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]
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
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
⊢ f = g
have 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)
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]
Cleared hypotheses: hu
-- 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
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
⊢ f = g
have obtain : ∀ (n : ℕ) (hn₀ : 0 < n) (hn₁ : u ^ n = 1), f = g
Tactic: obtain ⟨n, hn₀, hn₁⟩ := isOfFinOrder_iff_pow_eq_one.mp this
-- 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
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
⊢ f = g
have hn₂ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id
Tactic: replace hn₁ : (↑(u ^ n) : M →ₗ[R] M) = LinearMap.id := LinearEquiv.toLinearMap_inj.mpr hn₁
Cleared hypotheses: hn₁
-- 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
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)
⊢ f = g
have suffices : IsOfFinOrder u
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
-- 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
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)) ⋯)
⊢ 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 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 Φ))
Tactic: rw [← finite_coe_iff] at hΦ₁
Cleared hypotheses: hΦ₁, hx, f, g, hf₁, hf₂, hg₁, hg₂, Φ'
-- 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)) ⋯)
⊢ 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 hΦ'₁ : Φ'.Finite
Tactic: have hΦ'₁ : Φ'.Finite := finite_range (inclusion Submodule.subset_span)
-- 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
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 (range (inclusion (s := Φ) (t := (↑(span R Φ) : Set M)) ⋯))) ⊤
have rw : Eq.{u_2 + 1} (α := Submodule R ↥(span R Φ)) (span R {x : (↑(↑(span R Φ) : Set M) : Type u_2) | (↑x : M) ∈ Φ}) ⊤
Tactic: rw [range_inclusion]
-- 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
⊢ 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 hΦ'₂ : Eq (α := Submodule R ↥(span R Φ)) (span R Φ') ⊤
Tactic: have hΦ'₂ : span R Φ' = ⊤ := by
    simp only [Φ']
    rw [range_inclusion]
    simp
-- 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
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) Φ Φ
⊢ MapsTo
    (⇑(preReflection x' ((LinearMap.dualMap (Submodule.subtype (span R Φ)) : (a : Dual R M) → Dual R ↥(span R Φ)) F)) :
      (a : ↥(span R Φ)) → ↥(span R Φ))
    Φ' Φ'
have 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 Φ))
Tactic: ⟨y, hy⟩
-- 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
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 (α := ↥(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 Φ))
have 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'
Cleared hypotheses: 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
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 Φ)) (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 Φ))
have 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 Φ))
Tactic: rw [range_inclusion]