mathlib-initiative/mathlib-tactics huggingface dataset:
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; simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
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; simp [Algebra.algebraMap_eq_smul_one]

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
⊢ (↑↑(RingHom.pi fun i ↦ (g i).toRingHom)).toFun ((algebraMap R B) r) = (algebraMap R ((i : ι) → A i)) r

Tactic:
ext; simp

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

Goal state before:
pp: case neg
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)
⊢ c • a • x + -(a • c • x) = 0

Tactic:
module

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

Goal state before:
pp: case neg
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)
⊢ (b * c) • x + (b * d) • y + ((-b * c) • x + (-b * d) • y) = 0

Tactic:
module

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 = d • a • x + d • b • y + (-(b • c • x) + -(b • d • y))

Tactic:
module

Goal state after:
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) • y = -(c • a • x) + -(c • b • y) + (a • c • x + a • d • y)

Tactic:
module

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
⊢ { toFun := fun ψ ↦ ψ 0, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } = 0

Tactic:
ext; 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
⊢ mapDomainLinearEquiv R S (e₁.trans e₂) = mapDomainLinearEquiv R S e₁ ≪≫ₗ mapDomainLinearEquiv R S e₂

Tactic:
ext; 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 : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
linearIndependent_finCons

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K v ∧ x ∉ span K (range v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)
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
t : Set V
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val

Tactic:
obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
    exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
t b : Set V
hb₁ : b ⊆ t
hb₂ : t ⊆ ↑(span K b)
hb₃ : LinearIndepOn K id b
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val
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
⊢ mapDomain f 0 = 0

Tactic:
ext; 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
⊢ mapDomain f (single a r) = single (f a) r

Tactic:
ext; 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
⊢ map f 0 = 0

Tactic:
ext; 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]
⊢ map f (x + y) = map f x + map f y

Tactic:
ext; 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]
⊢ map f (∑ i ∈ s, x i) = ∑ i ∈ s, map f (x i)

Tactic:
ext; 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 : M
⊢ map f (single m r) = single m (f r)

Tactic:
ext; 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]
⊢ map (AddMonoidHom.id R) x = x

Tactic:
ext; 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]
⊢ map f (map g x) = map (f.comp g) x

Tactic:
ext; 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
hf : Injective f
⊢ comapDomain f hf 0 = 0

Tactic:
ext; 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
hf : Injective f
m : M
r : R
⊢ comapDomain f hf (single (f m) r) = single m r

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id R[M]

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[M]
⊢ (fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x) = x

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[N]
⊢ (fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x) = x

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x y : R[M]
⊢ mapDomain (⇑e) (x + y) = mapDomain (⇑e) x + mapDomain (⇑e) y

Tactic:
ext; 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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
⊢ mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : R[M]
⊢ map (↑e.symm) (map (↑e) x) = x

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : S[M]
⊢ map (↑e) (map (↑e.symm) x) = x

Tactic:
ext; 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
inst✝ : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
⊢ mapAddEquiv M (e₁.trans e₂) = (mapAddEquiv M e₁).trans (mapAddEquiv M e₂)

Tactic:
ext; 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
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
⊢ mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

Tactic:
ext; 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
inst✝ : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
⊢ mapRingEquiv M (e₁.trans e₂) = (mapRingEquiv M e₁).trans (mapRingEquiv M e₂)

Tactic:
ext; 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✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x : R[M]
⊢ map f (-x) = -map f x

Tactic:
ext; 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✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x y : R[M]
⊢ map f (x - y) = map f x - map f y

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff))
      ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff)) x) =
    x

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : MonoidAlgebra R (Multiplicative M)
⊢ (fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff)) x) =
    x

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ erase m 0 = 0

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
r : R
⊢ erase m (single m r) = 0

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff))
      ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff)) x) =
    x

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
A : Type u_8
inst✝ : SMulZeroClass A R
a : A
m : M
r : R
⊢ a • single m r = single m (a • r)

Tactic:
ext; simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : AddMonoidAlgebra R (Additive M)
⊢ (fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff)) x) =
    x

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
r₁ r₂ : R
⊢ single m (r₁ + r₂) = single m r₁ + single m r₂

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
m : M
r : R
⊢ (toAdditive R M) (single m r) = AddMonoidAlgebra.single (Additive.ofMul m) r

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
f : R[M]
⊢ f.coeff.sum single = f

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
⊢ MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Tactic:
ext; simp

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

Goal state before:
pp: case refine_2.inr
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
bg : b0 ∉ g.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
rw [notMem_support_iff.mp bg, mul_zero]

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

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
⊢ g₁ = g₂

Tactic:
have h := coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : (f * g₁).coeff (af * ag) = f.coeff af * g₁.coeff ag
⊢ g₁ = g₂
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r : R
⊢ single m (-r) = -single m r

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r s : R
⊢ single m (r - s) = single m r - single m s

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
⊢ univ⁻¹ = univ

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_pow hn

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
H : ∀ (x : M), f x = (b.repr (f (b i))) i • x
r : R
⊢ r * (b.coord i) (f (b i)) = (b.coord i) (f (b i)) * r

Tactic:
by simpa using congr(b.coord i $(H <| r • b i))

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R {x | ∃ i x_1, single i x_1 = x} = ⊤

Tactic:
refine eq_top_iff'.mpr fun x ↦ ?_
  induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
this : ⨆ i, ⨆ (_ : i ∈ S ∧ i ∈ s), i = ⨆ i ∈ s, i
⊢ m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i

Tactic:
simpa only [Finset.mem_preimage, iSup_subtype, iSup_and', this]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
by
  simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ + x✝)) = mapRange.linearMap (id.flip x✝¹) + mapRange.linearMap (id.flip x✝)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ : R
x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ • x✝)) = (RingHom.id R) x✝¹ • mapRange.linearMap (id.flip x✝)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Finite ι
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (equivFunOnFinite.symm fun i ↦ lapply i ∘ₗ x) = x

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype = LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p q : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h : IsCompl p q
inst✝ : Module R M
f : M →ₗ[R] ↥p
⊢ p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f = f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h✝ : IsComplemented p
inst✝ : Module R M
q : Submodule R E
h : IsCompl p q
f : ↥p →ₗ[R] M
⊢ (fun f ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) = f

Tactic:
ext; simp

Goal state after: