mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.sum fun x ↦ id).choose ((x :: l).toFinsupp 0) * ((x :: l).toFinsupp.update 0 0).multinomial =
    (x + l.sum).choose x * l.toFinsupp.multinomial

Tactic:
congr 1

Goal state after:
case e_a
x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.sum fun x ↦ id).choose ((x :: l).toFinsupp 0) = (x + l.sum).choose x

case e_a
x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.update 0 0).multinomial = l.toFinsupp.multinomial
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ m.degree (X s) = Finsupp.single s 1

Tactic:
change m.degree (monomial (Finsupp.single s 1) (1 : R)) = _
  rw [degree_monomial, if_neg one_ne_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : m.toSyn (m.degree (f ^ n)) ≤ m.toSyn (n • m.degree f)
⊢ m.toSyn (m.degree (f ^ (n + 1))) ≤ m.toSyn ((n + 1) • m.degree f)

Tactic:
| succ n hrec =>

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case succ
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hrec : coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
⊢ coeff ((n + 1) • m.degree f) (f ^ (n + 1)) = m.leadingCoeff f ^ (n + 1)

Tactic:
| succ n hrec =>

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.withBotDegree ((monomial d) c) = if c = 0 then ⊥ else ↑d

Tactic:
split_ifs <;> simp [withBotDegree_eq, *, m.degree_monomial]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

pp: case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

pp: case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
· exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩

Goal state after:
case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toWithBotSyn (m.withBotDegree (f * g)) ≤ m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g)

Tactic:
by_cases h0 : f * g = 0
  · simp [h0]
  simp [m.withBotDegree_eq_coe_degree_iff f |>.mpr (by grind),
    m.withBotDegree_eq_coe_degree_iff g |>.mpr (by grind),
    m.withBotDegree_eq_coe_degree_iff _ |>.mpr h0, ← WithBot.coe_add,
    m.toSyn_degree_mul_le]

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

Goal state before:
pp: case e_s.mp
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N ∧ n * a✝¹ ≤ N → a✝¹ ≤ N / n

Tactic:
intro ⟨_, h⟩
    grw [← h, Nat.mul_div_cancel_left _ (by lia)]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g i)) (g i) =
    coeff (m.degree (g b)) (g b) + ∑ i ∈ B, coeff (m.degree (g b)) (g i)

Tactic:
congr 1

Goal state after:
case e_a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
⊢ ∑ i ∈ B, coeff (m.degree (g i)) (g i) = ∑ i ∈ B, coeff (m.degree (g b)) (g i)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

Tactic:
obtain h | h := le_total |y|ₘ |z|ₘ

Goal state after:
case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |y|ₘ ≤ |z|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)
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
⊢ mk b ≤ mk (a / b) ↔ mk b ≤ mk a

Tactic:
rw [mk_div_comm, mk_left_le_mk_div_iff]

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
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
⊢ mk (a * b) ∈ ↑s

Tactic:
obtain h | h := min_le_iff.mp (min_le_mk_mul a b)

Goal state after:
case inl
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk a ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s

case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : mk a ∈ ↑s
hb : mk b ∈ ↑s
h : mk b ≤ mk (a * b)
⊢ mk (a * b) ∈ ↑s
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈0⌉ₑ = 0

Tactic:
by simpa using ceil_natCast 0

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - ↑(#s)) c, x

Tactic:
set r := Ioc (c - #s) c

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Icc a b).val = (map (fun x ↦ c + x) (Finset.Icc a b).val).dedup

Tactic:
((Finset.nodup _).map <| add_right_injective c).dedup

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Icc a b).val = map (fun x ↦ c + x) (Finset.Icc a b).val
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ico a b).val = (map (fun x ↦ c + x) (Finset.Ico a b).val).dedup

Tactic:
((Finset.nodup _).map <| add_right_injective c).dedup

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ico a b).val = map (fun x ↦ c + x) (Finset.Ico a b).val
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = (map (fun x ↦ c + x) (Finset.Ioc a b).val).dedup

Tactic:
((Finset.nodup _).map <| add_right_injective c).dedup

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioc a b).val = map (fun x ↦ c + x) (Finset.Ioc a b).val
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = (map (fun x ↦ c + x) (Finset.Ioo a b).val).dedup

Tactic:
((Finset.nodup _).map <| add_right_injective c).dedup

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ c + x) (Finset.Ioo a b).val = map (fun x ↦ c + x) (Finset.Ioo a b).val
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : 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 : s ≤ t
hc : s ≤ c
⊢ ↑s ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
    else ⊥

Tactic:
dif_pos,

Goal state after:
α : 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 : s ≤ t
hc : s ≤ c
⊢ ↑s ≤ ↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

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 : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : 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 : s ≤ t
hc : s ≤ c
⊢ s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

Tactic:
exact ⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).coeff a = r

Tactic:
by
  classical exact Pi.single_eq_same (M := fun _ => R) a r

Goal state after:
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 Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
rw [dif_pos (Set.mem_image_of_mem f ha)]

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff (Classical.choose ⋯) = x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
· simp [hxy]

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g + 0 ≠ 0

Tactic:
add_zero

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
g : Γ := ⋯.min ⋯
⊢ x.coeff g ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.coeff (x.orderTop.untop ⋯) + 0 = x.coeff (x.orderTop.untop ⋯)

Tactic:
add_zero

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g + 0
⊢ g ∈ x.support

Tactic:
add_zero

Goal state after:
case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g
⊢ g ∈ x.support
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case a
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ ArchimedeanClass.mk a ≤ ↑c

pp: case a
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a

Tactic:
· contrapose! h0 with hlt
    have ha' : a ∈ ball K c := (mem_ball_iff K).mpr fun _ ↦ hlt
    exact (Submodule.disjoint_def.mp (u.disjoint_ball_stratum _)) _ ha' ha

Goal state after:
case a
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ ↑c ≤ ArchimedeanClass.mk a
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ sSup {x, y} * z = ⨆ x_1 ∈ {x, y}, x_1 * z

Tactic:
sSup_mul_distrib

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ ⨆ y_1 ∈ {x, y}, y_1 * z = ⨆ x_1 ∈ {x, y}, x_1 * z
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ sSup ∅ * x = sSup ∅

Tactic:
sSup_mul_distrib

Goal state after:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, y * x = sSup ∅
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✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

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✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ 0 = 0
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✝³ : NonAssocSemiring α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a

Tactic:
exact nsmul_le hna

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✝⁴ : AddMonoidWithOne α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
⊢ f (n • 1) ≤ f 1

Tactic:
exact nsmul_le hna

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

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y z : R
⊢ mk x + mk y + mk z = mk x + (mk y + mk z)

Tactic:
simp_rw [← mk_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
⊢ f (a + b) = max (f a) (f b)

Tactic:
wlog hab : f a > f b generalizing a b with H

Goal state after:
case inr
α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
H : ∀ {a b : α}, f a ≠ f b → f a > f b → f (a + b) = max (f a) (f b)
hab : ¬f a > f b
⊢ f (a + b) = max (f a) (f b)

α : Type u_2
S : Type u_3
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
fna : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
⊢ f (a + b) = max (f a) (f b)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ (a1, a2) ∈ antidiagonal ⋯ ⋯ (a + b) ↔ (a1, a2) ∈ {(a, b)}

Tactic:
simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_antidiagonal, mem_singleton]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
a1 a2 : Γ
⊢ a1 ∈ x.support ∧ a2 = b ∧ a1 + a2 = a + b ↔ a1 = a ∧ a2 = b
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ x.coeff a * r = x.coeff (a + 0) * r

Tactic:
add_zero

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ x.coeff a * r = x.coeff a * r
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ r * x.coeff a = r * x.coeff (a + 0)

Tactic:
add_zero

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ r * x.coeff a = r * x.coeff a
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
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
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ (f.support.erase (f.support.min' hsupport)).min' hsupport' ∈ f.support.erase (f.support.min' hsupport)

Tactic:
apply Finset.min'_mem _ _

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

Goal state before:
pp: case inr.inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
hx' : mk x ≠ ⊤
⊢ mk x⁻¹ = mk y⁻¹

Tactic:
apply add_left_cancel_of_ne_top hx'

Goal state after:
case inr.inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
hx : x ≠ 0
hy : y ≠ 0
hx' : mk x ≠ ⊤
⊢ mk x + mk x⁻¹ = mk x + mk y⁻¹
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ Int.negSucc n) = -(↑n.succ • mk x)

Tactic:
zpow_negSucc,

Goal state after:
case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ (n + 1))⁻¹ = -(↑n.succ • mk x)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
⊢ 0 < (x - 1).orderTop → x.orderTop = 0 ∧ x.leadingCoeff = 1

Tactic:
intro hx
    constructor
    · rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
      exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)
    · rw [← sub_add_cancel x 1, add_comm, ← leadingCoeff_one (Γ := Γ) (R := R)]
      exact leadingCoeff_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Goal state after: