awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have pos : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) (annIdeal 𝕜 a)
Tactic: rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) (annIdeal 𝕜 a)
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have pos₁ : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) ⊥
Tactic: rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) (annIdeal 𝕜 a)
pos₁ : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) ⊥
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have pos₂ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) (Ideal.span 0) ⊥
Tactic: rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) (annIdeal 𝕜 a)
pos₁ : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) ⊥
pos₂ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) (Ideal.span 0) ⊥
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have pos₃ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) ⊥ ⊥
Tactic: rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have neg : IsUnit (M := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ : 𝕜[X])
Tactic: rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ IsUnit (M := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ : 𝕜[X])
have neg : IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹
Tactic: apply Polynomial.isUnit_C.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹
have neg : (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0
Tactic: apply IsUnit.mk0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0
have neg : ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0
Tactic: apply inv_eq_zero.not.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0
have neg : ¬Eq (α := 𝕜[X]) (IsPrincipal.generator (annIdeal 𝕜 a)) 0
Tactic: apply Polynomial.leadingCoeff_eq_zero.not.mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    ∃ (s : 𝕜[X]), p = HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a)
have simp_rw : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ ∃ (s : 𝕜[X]), HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a) = p
Tactic: simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
simp_rw :
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    ∃ (s : 𝕜[X]), HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a) = p
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    ∃ (s : 𝕜[X]), p = HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a)
have simp_rw₁ : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
  Membership.mem (γ := Submodule 𝕜[X] 𝕜[X]) (𝕜[X] ∙ annIdealGenerator 𝕜 a) p
Tactic: simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ annIdealGenerator 𝕜 a ∣ p
have rw : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
  Membership.mem (γ := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) p
Tactic: rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
rw :
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    Membership.mem (γ := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) p
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ annIdealGenerator 𝕜 a ∣ p
have rw₁ : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p
Tactic: rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
have pos : ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0), Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
Tactic: by_cases h : annIdealGenerator 𝕜 a = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
pos : ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0), Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
have neg : ∀ (h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0), Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
Tactic: by_cases h : annIdealGenerator 𝕜 a = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
have pos : ¬IsIntegral 𝕜 a
Tactic: rw [h, minpoly.eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
p : 𝕜[X]
p_monic : p.Monic
hp : Eq.{u_2 + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
⊢ False
have pos : Membership.mem (γ := Ideal 𝕜[X]) ⊥ p
Tactic: refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
⊢ annIdealGenerator 𝕜 a = p
have pos : ∀ (h : p = 0), annIdealGenerator 𝕜 a = p
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
pos : ∀ (h : p = 0), annIdealGenerator 𝕜 a = p
⊢ annIdealGenerator 𝕜 a = p
have neg : ∀ (h : ¬p = 0), annIdealGenerator 𝕜 a = p
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
h : p = 0
⊢ annIdealGenerator 𝕜 a = p
have pos : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
Tactic: rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
h : p = 0
pos : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ annIdealGenerator 𝕜 a = p
have pos₁ : Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 a) ⊥
Tactic: rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
h : p = 0
pos : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos₁ : Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 a) ⊥
⊢ annIdealGenerator 𝕜 a = p
have pos₂ : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) ⊥
Tactic: rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
h : p = 0
pos : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos₁ : Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 a) ⊥
pos₂ : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) ⊥
⊢ annIdealGenerator 𝕜 a = p
have pos₃ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) ⊥ ⊥
Tactic: rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
have p_gen₁ : Associated p (annIdealGenerator 𝕜 a)
Tactic: rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
Cleared hypotheses: p_gen, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
have neg : p = annIdealGenerator 𝕜 a
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a
have apply : Monic (annIdealGenerator 𝕜 a)
Tactic: apply eq_of_monic_of_associated p_monic _ p_gen
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {minpoly 𝕜 f}) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))
have rw : Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 f) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))
Tactic: rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
⊢ Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 f) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))
have h : ∀ (x : 𝕜[X]),
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 f) x ↔
    Membership.mem (γ := Ideal 𝕜[X]) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
x : 𝕜[X]
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 f) x ↔
    Membership.mem (γ := Ideal 𝕜[X]) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f)) x
have h : (∀ (x_1 : M),
    Eq (α := M) ((((aeval f : (a : 𝕜[X]) → Module.End 𝕜 M) x : Module.End 𝕜 M) : (a : M) → M) x_1 : M)
      ((0 : (a : M) → M) x_1 : M)) ↔
  ∀ (m : Module.AEval' f), x • m = 0
Tactic: rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
⊢ (↑b.repr : M →ₗ[R] ι →₀ R).range = supported R R univ
have rw : Eq (α := Submodule R (ι →₀ R)) ⊤ (supported R R univ)
Tactic: rw [LinearEquiv.range, Finsupp.supported_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
rw : Eq (α := Submodule R (ι →₀ R)) ⊤ (supported R R univ)
⊢ (↑b.repr : M →ₗ[R] ι →₀ R).range = supported R R univ
have rw₁ : Eq (α := Submodule R (ι →₀ R)) ⊤ ⊤
Tactic: rw [LinearEquiv.range, Finsupp.supported_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
s : Set ι
m : M
hm : Membership.mem (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' s)) m
⊢ (↑(Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : M) → ι →₀ R) m)) : Set ι) ⊆ s
have rcases : ∀ (l : ι →₀ R) (hl : Membership.mem (γ := Submodule R (ι →₀ R)) (supported R R s) l)
  (hm :
    Membership.mem.{u_5, u_5} (α := M) (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' s))
      ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) l : M)),
  (↑(Finsupp.support.{u_1, u_3} (M := R)
          ((b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) l))) :
      Set ι) ⊆
    s
Tactic: rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : Membership.mem (γ := Submodule R (ι →₀ R)) (supported R R s) l
hm :
  Membership.mem.{u_5, u_5} (α := M) (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' s))
    ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) l : M)
⊢ (↑(Finsupp.support.{u_1, u_3} (M := R)
          ((b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) l))) :
      Set ι) ⊆
    s
have rwa : (↑l.support : Set ι) ⊆ s
Tactic: rwa [repr_linearCombination, ← Finsupp.mem_supported R l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
p : Submodule R M
⊢ p = ⊤ ↔ ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)
have refine : ∀ (h : ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)), p = ⊤
Tactic: refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
p : Submodule R M
h : ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)
⊢ p = ⊤
have h₁ : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ⊆ (↑p : Set M)
Tactic: replace h : range b ⊆ p := by rintro - ⟨i, rfl⟩; exact h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Nontrivial M
⊢ Nonempty ι
have obtain : ∀ (x y : M) (ne : x ≠ y), Nonempty ι
Tactic: obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
inst_3 : Nontrivial M
x y : M
ne : x ≠ y
⊢ Nonempty ι
have obtain : ∀ (i : ι),
  ¬Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
        ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R) →
    Nonempty ι
Tactic: obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy :
  Eq.{u_5 + 1} (α := M) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x : M)
    ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) y : M)
⊢ x = y
have rw : (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x) = y
Tactic: rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy :
  Eq.{u_5 + 1} (α := M) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x : M)
    ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) y : M)
rw : (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x) = y
⊢ x = y
have rw₁ : (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) y) = y
Tactic: rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy :
  Eq.{u_5 + 1} (α := M) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x : M)
    ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) y : M)
rw : (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) x) = y
rw₁ : (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) y) = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
M : Type u_5
inst : AddCommMonoid M
R : Type u_7
inst_1 : CommSemiring R
inst_2 : Module R M
b : Basis ι R M
⊢ LinearIndependent R b.coord
have refine : ∀ (s : Finset ι) (l₁ l₂ : ι → R) (h : Eq (α := M →ₗ[R] R) (∑ i ∈ s, l₁ i • b.coord i) (∑ i ∈ s, l₂ i • b.coord i))
  (j : ι) (hj : j ∈ s), l₁ j = l₂ j
Tactic: refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
M : Type u_5
inst : AddCommMonoid M
R : Type u_7
inst_1 : CommSemiring R
inst_2 : Module R M
b : Basis ι R M
⊢ LinearIndependent R b.coord
have refine : ∀ (s : Finset ι) (l₁ l₂ : ι → R) (h : Eq (α := M →ₗ[R] R) (∑ i ∈ s, l₁ i • b.coord i) (∑ i ∈ s, l₂ i • b.coord i))
  (j : ι) (hj : j ∈ s), l₁ j = l₂ j
Tactic: classical
  refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_
  simpa [hj, Finsupp.single_apply] using congr($h (b j))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (range v))
inst_3 : DecidableEq ι
i j : ι
⊢ Eq.{u_3 + 1} (α := R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v j) : R) (if j = i then 1 else 0 : R)
have inl : ∀ (h : j = i), Eq.{u_3 + 1} (α := R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v j) : R) (if j = i then 1 else 0 : R)
Tactic: rcases eq_or_ne j i with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (range v))
inst_3 : DecidableEq ι
i j : ι
inl :
  ∀ (h : j = i),
    Eq.{u_3 + 1} (α := R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v j) : R) (if j = i then 1 else 0 : R)
⊢ Eq.{u_3 + 1} (α := R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v j) : R) (if j = i then 1 else 0 : R)
have inr : ∀ (h : j ≠ i), Eq.{u_3 + 1} (α := R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v j) : R) (if j = i then 1 else 0 : R)
Tactic: rcases eq_or_ne j i with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
⊢ Membership.mem (γ := Submodule R ↥(span R (range v)))
    (span R
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯))
    x
have this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
Tactic: have : ∀ i, v i ∈ span R (range v) := fun i ↦ subset_span (Set.mem_range_self _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
v : ι → M
x_1 y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
h : Membership.mem (γ := Submodule R ↥(span R (range v))) ⊤ x
this : ∀ (i : ι), Membership.mem (γ := Submodule R M) (span R (range v)) (v i)
⊢ image (α := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x))
      (range fun (i : ι) ↦
        Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) =
    range v
have simp : range.{u_5, u_1 + 1} (ι := ι)
    (comp (β := ↥(span R (range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x)) fun (i : ι) ↦
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) sorry) =
  range v
Tactic: simp only [← Set.range_comp]