mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ (spectrum R (a, b))ᶜ = (spectrum R a ∪ spectrum R b)ᶜ

Tactic:
simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.ofPred_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : αᵐᵒᵖ
hab : a ≤ b
c : αᵐᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Order.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : αᵃᵒᵖ
hab : a ≤ b
c : αᵃᵒᵖ
⊢ unop a ≤ unop b

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
⊢ LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t

Tactic:
by
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
  · exact h.mono subset_union_left
  apply (h.mono subset_union_right).map
  simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: F : Type u_6
E : Type u_7
R : Type u_8
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : PartialOrder E
inst✝⁸ : StarAddMonoid E
inst✝⁷ : NonUnitalRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : SelfAdjointDecompose E
inst✝² : FunLike F E R
inst✝¹ : OrderHomClass F E R
inst✝ : AddMonoidHomClass F E R
a : E
ha : IsSelfAdjoint a
f : F
⊢ IsSelfAdjoint (f a)

Tactic:
by
  obtain ⟨b, c, hb, hc, rfl⟩ := ha.exists_nonneg_sub_nonneg
  have h₁ := OrderHomClass.mono f hb
  have h₂ := OrderHomClass.mono f hc
  cfc_tac

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : ↑s
a : R
ha : a ≠ 0
ha' : a • ↑i = 0
⊢ (Finsupp.linearCombination R fun x ↦ id ↑x) (Finsupp.single i a) = 0

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndepOn R id ↑s.toFinset

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndepOn R id ↑s.toFinset

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f))) (f ↑b) = ↑b

Tactic:
fb_eq,

Goal state after:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f))) (hC ⟨f ↑b, ⋯⟩) = ↑b
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
h✝ : Nontrivial R
⊢ finrank R M = 0

Tactic:
obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
⊢ finrank R M = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ ⟨↑v, ⋯⟩ ≠ ⟨w, ⋯⟩

Tactic:
apply_fun (f ∘ (↑))
    simp [hw]

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
h_star : Commute a (star b)
⊢ ∀ b_1 ∈ {b}, Commute a (star b_1)

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = σ (Classical.choose ⋯) • y + σ (Classical.choose ⋯) • y

Tactic:
← add_smul,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = (σ (Classical.choose ⋯) + σ (Classical.choose ⋯)) • y
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * f = 1

Tactic:
← this

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
f g : End K (Fin n → K)
hfg : f * g = 1
ginj : Injective ⇑g
i : (Fin n → K) →ₗ[K] Fin n → K
hi : g ∘ₗ i = id
this : i = f
⊢ g * i = 1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ ∀ x ∈ f.ker, g x ∈ f.ker

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
have := nontrivial_of_invariantBasisNumber K
  obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)
  -- `Module.Finite.finite_basis` is in a much later file, so we copy its proof to here
  have : Finite s := by
    obtain ⟨t, ht⟩ := ‹Module.Finite K V›
    exact basis_finite_of_finite_spans t.finite_toSet ht hs
  have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩
  rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this

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

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
w : V
hS : finrank K ↥S = 1
hw : w ∈ S
hw0 : w ≠ 0
this : FiniteDimensional K ↥S
⊢ K ∙ w ≤ S

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑z₁ + ↑0 = ↑z₂

Tactic:
simpa

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

Goal state before:
pp: K : Type u
V : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
W : Type u_1
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Module A V
inst✝³ : AddCommGroup W
inst✝² : Module K W
inst✝¹ : Module A W
inst✝ : LinearMap.CompatibleSMul V W K A
h : finrank K W = 1
f : V →ₗ[A] W
w : f ≠ 0
⊢ Surjective ⇑f

Tactic:
by
  change Surjective (f.restrictScalars K)
  obtain ⟨v, n⟩ := DFunLike.ne_iff.mp w
  intro z
  obtain ⟨c, rfl⟩ := (finrank_eq_one_iff_of_nonzero' (f v) n).mp h z
  exact ⟨c • v, by simp⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_comm
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ = liftFun R X f b✝ + liftFun R X f a✝

Tactic:
add_comm

Goal state after:
case add_comm
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f b✝ + liftFun R X f a✝ = liftFun R X f b✝ + liftFun R X f a✝
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f y

Tactic:
← this

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S✝
σ : R →+* S✝
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S✝ F
f : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
this : (Submodule.inclusion ⋯) x = y
⊢ ↑(f.domRestrict S) x = ↑f ((Submodule.inclusion ⋯) x)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ n.minFacProp (n.minFacAux x✝)

Tactic:
minFacAux

Goal state after:
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ -a

Tactic:
lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b

Goal state after:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
b : ℕ
⊢ ↑↑b = 0 ↔ ↑p ∣ ↑b
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ 0 = 1 ↔ Subsingleton R

Tactic:
subsingleton_iff_zero_eq_one

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ Subsingleton R ↔ Subsingleton R
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Subsingleton R
⊢ ringChar R = 1

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ¬↑k = 0

Tactic:
← Ne,

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
k : ℕ
h : NeZero ↑k
⊢ ↑k ≠ 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃! b, (a, b) ∈ g

Tactic:
refine existsUnique_of_exists_of_unique ?_ ?_
  · convert! ha
    simp
  intro y₁ y₂ hy₁ hy₂
  have hy : ((0 : E), y₁ - y₂) ∈ g := by
    convert! g.sub_mem hy₁ hy₂
    exact (sub_self _).symm
  exact sub_eq_zero.mp (hg hy (by simp))

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : A →ₐ[R] B
g : M →* B
h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
by simp [liftNCRingHom]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
⊢ (r • p).support ⊆ p.support

Tactic:
intro i hi

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
g : Multiplicative M →* B
h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)
⊢ ∀ (r : R), (↑↑(liftNCRingHom (↑f) g h_comm)).toFun ((algebraMap R A[M]) r) = (algebraMap R B) r

Tactic:
by simp [liftNCRingHom]

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

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f * fs.prod).coeff.support.sup degb ≤ (List.map (fun f ↦ f.coeff.support.sup degb) (f :: fs)).sum

Tactic:
List.map_cons,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f : R[A]
fs : List R[A]
⊢ (f * fs.prod).coeff.support.sup degb ≤
    (f.coeff.support.sup degb :: List.map (fun f ↦ f.coeff.support.sup degb) fs).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case hnc
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 0
⊢ p.natDegree ≤ 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).leadingCoeff = p.leadingCoeff

Tactic:
add_comm

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (q + p).leadingCoeff = p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
rcases h1 with ⟨q, rfl⟩

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬p.coeff (Function.invFun D (supDegree D p)) = 0

Tactic:
← Ne,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ p.coeff (Function.invFun D (supDegree D p)) ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ p.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff * (X ^ n).leadingCoeff ≠ 0

Tactic:
simpa

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

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D (0 * q) = supDegree D 0 + supDegree D q

Tactic:
Subsingleton.eq_zero q,

Goal state after:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D (0 * 0) = supDegree D 0 + supDegree D 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h : Function.Injective (map f)
r r' : R
eq : f r = f r'
⊢ map f (C r) = map f (C r')

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x a : A
h : a ∈ R[x]
⊢ ∃ p, (aeval x) p = a

Tactic:
Algebra.adjoin_singleton_eq_range_aeval

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x a : A
h : a ∈ (aeval x).range
⊢ ∃ p, (aeval x) p = a
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ R[x]
h : y = ↑a
⊢ ∃ p, (aeval x) p = y

Tactic:
Algebra.adjoin_singleton_eq_range_aeval

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
a : ↥R[x]
y : A := ↑a
this : y ∈ (aeval x).range
h : y = ↑a
⊢ ∃ p, (aeval x) p = y
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.coeff f.natDegree

Tactic:
rw [(degree_eq_iff_natDegree_eq _).1 dz]

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f.coeff 0 = f.coeff Zero.zero

R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : f.degree = 0
⊢ f ≠ 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝⁴ : Zero α
inst✝³ : AddCommMonoid β
inst✝² : Preorder β
inst✝¹ : IsOrderedCancelAddMonoid β
inst✝ : AddLeftStrictMono β
f : ι →₀ α
g : ι → α → β
h : ∀ i ∈ f.support, 0 < g i (f i)
hf : f ≠ 0
⊢ f.support.Nonempty

Tactic:
simpa

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ m > P.natDegree, P.coeff m • Q = 0

Tactic:
intro i hi

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
i : ℕ
hi : i > P.natDegree
⊢ P.coeff i • Q = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case step.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h✝ : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P * P.coeff l • Q = 0

Tactic:
smul_eq_C_mul,

Goal state after:
case step.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h✝ : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P * (C (P.coeff l) * Q) = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = 0 ↔ a = 0

Tactic:
by rw [← map_zero C, C_inj]

Goal state after: