mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R✝ : Type u_1
R₂✝ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴⁶ : Semiring R✝
inst✝⁴⁵ : Semiring R₂✝
inst✝⁴⁴ : Semiring S
inst✝⁴³ : Semiring S₂
M✝ : Type u_5
M₂ : Type u_6
N✝ : Type u_7
N₂ : Type u_8
P✝ : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝⁴² : AddCommMonoid M✝
inst✝⁴¹ : AddCommMonoid M₂
inst✝⁴⁰ : AddCommMonoid N✝
inst✝³⁹ : AddCommMonoid N₂
inst✝³⁸ : AddCommMonoid P✝
inst✝³⁷ : AddCommMonoid P₂
inst✝³⁶ : AddCommMonoid Pₗ
inst✝³⁵ : Module R✝ M✝
inst✝³⁴ : Module R✝ M₂
inst✝³³ : Module S N✝
inst✝³² : Module S N₂
inst✝³¹ : Module R₂✝ P✝
inst✝³⁰ : Module S₂ P✝
inst✝²⁹ : Module R✝ P₂
inst✝²⁸ : Module S₂ P₂
inst✝²⁷ : Module R✝ Pₗ
inst✝²⁶ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²⁵ : AddCommGroup M'
inst✝²⁴ : AddCommGroup P'
inst✝²³ : Module R✝ M'
inst✝²² : Module R₂✝ P'
inst✝²¹ : Module S₂ P'
inst✝²⁰ : SMulCommClass S₂ R₂✝ P✝
inst✝¹⁹ : SMulCommClass S R✝ Pₗ
inst✝¹⁸ : SMulCommClass S₂ R₂✝ P'
inst✝¹⁷ : SMulCommClass S₂ R✝ P₂
ρ₁₂ : R✝ →+* R₂✝
σ₁₂✝ : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
inst✝¹³ : Semiring R₄
inst✝¹² : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ N
inst✝⁵ : Module R₃ P
inst✝⁴ : Module R₄ Q
inst✝³ : Module R₅ P
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x✝¹ : R
x✝ : M
⊢ (lcompₛₗ R₅ P σ₂₃ g) (h (x✝¹ • x✝)) = σ₁₅ x✝¹ • (lcompₛₗ R₅ P σ₂₃ g) (h x✝)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R₂ N
inst✝² : Module R₃ P
inst✝¹ : Module R₅ P
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
⊢ h.compl₂ id = h

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∃ f, (f.sum fun x xi ↦ ↑xi) = a

Tactic:
· refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝²⁹ : Semiring R
inst✝²⁸ : Semiring R₂
inst✝²⁷ : Semiring S
inst✝²⁶ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝²⁵ : AddCommMonoid M
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Pₗ
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R M₂
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module S N₂
inst✝¹⁴ : Module R₂ P
inst✝¹³ : Module S₂ P
inst✝¹² : Module R P₂
inst✝¹¹ : Module S₂ P₂
inst✝¹⁰ : Module R Pₗ
inst✝⁹ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup P'
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
m₁ m₂ : M
x✝ : ↥q
⊢ ((f (m₁ + m₂)).domRestrict q) x✝ = ((f m₁).domRestrict q + (f m₂).domRestrict q) x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝²⁹ : Semiring R
inst✝²⁸ : Semiring R₂
inst✝²⁷ : Semiring S
inst✝²⁶ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝²⁵ : AddCommMonoid M
inst✝²⁴ : AddCommMonoid M₂
inst✝²³ : AddCommMonoid N
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P
inst✝²⁰ : AddCommMonoid P₂
inst✝¹⁹ : AddCommMonoid Pₗ
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R M₂
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module S N₂
inst✝¹⁴ : Module R₂ P
inst✝¹³ : Module S₂ P
inst✝¹² : Module R P₂
inst✝¹¹ : Module S₂ P₂
inst✝¹⁰ : Module R Pₗ
inst✝⁹ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup P'
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
c : R
m : M
x✝ : ↥q
⊢ ((f (c • m)).domRestrict q) x✝ = (ρ₁₂ c • (f m).domRestrict q) x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
this : Std.Refl r
⊢ ↑f.support ∪ ↑g.support ⊆ ⋃ i ∈ c, ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (B (r' • m)) x✝ = r' • (B m) x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
⊢ ∀ (c : Set X), IsChain r c → indep (⋃ I ∈ c, ↑I)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R₁ : Type u_3
R₂ : Type u_4
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
inst✝⁷ : AddCommMonoid Mₗ
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid Pₗ
inst✝⁴ : Module R₁ Mₗ
inst✝³ : Module R₂ N
inst✝² : Module R₂ Pₗ
inst✝¹ : Module R₁ Pₗ
inst✝ : SMulCommClass R₂ R₁ Pₗ
f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
⊢ f.compl₁₂ id id = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ((lsum ℕ) fun i ↦ (p i).subtype) (single i x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : span R (range v) = ⊤
s t : Set ι
hst : Codisjoint s t
⊢ Codisjoint (span R (v '' s)) (span R (v '' t))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LinearIndependent R v ↔ ((LinearMap.lsum R (fun x ↦ R) ℕ) fun i ↦ LinearMap.id.smulRight (v i)).ker = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
      (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) =
    Finsupp.linearCombination R v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)

Goal state after:
ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
⊢ iSupIndep p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
⊢ t ⊆ {i, j}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
this : ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ + x✝) = ↑R g ∘ₗ f x✝¹ + ↑R g ∘ₗ f x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝³⁴ : Semiring A
inst✝³³ : CommSemiring R
inst✝³² : Semiring R₁
inst✝³¹ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid Mₗ
inst✝²⁸ : AddCommMonoid N
inst✝²⁷ : AddCommMonoid Nₗ
inst✝²⁶ : AddCommMonoid Pₗ
inst✝²⁵ : AddCommMonoid Qₗ
inst✝²⁴ : AddCommMonoid Qₗ'
inst✝²³ : Module R M
inst✝²² : Module R Mₗ
inst✝²¹ : Module R₁ Mₗ
inst✝²⁰ : Module R₂ N
inst✝¹⁹ : Module R Nₗ
inst✝¹⁸ : Module R Pₗ
inst✝¹⁷ : Module R₂ Pₗ
inst✝¹⁶ : Module R₁ Pₗ
inst✝¹⁵ : Module R Qₗ
inst✝¹⁴ : Module R₁ Qₗ
inst✝¹³ : Module R Qₗ'
inst✝¹² : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝¹¹ : AddCommMonoid Tₗ
inst✝¹⁰ : AddCommMonoid Tₗ'
inst✝⁹ : Module R₁ Tₗ
inst✝⁸ : Module R₂ Tₗ'
inst✝⁷ : Module A Pₗ
inst✝⁶ : SMulCommClass R A Pₗ
inst✝⁵ : Module R A
inst✝⁴ : Module A M
inst✝³ : Module A Qₗ
inst✝² : SMulCommClass R A Qₗ
inst✝¹ : IsScalarTower R A Qₗ
inst✝ : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x✝¹ : A
x✝ : M
⊢ ↑R g ∘ₗ f (x✝¹ • x✝) = (RingHom.id A) x✝¹ • ↑R g ∘ₗ f x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_2
inst✝⁸ : CommSemiring R
M : Type u_5
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid Nₗ
inst✝⁵ : AddCommMonoid Pₗ
inst✝⁴ : AddCommMonoid Qₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
inst✝¹ : Module R Pₗ
inst✝ : Module R Qₗ
f : M →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Pₗ ≃ₗ[R] Qₗ
hf : Surjective ⇑f
⊢ ↑g ∘ₗ ↑g.symm = id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ 0 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
rw [← linearIndepOn_univ_iff, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0,1} from rfl,
    Finset.coe_insert, Finset.coe_singleton, LinearIndepOn.pair_iff _ (by trivial)]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_2
inst✝¹⁶ : CommSemiring R
R₂ : Type u_14
R₃ : Type u_15
R₄ : Type u_16
M : Type u_17
N : Type u_18
P : Type u_19
Q : Type u_20
inst✝¹⁵ : CommSemiring R₂
inst✝¹⁴ : CommSemiring R₃
inst✝¹³ : CommSemiring R₄
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : AddCommMonoid Q
inst✝⁸ : Module R M
inst✝⁷ : Module R₂ N
inst✝⁶ : Module R₃ P
inst✝⁵ : Module R₄ Q
σ₁₃ : R →+* R₃
σ₁₄ : R →+* R₄
σ₂₃ : R₂ →+* R₃
σ₂₄ : R₂ →+* R₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝³ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝² : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝¹ : RingHomInvPair σ₃₄ σ₄₃
inst✝ : RingHomInvPair σ₄₃ σ₃₄
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
g : P ≃ₛₗ[σ₃₄] Q
hf : Surjective ⇑f
⊢ ↑g ∘ₛₗ ↑g.symm = id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, y] → LinearIndependent R ![y, x]
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝²⁸ : Semiring A
inst✝²⁷ : CommSemiring R
inst✝²⁶ : Semiring R₁
inst✝²⁵ : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝²⁴ : AddCommMonoid M
inst✝²³ : AddCommMonoid Mₗ
inst✝²² : AddCommMonoid N
inst✝²¹ : AddCommMonoid Nₗ
inst✝²⁰ : AddCommMonoid Pₗ
inst✝¹⁹ : AddCommMonoid Qₗ
inst✝¹⁸ : AddCommMonoid Qₗ'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module R Mₗ
inst✝¹⁵ : Module R₁ Mₗ
inst✝¹⁴ : Module R₂ N
inst✝¹³ : Module R Nₗ
inst✝¹² : Module R Pₗ
inst✝¹¹ : Module R₂ Pₗ
inst✝¹⁰ : Module R₁ Pₗ
inst✝⁹ : Module R Qₗ
inst✝⁸ : Module R₁ Qₗ
inst✝⁷ : Module R Qₗ'
inst✝⁶ : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst✝⁵ : AddCommMonoid Tₗ
inst✝⁴ : AddCommMonoid Tₗ'
inst✝³ : Module R₁ Tₗ
inst✝² : Module R₂ Tₗ'
inst✝¹ : Module A Pₗ
inst✝ : SMulCommClass R A Pₗ
r s : R
m : M
⊢ s • r • m = r • s • m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : iSupIndep p
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)

Tactic:
← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)

Goal state after:
ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
⊢ k ((i.restrictScalarsRange k hk f hf) m) = f (i m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ -s • -x + t • y = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : SMul S R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
inst✝⁷ : Module S M
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower S R M
inst✝⁴ : IsScalarTower S R P
inst✝³ : AddCommMonoid M'
inst✝² : Module S M'
inst✝¹ : AddCommMonoid P'
inst✝ : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective ⇑k
f : M →ₗ[R] P
hf : ∀ (m : M'), f (i m) ∈ k.range
m : M'
p : P'
⊢ p = (i.restrictScalarsRange k hk f hf) m ↔ k p = f (i m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ -s • x + t • y = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]

Tactic:
by

Goal state after: