mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (m * n).primeFactorsList.length = Ω m + Ω n

Tactic:
cardFactors_apply,

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (m * n).primeFactorsList.length = m.primeFactorsList.length + Ω n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (m * n).primeFactorsList.length = m.primeFactorsList.length + Ω n

Tactic:
cardFactors_apply,

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: s : Multiset ℕ
h0 : s.prod ≠ 0
⊢ Ω s.prod = (Multiset.map (⇑Ω) s).sum

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons ih => simp_all [cardFactors_mul, not_or]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (zeta * pow 0) n = ∑ n ∈ Ioc 0 N, N / n

Tactic:
pow_zero_eq_zeta

Goal state after:
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (zeta * zeta) n = ∑ n ∈ Ioc 0 N, N / n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.snd.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).2.2

Tactic:
trans gcd (b1 * b2) (a2 * b2)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).2.2 = (b1 * b2).gcd (a2 * b2)

R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (b1 * b2).gcd (a2 * b2) = ((c1, c2), d1, d2).2.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f n = g n

Tactic:
rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : mk b < mk a
⊢ mk (a / b) = mk b

Tactic:
by
  simpa [h, div_eq_mul_inv] using mk_mul_eq_mk_right (a := a) (b := b⁻¹)

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
hn : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0

Tactic:
rcases hmn with ⟨k, rfl⟩

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
hn : Squarefree (m * k)
⊢ f (m * k) = 0
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
⊢ (0 + a - 1) / a = 0

Tactic:
by cases a <;> simp [Nat.div_eq_zero_iff]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
by
  obtain hab | hba := le_total a (b - 1)⁻¹
  · calc
      ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity
  · rw [← sub_pos] at hb
    calc
      ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
      _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
      _ ≤ a + (b - 1) * a := by gcongr
      _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s

Tactic:
mk,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), ⟨MulArchimedeanClass.mk a, ⋯⟩ ∈ s
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s))

Tactic:
rw [inter_comm, card_sdiff_comm]

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ #s = #r
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ ∃ x_1 ∈ Set.Iio #s, c - ↑x_1 = x

Tactic:
Set.mem_Iio

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ ∃ x_1 < #s, c - ↑x_1 = x
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + ↑(#s)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s))

Tactic:
rw [inter_comm, card_sdiff_comm]

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ #r = #s
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ ∃ x_1 ∈ Set.Iio #s, c + ↑x_1 = x

Tactic:
Set.mem_Iio

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ ∃ x_1 < #s, c + ↑x_1 = x
Module: Mathlib.Algebra.Order.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
⊢ |a • b| = |a| • |b|

Tactic:
obtain ha | ha := le_total a 0

Goal state after:
case inl
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
⊢ |a • b| = |a| • |b|

case inr
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
⊢ |a • b| = |a| • |b|
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
⊢ mk (k • a) = mk a

Tactic:
have : Nontrivial K := nontrivial_iff.mpr ⟨k, 0, h⟩

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
⊢ mk (k • a) = mk a
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hc : s ≤ c
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2

Tactic:
rcases hc with ⟨hc₁, hc₂⟩

Goal state after:
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb₁ : t.toProd.1 ≤ s.toProd.1
hb₂ : s.toProd.2 ≤ t.toProd.2
hc₁ : c.toProd.1 ≤ s.toProd.1
hc₂ : s.toProd.2 ≤ c.toProd.2
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff x.order = 0

Tactic:
order_of_ne hx

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff (⋯.min ⋯) = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order

Tactic:
order_of_ne hx

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : r = 0
⊢ g' ∉ ⇑f '' ((single g) r).support

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : ¬r = 0
⊢ g' ∉ ⇑f '' ((single g) r).support

Tactic:
· simp [hr]

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : ¬r = 0
⊢ g' ∉ ⇑f '' ((single g) r).support
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : (embDomain f x).coeff = (embDomain f y).coeff
g : Γ
⊢ x.coeff g = y.coeff g

Tactic:
funext_iff

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : (fun a ↦ AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) =
    if h : x.coeff = coeff 0 then ⊤ else ↑(⋯.min ⋯)

Tactic:
funext_iff

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else ↑(⋯.min ⋯)) =
    if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else ↑(⋯.min ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
hpos : 0 < (ofLex x).leadingCoeff
hne : ofLex x ≠ 0
htop : (ofLex x).orderTop ≠ ⊤
⊢ (ofLex 0).coeff ((ofLex x).orderTop.untop htop) < (ofLex x).coeff ((ofLex x).orderTop.untop htop)

Tactic:
simpa [coeff_untop_eq_leadingCoeff] using hpos

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

Goal state before:
pp: case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ArchimedeanClass.mk ↑(f (f.support.min' hsupport)) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
rw [seed.archimedeanClassMk_of_mem_stratum (f _).prop
    (by simpa using! f.support.min'_mem hsupport)]

Goal state after:
case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : Quotient s
⊢ x ≤ y ∨ y ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x
    induction y using Quotient.inductionOn with | h y
    obtain h | h := total_of (· ≤ ·) x y
    · exact .inl <| .single <| .inl h
    · exact .inr <| .single <| .inl h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
⊢ x * a ∈ P ∧ -(x * a) ∈ P

Tactic:
set y := (1 + x) * half

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : IsUnit 2
x a : R
a✝¹ : a ∈ P
a✝ : -a ∈ P
half : R
h2 : 2 * half = 1
y : R := (1 + x) * half
⊢ x * a ∈ P ∧ -(x * a) ∈ P
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : (C r).coeff = (C s).coeff
⊢ r = s

Tactic:
funext_iff

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
⊢ r = s
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
⊢ A = B ∨ B = ⊤

Tactic:
obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top (A.primeSpectrumEquiv.symm ⟨B, hle⟩)

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊥
⊢ A = B ∨ B = ⊤

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
h : A.primeSpectrumEquiv.symm ⟨B, hle⟩ = ⊤
⊢ A = B ∨ B = ⊤
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
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) = ArchimedeanClass.mk (↑z - ↑y)

Tactic:
ArchimedeanClass.mk_sub_comm z.val y.val,

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
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
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑y - x) = ArchimedeanClass.mk (↑y - ↑z)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
split_ifs with hpq

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: 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
x : A
p : A[X]
⊢ d (eval x p) = (PolynomialModule.eval x) (d.mapCoeffs p) + eval x (derivative p) • d x

Tactic:
convert! apply_aeval_eq d x p

Goal state after:
case e'_3.e'_5
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
x : A
p : A[X]
⊢ d.mapCoeffs p = (PolynomialModule.map A LinearMap.id) ((compAlgebraMap A d).mapCoeffs p)
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ((aeval x) p)′ = (aeval x) (mapCoeffs p) + (aeval x) (derivative p) * x′

Tactic:
convert! Derivation.apply_aeval_eq' Differential.deriv _ (Algebra.linearMap A R) ..
  · simp [mapCoeffs]
  · simp [deriv_algebraMap]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
⊢ IsTorsion R[X] (AEval R M a)

Tactic:
have hp : p ∈ nonZeroDivisors R[X] := mem_nonZeroDivisors_iff_right.mpr
    fun q hq ↦ Or.resolve_right (mul_eq_zero.mp hq) h'

Goal state after:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
hp : p ∈ nonZeroDivisors R[X]
⊢ IsTorsion R[X] (AEval R M a)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * X ^ (p * q).natTrailingDegree =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
natTrailingDegree_mul hp hq,

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * X ^ (p.natTrailingDegree + q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (↑0).smeval x = 0 • x ^ 0

Tactic:
simp only [smeval_zero, Nat.cast_zero, zero_smul]

Goal state after: