awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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 : ι'
h : Eq.{u_3 + 1} (α := R) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inr j) : R) (0 : R)
⊢ 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:
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]

Premises used: Finsupp.snd_sumFinsuppLEquivProdFinsupp, map_zero, LinearEquiv.symm_trans_apply, Module.Basis.repr, LinearEquiv.symm_symm, Module.Basis.prod, Finsupp.zero_apply, LinearEquiv.prodCongr_symm, Module.Basis.coe_ofRepr, LinearEquiv.prodCongr_apply, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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) ((single (Sum.inl i) 1 : (a : ι ⊕ ι') → R) (Sum.inr j) : R) (0 : R)

Tactic:
apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

Premises used: Finsupp.single_eq_of_ne, Sum.inr_ne_inl
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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 : ι'
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)
⊢ 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)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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 : ι'
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)
⊢ 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)

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]

Premises used: Finsupp.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.symm_trans_apply, Module.Basis.repr, LinearEquiv.symm_symm, Module.Basis.prod, LinearEquiv.prodCongr_symm, Module.Basis.coe_ofRepr, LinearEquiv.prodCongr_apply, LinearEquiv.apply_symm_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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) ((single (Sum.inr i_1) 1 : (a : ι ⊕ ι') → R) (Sum.inr i) : R)
    ((single i_1 1 : (a : ι') → R) i : R)

Tactic:
apply Finsupp.single_apply_left Sum.inr_injective

Premises used: Sum.inr_injective, Finsupp.single_apply_left
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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
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
⊢ 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')

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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
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
⊢ 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:
cases i
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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
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
⊢ 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:
cases i
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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'
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:
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Premises used: LinearMap.inr_apply, Module.Basis.prod_apply_inr_fst, Module.Basis.prod_apply_inl_snd, Function.comp, Sum.elim_inr, Sum.elim_inl, LinearMap.inl_apply, Module.Basis.prod_apply_inl_fst, Module.Basis.prod_apply_inr_snd
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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'
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:
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Premises used: LinearMap.inr_apply, Module.Basis.prod_apply_inr_fst, Module.Basis.prod_apply_inl_snd, Function.comp, Sum.elim_inr, Sum.elim_inl, LinearMap.inl_apply, Module.Basis.prod_apply_inl_fst, Module.Basis.prod_apply_inr_snd
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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'
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:
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Premises used: LinearMap.inr_apply, Module.Basis.prod_apply_inr_fst, Module.Basis.prod_apply_inl_snd, Function.comp, Sum.elim_inr, Sum.elim_inl, LinearMap.inl_apply, Module.Basis.prod_apply_inl_fst, Module.Basis.prod_apply_inr_snd
-- Module: Mathlib.LinearAlgebra.Basis.Prod
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'
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:
simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Premises used: LinearMap.inr_apply, Module.Basis.prod_apply_inr_fst, Module.Basis.prod_apply_inl_snd, Function.comp, Sum.elim_inr, Sum.elim_inl, LinearMap.inl_apply, Module.Basis.prod_apply_inl_fst, Module.Basis.prod_apply_inr_snd
-- Module: Mathlib.LinearAlgebra.Basis.Prod
Goal:
ι : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
M_1 : Type u_5
M' : Type u_6
R : Type u_7
M : Type u_8
N : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Free R N
⊢ Free R (M × N)

Tactic:
.of_basis <| (Module.Free.chooseBasis R M).prod (Module.Free.chooseBasis R N)

Premises used: Module.Basis.prod, Module.Free.of_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : DistribMulAction G M
inst_5 : SMulCommClass G R M
g : G
b : Basis ι R M
i : ι
⊢ (g • b : (a : ι) → M) i = HSMul.hSMul (β := M) g ((b : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : DistribMulAction G M
inst_5 : SMulCommClass G R M
g : G
b : Basis ι R M
⊢ (⇑(g • b) : (a : ι) → M) = HSMul.hSMul (β := (a : ι) → M) g (⇑b : (a : ι) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : M ≃ₗ[R] M
b : Basis ι R M
⊢ g • b = b.map g

Tactic:
rfl

Premises used: DistribMulAction.toLinearEquiv, rfl
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : DistribMulAction G M
inst_5 : SMulCommClass G R M
g : G
b : Basis ι R M
⊢ (g • b).repr = LinearEquiv.symm (DistribMulAction.toLinearEquiv R M g) ≪≫ₗ b.repr

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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
rw : LE.le (α := Submodule R M) ⊤ (span R (range (w • v)))
⊢ Eq (α := Submodule R M) (span R (range (w • v))) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 v)) j

Tactic:
rw [← hv] at hj
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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
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
⊢ Membership.mem (γ := Submodule R M) (span R (range (w • v))) j

Tactic:
rw [Submodule.mem_span] at hj ⊢

Premises used: Submodule.mem_span
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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

Tactic:
fun p hp => hj p fun u hu => ?_
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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
refine : ∀ (p : Submodule R M) (hp : range (w • v) ⊆ (↑p : Set M)) (u : M) (hu : u ∈ range v), u ∈ (↑p : Set M)
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ (↑p : Set M) → j ∈ p

Tactic:
refine fun p hp => hj p fun u hu => ?_
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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
obtain : ∀ (i : ι), v i ∈ (↑p : Set M)
⊢ u ∈ (↑p : Set M)

Tactic:
obtain ⟨i, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : ι
⊢ 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⟩)
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : v i ∈ p), v i ∈ (↑p : Set M)
⊢ v i ∈ (↑p : Set M)

Tactic:
rwa [smul_one_smul, inv_smul_smul] at this

Premises used: inv_smul_smul, smul_one_smul
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : DistribMulAction G R
inst_5 : DistribMulAction G M
inst_6 : IsScalarTower G R M
inst_7 : SMulCommClass G R M
v : Basis ι R M
w : ι → G
i : ι
⊢ (v.groupSMul w : (a : ι) → M) i = HSMul.hSMul (β := (a : ι) → M) w (⇑v : (a : ι) → M) i

Tactic:
mk_apply (LinearIndependent.group_smul v.linearIndependent w)
    (groupSMul_span_eq_top v.span_eq).ge i

Premises used: Eq.ge, Module.Basis.groupSMul_span_eq_top, Module.Basis.mk_apply, Module.Basis.linearIndependent, LinearIndependent.group_smul, Module.Basis.span_eq
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (span R (range v)) ⊤
w : ι → Rˣ
⊢ Eq (α := Submodule R M) (span R (range (w • v))) ⊤

Tactic:
groupSMul_span_eq_top hv

Premises used: Module.Basis.groupSMul_span_eq_top
-- Module: Mathlib.LinearAlgebra.Basis.SMul
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : Basis ι R M
w : ι → Rˣ
i : ι
⊢ (v.unitsSMul w : (a : ι) → M) i = HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)

Tactic:
mk_apply (LinearIndependent.units_smul v.linearIndependent w)
    (units_smul_span_eq_top v.span_eq).ge i

Premises used: Eq.ge, Module.Basis.mk_apply, Module.Basis.linearIndependent, LinearIndependent.units_smul, Module.Basis.span_eq, Module.Basis.units_smul_span_eq_top
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 :
  ∀ (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₂)
⊢ (e.unitsSMul w).coord i = (w i)⁻¹ • e.coord i

Tactic:
apply e.ext

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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₂)
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₂)
⊢ 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₂)

Tactic:
trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)

Premises used: Module.Basis.coord, Module.Basis.unitsSMul, Inv.inv, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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₂)
    (((e.unitsSMul w).coord i : (a : M) → R₂) (HSMul.hSMul (β := M) (w j)⁻¹ ((e.unitsSMul w : (a : ι) → M) j : M)) : R₂)

Tactic:
simp [Basis.unitsSMul, ← mul_smul]

Premises used: Module.Basis.unitsSMul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : ι
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)
⊢ 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:
simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def,
      map_smul, Finsupp.single_apply]

Premises used: LinearMap.smul_apply, Units.smul_def, Finsupp.single_apply, Module.Basis.coord_apply, Module.Basis.repr_self, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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
neg : ∀ (h : ¬j = i), HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 0 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 0
⊢ 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:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : ι
h : j = i
⊢ HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 1 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Basis.SMul
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 : ι
h : ¬j = i
⊢ HSMul.hSMul (β := R₂) (↑(w j)⁻¹ : R₂) 0 = HSMul.hSMul (β := R₂) (↑(w i)⁻¹ : R₂) 0

Tactic:
simp [h]