mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
simp [← m.leadingCoeff_eq_zero_iff (f := f * g),
    m.leadingCoeff_mul_of_left_mem_nonZeroDivisors hf, mul_left_mem_nonZeroDivisors_eq_zero_iff hf]

Goal state after:
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 g ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
mul_comm,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff g ∈ R⁰
⊢ m.withBotDegree (g * f) = m.withBotDegree f + m.withBotDegree g
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
hg : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

Tactic:
simp_rw [toWithBotSyn_apply]
    aesop

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
hg : ¬g = 0
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.withBotDegree (f + g) = m.withBotDegree f

Tactic:
simp only [withBotDegree_eq_withBotDegree_iff, show f ≠ 0 by contrapose h; simp [h], iff_false]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : ¬g = 0
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + g) = m.degree f ∧ ¬f + g = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∈ {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}

Tactic:
hsa,

Goal state after:
case refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∈ {x ∈ range (b ^ 2 * a + 1) | x ∣ b ^ 2 * a ∧ ∃ x_1, x = x_1 ^ 2}
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ dirichletInverse (⇑f) hf * f = 1

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ f * dirichletInverse (⇑f) hf = 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, True ∧ { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } a = x) ↔ x.1 * x.2 = n

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, True ∧ (⟨(↑a).1, ⋯⟩, ⟨(↑a).2, ⋯⟩) = x) ↔ x.1 * x.2 = n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a,
      ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧
        (fun x ↦ { toFun := PNat.val, inj' := PNat.coe_injective } (Additive.toMul (a x))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ a, ∑ i, a i = Additive.ofMul ⟨n, h⟩ ∧ (fun x ↦ ↑(Additive.toMul (a x))) = f) ↔ ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

Tactic:
← n.primeFactorsList.dedup_sublist.eq_of_length h

Goal state after:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.dedup.Nodup
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
convert! sum_Ioc_mul_zeta_eq_sum zeta N using 1

Goal state after:
case e'_3
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, N / n = ∑ n ∈ Ioc 0 N, zeta n * ↑(N / n)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
⊢ d.primeFactorsPiBij n f hf = d.primeFactorsPiBij n g hg → f = g

Tactic:
contrapose!
  simp_rw [Function.ne_iff]
  intro ⟨p, hp, hfg⟩
  use f p hp
  dsimp only [Nat.primeFactorsPiBij]
  apply ne_of_mem_of_not_mem (s := {x | p ∣ x}) <;> simp_rw [Set.mem_ofPred_eq]
  · rw [Finset.prod_filter]
    convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
    rw [if_pos rfl]
  · rw [mem_primeFactors] at hp
    rw [Prime.dvd_finsetProd_iff hp.1.prime]
    push Not
    intro q hq
    rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_primeFactorsList
      <| List.mem_toFinset.mp q.2)]
    rintro rfl
    rw [(mem_filter.mp hq).2] at hfg
    exact hfg rfl

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

Goal state before:
pp: 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).1.2 = (a1 * a2).gcd (a2 * b2)

Tactic:
mul_comm,

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).1.2 = (a2 * a1).gcd (a2 * b2)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).gcd (((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2) =
    ((c1, c2), d1, d2).1.2

Tactic:
mul_comm,

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
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
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
⊢ (((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).1.1).gcd (((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2) =
    ((c1, c2), d1, d2).1.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: 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.1 = (b1 * b2).gcd (a1 * b1)

Tactic:
mul_comm,

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.1 = (b2 * b1).gcd (a1 * b1)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
⊢ a ≤ b ∨ b ≤ a

Tactic:
by
    obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
    · exact .inr ⟨1, by simpa using hab⟩
    · exact .inl ⟨1, by simpa using hab⟩

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
⊢ mk b ≤ mk (a * b) ↔ mk b ≤ mk a

Tactic:
mul_comm,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
⊢ mk b ≤ mk (b * a) ↔ mk b ≤ mk a
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ 0 ≤ 1 - x

Tactic:
simpa using h'x.le

Goal state after:
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:
have hσinv : { x | σ⁻¹ x ≠ x } ⊆ s := (set_support_symm_eq _).subset.trans hσ

Goal state after:
ι : 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
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g i ↔ MonovaryOn (f ∘ ⇑σ) g ↑s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (∏ i ∈ s, a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ (mk ∘ a) i < (mk ∘ a) (s.min' hs)

Tactic:
rw [ih] at hlt

Goal state after:
case inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a i) < mk (a (s.min' hs))
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ (mk ∘ a) i < (mk ∘ a) (s.min' hs)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk (a i * ∏ x ∈ s, a x) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
mul_comm,

Goal state after:
case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ mk ((∏ x ∈ s, a x) * a i) = mk (a ((Finset.cons i s hi).min' ⋯))
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ (mk ∘ a) (s.min' hs) < (mk ∘ a) y

Tactic:
rw [ih] at hlt

Goal state after:
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
s : Finset ι
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
y : ι
hi : y ∉ s
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons y s hi)
hminmem : s.min' hs ∈ Finset.cons y s hi
hne : mk (a y) ≠ mk (∏ i ∈ s, a i)
hlt : mk (a (s.min' hs)) < mk (a y)
hy : y ∈ Finset.cons y s hi
⊢ (mk ∘ a) (s.min' hs) < (mk ∘ a) y
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 a < mk b
hpos : 1 ≤ a
h : a⁻¹ < b ∧ b < a
⊢ b < a

Tactic:
exact h.2

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

Goal state before:
pp: case neg
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 : 1 < x
hxy : mk x = mk y
left✝ : ∃ m, |y|ₘ ≤ |x|ₘ ^ m
m : ℕ
hm : x ≤ y ^ m
⊢ ∃ n, x ≤ y ^ n

Tactic:
exact ⟨m, hm⟩

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

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
a b : M
hle : mk a ≤ mk b
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ (mk b)

Tactic:
simpa using h a b (mk_le_mk.mp hle)

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
⊢ (if h : a = 1 then ⊤ else ↑(f ⟨a, h⟩)) = if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)

pp: case refine_2
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A ≠ ⊤

Tactic:
· split_ifs with ha hb hb
    · rfl
    · exact (hb (MulArchimedeanClass.mk_eq_top_iff.mp (ha ▸ h').symm)).elim
    · exact (ha (MulArchimedeanClass.mk_eq_top_iff.mp (by apply hb ▸ h'))).elim
    · rw [h ⟨a, ha⟩ ⟨b, hb⟩ (by simpa [mk] using h')]

Goal state after:
case refine_2
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A ≠ ⊤
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun b ↦ 1 * b) s = s

Tactic:
one_mul,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun b ↦ b) s = s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ lowerBounds s₁
⊢ 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:
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.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 = embDomain f y
⊢ x = y

Tactic:
by
  ext g
  rw [HahnSeries.ext_iff, funext_iff] at xy
  have xyg := xy (f g)
  rwa [embDomain_coeff, embDomain_coeff] at xyg

Goal state after:
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 ⋯
hcxyne : (x + y).coeff g ≠ 0
hxyx : (x + y).orderTop ≤ x.orderTop
⊢ (x + y).orderTop = x.orderTop

Tactic:
exact le_antisymm hxyx (le_of_eq_of_le (min_eq_left_of_lt hxy).symm min_orderTop_le_orderTop_add)

Goal state after:
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
⊢ (ofLex |x|).order = (ofLex x).order

Tactic:
· have hne' : ofLex x ≠ 0 := hne
    have habs : ofLex |x| ≠ 0 := by simpa using hne
    apply WithTop.coe_injective
    rw [order_eq_orderTop_of_ne_zero habs, order_eq_orderTop_of_ne_zero hne']
    apply orderTop_abs

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

Goal state before:
pp: case inr.mp
Γ : 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 = (ofLex ((n + 1) • |x|)).coeff j_1
hi : (ofLex |y|).coeff j < (ofLex ((n + 1) • |x|)).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
simp_rw [ofLex_smul, coeff_smul] at hj hi

Goal state after:
case inr.mp
Γ : 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 y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|