mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (∀ (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

Tactic:
simp

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 = k ((i.restrictScalarsRange k hk f hf) m)

Tactic:
hk.eq_iff

Goal state after:
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 ↔ p = (i.restrictScalarsRange k hk f hf) m
Module: Mathlib.LinearAlgebra.BilinearMap

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

Tactic:
hk.eq_iff

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
p : P'
⊢ p = ((i.restrictScalarsRange₂ j k hk B hB) m) n ↔ p = ((i.restrictScalarsRange₂ j k hk B hB) m) n
Module: Mathlib.Tactic.Module

Goal state before:
pp: case e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
p : R × M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (-x.1, x.2)) p = ((fun x ↦ -x) ∘ fun x ↦ x.1 • x.2) p

Tactic:
simp

Goal state after:
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
x : ↥(p ⊔ p')
⊢ Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') 0 ↔ ↑x ∈ p'

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x✝¹ : (M ⧸ S) ⧸ map S.mkQ T
x✝ : M ⧸ S
x : M
⊢ (T.mapQ (map S.mkQ T) S.mkQ ⋯) ((S.quotientQuotientEquivQuotientAux T h) (Quotient.mk (Quotient.mk x))) =
    Quotient.mk (Quotient.mk x)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x✝ : M ⧸ T
x : M
⊢ (S.quotientQuotientEquivQuotientAux T h) ((T.mapQ (map S.mkQ T) S.mkQ ⋯) (Quotient.mk x)) = Quotient.mk x

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A₁ i)
inst✝⁴ : (i : ι) → Semiring (A₂ i)
inst✝³ : (i : ι) → Semiring (A₃ i)
inst✝² : (i : ι) → Algebra R (A₁ i)
inst✝¹ : (i : ι) → Algebra R (A₂ i)
inst✝ : (i : ι) → Algebra R (A₃ i)
e : (i : ι) → A₁ i ≃ₐ[R] A₂ i
r : R
i : ι
⊢ (e i) ((algebraMap R ((i : ι) → A₁ i)) r i) = (algebraMap R ((i : ι) → A₂ i)) r i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → Semiring (A₁ i)
inst✝⁷ : (i : ι) → Semiring (A₂ i)
inst✝⁶ : (i : ι) → Semiring (A₃ i)
inst✝⁵ : (i : ι) → Algebra R (A₁ i)
inst✝⁴ : (i : ι) → Algebra R (A₂ i)
inst✝³ : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Unique ι
⊢ ∀ (x : R), (RingEquiv.piUnique fun i ↦ S) ((algebraMap R (ι → S)) x) = (algebraMap R S) x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : α
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).1 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: case snd
α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
x✝¹ : R
x✝ : β
⊢ ((RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x✝¹)).2 x✝ =
    ((algebraMap R ((α → S) × (β → S))) x✝¹).2 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
v w : ι → R
⊢ ⇑(algebraMap R A) ∘ (v + w) = ⇑(algebraMap R A) ∘ v + ⇑(algebraMap R A) ∘ w

Tactic:
simp

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
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
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ 1 = 0 → 0 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case «0»
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
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨0, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

Goal state after:
case «0»
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
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • x = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case «1»
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
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] ((fun i ↦ i) ⟨1, ⋯⟩) =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

Goal state after:
case «1»
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
inst✝ : Nontrivial R
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
⊢ (a * d - b * c) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • 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
c : S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
rcases subsingleton_or_nontrivial S with hS | hS

Goal state after:
case inl
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
c : S
hS : Subsingleton S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

case inr
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
c : S
hS : Nontrivial S
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, 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
b : S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

Tactic:
rcases subsingleton_or_nontrivial S with hS | hS

Goal state after:
case inl
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
b : S
hS : Subsingleton S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]

case inr
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
b : S
hS : Nontrivial S
⊢ LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x✝ a✝ : X
⊢ (((toFinsupp.comp toFreeAbelianGroup).comp (singleAddHom x✝)) 1) a✝ =
    (((AddMonoidHom.id (X →₀ ℤ)).comp (singleAddHom x✝)) 1) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a.support.card = 0 ↔ a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: case empty
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
⊢ sum 0 • t.sum = (map (fun p ↦ p.1 • p.2) (0 ×ˢ t)).sum

Tactic:
simp

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

Goal state before:
pp: case h.empty
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ i ∈ ∅, f i)

Tactic:
simp

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
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
hImaximal : ∀ (t : Set ι), I ⊆ t → LinearIndepOn R v t → I = t
i : ι
hi : i ∉ I
⊢ I ⊆ I ∪ {i}

Tactic:
simp

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

Goal state before:
pp: K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L (⇑(ltoFun K M L L) ∘ AlgHom.toLinearMap)

Tactic:
exact (linearIndependent_monoidHom M L).comp
    (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
    (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
this : (Finsupp.sum 0 fun i a ↦ a • v i) ∈ span R (Set.range v)
hx : (Finsupp.sum 0 fun a b ↦ b • f (v a)) = 0
⊢ (Finsupp.sum 0 fun i a ↦ a • v i) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
a : A
⊢ 0 a = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
a : A
⊢ ∀ (a_1 b : AddChar A M), (a_1 + b) a = a_1 a * b a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝ : AddChar A M
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) ↦
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (f '' range fun x ↦ ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
simp

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hxs : x ∉ s
⊢ LinearIndepOn K id s ∧ id x ∉ span K (id '' s) ↔ LinearIndepOn K id s ∧ x ∉ span K s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Module R S
e₁ : M ≃ N
e₂ : N ≃ O
x✝ : S[M]
a✝ : O
⊢ ((mapDomainLinearEquiv R S (e₁.trans e₂)) x✝).coeff a✝ =
    ((mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂) x✝).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : Module R S
s t : Set M
x✝ : S[M]
inst✝¹ : One M
inst✝ : Subsingleton M
r : R
x : S[M]
⊢ (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun (r • x) =
    (RingHom.id R) r • (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝² : Semiring S✝
inst✝¹ : Monoid R
inst✝ : DistribMulAction R S✝
a : M
S : R
m : S✝
⊢ (↑(singleAddHom a)).toFun (S • m) = (MonoidHom.id R) S • (↑(singleAddHom a)).toFun m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Semiring R
inst✝ : MulOneClass M
m : M
r : R
⊢ r • (of R M) m = single m r

Tactic:
simp

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ 0 ≠ 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ (∀ (c : K), c • ![x, y] 0 ≠ ![x, y] 1) ↔ ∀ (a : K), a • x ≠ y

Tactic:
simp

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

Goal state before:
pp: case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ t = id '' t

Tactic:
simp

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

Goal state before:
pp: case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
x✝ : Set V
⊢ x✝ = id '' x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
⊢ ↑(image₂ f ∅ t) = ↑∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
⊢ ↑(image₂ f s ∅) = ↑∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
x : γ
⊢ x ∈ image₂ f {a} t ↔ x ∈ image (fun b ↦ f a b) t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
x : γ
⊢ x ∈ image₂ f s {b} ↔ x ∈ image (fun a ↦ f a b) s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
a : α
b : β
⊢ image₂ f {a} {b} = {f a b}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
a✝ : N
⊢ (mapDomain f 0).coeff a✝ = (coeff 0) a✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t = id '' t

Tactic:
simp

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

Goal state before:
pp: case e'_4
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ hs.extend hst = id '' hs.extend hst

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
a : M
r : R
a✝ : N
⊢ (mapDomain f (single a r)).coeff a✝ = (single (f a) r).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
a✝ : M
⊢ (map f 0).coeff a✝ = (coeff 0) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
x y : R[M]
a✝ : M
⊢ (map f (x + y)).coeff a✝ = (map f x + map f y).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
s : Finset ι
x : ι → R[M]
a✝ : M
⊢ (map f (∑ i ∈ s, x i)).coeff a✝ = (∑ i ∈ s, map f (x i)).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
r : R
m a✝ : M
⊢ (map f (single m r)).coeff a✝ = (single m (f r)).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝ : Semiring R
x : R[M]
a✝ : M
⊢ (map (AddMonoidHom.id R) x).coeff a✝ = x.coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+ T
g : R →+ S
x : R[M]
a✝ : M
⊢ (map f (map g x)).coeff a✝ = (map (f.comp g) x).coeff a✝

Tactic:
simp

Goal state after: