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 ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ • x✝)) i✝ = ((RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝) i✝

Tactic:
;

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 ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ • x✝)) i✝ = ((RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝) i✝
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 ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ + x✝)) i✝¹) i✝ = ((__spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝) i✝¹) i✝

Tactic:
;

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 ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ + x✝)) i✝¹) i✝ = ((__spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝) i✝¹) i✝
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 ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ • x✝)) i✝¹) i✝ = (((RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝) i✝¹) i✝

Tactic:
;

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 ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ • x✝)) i✝¹) i✝ = (((RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝) i✝¹) i✝
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✝ : Fintype ι
x✝² x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² + x✝¹) x✝ = (equivFunOnFintype.toFun x✝² + equivFunOnFintype.toFun x✝¹) x✝

Tactic:
;

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✝ : Fintype ι
x✝² x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² + x✝¹) x✝ = (equivFunOnFintype.toFun x✝² + equivFunOnFintype.toFun x✝¹) x✝
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✝ : Fintype ι
x✝² : R
x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² • x✝¹) x✝ = ((RingHom.id R) x✝² • equivFunOnFintype.toFun x✝¹) x✝

Tactic:
;

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✝ : Fintype ι
x✝² : R
x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² • x✝¹) x✝ = ((RingHom.id R) x✝² • equivFunOnFintype.toFun x✝¹) x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (FinVec.Forall fun x_1 ↦
      FinVec.Forall fun x_2 ↦ x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (FinVec.Forall fun x_1 ↦
      FinVec.Forall fun x_2 ↦ x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'
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
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this✝ : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
this : ↑((Finsupp.lsingle i) m).support ⊆ {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥

Tactic:
;

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this✝ : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
this : ↑((Finsupp.lsingle i) m).support ⊆ {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)

Tactic:
;

Goal state after:
ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)
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✝¹ : ι
x✝ : M
⊢ x✝ ∈ R ∙ v x✝¹ ↔ x✝ ∈ Submodule.map (Finsupp.linearCombination R v) (Finsupp.lsingle x✝¹).range

Tactic:
;

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
a✝ : ι
⊢ a✝ ∈ (DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩).support ↔ a✝ ∈ f.support

Tactic:
;

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.BilinearMap

Goal state before:
pp: 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₁ : 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'

Tactic:
;

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

Tactic:
;

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
x✝ : Nₗ
⊢ (↑R g ∘ₗ f (x✝² • x✝¹)) x✝ = ((RingHom.id A) x✝² • ↑R g ∘ₗ f x✝¹) x✝

Tactic:
;

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.DFinsupp

Goal state before:
pp: case neg
ι : 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 : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h✝ : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
h : ¬j = i
⊢ f j ∈ p j

Tactic:
· simpa [h] using hf j

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨x, hx⟩ ∈ (subToSupQuotient p p').range

Tactic:
;

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨x, hx⟩ ∈ (subToSupQuotient p p').range
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
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)

Tactic:
;

Goal state after:
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
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)
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
this : (a * d) • s = (b * c) • s
hs : ¬s = 0
⊢ False

Tactic:
;

Goal state after:
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
this : (a * d) • s = (b * c) • s
hs : ¬s = 0
⊢ False
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: 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
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (subToSupQuotient p p') ⟨y, hy⟩ = Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩

Tactic:
;

Goal state after:
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
x✝ : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ (subToSupQuotient p p') ⟨y, hy⟩ = Quot.mk ⇑(comap (p ⊔ p').subtype p').quotientRel ⟨y + z, hx⟩
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
this : (a * d) • t = (b * c) • t
ht : ¬t = 0
⊢ False

Tactic:
;

Goal state after:
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
this : (a * d) • t = (b * c) • t
ht : ¬t = 0
⊢ False
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✝)) 1 = ((algebraMap R (Module.End A A)) x✝) 1

Tactic:
;

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✝)) 1 = ((algebraMap R (Module.End Aᵐᵒᵖ A)) x✝) 1

Tactic:
;

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
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝ = (f * (RingHom.pi fun i ↦ algebraMap R (A i)) a) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝ = (f * (RingHom.pi fun i ↦ algebraMap R (A i)) a) x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ (a • f) x✝ = ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
a : R
f : (i : ι) → A i
x✝ : ι
⊢ (a • f) x✝ = ((RingHom.pi fun i ↦ algebraMap R (A i)) a * f) x✝
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A i)
inst✝² : (i : ι) → Algebra R (A i)
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
g : (i : ι) → B →ₐ[R] A i
r : R
x✝ : ι
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) x✝ = (algebraMap R ((i : ι) → A i)) r x✝

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
A : ι → Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (A i)
inst✝² : (i : ι) → Algebra R (A i)
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
g : (i : ι) → B →ₐ[R] A i
r : R
x✝ : ι
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) x✝ = (algebraMap R ((i : ι) → A i)) r x✝