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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b : β
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
induction hb with | _ b hb ihb

Goal state after:
case intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : β}, Acc rβ b → Acc (Prod.GameAdd rα rβ) (y, b)
b✝ b : β
hb : ∀ (y : β), rβ y b → Acc rβ y
ihb : ∀ (y : β), rβ y b → Acc (Prod.GameAdd rα rβ) (a, y)
⊢ Acc (Prod.GameAdd rα rβ) (a, b)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case trans
m : Multiset ℕ
l✝ l'✝ l l' l'' : List ℕ
h : l.Perm l'
h' : l'.Perm l''
ih : l.multinomial = l'.multinomial
ih' : l'.multinomial = l''.multinomial
⊢ l'.multinomial = l''.multinomial

Tactic:
ih'

Goal state after:
case trans
m : Multiset ℕ
l✝ l'✝ l l' l'' : List ℕ
h : l.Perm l'
h' : l'.Perm l''
ih : l.multinomial = l'.multinomial
ih' : l'.multinomial = l''.multinomial
⊢ l''.multinomial = l''.multinomial
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b : α
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
induction hb with | _ b hb ihb

Goal state after:
case intro.intro
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
⊢ Acc (Sym2.GameAdd rα) s(a, b)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
simp only [leadingCoeff, degree_prod_of_regular H, coeff_prod_sum_degree]

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

Goal state before:
pp: n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

Tactic:
refine ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => ?_⟩

Goal state after:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ n.factorization p = m.factorization p
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ (eval xₜ) pₖ = 0

Tactic:
rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

Tactic:
m.withBotDegree_le_withBotDegree_iff_of_ne_zero _ hg

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
⊢ IsPrimePow n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn')
  · simp_all
  refine ⟨_, _, (Nat.minFac_prime hn).prime, ?_, h⟩
  simp [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.support_factorization, hn',
    Nat.minFac_prime hn, Nat.minFac_dvd]

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

Goal state before:
pp: case succ.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ [x]

Tactic:
List.mem_singleton

Goal state after:
case succ.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x = x
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k

Tactic:
obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'

Goal state after:
case mp
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k
hs : s.Infinite
n : R
n' : ℕ
hn' : n < n' • r
t : Finset ℕ
t_s : ↑t ⊆ s
t_card : #t = n'
⊢ ∃ a, n ≤ ∑ k ∈ Finset.range a, s.indicator (fun x ↦ r) k
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬Tendsto (fun x ↦ Nat.card ↑s • r) atTop atTop

Tactic:
tendsto_atTop_atTop

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : PartialOrder R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : Set ℕ
hs : s.Finite
⊢ ¬∀ (b : R), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ Nat.card ↑s • r
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
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x - ∑ x ∈ B, (m.leadingCoeff (g x) * ↑isunit_gb.unit⁻¹) • g b

Tactic:
sub_eq_add_neg,

Goal state after:
σ : 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
this : -∑ i ∈ B, m.leadingCoeff (g i) = m.leadingCoeff (g b)
⊢ ∑ b ∈ B, g b + g b = ∑ x ∈ B, g x + -∑ x ∈ B, (m.leadingCoeff (g x) * ↑isunit_gb.unit⁻¹) • g b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i - C r) = single i 1

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i + -C r) = single i 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i - C r)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.Monic (X i + -C r)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ ⊤.out = 1

Tactic:
← mk_eq_top_iff,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ mk ⊤.out = ⊤
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case h
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : x ≤ 1
⊢ x ≤ y ^ 0

Tactic:
simpa using hx

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
inst✝ : Nontrivial M
x : M
hx : x ≠ 1
⊢ ↑(mk x hx) ≠ ⊤

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)
  exact ⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
y z : M
hz : Minimal (fun x ↦ x ∈ I) z
⊢ y * z ∈ I

Tactic:
apply SubMulAction.smul_mem

Goal state after:
case mpr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
y z : M
hz : Minimal (fun x ↦ x ∈ I) z
⊢ z ∈ I
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 ∈ s ∩ r, x + #(s \ r) • (c + ↑(#s)) ≤ ∑ x ∈ s ∩ r, x + ∑ x ∈ s \ r, x

Tactic:
card_nsmul_le_sum _ _ _ fun x mx ↦ ?_

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
⊢ ∑ x ∈ s ∩ r, x + (s \ r).sum ?m.228 ≤ ∑ x ∈ s ∩ r, x + ∑ x ∈ s \ r, x

s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := ⋯
⊢ ℤ → ℤ

s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : x ∈ s \ r
⊢ c + ↑(#s) ≤ ?m.228 x
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ hs.min hsn * ht.min htn ≤ (fun x1 x2 ↦ x1 * x2) x y

Tactic:
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)

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

Goal state before:
pp: case none.none
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : Interval α
⊢ (none * none)⁻¹ = none⁻¹ * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

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

Goal state before:
pp: case none.some
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t✝ : Interval α
t : NonemptyInterval α
⊢ (none * some t)⁻¹ = (some t)⁻¹ * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

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

Goal state before:
pp: case some.none
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t : Interval α
s : NonemptyInterval α
⊢ (some s * none)⁻¹ = none⁻¹ * (some s)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

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

Goal state before:
pp: case some.some
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ : Interval α
s t : NonemptyInterval α
⊢ (some s * some t)⁻¹ = (some t)⁻¹ * (some s)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)

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

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop ≠ ⊤

Tactic:
simpa using hx

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop y.orderTop ≤ (x - y).orderTop

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop y.orderTop ≤ (x + -y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
habs : ofLex |x| ≠ 0
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
apply WithTop.coe_injective

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
habs : ofLex |x| ≠ 0
⊢ ↑(ofLex |x|).order = ↑(ofLex x).order
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
this : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)
⊢ #(Ico 1 (a * b)) = #(Ico 1 a) + #(Ico 1 b)

Tactic:
rw [← this, Finset.card_union, Finset.card_Ico_mul_right]

Goal state after:
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
this : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)
⊢ #(Ico 1 b) + #(Ico 1 a) - #(Ico 1 b ∩ Ico (1 * b) (a * b)) = #(Ico 1 a) + #(Ico 1 b)
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
⊢ #(Ico 1 (a * b)) = #(Ico 1 a) + #(Ico 1 b)

Tactic:
have : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b) := by
    simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]
  rw [← this, Finset.card_union, Finset.card_Ico_mul_right]
  simp [add_comm]

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

Goal state before:
pp: Γ : 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 : ℕ
hn : |y| ≤ n • |x|
⊢ 0 < |x|

Tactic:
simpa using hx

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

Goal state before:
pp: Γ : 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 : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
⊢ ofLex |x| ≠ 0

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a : M
u : Mˣ
⊢ a * ↑u⁻¹ ≤ 1 ↔ a ≤ ↑u

Tactic:
rw [u.mul_inv_le_iff, one_mul]

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

Goal state before:
pp: Γ : 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 : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ (ofLex x).orderTop ≠ ⊤

Tactic:
simpa using hx

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

Goal state before:
pp: Γ : 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 : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).leadingCoeff
⊢ ofLex |x| ≠ 0

Tactic:
simpa using hx

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ↑(f x) ≠ 0

Tactic:
simpa using hx

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop.untop ⋯ = (ofLex b).orderTop.untop ⋯ ∧
      FiniteArchimedeanClass.mk (ofLex a).leadingCoeff ⋯ ≤ FiniteArchimedeanClass.mk (ofLex b).leadingCoeff ⋯

Tactic:
FiniteArchimedeanClass.mk_le_mk

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop.untop ⋯ = (ofLex b).orderTop.untop ⋯ ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
a : R
ha : a ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

Tactic:
induction bc using FiniteArchimedeanClass.ind with | mk b hb

Goal state after:
case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, FiniteArchimedeanClass.mk b hb))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hb
Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ (ofLex (c - b)).leadingCoeff

Tactic:
rwa [leadingCoeff_nonneg_iff]

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

Goal state before:
pp: case ha
Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ (ofLex (c - b)).leadingCoeff

Tactic:
rwa [leadingCoeff_nonneg_iff]

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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (((decompose seed.stratum') x) c) = f c

Tactic:
have hx : x = (decompose seed.stratum').symm f' := by
    change x = f'.coeAddMonoidHom _
    apply Submodule.subtype_injective
    rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]
    simp [h]

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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
hx : x = (decompose seed.stratum').symm f'
⊢ (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (((decompose seed.stratum') x) c) = f c