mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
⊢ NonUnitalSemiring α

Tactic:
apply e.injective.nonUnitalSemiring _ <;> intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
nsmul : SMul ℕ α := ⋯
⊢ e 0 = 0

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
nsmul : SMul ℕ α := Equiv.smul ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ (fun x ↦ -r + x) ⁻¹' σ a ↔ x ∈ σ (↑ₐ r + a)

Tactic:
mem_preimage,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ -r + x ∈ σ a ↔ x ∈ σ (↑ₐ r + a)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B), (0 * x ⊗ₜ[R] y) • m = 0 • x ⊗ₜ[R] y • m

Tactic:
intro a b
      simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
hx : ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := hx

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R ↑a = quasispectrum R a

Tactic:
quasispectrum_eq_spectrum_union_zero,

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ spectrum R ↑a ∪ {0} = quasispectrum R a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Function.LeftInverse e ⇑(algebraMap R₁ R₃)

Tactic:
convert! hfge ▸ hf.left_inv.comp hg.left_inv

Goal state after:
R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ ⇑(algebraMap R₁ R₃) = ⇑(algebraMap R₂ R₃) ∘ ⇑(algebraMap R₁ R₂)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S b)

Tactic:
quasispectrum_eq_spectrum_union_zero,

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S b ∪ {0})
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x : S ⊗[R] S
x✝¹ x✝ : S
⊢ (LinearMap.mul' R S).toFun (s • x✝¹ ⊗ₜ[R] x✝) = (RingHom.id S) s • (LinearMap.mul' R S).toFun (x✝¹ ⊗ₜ[R] x✝)

Tactic:
by simp [TensorProduct.smul_tmul', mul_assoc]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ IsSelfAdjoint ↑a ↔ IsSelfAdjoint a

Tactic:
by
  simp only [isSelfAdjoint_iff, ← inr_star, inr_injective.eq_iff]

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a

Tactic:
simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]
  lift u to Aˣ using hu
  rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
⊢ 0 ≤ c * a * star c

Tactic:
by
  simpa only [star_star] using star_left_conjugate_nonneg ha (star c)

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c

Tactic:
simpa only [star_star] using star_left_conjugate_le_conjugate hab (star c)

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
inst✝ : Nontrivial R
n : ℕ
H : ∃ f, LinearIndependent R f
⊢ ↑n ≤ Module.rank R M

Tactic:
by simpa using H.choose_spec.cardinal_lift_le_rank

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

Goal state before:
pp: case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : ∃ v, v ≠ 0 ∧ W = K ∙ v
⊢ IsAtom W

Tactic:
rcases h with ⟨v, ⟨hv, rfl⟩⟩

Goal state after:
case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (K ∙ v)
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
inst✝ : Free R M
h : ∀ (s : Set M) (a : Basis (↑s) R M), ¬s.Finite
⊢ finrank R M = 0

Tactic:
by
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R M
    exact (h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim
  obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›
  have := Set.Infinite.to_subtype (h _ b)
  exact b.linearIndependent.finrank_eq_zero_of_infinite

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

Goal state before:
pp: case hx
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
⊢ w ∉ span K s

Tactic:
simp [hs, hw]

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

Goal state before:
pp: case h
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ x + -f x • w ∈ span K s

Tactic:
simp [hs, hw]

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
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
⊢ ∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y

Tactic:
set fg := fun z => f ⟨x z, hx z⟩ + g ⟨y z, hy z⟩

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 g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
⊢ ∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F E
⊢ ⊥ = ⊤ ↔ Module.rank F E = 1

Tactic:
by
  have := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← rank_top, Subalgebra.rank_eq_one_iff, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ((p + q).sum fun e a ↦ f a * x ^ e) = (p.sum fun e a ↦ f a * x ^ e) + q.sum fun e a ↦ f a * x ^ e

Tactic:
apply sum_add_index <;> simp [add_mul]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
⊢ motive a

Tactic:
by
  -- the arguments are enough to construct a subalgebra, and a mapping into it from X
  let s : Subalgebra R (FreeAlgebra R X) :=
    { carrier := {x | motive x}
      mul_mem' := mul _ _
      add_mem' := add _ _
      algebraMap_mem' := grade0 }
  let of : X → s := Subtype.coind (ι R) grade1
  -- the mapping through the subalgebra is the identity
  have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) := by
    ext
    simp [of]
  -- finding a proof is finding an element of the subalgebra
  suffices a = lift R of a by
    rw [this]
    exact Subtype.prop (lift R of a)
  simp only [AlgHom.ext_iff, AlgHom.coe_id, id_eq, AlgHom.coe_comp, Subalgebra.coe_val,
    Function.comp_apply] at of_id
  exact of_id a

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
⊢ ringChar R = 0 ↔ CharZero R

Tactic:
by
  rw [ringChar.eq_iff, charP_zero_iff_charZero]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case refine_2
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
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂

Tactic:
intro y₁ y₂ hy₁ hy₂

Goal state after:
case refine_2
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
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ y₁ = y₂
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natDegree
H : p = 0
⊢ False

Tactic:
simp [H] at h

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

Goal state before:
pp: R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
p : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ ↑n = 0

Tactic:
← C_inj (R := R),

Goal state after:
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
p : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ C ↑n = C 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
    Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
by
  rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
  · rw [mem_antidiagonal]
  rintro ⟨df', dg'⟩ hmem hne
  obtain h | hdf' := lt_or_ge df df'
  · rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
  obtain h | hdg' := lt_or_ge dg dg'
  · rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
  obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
  exact (hne rfl).elim

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = 1

Tactic:
← coeff_one_zero,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = coeff 1 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ n a, f = (monomial n) a

Tactic:
Finset.card_le_one_iff_subset_singleton

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))

Tactic:
refine sum_congr rfl fun y _hy => ?_

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑d.succ
y : ℕ
_hy : y ∈ range d
⊢ ↑d.succ * (↑(d.choose y) * y✝ ^ y) = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
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:
by
  rw [Algebra.adjoin_singleton_eq_range_aeval] at h
  simp_all

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ (∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i) → g₁ ≤ g₂

Tactic:
intro h' x

Goal state after:
case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
x : ι
⊢ g₁ x ≤ g₂ x
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ (↑c).coeff 0 • p = ↑c * p

Tactic:
← Polynomial.C_mul',

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ C ((↑c).coeff 0) * p = ↑c * p
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ s a = 0 a

Tactic:
simp [← cons_succ a y s, c]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
k : ℕ
h : p ≠ 0
⊢ degreeOf i (p * X i ^ k) = degreeOf i p + k

Tactic:
by
  induction k with
  | zero => rw [pow_zero, mul_one, add_zero]
  | succ k hk =>
    have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
    rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d ≠ 0 → (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

Tactic:
hd0

Goal state after:
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N a b : ℕ
⊢ revAtFun N a = revAtFun N b → a = b

Tactic:
hab

Goal state after:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
i : ℕ
⊢ (reflect N f).coeff i = f.coeff ((revAt N) i)

Tactic:
rcases f with ⟨f⟩
  simp only [reflect, coeff]
  calc
    f.coeff.embDomain (revAt N) i
      = f.coeff.embDomain (revAt N) (revAt N (revAt N i)) := by rw [revAt_invol]
    _ = f.coeff (revAt N i) := Finsupp.embDomain_apply_self _ _ _

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ Polynomial.eval₂ φ (a default) (eval₂ Polynomial.C (fun x ↦ Polynomial.X) ((monomial d) r)) =
    eval₂ φ a ((monomial d) r)

Tactic:
rw [← MvPolynomial.uniqueAlgEquiv_apply (R := R) (σ := σ), uniqueAlgEquiv_monomial]
    simp only [Polynomial.eval₂_monomial, eval₂_monomial]
    rw [Finsupp.unique_single d, Finsupp.prod_single_index]
    · simp
    · simp only [pow_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ N

Tactic:
rw [← Nat.sub_add_cancel hnN]

Goal state after:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ (N - n + n)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
refine C_mul_pow _ _ ?_ df
      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
      exact Nat.succ_ne_zero _

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

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ ¬(Multiset.map leadingCoeff t).prod = 0

Tactic:
apply right_ne_zero_of_mul h

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Tactic:
change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - 1 - n) = (x + y) ^ n

Tactic:
← tsub_add_eq_tsub_tsub,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
⊢ (x + y) ^ n * y ^ (n + 1 - (1 + n)) = (x + y) ^ n