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
r : R
x : A
⊢ ((algebraMap R A).toOpposite ⋯) r * op x = op x * ((algebraMap R A).toOpposite ⋯) r

Tactic:
by
    simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]

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

Goal state before:
pp: 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
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ ¬LinearIndependent R ![a • x + b • y, c • x + d • y]

Tactic:
rw [pair_iff]

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
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0
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)
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
refine ⟨c • 1, -a • 1, ?_, by aesop⟩

Goal state after:
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 • 1) • a • x + (-a • 1) • c • x = 0
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
hS : Nontrivial S
a✝ : Nontrivial R
⊢ LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]

Tactic:
simpa using

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

Tactic:
simpa using

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
b : S
hS : Nontrivial S
a✝ : Nontrivial R
⊢ LinearIndependent R ![x + b • y, 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
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y]

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y]
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
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
s : Finset ι
g : ι → R
hrel : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
aux : ∀ j ∈ s, j ≠ i → g j * (f i) (v j) = 0
⊢ g i = 0

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
s : Finset ι
g : ι → R
hrel : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
aux : ∀ j ∈ s, j ≠ i → g j * (f i) (v j) = 0
⊢ g i = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M₀ : Type u_2
inst✝² : AddGroup A
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
ψ : AddChar A M₀
h : ψ 0 = 0 0
⊢ False

Tactic:
simpa using

Goal state after:
A : Type u_1
M₀ : Type u_2
inst✝² : AddGroup A
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
ψ : AddChar A M₀
h : ψ 0 = 0 0
⊢ False
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
v : ι → V
s : Set ι
x : ι
hs : LinearIndepOn K v s
hx : v x ∉ span K (v '' s)
⊢ LinearIndepOn K v (insert x s)

Tactic:
by
  rw [← union_singleton]
  have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
  apply hs.union (LinearIndepOn.singleton x0)
  rwa [image_singleton, disjoint_span_singleton' x0]

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
a : V
s : Set V
⊢ LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s)

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
a : V
s : Set V
⊢ LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s)
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
a : V
h : LinearIndepOn K id s
⊢ a ∈ span K s ↔ LinearIndepOn K id (insert a s) → a ∈ s

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
a : V
h : LinearIndepOn K id s
⊢ a ∈ span K s ↔ LinearIndepOn K id (insert a s) → a ∈ s
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : MulOneClass M
s : Set M
m : M
inst✝ : Nontrivial R
h : (of R M) m ∈ Submodule.span R ↑(Submonoid.map (of R M) (Submonoid.closure s))
⊢ m ∈ Submonoid.closure s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ x ∈ span K (range v)

Tactic:
(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq),

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ ((algebraMap R K) c)⁻¹ • -y ∈ 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
s : Set V
t✝ : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t✝)
t s' : Finset V
hs' : ↑s' ⊆ s
x✝ : s ∩ ↑∅ = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ ∅))
⊢ s ⊆ ↑(span K ↑s')

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝ : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t✝)
t s' : Finset V
hs' : ↑s' ⊆ s
x✝ : s ∩ ↑∅ = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ ∅))
⊢ s ⊆ ↑(span K ↑s')
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
he : Injective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Injective (map f)

Tactic:
simpa using

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Injective (mapRange ⇑f ⋯)
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
he : Surjective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Surjective (map f)

Tactic:
simpa using

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Surjective (mapRange ⇑f ⋯)
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
x : R[N]
hx : ↑x.coeff.support ⊆ Set.range f
hf : Injective f
⊢ mapDomain f (comapDomain f hf x) = x

Tactic:
ext : 1; exact Finsupp.mapDomain_comapDomain _ hf _ hx

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
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ s ⊆ ↑(K ∙ b₁ ⊔ (span K ↑s' ⊔ span K ↑t))
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
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

Tactic:
simpa using

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ span K (insert b₂ (↑s' ∪ ↑t))
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
e : M ≃* N
r : R
m : M
⊢ (mapDomainRingEquiv R e) (single m r) = single (e m) r

Tactic:
simp [mapDomainRingEquiv]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
N : Type u_8
inst✝ : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ ∀ (m : M) (r : R), f (single m r) = g (single m r)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
N : Type u_8
inst✝ : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ ∀ (m : M) (r : R), f (single m r) = g (single m r)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
motive : R[M] → Prop
x : R[M]
zero : motive 0
single_add : ∀ (m : M) (r : R) (x : R[M]), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Semiring R
motive : R[M] → Prop
x : R[M]
zero : motive 0
single_add : ∀ (m : M) (r : R) (x : R[M]), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)
⊢ motive 0
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (a a_1 : R[M]) (a_2 : M),
    (a_1.coeff.sum fun m₁ r₁ ↦ a.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = a_2 then r₁ * r₂ else 0) =
      a.coeff.sum fun i n ↦ a_1.coeff.sum fun i_1 n_1 ↦ if i_1 * i = a_2 then n_1 * n else 0

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ ∀ (a a_1 : R[M]) (a_2 : M),
    (a_1.coeff.sum fun m₁ r₁ ↦ a.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = a_2 then r₁ * r₂ else 0) =
      a.coeff.sum fun i n ↦ a_1.coeff.sum fun i_1 n_1 ↦ if i_1 * i = a_2 then n_1 * n else 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = d * g
⊢ ∀ (d : M), d * g ≠ g'

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = d * g
⊢ ∀ (d : M), ¬g' = d * g
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = g * d
⊢ ∀ (d : M), g * d ≠ g'

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = g * d
⊢ ∀ (d : M), ¬g' = g * d
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Nontrivial R
a b : M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Nontrivial R
a b : M
h : (of R M) a = (of R M) b
⊢ a = b
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (r : R), f (single 1 r) = g (single 1 r)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (r : R), f (single 1 r) = g (single 1 r)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (m : M), f (single m 1) = g (single m 1)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (m : M), f (single m 1) = g (single m 1)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (single m r)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : AddZeroClass M
a b : Multiplicative M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : AddZeroClass M
a b : Multiplicative M
h : (of R M) a = (of R M) b
⊢ a = b
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive 0
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
l : List α
h : ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) l → ∀ (b : α), b ∈ Quot.mk (⇑(isSetoid α)) l → (r a b ↔ r' (f a) (f b))
⊢ ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → decide (r a b) = decide (r' (f a) (f b))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
l : List α
h : ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) l → ∀ (b : α), b ∈ Quot.mk (⇑(isSetoid α)) l → (r a b ↔ r' (f a) (f b))
⊢ ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (r a b ↔ r' (f a) (f b))