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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
i : ι
⊢ (fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
        ((fun F i ↦ F ∘ₗ lsingle i) F) ∘ₗ
      lsingle i =
    F ∘ₗ lsingle i

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
i : ι
x✝ : M i
⊢ ((fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
          ((fun F i ↦ F ∘ₗ lsingle i) F) ∘ₗ
        lsingle i)
      x✝ =
    (F ∘ₗ lsingle i) x✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
⊢ AddMonoidHom.mker (mapRange.addMonoidHom f) =
    AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mker (f i))

Tactic:
ext

Goal state after:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x✝ : Π₀ (i : ι), β₁ i
⊢ x✝ ∈ AddMonoidHom.mker (mapRange.addMonoidHom f) ↔
    x✝ ∈ AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mker (f i))
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁴ : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (r • g) = r • mapRange f hf g

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
inst✝⁴ : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (r • g)) i✝ = (r • mapRange f hf g) i✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝² : Semiring R
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
⊢ (linearMap fun i ↦ LinearMap.id) = LinearMap.id

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
inst✝² : Semiring R
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
x✝ : Π₀ (i : ι), β₂ i
i✝ : ι
⊢ ((linearMap fun i ↦ LinearMap.id) x✝) i✝ = (LinearMap.id x✝) i✝
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 : LinearIndependent R v
x✝ : ι
⊢ R ∙ v x✝ = Submodule.map (Finsupp.linearCombination R v) (Finsupp.lsingle x✝).range

Tactic:
ext

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
x✝¹ : ι
x✝ : M
⊢ x✝ ∈ R ∙ v x✝¹ ↔ x✝ ∈ Submodule.map (Finsupp.linearCombination R v) (Finsupp.lsingle x✝¹).range
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ (DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩).support = f.support

Tactic:
ext

Goal state after:
case refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
a✝ : ι
⊢ a✝ ∈ (DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩).support ↔ a✝ ∈ f.support
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
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
constructor

Goal state after:
case mp
ι : 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
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = a) → ∃ μ, ∑ i ∈ s, ↑(μ i) = a

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 ∈ s, ↑(μ i) = a) → ∃ f, (f.sum fun x xi ↦ ↑xi) = a
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
LinearIndependent,

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑(linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')))
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : 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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ μ x = 0

Tactic:
ext

Goal state after:
case h.h
ι : 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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ ↑(μ x) = ↑0
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:
ext

Goal state after:
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
x✝¹ : M
x✝ : N
⊢ ((h.compl₂ id) x✝¹) x✝ = (h x✝¹) x✝
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:
ext

Goal state after:
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ₗ
x✝¹ : Mₗ
x✝ : N
⊢ ((f.compl₁₂ id id) x✝¹) x✝ = (f x✝¹) x✝
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:
constructor

Goal state after:
case mp
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₂

case mpr
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₁ = f₂ → f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
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:
ext

Goal state after:
ι : 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
a✝ : ι
⊢ ((((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
          (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R)) ∘ₗ
        Finsupp.lsingle a✝)
      1 =
    (Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a✝) 1
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:
simpa [← Finset.coe_subset]

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:
ext

Goal state after:
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
x✝ : Nₗ
⊢ (↑R g ∘ₗ f (x✝² + x✝¹)) x✝ = (↑R g ∘ₗ f x✝² + ↑R g ∘ₗ f x✝¹) x✝
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:
ext

Goal state after:
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
x✝ : Nₗ
⊢ (↑R g ∘ₗ f (x✝² • x✝¹)) x✝ = ((RingHom.id A) x✝² • ↑R g ∘ₗ f x✝¹) x✝
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
⊢ LinearIndepOn R ![x, y] {0, 1} ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
LinearIndepOn.pair_iff _ (by trivial)

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ (∀ (c d : R), c • ![x, y] 0 + d • ![x, y] 1 = 0 → c = 0 ∧ d = 0) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ((comap p.subtype (p ⊓ p')).liftQ (subToSupQuotient p p') ⋯).ker = ⊥

Tactic:
ker_liftQ_eq_bot

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ⊥ = ⊥

case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0 ∧ t = 0

Tactic:
constructor

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0

case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) ↔
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: case e_f
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ ((Algebra.algebraMap S R) x.1, x.2)) = fun x ↦ x.1 • x.2

Tactic:
ext

Goal state after:
case e_f
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
x✝ : S × M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ ((Algebra.algebraMap S R) x.1, x.2)) x✝ = x✝.1 • x✝.2
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ (RingEquiv.moduleEndSelf A).toFun ((algebraMap R Aᵐᵒᵖ) x✝) = (algebraMap R (Module.End A A)) x✝

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ ((RingEquiv.moduleEndSelf A).toFun ((algebraMap R Aᵐᵒᵖ) x✝)) 1 = ((algebraMap R (Module.End A A)) x✝) 1
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ (RingEquiv.moduleEndSelfOp A).toFun ((algebraMap R A) x✝) = (algebraMap R (Module.End Aᵐᵒᵖ A)) x✝

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
x✝ : R
⊢ ((RingEquiv.moduleEndSelfOp A).toFun ((algebraMap R A) x✝)) 1 = ((algebraMap R (Module.End Aᵐᵒᵖ A)) x✝) 1