awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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}) ⊥
pos₃ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) ⊥ ⊥
pos₄ : p = 0
pos₅ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) ⊥ ⊥
pos₆ pos₇ pos₈ : p = 0
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]

Premises used: Iff.mpr, Ideal.span_singleton_eq_bot, Polynomial.annIdealGenerator_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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
⊢ Associated p (annIdealGenerator 𝕜 a)

Tactic:
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen

Premises used: Ideal.span_singleton_eq_span_singleton, Polynomial.span_singleton_annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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
p_gen₁ : Associated p (annIdealGenerator 𝕜 a)
⊢ ¬p = 0

Tactic:
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen

Premises used: Ideal.span_singleton_eq_span_singleton, Polynomial.span_singleton_annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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
neg : p = annIdealGenerator 𝕜 a
⊢ annIdealGenerator 𝕜 a = p

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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
apply : Monic (annIdealGenerator 𝕜 a)
⊢ p = annIdealGenerator 𝕜 a

Tactic:
apply eq_of_monic_of_associated p_monic _ p_gen

Premises used: Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
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
⊢ Monic (annIdealGenerator 𝕜 a)

Tactic:
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)

Premises used: Associated.ne_zero_iff, Iff.mp, Polynomial.monic_annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
rw : Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 f) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {minpoly 𝕜 f}) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))

Tactic:
rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]

Premises used: Polynomial.span_singleton_annIdealGenerator, Polynomial.annIdealGenerator_eq_minpoly
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
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
⊢ Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 f) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
x : 𝕜[X]
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
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 f) x ↔
    Membership.mem (γ := Ideal 𝕜[X]) (Module.annihilator.{u_1, u_3} 𝕜[X] (Module.AEval' f)) x

Tactic:
rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]

Premises used: Module.mem_annihilator, Polynomial.mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
inst : Field 𝕜
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
f : Module.End 𝕜 M
x : 𝕜[X]
⊢ (∀ (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:
rfl
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
rw₁ rw₂ : Eq (α := Submodule R (ι →₀ R)) ⊤ ⊤
⊢ (↑b.repr : M →ₗ[R] ι →₀ R).range = supported R R univ

Tactic:
rw [LinearEquiv.range, Finsupp.supported_univ]

Premises used: Finsupp.supported_univ, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
m : M
⊢ Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R))
      (supported R R (↑(Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : M) → ι →₀ R) m)) : Set ι))
      ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) ∧
    (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) = m

Tactic:
simp [Finsupp.mem_supported_support]

Premises used: Finsupp.mem_supported_support
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
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
⊢ (↑(Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : M) → ι →₀ R) m)) : Set ι) ⊆ s

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩

Premises used: Iff.mp, Finsupp.mem_span_image_iff_linearCombination, rfl
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
rwa : (↑l.support : Set ι) ⊆ s
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Submodule R (ι →₀ R)) (supported R R s) l
⊢ (↑(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:
rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

Premises used: Finsupp.mem_supported, Module.Basis.repr_linearCombination
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
m : M
s : Set ι
⊢ 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

Tactic:
⟨repr_support_subset_of_mem_span _ _, fun h ↦
    span_mono (Set.image_mono h) (mem_span_repr_support b _)⟩

Premises used: Set.image_mono, Submodule.span_mono, Iff.intro, Module.Basis.repr_support_subset_of_mem_span, Module.Basis.mem_span_repr_support
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 R
i : ι
s : Set ι
⊢ Membership.mem.{u_5, u_5} (α := M) (γ := Submodule R M) (span R ((⇑b : (a : ι) → M) '' s)) ((b : (a : ι) → M) i : M) ↔
    i ∈ s

Tactic:
simp [mem_span_image, Finsupp.support_single]

Premises used: Finsupp.support_single, Module.Basis.mem_span_image
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : M
⊢ Membership.mem (γ := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) x

Tactic:
span_mono (image_subset_range _ _) (mem_span_repr_support b x)

Premises used: Set.image_subset_range, Submodule.span_mono, Module.Basis.mem_span_repr_support
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
⊢ Eq.{u_5 + 1} (α := Submodule R M) (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) ⊤

Tactic:
eq_top_iff.mpr fun x _ => b.mem_span x

Premises used: Iff.mpr, Module.Basis.mem_span, eq_top_iff
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : p = ⊤
⊢ ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
refine : ∀ (h : ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)), p = ⊤
⊢ p = ⊤ ↔ ∀ (i : ι), Membership.mem (α := M) p ((b : (a : ι) → M) i : M)

Tactic:
refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
i : ι
⊢ Membership.mem (α := M) (↑p : Set M) ((b : (a : ι) → M) i : M)

Tactic:
h i
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
i : ι
⊢ Membership.mem (α := M) (↑p : Set M) ((b : (a : ι) → M) i : M)

Tactic:
exact h i
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ⊆ (↑p : Set M)
⊢ p = ⊤

Tactic:
simpa using span_mono (R := R) h

Premises used: Submodule.span_mono
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : M) (y : M), x ≠ y

Tactic:
Nontrivial.exists_pair_ne

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
obtain : ∀ (x y : M) (ne : x ≠ y), Nonempty ι
⊢ Nonempty ι

Tactic:
obtain ⟨x, y, ne⟩ : ∃ x y : M, x ≠ y := Nontrivial.exists_pair_ne

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
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 ι
⊢ Nonempty ι

Tactic:
obtain ⟨i, _⟩ := not_forall.mp (mt b.ext_elem_iff.2 ne)

Premises used: Iff.mpr, mt, Iff.mp, Module.Basis.ext_elem_iff, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
i : ι
h :
  ¬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:
⟨i⟩

Premises used: Nonempty.intro
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
i : ι
h :
  ¬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:
exact ⟨i⟩
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

Premises used: Module.Basis.repr_linearCombination
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 ι
⊢ LinearIndepOn.{u_1, u_3, u_5} R (M := M) (⇑b : (a : ι) → M) s

Tactic:
b.linearIndependent.linearIndepOn s

Premises used: LinearIndependent.linearIndepOn, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 R
i : ι
⊢ Ne.{u_5 + 1} (α := M) ((b : (a : ι) → M) i : M) (0 : M)

Tactic:
b.linearIndependent.ne_zero i

Premises used: LinearIndependent.ne_zero, Module.Basis.linearIndependent
-- Module: Mathlib.LinearAlgebra.Basis.Basic
Goal:
ι : Type u_1
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
inst_5 : Semiring R₂
inst_6 : Module R₂ M'
inst_7 : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x x_1 : M
hab :
  Eq.{u_6 + 1} (α := M') ((((b.constr R₂ : (a : ι → M') → M →ₗ[R] M') v : M →ₗ[R] M') : (a : M) → M') x : M')
    ((((b.constr R₂ : (a : ι → M') → M →ₗ[R] M') v : M →ₗ[R] M') : (a : M) → M') x_1 : M')
⊢ Eq.{u_6 + 1} (α := M') ((linearCombination R v : (a : ι →₀ R) → M') ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : M')
    ((linearCombination R v : (a : ι →₀ R) → M') ((b.repr : (a : M) → ι →₀ R) x_1 : ι →₀ R) : M')

Tactic:
simpa [constr_def] using hab

Premises used: Module.Basis.constr_def
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
x : M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (range v))
⊢ Eq (α := ι →₀ R) (((Basis.mk hli hsp).repr : (a : M) → ι →₀ R) x : ι →₀ R)
    ((hli.repr : (a : ↥(span R (range v))) → ι →₀ R)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) x ⋯) :
      ι →₀ R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
i : ι
⊢ (linearCombination R v : (a : ι →₀ R) → M) (single i 1) = v i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
⊢ (⇑(Basis.mk hli hsp) : (a : ι) → M) = v

Tactic:
funext (mk_apply _ _)

Premises used: Module.Basis.mk_apply, funext
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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

Tactic:
linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'ₛ
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
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
⊢ LinearIndependent R b.coord

Tactic:
refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'ₛ
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
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:
simpa [hj, Finsupp.single_apply] using congr($h (b j))

Premises used: Finsupp.single_apply
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
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
⊢ LinearIndependent R b.coord

Tactic:
classical
  refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_
  simpa [hj, Finsupp.single_apply] using congr($h (b j))

Premises used: Iff.mpr, Finsupp.single_apply, linearIndependent_iff'ₛ
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    ((((hli.repr : (a : ↥(span R (range v))) → ι →₀ R)
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v i) ⋯) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    (1 : R)

Tactic:
simp [hli.repr_eq_single i]

Premises used: LinearIndependent.repr_eq_single
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
i j : ι
h : j ≠ i
⊢ Eq.{u_3 + 1} (α := R)
    ((((hli.repr : (a : ↥(span R (range v))) → ι →₀ R)
              (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (range v)) x) (v j) ⋯) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    (0 : R)

Tactic:
simp [hli.repr_eq_single j, h]

Premises used: LinearIndependent.repr_eq_single
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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)
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)
⊢ 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

Premises used: eq_or_ne
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
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:
simp only [h, if_true, mk_coord_apply_eq i]

Premises used: Module.Basis.mk_coord_apply_eq, if_true
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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 : ι
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:
simp only [h, if_false, mk_coord_apply_ne h]

Premises used: Module.Basis.mk_coord_apply_ne, if_false
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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))
_ :
  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
⊢ 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

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Basis.Basic
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
⊢ ∀ (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 _)