awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0
h : (∀ i ∈ s, v i ∈ p i ∧ 0 i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, 0 i) → ∀ i ∈ s, v i = 0 i
⊢ ∀ i ∈ s, v i = 0

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
N : Type u_6
inst : DecidableEq ι
inst_1 : AddCommGroup N
p : ι → AddSubgroup N
⊢ iSupIndep p ↔
    Function.Injective (α := Π₀ (i : ι), ↥(p i)) (β := N)
      (⇑(sumAddHom (β := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦ (p i).subtype) : (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
⟨iSupIndep.dfinsuppSumAddHom_injective, iSupIndep_of_dfinsuppSumAddHom_injective' p⟩

Premises used: iSupIndep.dfinsuppSumAddHom_injective, iSupIndep_of_dfinsuppSumAddHom_injective', Iff.intro
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : Eq.{u_6 + 1} (α := Submodule R N) (⨆ (i : ι), p i) ⊤
rwa :
  Eq.{u_6 + 1} (α := Submodule R N)
    (LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
      ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
        fun (i : ι) ↦ (p i).subtype))
    ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : iSup p = ⊤
⊢ Function.Surjective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)

Tactic:
rwa [← LinearMap.range_eq_top, ← Submodule.iSup_eq_range_dfinsupp_lsum]

Premises used: Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : Eq.{u_6 + 1} (α := Submodule R N) (⨆ (i : ι), p i) ⊤
i : ι
x : N
h : x ∈ p i
⊢ Eq (α := Π₀ (i : ι), ↥(p i)) (((ind.linearEquiv iSup_top).symm : (a : N) → Π₀ (i : ι), ↥(p i)) x : Π₀ (i : ι), ↥(p i))
    (single (β := fun (i : ι) ↦ ↥(p i)) i (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) x h) : Π₀ (i : ι), ↥(p i))

Tactic:
simp [← LinearEquiv.eq_symm_apply, iSupIndep.linearEquiv]

Premises used: LinearEquiv.eq_symm_apply, iSupIndep.linearEquiv
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
rw : ∀ (l : ι →₀ R), Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N) → l = 0
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff]

Premises used: linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
a₁ :
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        a :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        0 :
      N)
⊢ a = 0

Tactic:
apply hp.dfinsupp_lsum_injective

Premises used: iSupIndep.dfinsupp_lsum_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
a₁ a₂ a₃ a₄ :
  ∀
    (hl :
      Eq.{u_6 + 1} (α := N)
        ((((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                  fun (i : ι) ↦ (p i).subtype) ∘ₗ
                (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
                    LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯)) ∘ₗ
                  (↑(finsuppLequivDFinsupp R) : (ι →₀ R) →ₗ[R] Π₀ (x : ι), R) :
              (a : ι →₀ R) → N)
            l :
          N)
        (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    Eq.{u_6 + 1} (α := N)
      (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
              fun (i : ι) ↦ (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          a :
        N)
      (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
              fun (i : ι) ↦ (p i).subtype :
            (a : Π₀ (i : ι), ↥(p i)) → N)
          0 :
        N)
⊢ Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        a :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        0 :
      N)

Tactic:
rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl

Premises used: lsum_comp_mapRange_toSpanSingleton
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
⊢ a = 0

Tactic:
have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
h : ∀ (i : ι), Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
⊢ l = 0

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
h :
  Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i)) ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
⊢ Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)

Tactic:
apply smul_left_injective R (hv' i)

Premises used: smul_left_injective
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
⊢ HSMul.hSMul.{u_3, u_6, u_6} (α := R) ((l : (a : ι) → R) i : R) (v i) = (↑((a : (a : ι) → ↥(p a)) i) : N)

Tactic:
have : l i • v i = a i := rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
this : HSMul.hSMul.{u_3, u_6, u_6} (α := R) ((l : (a : ι) → R) i : R) (v i) = (↑((a : (a : ι) → ↥(p a)) i) : N)
⊢ Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) ∨ v i = 0

Tactic:
simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this

Premises used: Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, DFinsupp.coe_zero
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
this : Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) ∨ v i = 0
⊢ Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i)) ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
ι : Type u_11
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
γ : ι → Type u_12
inst_6 : DecidableEq ι
inst_7 : (i : ι) → Zero (γ i)
inst_8 : (i : ι) → (x : γ i) → Decidable (x ≠ 0)
t : Π₀ (i : ι), γ i
g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂
⊢ Eq (α := (a : M) → M₂) (⇑(t.sum (β := γ) g) : (a : M) → M₂)
    (⇑(t.sum (β := γ) fun (i : ι) (d : γ i) ↦ g i d) : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
ι : Type u_11
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
γ : ι → Type u_12
inst_6 : DecidableEq ι
inst_7 : (i : ι) → Zero (γ i)
inst_8 : (i : ι) → (x : γ i) → Decidable (x ≠ 0)
t : Π₀ (i : ι), γ i
g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂
b : M
⊢ Eq.{u_10 + 1} (α := M₂) ((t.sum (β := γ) g : (a : M) → M₂) b : M₂)
    (t.sum (β := γ) fun (i : ι) (d : γ i) ↦ (g i d : (a : M) → M₂) b : M₂)

Tactic:
sum_apply _ _ _

Premises used: DFinsupp.sum, LinearMap.sum_apply
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
ι : Type u_11
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ₁₂ : R →+* R₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
γ : ι → Type u_12
inst_6 : DecidableEq ι
inst_7 : (i : ι) → AddZeroClass (γ i)
f : M →ₛₗ[σ₁₂] M₂
t : Π₀ (i : ι), γ i
g : (i : ι) → AddMonoidHom.{u_12, u_9} (γ i) M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((sumAddHom (β := γ) g : (a : Π₀ (i : ι), γ i) → M) t : M) : M₂)
    ((sumAddHom (β := γ) fun (i : ι) ↦ f.toAddMonoidHom.comp (g i) : (a : Π₀ (i : ι), γ i) → M₂) t : M₂)

Tactic:
f.toAddMonoidHom.map_dfinsuppSumAddHom _ _

Premises used: LinearMap.toAddMonoidHom, AddMonoidHom.map_dfinsuppSumAddHom
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
ι : Type u_11
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair τ₁₂ τ₂₁
inst_7 : RingHomInvPair τ₂₁ τ₁₂
γ : ι → Type u_12
inst_8 : DecidableEq ι
inst_9 : (i : ι) → AddZeroClass (γ i)
f : M ≃ₛₗ[τ₁₂] M₂
t : Π₀ (i : ι), γ i
g : (i : ι) → AddMonoidHom.{u_12, u_9} (γ i) M
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) ((sumAddHom (β := γ) g : (a : Π₀ (i : ι), γ i) → M) t : M) : M₂)
    ((sumAddHom (β := γ) fun (i : ι) ↦ AddMonoidHom.comp f.toAddEquiv.toAddMonoidHom (g i) : (a : Π₀ (i : ι), γ i) → M₂)
        t :
      M₂)

Tactic:
f.toAddEquiv.map_dfinsuppSumAddHom _ _

Premises used: AddEquiv.map_dfinsuppSumAddHom, LinearEquiv.toAddEquiv
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
A : Type u_5
inst : CommRing A
n : Type u_7
inst_1 : Fintype n
inst_2 : DecidableEq n
M N : Matrix n n A
rw : M.det * N.det = (N * M).det
rw₁ : M.det * N.det = N.det * M.det
rw₂ rw₃ : N.det * M.det = N.det * M.det
⊢ (M * N).det = (N * M).det

Tactic:
rw [det_mul, det_mul, mul_comm]

Premises used: Matrix.det_mul, mul_comm
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
rw₁ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
rw₂ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))
        (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))).det
rw₃ : (M * N).det = det (n := n) ((M * N).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n))
rw₄ : (M * N).det = ((M * N).submatrix _root_.id _root_.id).det
rw₅ rw₆ : (M * N).det = (M * N).det
⊢ (M * N).det = (N * M).det

Tactic:
rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Premises used: Equiv.coe_refl, Matrix.submatrix_id_id, Matrix.det_submatrix_equiv_self, Matrix.submatrix_mul_equiv, Equiv.refl, Matrix.det_comm
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
rw : (M' * (M * N)).det = N.det
rw₁ : (M' * M * N).det = N.det
rw₂ : (1 * N).det = N.det
rw₃ rw₄ : N.det = N.det
⊢ (M * N * M').det = N.det

Tactic:
rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]

Premises used: Matrix.mul_assoc, Matrix.det_comm', Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hMM' :
  HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1
hM'M :
  HMul.hMul (α := Matrix ι κ A) (β := Matrix κ ι A) (b.toMatrix (⇑c : (a : κ) → M)) (c.toMatrix (⇑b : (a : ι) → M)) = 1
⊢ Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f))
    (det.{u_5, u_6} (n := κ) ((toMatrix c c : (a : M →ₗ[A] M) → Matrix κ κ A) f))

Tactic:
rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one]

Premises used: linearMap_toMatrix_mul_basis_toMatrix, basis_toMatrix_mul_linearMap_toMatrix, Matrix.det_conj_of_mul_eq_one
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hMM' : Eq (α := Matrix κ κ A) (c.toMatrix (⇑c : (a : κ) → M)) 1
hMM'₁ hMM'₂ : Eq (α := Matrix κ κ A) 1 1
⊢ HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1

Tactic:
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Premises used: Module.Basis.toMatrix_self, Module.Basis.toMatrix_mul_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hM'M : Eq (α := Matrix ι ι A) (b.toMatrix (⇑b : (a : ι) → M)) 1
hM'M₁ hM'M₂ : Eq (α := Matrix ι ι A) 1 1
⊢ HMul.hMul (α := Matrix ι κ A) (β := Matrix κ ι A) (b.toMatrix (⇑c : (a : κ) → M)) (c.toMatrix (⇑b : (a : ι) → M)) = 1

Tactic:
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Premises used: Module.Basis.toMatrix_self, Module.Basis.toMatrix_mul_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Basis ι A M
f : M →ₗ[A] M
rw :
  Eq.{u_5 + 1} (α := A)
    ((Trunc.lift
            (fun (b : Basis ι A M) ↦ MonoidHom.comp detMonoidHom (↑(toMatrixAlgEquiv b) : (M →ₗ[A] M) →* Matrix ι ι A))
            ⋯ (Trunc.mk b) :
          (a : M →ₗ[A] M) → A)
        f :
      A)
    (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)

Tactic:
rw [detAux]

Premises used: LinearMap.detAux
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ Eq.{u_5 + 1} (α := A)
    ((Trunc.lift
            (fun (b : Basis ι A M) ↦ MonoidHom.comp detMonoidHom (↑(toMatrixAlgEquiv b) : (M →ₗ[A] M) →* Matrix ι ι A))
            ⋯ (Trunc.mk b) :
          (a : M →ₗ[A] M) → A)
        f :
      A)
    (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
ι' : Type u_7
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
h :
  Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f))
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
h₁ h₂ :
  Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)

Tactic:
rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

Premises used: LinearMap.detAux_def', LinearMap.det_toMatrix_eq_det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
ι' : Type u_7
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
h :
  ∀ (b : Basis ι A M),
    Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
      (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)
⊢ Eq.{u_5 + 1} (α := A) ((detAux tb : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)

Tactic:
induction tb using Trunc.induction_on with
  | h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']

Premises used: LinearMap.detAux_def'
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Trunc (Basis ι A M)
⊢ Eq.{u_5 + 1} (α := A) ((detAux b : (a : M →ₗ[A] M) → A) id : A) (1 : A)

Tactic:
(LinearMap.detAux b).map_one

Premises used: LinearMap.detAux, MonoidHom.map_one
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Trunc (Basis ι A M)
f g : M →ₗ[A] M
⊢ (detAux b : (a : M →ₗ[A] M) → A) (f ∘ₗ g) =
    HMul.hMul (α := A) (β := A) ((detAux b : (a : M →ₗ[A] M) → A) f : A) ((detAux b : (a : M →ₗ[A] M) → A) g : A)

Tactic:
(LinearMap.detAux b).map_mul f g

Premises used: LinearMap.detAux, MonoidHom.map_mul