mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } ≤ some s

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some s

Tactic:
· exact WithBot.coe_le_coe.2 ⟨le_sup_left, inf_le_left⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ : Interval α
s t : NonemptyInterval α
h✝ : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ⊥ ≤ some s
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
by
  simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ s t : NonemptyInterval α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
    rw [inv_pure, inv_eq_of_mul_eq_one_right hab]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
a : Γ
r s : R
⊢ (single a) (r + s) = (single a) r + (single a) s

Tactic:
ext : 1; exact Pi.single_add (f := fun _ => R) a r s

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
this : x.coeff x.order = 0
⊢ x = 0

Tactic:
rwa [coeff_order_eq_zero] at this

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ b = a + b - a

Tactic:
abel

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mpr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|

Tactic:
intro ⟨n, hn⟩
    refine ⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩
    refine ⟨(ofLex x).orderTop.untop (by simpa using hx), ?_, ?_⟩
    · -- all coefficients before the leading coefficient are zero
      intro j hj
      trans 0
      · apply coeff_eq_zero_of_lt_orderTop
        simpa [← h] using hj
      · suffices (ofLex |x|).coeff j = 0 by simp [this]
        apply coeff_eq_zero_of_lt_orderTop
        simpa using hj
    -- the leading coefficient determines the relation
    rw [ofLex_smul, coeff_smul]
    suffices |(ofLex y).leadingCoeff| < (n + 1) • |(ofLex x).leadingCoeff| by
      simp_rw [← leadingCoeff_abs] at this
      rw [leadingCoeff_of_ne_zero (by simpa using hy), leadingCoeff_of_ne_zero (by simpa using hx)]
        at this
      convert! this using 3 <;> simp [h]
    refine lt_of_le_of_lt hn <| nsmul_lt_nsmul_left ?_ (by simp)
    rwa [abs_pos, leadingCoeff_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x✝ : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx : x ∈ ((of R).symm (x✝ • y)).support
⊢ (VAddAntidiagonal x ⋯).Nonempty

Tactic:
contrapose! hx

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
x✝ : R⟦Γ⟧
y : HahnModule Γ' R V
x : Γ'
hx : VAddAntidiagonal x ⋯ = ∅
⊢ x ∉ ((of R).symm (x✝ • y)).support
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
⊢ f (∑ i ∈ cons i s h✝, l i) ≤ (cons i s h✝).sup' ⋯ fun i ↦ f (l i)

Tactic:
simp only [sum_cons, le_sup'_iff, mem_cons, exists_eq_or_imp]

Goal state after:
case cons
R : Type u_1
inst✝¹ : LinearOrder R
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : α → R
nonarch : IsNonarchimedean f
s✝ : Finset β
l : β → α
i : β
s : Finset β
h✝ : i ∉ s
hs : s.Nonempty
hind : f (∑ i ∈ s, l i) ≤ s.sup' hs fun i ↦ f (l i)
⊢ f (l i + ∑ i ∈ s, l i) ≤ f (l i) ∨ ∃ a ∈ s, f (l i + ∑ i ∈ s, l i) ≤ f (l a)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
by
  by_cases hx : x = (0 : R⟦Γ⟧); · simp [HahnSeries.coeff_zero, hx]
  by_cases hy : (of R).symm y = 0; · simp [hy, coeff_smul]
  rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, coeff_smul,
    HahnSeries.leadingCoeff_of_ne_zero hx, HahnSeries.leadingCoeff_of_ne_zero hy, ← vadd_eq_add,
    Finset.vaddAntidiagonal_min_vadd_min, Finset.sum_singleton]
  simp [HahnSeries.orderTop, hx, hy]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∃ m < n + 1, f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
by
  obtain ⟨m, hm_lt, hM⟩ := finset_image_add (by aesop) (by aesop) hna
    (fun m => a ^ m * b ^ (n - m) * ↑(n.choose m)) (Finset.range (n + 1))
  simp only [Finset.nonempty_range_iff, ne_eq, Nat.succ_ne_zero, not_false_iff, Finset.mem_range,
    forall_true_left] at hm_lt
  refine ⟨m, hm_lt, ?_⟩
  simp only [← add_pow] at hM
  rw [mul_comm] at hM
  exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).coeff (x.order + y.order) ≠ 0

Tactic:
coeff_mul_order_add_order x y

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x.leadingCoeff * y.leadingCoeff ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop

Tactic:
rw [add_nsmul, pow_add]

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop

Tactic:
by rw [pow_one]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
⊢ ∀ (a₁ b₁ a₂ b₂ : α),
    a₁ ≈ a₂ →
      b₁ ≈ b₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) a₁ b₁ = Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) a₂ b₂

Tactic:
refine fun x₁ x₂ y₁ y₂ hx hy ↦ propext ⟨?_, ?_⟩ <;> intro h
    · exact .trans (.single <| .inr (symm hx)) <| .trans h (.single <| .inr hy)
    · exact .trans (.single <| .inr hx) <| .trans h (.single <| .inr (symm hy))

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.single
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ : α
a✝ : x ≤ b✝ ∨ x ≈ b✝
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧

pp: case h.h.tail
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ c✝ : α
a✝¹ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
a✝ : b✝ ≤ c✝ ∨ b✝ ≈ c✝
a_ih✝ : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦c✝⟧

Tactic:
on_goal 2 => rename_i IH; apply IH.trans

Goal state after:
case h.h.single
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ : α
a✝ : x ≤ b✝ ∨ x ≈ b✝
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧

case h.h.tail
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y b✝ c✝ : α
a✝¹ : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x b✝
a✝ : b✝ ≤ c✝ ∨ b✝ ≈ c✝
IH : Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H ⟦b✝⟧
⊢ Quotient.lift f H ⟦b✝⟧ ≤ Quotient.lift f H ⟦c✝⟧
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
f : Partial seed
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
⊢ ↑↑f x = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))

Tactic:
← f.prop.baseEmbedding_le.2 heq

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
f : Partial seed
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
⊢ ↑seed.baseEmbedding ⟨↑x, hx'⟩ = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h.inr
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₂ : y ≤ x ∨ y ≈ x
h : x ≈ y
⊢ ⟦x⟧ = ⟦y⟧

Tactic:
exact Quotient.sound h

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
⊢ x - ↑y = x - ↑z + (↑z - ↑y)

Tactic:
abel

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup = B.unitGroup
⊢ A = B

Tactic:
by simpa only [le_antisymm_iff, unitGroup_le_unitGroup] using h

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
⊢ ↑y - ↑z = ↑y - x + (x - ↑z)

Tactic:
abel

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : FiniteElement K
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := x.2
    refine ⟨n, (le_abs_self x).trans ?_⟩
    simpa using! hn

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk ↑(↑n / ↑d) ⋯) = ↑(↑n / ↑d)

Tactic:
| div n d hd
   => 

Goal state after:
case div
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
n : ℤ
d : ℕ
hd : d ≠ 0
a✝ : n.natAbs.Coprime d
⊢ mk (FiniteElement.mk ↑(↑n / ↑d) ⋯) = ↑(↑n / ↑d)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
x y : R
⊢ mk (FiniteElement.mk (f x * f y) ⋯) = mk (FiniteElement.mk (f x) ⋯) * mk (FiniteElement.mk (f y) ⋯)

Tactic:
exact mk.map_mul
      (.mk _ (mk_map_nonneg_of_archimedean f x)) (.mk _ (mk_map_nonneg_of_archimedean f y))

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case monomial.monomial
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
⊢ (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a * (monomial m) b)) =
    (monomial n) a • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial m) b)) +
      (monomial m) b • (PolynomialModule.map A ↑d) (PolynomialModule.equivPolynomial.symm ((monomial n) a))

Tactic:
| monomial m b =>

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module A M
inst✝⁷ : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : AddCommGroup M'
inst✝² : Module B M'
inst✝¹ : Module R M'
inst✝ : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)
x : B
p✝ q✝ : A[X]
a✝¹ :
  d' ((aeval x) p✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x
a✝ :
  d' ((aeval x) q✝) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x
⊢ (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) + (aeval x) (derivative p✝) • d' x +
      ((PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) + (aeval x) (derivative q✝) • d' x) =
    (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p✝)) +
        (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs q✝)) +
      ((aeval x) (derivative p✝) • d' x + (aeval x) (derivative q✝) • d' x)

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = evalEval x x✝

Tactic:
← coe_evalEvalRingHom,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ eval₂ (evalRingHom x) x✝ = ⇑(evalEvalRingHom x x✝)
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ ↑(Fintype.card Fq) ^ p.natDegree ≠ 0

Tactic:
exact ⟨h, (pow_pos _).ne'⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ ∀ i ∈ antidiagonal n, ((MvPolynomial.monomial fun₀ | 0 => i.1 | 1 => i.2) (p.coeff i.1)).IsHomogeneous n

Tactic:
simp only [Prod.forall, mem_antidiagonal]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ ∀ (a b : ℕ), a + b = n → ((MvPolynomial.monomial fun₀ | 0 => a | 1 => b) (p.coeff a)).IsHomogeneous n
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
· simpa [destutter_cons_cons, hab] using! hl₁.tail.length_le_length_destutter (hl.cons _)

Goal state after:
case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
have hc (j : ι) : ∃ a b, j ∈ s → a * g i + b * g j = 1 :=
      if h : j ∈ s ∧ i ≠ j then
        (hgg.2 j h.1 h.2).1.elim fun a h => h.elim fun b h => ⟨a, b, fun _ => h⟩
      else
        ⟨0, 0, fun hj => (h ⟨hj, hjs hj⟩).elim⟩

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hc : ∀ (j : ι), ∃ a b, j ∈ s → a * g i + b * g j = 1
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r
      (∑ x ∈ range k.succ,
        (X - C r) ^ 1 *
          ((k.choose x * q.descFactorial (k - x)) • (X - C r) ^ (q - (k - x) - 1) * (⇑derivative)^[x] p')) =
    0

Tactic:
← mul_sum,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r
      ((X - C r) ^ 1 *
        ∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) • (X - C r) ^ (q - (k - i) - 1) * (⇑derivative)^[i] p') =
    0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ ↑v = (trinomial k k✝ n ↑u ↑v ↑w).coeff k✝

Tactic:
by rw [trinomial_middle_coeff hkm hmn]

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * b j * g j + (r j * a j /ₘ g j * g i * g j + r j * a j %ₘ g j * g i)

Tactic:
mul_right_comm (_ /ₘ g j),

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
j : ι
hj : j ∈ s
⊢ r j = r j * b j * g j + (r j * a j /ₘ g j * g j * g i + r j * a j %ₘ g j * g i)