awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i_1 : ι'
i : ι
⊢ Eq.{u_3 + 1} (α := R)
    (((b.repr : (a : M) → ι →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i_1)).1 : (a : ι) → R) i : R)
    (((b.repr : (a : M) → ι →₀ R) 0 : (a : ι) → R) i : R)
have h : Eq.{u_3 + 1} (α := R) ((single (Sum.inr i_1) 1 : (a : ι ⊕ ι') → R) (Sum.inl i) : R) (0 : R)
Tactic: simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b.repr.apply_symm_apply,
      LinearEquiv.symm_symm, Finsupp.fst_sumFinsuppLEquivProdFinsupp,
      map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι
⊢ Eq (α := ι' →₀ R) ((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).2)
    ((b'.repr : (a : M') → ι' →₀ R) 0)
have h : ∀ (j : ι'),
  Eq.{u_3 + 1} (α := R)
    (((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).2 : (a : ι') → R) j : R)
    (((b'.repr : (a : M') → ι' →₀ R) 0 : (a : ι') → R) j : R)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι
j : ι'
⊢ Eq.{u_3 + 1} (α := R)
    (((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl i)).2 : (a : ι') → R) j : R)
    (((b'.repr : (a : M') → ι' →₀ R) 0 : (a : ι') → R) j : R)
have h : Eq.{u_3 + 1} (α := R) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inr j) : R) (0 : R)
Tactic: simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, Finsupp.snd_sumFinsuppLEquivProdFinsupp,
      map_zero, Finsupp.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι'
⊢ Eq (α := ι' →₀ R) ((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).2 : ι' →₀ R)
    ((b'.repr : (a : M') → ι' →₀ R) ((b' : (a : ι') → M') i) : ι' →₀ R)
have h : ∀ (i_1 : ι'),
  Eq.{u_3 + 1} (α := R)
    (((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i)).2 : (a : ι') → R) i_1 : R)
    ((((b'.repr : (a : M') → ι' →₀ R) ((b' : (a : ι') → M') i) : ι' →₀ R) : (a : ι') → R) i_1 : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i_1 i : ι'
⊢ Eq.{u_3 + 1} (α := R)
    (((b'.repr : (a : M') → ι' →₀ R) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr i_1)).2 : (a : ι') → R) i : R)
    ((((b'.repr : (a : M') → ι' →₀ R) ((b' : (a : ι') → M') i_1) : ι' →₀ R) : (a : ι') → R) i : R)
have h : Eq.{u_3 + 1} (α := R) ((single (Sum.inr i_1) 1 : (a : ι ⊕ ι') → R) (Sum.inr i) : R)
  ((single i_1 1 : (a : ι') → R) i : R)
Tactic: simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, repr_self, Finsupp.snd_sumFinsuppLEquivProdFinsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ Eq (α := M × M') ((b.prod b' : (a : ι ⊕ ι') → M × M') i : M × M')
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i :
      M × M')
have fst : Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') i).1
  (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
      (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
fst :
  Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') i).1
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).1
⊢ Eq (α := M × M') ((b.prod b' : (a : ι ⊕ ι') → M × M') i : M × M')
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i :
      M × M')
have snd : Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') i).2
  (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
      (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') i).1
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).1
have fst : ∀ (val : ι),
  Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl val)).1
    (Sum.elim (β := ι') (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inl val)).1
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
fst :
  ∀ (val : ι),
    Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl val)).1
      (Sum.elim (β := ι') (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
          (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inl val)).1
⊢ Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') i).1
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).1
have fst₁ : ∀ (val : ι'),
  Eq.{u_5 + 1} (α := M) ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr val)).1
    (Sum.elim (α := ι) (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inr val)).1
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') i).2
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).2
have snd : ∀ (val : ι),
  Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl val)).2
    (Sum.elim (β := ι') (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inl val)).2
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Prod (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
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
b' : Basis ι' R M'
i : ι ⊕ ι'
snd :
  ∀ (val : ι),
    Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inl val)).2
      (Sum.elim (β := ι') (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
          (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inl val)).2
⊢ Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') i).2
    (Sum.elim (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) i).2
have snd₁ : ∀ (val : ι'),
  Eq.{u_6 + 1} (α := M') ((b.prod b' : (a : ι ⊕ ι') → M × M') (Sum.inr val)).2
    (Sum.elim (α := ι) (comp (β := M) (⇑(LinearMap.inl R M M') : (a : M) → M × M') (⇑b : (a : ι) → M))
        (comp (β := M') (⇑(LinearMap.inr R M M') : (a : M') → M × M') (⇑b' : (a : ι') → M')) (Sum.inr val)).2
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
⊢ Eq (α := Submodule R M) (span R (range (w • v))) ⊤
have rw : LE.le (α := Submodule R M) ⊤ (span R (range (w • v)))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : Membership.mem (γ := Submodule R M) ⊤ j
⊢ Membership.mem (γ := Submodule R M) (span R (range (w • v))) j
have hj₁ : Membership.mem (γ := Submodule R M) (span R (range v)) j
Tactic: rw [← hv] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : Membership.mem (γ := Submodule R M) (span R (range v)) j
⊢ Membership.mem (γ := Submodule R M) (span R (range (w • v))) j
have rw : ∀ (hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p) (p : Submodule R M), range (w • v) ⊆ (↑p : Set M) → j ∈ p
Tactic: rw [Submodule.mem_span] at hj ⊢
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ (↑p : Set M) → j ∈ p
have refine : ∀ (p : Submodule R M) (hp : range (w • v) ⊆ (↑p : Set M)) (u : M) (hu : u ∈ range v), u ∈ (↑p : Set M)
Tactic: refine fun p hp => hj p fun u hu => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ (↑p : Set M)
u : M
hu : u ∈ range v
⊢ u ∈ (↑p : Set M)
have obtain : ∀ (i : ι), v i ∈ (↑p : Set M)
Tactic: obtain ⟨i, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ (↑p : Set M)
i : ι
⊢ v i ∈ (↑p : Set M)
have this : HSMul.hSMul (β := R) (w i)⁻¹ 1 • w i • v i ∈ p
Tactic: have : ((w i)⁻¹ • (1 : R)) • w i • v i ∈ p := p.smul_mem ((w i)⁻¹ • (1 : R)) (hp ⟨i, rfl⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ (↑p : Set M)
i : ι
this : HSMul.hSMul (β := R) (w i)⁻¹ 1 • w i • v i ∈ p
⊢ v i ∈ (↑p : Set M)
have rwa : ∀ (this : (w i)⁻¹ • w i • v i ∈ p), v i ∈ (↑p : Set M)
Tactic: rwa [smul_one_smul, inv_smul_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_5
inst_3 : Group G
inst_4 : SMul G R
inst_5 : MulAction G M
inst_6 : IsScalarTower G R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ (↑p : Set M) → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ (↑p : Set M)
i : ι
this : HSMul.hSMul (β := R) (w i)⁻¹ 1 • w i • v i ∈ p
rwa : ∀ (this : (w i)⁻¹ • w i • v i ∈ p), v i ∈ (↑p : Set M)
⊢ v i ∈ (↑p : Set M)
have rwa₁ : ∀ (this : v i ∈ p), v i ∈ (↑p : Set M)
Tactic: rwa [smul_one_smul, inv_smul_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
have apply : ∀ (i_1 : ι),
  Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) i_1 : M) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) i_1 : M) : R₂)
Tactic: apply e.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
have trans : Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
  (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
Tactic: trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
trans :
  Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
    (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
⊢ Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
have trans₁ : Eq.{u_3 + 1} (α := R₂)
  (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
  (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
Tactic: trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ Eq.{u_3 + 1} (α := R₂)
    (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
have simp : HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) (if j = i then 1 else 0) =
  HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) (if j = i then 1 else 0)
Tactic: simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
⊢ HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) (if j = i then 1 else 0) =
    HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) (if j = i then 1 else 0)
have pos : ∀ (h : j = i), HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 1 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i j : ι
pos : ∀ (h : j = i), HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 1 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 1
⊢ HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) (if j = i then 1 else 0) =
    HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) (if j = i then 1 else 0)
have neg : ∀ (h : ¬j = i), HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 0 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
have apply : ∀ (i_1 : ι),
  Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) i_1 : M) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) i_1 : M) : R₂)
Tactic: classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
apply apply₁ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
have apply₂ : ∀ (j : ι),
  Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
    (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
Tactic: classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
apply apply₁ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
apply₂ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) :
        R₂)
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
have apply₃ : ∀ (j : ι),
  Eq.{u_3 + 1} (α := R₂)
    (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)
    (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
Tactic: classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.SMul (goal)
Goal:
ι : Type u_1
R₂ : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : CommSemiring R₂
inst_2 : Module R₂ M
e : Basis ι R₂ M
w : ι → R₂ˣ
i : ι
apply apply₁ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
apply₂ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂) (((e.unitsSMul w).coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
      (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) :
        R₂)
apply₃ apply₄ :
  ∀ (j : ι),
    Eq.{u_3 + 1} (α := R₂)
      (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) :
        R₂)
      (((w i)⁻¹ • e.coord i : (a : M) → R₂) ((e : (a : ι) → M) j : M) : R₂)
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i
have apply₅ : ∀ (j : ι),
  HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) (if j = i then 1 else 0) =
    HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) (if j = i then 1 else 0)
Tactic: classical
    apply e.ext
    intro j
    trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
    · simp [Basis.unitsSMul, ← mul_smul]
    simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]
    split_ifs with h <;> simp [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (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
P : Submodule R M
b : Basis.{u_1, u_3, u_5} ι R ↥P
x : M
| x ∈ P
have rw : Membership.mem (γ := Submodule R M)
  (LinearMap.range (M := ι →₀ R) (linearCombination R (comp (β := ↥P) (⇑P.subtype : (a : ↥P) → M) (⇑b : (a : ι) → ↥P))))
  x
Tactic: rw [← P.range_subtype, ← Submodule.map_top, ← b.span_eq, Submodule.map_span, ← Set.range_comp,
        ← Finsupp.range_linearCombination]