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

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this : Add α := e.add
⊢ Sort ?u.14

Tactic:
letI := Equiv.mul e

Goal state after:
α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
this✝ : Add α := e.add
this : Mul α := e.mul
⊢ Sort ?u.14
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ f.range ⊔ ((AlgHom.id R S).comp g).range = f.range ⊔ g.range

Tactic:
AlgHom.id_comp

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
⊢ f.range ⊔ g.range = f.range ⊔ g.range
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < Module.rank R M ↔ ∃ x, x ≠ 0

Tactic:
contrapose!; rw [nonpos_iff_eq_zero]; exact rank_zero_iff_forall_zero

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (x + y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x +
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ y

Tactic:
by
        dsimp only [SetLike.coe_sort_coe, NonUnitalAlgHom.coe_comp, Function.comp_apply,
          inclusion_mk, Eq.ndrec, id_eq, eq_mpr_eq_cast]
        apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
        all_goals simp

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
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
⊢ False

Tactic:
simp only [h', ne_eq] at H

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
h' : v₀ = 0
H : ¬⟨0, ⋯⟩ = 0
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
⊢ ∃ r, r • v₀ = v

Tactic:
obtain ⟨r, hr⟩ := h ⟨v, hv⟩

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : ⟨v₀, hv₀⟩ ≠ 0
h : ∀ (v : ↥s), ∃ r, r • ⟨v₀, hv₀⟩ = v
v : V
hv : v ∈ s
r : K
hr : r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩
⊢ ∃ r, r • v₀ = v
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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
⊢ x ∈ p ⊔ f.ker

Tactic:
obtain ⟨⟨y, hy⟩, hxy⟩ :=
    surjective_of_injective ((injective_restrict_iff h).mpr h') ⟨f x, hx⟩

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
h' : Disjoint p f.ker
x : V
hx : x ∈ comap f p
y : V
hy : y ∈ p
hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩
⊢ x ∈ p ⊔ f.ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ → IsUnit f

Tactic:
intro h_inj

Goal state after:
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
h_inj : f.ker = ⊥
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
a : R
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
h : Commute (f a) x
⊢ eval₂ f x (p * C a) = eval₂ f x p * f a

Tactic:
rw [eval₂_mul_noncomm, eval₂_C]
  intro k
  by_cases hk : k = 0
  · simp only [hk, h, coeff_C_zero]
  · simp only [coeff_C_of_ne_zero hk, map_zero, Commute.zero_left]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x (p * q) = 0

Tactic:
by
  rw [eval₂_mul f x]
  exact mul_eq_zero_of_right (p.eval₂ f x) hq

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ eval₂ f (↑n) p = f (eval (↑n) p)

Tactic:
convert! eval₂_at_apply (p := p) f n
  simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ map f ↑n = ↑n

Tactic:
rw [Polynomial.map_natCast]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
ι : Type u_1
s : Finset ι
p : ι → R[X]
x : R
⊢ (∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x

Tactic:
simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p

Tactic:
rw [hn, mul_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ eval₂ f (↑n) p = f (eval (↑n) p)

Tactic:
convert! eval₂_at_apply (p := p) f n
  simp

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False

Tactic:
rw [zero_dvd_iff] at mdvd

Goal state after:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Tactic:
obtain ⟨p, hchar⟩ := CharP.exists R
  rcases char_is_prime_or_zero R p with h | rfl
  exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]

Goal state after:
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
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
⊢ Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph) =
    Submodule.map (LinearMap.fst R E F) f.graph

Tactic:
← LinearEquiv.snd_comp_prodComm,

Goal state after:
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
f : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
⊢ Submodule.map (LinearMap.snd R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph) =
    Submodule.map (LinearMap.snd R F E ∘ₗ ↑(LinearEquiv.prodComm R E F)) f.graph
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsRegular (X ^ n)

Tactic:
suffices IsLeftRegular (X ^ n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ IsLeftRegular (X ^ n)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ (∑ m ∈ range (n + 1), X ^ m * C r ^ (n - m) * ↑(n.choose m)).coeff k = r ^ (n - k) * ↑(n.choose k)

Tactic:
← lcoeff_apply,

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ (lcoeff R k) (∑ m ∈ range (n + 1), X ^ m * C r ^ (n - m) * ↑(n.choose m)) = r ^ (n - k) * ↑(n.choose k)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ((monomial n) a).degree ≤ ↑n

Tactic:
rw [h, (monomial n).map_zero, degree_zero]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree ≤ ↑p.natDegree

Tactic:
apply degree_le_natDegree

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

Goal state before:
pp: case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ q.degree ≤ ↑q.natDegree

Tactic:
apply degree_le_natDegree

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
⊢ (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
conv =>
        lhs
        rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (p - q).degree < q.degree

Tactic:
rw [← degree_neg, neg_sub]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (q - p).degree < q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).leadingCoeff = p.leadingCoeff * a

Tactic:
rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : k ≠ j
⊢ f k = 0

Tactic:
h k hk,

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ j
⊢ f k = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (p.sum fun e a ↦ f a * x ^ e) = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
p.sum_over_range' _ _ hn

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∑ a ∈ range n, f (p.coeff a) * x ^ a = ∑ i ∈ range n, f (p.coeff i) * x ^ i

R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∀ (n : ℕ), f 0 * x ^ n = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ (p.sum fun e a ↦ a * x ^ e) = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
p.sum_over_range' _ _ hn

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∑ a ∈ range n, p.coeff a * x ^ a = ∑ i ∈ range n, p.coeff i * x ^ i

R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
contrapose! hl

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a ≤ b
hne : ¬toLex a = toLex b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ (x : ι), x ∈ {i | a i ≠ b i} → ¬x < i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
contrapose! hl

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x, x ∈ {i | a i ≠ b i} ∧ x < i
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex x < toLex (update x i a) ↔ x i < a

Tactic:
refine ⟨?_, fun h => toLex_strictMono <| lt_update_self_iff.2 h⟩
  rintro ⟨j, hj, h⟩
  dsimp at h
  obtain rfl : j = i := by
    by_contra H
    rw [update_of_ne H] at h
    exact h.false
  rwa [update_self] at h

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
by
  simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
    and_iff_right_iff_imp] using Ne.ne_or_ne _

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g p = (eval g) ((map f) p)

Tactic:
simp [eval₂, eval]

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (p.coeff.sum fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) = ((map f) p).coeff.sum fun s a ↦ a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
r : R
⊢ k (eval₂ f g (C r)) = eval₂ k (⇑k ∘ g) ((map f) (C r))

Tactic:
rw [eval₂_C, map_C, eval₂_C]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : (map f) p = (map f) q
⊢ p = q

Tactic:
simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.vars = ∅

Tactic:
by rw [h]; simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree (C r).totalDegree = p.totalDegree

Tactic:
rw [totalDegree_C, Nat.max_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
rw [totalDegree, Finset.sup_lt_iff] at h

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, (b.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • q.degree ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree

Tactic:
degree_le_natDegree

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree ≤ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + ↑q.natTrailingDegree ≤ ↑(p * q).natTrailingDegree

Tactic:
← trailingDegree_eq_natTrailingDegree hq,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ ↑(p * q).natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
← eraseLead_add_C_mul_X_pow f,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ reflect (N + O) ((f.eraseLead + C f.leadingCoeff * X ^ f.natDegree) * g) =
    reflect N (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree) * reflect O g
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (Polynomial.aevalTower (rename Option.some) (X none)).comp
      (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) =
    AlgHom.id R (MvPolynomial (Option S₁) R)

Tactic:
by ext i : 2; cases i <;> simp

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
rw [key, C_comp] at h

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : C (p.coeff 0) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree

Tactic:
exact fc FG fg

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
apply natDegree_multiset_prod'

Goal state after:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
a✝ : Nontrivial R
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
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:
Nat.add_comm,

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 ^ (1 + n - (1 + n)) = (x + y) ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLE R ↑n = Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
apply le_antisymm
  · intro p hp
    replace hp := mem_degreeLE.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)
  rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
  intro k hk
  apply mem_degreeLE.2
  exact
    (degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I

Tactic:
obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0

Goal state after:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I