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

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (Multiset.map x ↑↑m).noncommProd ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
conv in m.1.1.map _ => rw [← m.1.1.filter_add_not (a = ·), Multiset.map_add]

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (Multiset.map x (Multiset.filter (fun x ↦ a = x) ↑↑m) +
            Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd
        ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
⊢ Acc (DFinsupp.Lex r s) (erase b x)

Tactic:
refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_

Goal state after:
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a ((erase b x) a))
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ coeff 0 f ∣ a ∧ f = C (coeff 0 f)

Tactic:
suffices f.totalDegree = 0 by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0

Goal state after:
case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ f.totalDegree = 0
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
hf : m.leadingCoeff f ∈ R⁰
hg : g ≠ 0
⊢ ¬m.leadingCoeff g = 0

Tactic:
simp [hg]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hg]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp [hg]

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

Goal state before:
pp: case mp
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a

Tactic:
use (UniqueFactorizationMonoid.normalizedFactors a).toFinset

Goal state after:
case h
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
hg : g = 0
⊢ m.withBotDegree (f + g) = m.withBotDegree f

Tactic:
simp [hg]

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

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝) * f (∏ x ∈ s✝, g x) = f (g a✝) * ∏ x ∈ s✝, f (g x)

pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ (g a✝).gcd (∏ x ∈ s✝, g x) = 1

Tactic:
ih hs.1

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (g a✝) * ∏ i ∈ s✝, f (g i) = f (g a✝) * ∏ x ∈ s✝, f (g x)

case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ (g a✝).gcd (∏ x ∈ s✝, g x) = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ (σ 1) n = ∑ d ∈ n.divisors, d

Tactic:
simp [sigma_apply]

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

Goal state before:
pp: n : ℕ
⊢ (σ 0) n = #n.divisors

Tactic:
simp [sigma_apply]

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

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

Tactic:
rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]

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

Goal state before:
pp: case e_s.mpr
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 ∧ n * a✝¹ ≤ N

Tactic:
intro hm

Goal state after:
case e_s.mpr
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
hm : a✝¹ ≤ N / n
⊢ a✝¹ ≤ N ∧ n * a✝¹ ≤ N
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = (fun x1 x2 ↦ x1 + x2) ↑qa ↑qb

Tactic:
beta_reduce; norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
⊢ f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n

Tactic:
by
  refine and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)
  rcases eq_or_ne m 0 with (rfl | hm)
  · simp
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  exact h hm hn hmn

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
hba : mk b ≤ mk a
⊢ mk b ≤ mk (a / b)

Tactic:
simpa [div_eq_mul_inv, hba] using mk_right_le_mk_mul (a := a) (b := b⁻¹)

Goal state after:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x

Tactic:
· rwa [tsub_pos_iff_lt]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha : a ≠ 0
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain ha | ha := ha.lt_or_gt <;> obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha

Goal state after:
case intro.inl.inl
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : a < 0
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

case intro.inl.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : IsEmpty ι
a : α
ha✝ : a ≠ 0
ha : 0 < a
b : α
hb : 0 < b
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s

Tactic:
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
    hfg.sum_comp_perm_smul_le_sum_smul hσ]

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
⊢ subgroup ⊤ = ⊥

Tactic:
simp [subgroup]

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 ≤ ∑ n ∈ range #s, (c - ↑n)

Tactic:
convert! sum_le_sum_Ioc hs

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ n ∈ range #s, (c - ↑n) = ∑ x ∈ Ioc (c - ↑(#s)) c, x
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

Goal state after:
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝ : CommMagma α
s t : Set α
a : α
x : α × α
⊢ x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a

Tactic:
simp [mul_comm, and_left_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
s : Interval α
⊢ dual (map f s) = map (OrderHom.dual f) (dual s)

Tactic:
cases s
  · rfl
  · exact WithBot.map_comm rfl _

Goal state after:
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : x✝ ⊆ {⊥}
⊢ s ≤ ⊥

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : ¬x✝ ⊆ {⊥}
⊢ s ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }

Tactic:
· exact (h ha).le

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : ¬x✝ ⊆ {⊥}
⊢ s ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Tactic:
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]

Goal state after:
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
⊢ IsGLB s₁
    (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥)

Tactic:
by
    constructor
    · intro s ha
      split_ifs with h
      · lift s to NonemptyInterval α using ne_of_mem_of_not_mem ha h.1
        -- Porting note: Lean failed to figure out the function `f` by itself,
        -- so I added it through manually
        let f := fun (s : NonemptyInterval α) (_ : ↑s ∈ s₁) => s.toProd.fst
        exact WithBot.coe_le_coe.2 ⟨le_iSup₂ (f := f) s ha, iInf₂_le s ha⟩
      · exact bot_le
    · intro s ha
      cases s with
      | bot => exact bot_le
      | coe s =>
        split_ifs with h
        · exact WithBot.coe_le_coe.2
            ⟨iSup₂_le fun t hb => (WithBot.coe_le_coe.1 <| ha hb).1,
              le_iInf₂ fun t hb => (WithBot.coe_le_coe.1 <| ha hb).2⟩
        · rw [not_and_or, not_not] at h
          rcases h with h | h
          · exact ha h
          · cases h fun b hb c hc ↦ (WithBot.coe_le_coe.1 <| ha hb).1.trans
              (s.fst_le_snd.trans (WithBot.coe_le_coe.1 <| ha hc).2)

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

Goal state before:
pp: case inl
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
hg : x.order ∈ y.support
⊢ x.order ∈ x.support

Tactic:
simpa using coeff_order_eq_zero.not.2 <| ne_zero_of_eq_add_single hxy hy

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.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
j : FiniteArchimedeanClass M
hj : j < f.support.min' hsupport
⊢ j ∉ f.support

Tactic:
contrapose! hj

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.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
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ f.support.min' hsupport ≤ j
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✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f x < f y
h : f (x + y) ≠ f y
h1 : f (x + y) ≤ f y
⊢ max (f (-x)) (f (x + y)) < max (f y) (f y)

Tactic:
by
      rw [max_self, map_neg_eq_map]
      exact max_lt h_lt <| lt_of_le_of_ne h1 h

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⟦Γ⟧
⊢ (x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff

Tactic:
by
  simp only [← of_symm_smul_of_eq_mul]
  exact HahnModule.coeff_smul_order_add_order x y

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
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
⊢ ((single g) r * x).order = g + x.order

Tactic:
by
  obtain _ | _ := subsingleton_or_nontrivial R
  · exact (hx <| Subsingleton.eq_zero x).elim
  have hrx : ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0 := by
    rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]
  rw [order_mul_of_ne_zero hrx, order_single <| IsRegular.ne_zero hr]

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

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 1 = leadingCoeff 1

Tactic:
leadingCoeff_one

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
h : x.orderTop = 0 ∧ x.leadingCoeff = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single (n • a)) (r ^ n) * (single a) r = (single ((n + 1) • a)) (r ^ n * r)

Tactic:
single_mul_single,

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single (n • a + a)) (r ^ n * r) = (single ((n + 1) • a)) (r ^ n * r)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
⊢ (single 0) (x * y) = (single 0) x * (single 0) y

Tactic:
single_mul_single,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
⊢ (single 0) (x * y) = (single (0 + 0)) (x * y)
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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ (ofLex (↑↑f y)).coeff (seq n) ≠ 0

Tactic:
convert hmem

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K (seq 0)
n : ℕ
hmem : f.evalCoeff x (seq n) ≠ 0
⊢ (ofLex (↑↑f y)).coeff (seq n) = f.evalCoeff x (seq n)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· use 0; right
      ext
      simp [h]

Goal state after:
case neg
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a