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

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

Tactic:
by
  ext p
  have : m / m.gcd n ≠ 0 := by simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]
  simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff,
    hm.ne_zero, hn, dvd_div_iff_mul_dvd (gcd_dvd_left _ _)]
  refine ⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_isUnit <| hm _ <|
    (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
      ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩
  rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]
  exact fun hpn ↦ hp.2 hp.1.1 <| hpn.trans <| gcd_dvd_right _ _

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

Goal state before:
pp: case neg.succ
m : ℕ
hm : ¬m = 0
n : ℕ
ih : Ω (m ^ n) = n * Ω m
⊢ Ω (m ^ n) + Ω m = (n + 1) * Ω m

Tactic:
ih

Goal state after:
case neg.succ
m : ℕ
hm : ¬m = 0
n : ℕ
ih : Ω (m ^ n) = n * Ω m
⊢ n * Ω m + Ω m = (n + 1) * Ω m
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (f a) + ω (∏ x ∈ s, f x) = ω (f a) + ∑ x ∈ s, ω (f x)

pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (f a).Coprime (∏ x ∈ s, f x)

Tactic:
ih

Goal state after:
case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (f a) + ∑ i ∈ s, ω (f i) = ω (f a) + ∑ x ∈ s, ω (f x)

case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (↑s).Pairwise (Coprime on f)

case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ (f a).Coprime (∏ x ∈ s, f x)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f ↦ f i) (d.finMulAntidiag n) = n.divisors

Tactic:
ext k
  simp only [mem_image, ne_eq, mem_divisors]
  constructor
  · rintro ⟨f, hf, rfl⟩
    exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩
  · simp_rw [mem_finMulAntidiag]
    rintro ⟨⟨r, rfl⟩, hn⟩
    have hs : Nontrivial (Fin d) := by
      rw [Fin.nontrivial_iff_two_le]
      obtain rfl | hd' := eq_or_ne d 0
      · exact i.elim0
      lia
    obtain ⟨i', hi_ne⟩ := exists_ne i
    use fun j => if j = i then k else if j = i' then r else 1
    simp only [ite_true, and_true]
    rw [← Finset.mul_prod_erase (h := mem_univ i),
      ← Finset.mul_prod_erase (a := i')]
    · simp_all
    exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩

Goal state after:
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 ℕ
⊢ s.Infinite → Tendsto (fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun x ↦ r) k) atTop atTop

Tactic:
have h_mono : Monotone fun n ↦ ∑ k ∈ Finset.range n, s.indicator (fun _ ↦ r) k := by
      refine (sum_mono_set_of_nonneg ?_).comp range_mono
      exact (fun _ ↦ indicator_nonneg (fun _ _ ↦ h.le) _)
    rw [h_mono.tendsto_atTop_atTop_iff]
    intro hs n
    obtain ⟨n', hn'⟩ := exists_lt_nsmul h n
    obtain ⟨t, t_s, t_card⟩ := hs.exists_subset_card_eq n'
    obtain ⟨m, hm⟩ := t.bddAbove
    use m + 1
    grw [hn', ← t_s]
    have h : t ⊆ Finset.range (m + 1) := by
      intro i i_t
      rw [Finset.mem_range]
      exact (hm i_t).trans_lt (lt_add_one m)
    rw [sum_indicator_subset (fun _ ↦ r) h, sum_eq_card_nsmul (fun _ _ ↦ rfl), t_card]

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ 0 ∈ cutMap β (a * a)

Tactic:
← Rat.cast_zero,

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ↑0 ∈ cutMap β (a * a)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α), (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
by
      suffices ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x by
        intro x
        obtain h | rfl | h := lt_trichotomy x 0
        · convert! this (-x) (neg_pos.2 h) using 1
          · rw [neg_mul, mul_neg, neg_neg]
          · simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
        · simp only [mul_zero, map_zero]
        · exact this x h
        -- prove that the (Sup of rationals less than x) ^ 2 is the Sup of the set of rationals less
        -- than (x ^ 2) by showing it is an upper bound and any smaller number is not an upper bound
      refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
      · exact le_inducedMap_mul_self_of_mem_cutMap hx
      · exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx

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

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

Tactic:
by_cases hb0 : g b = 0
    · simp_all
    simp? [Finset.sum_insert hb, hb0] at hfd hd says
      simp only [Finset.sum_insert hb, Finset.mem_insert, forall_eq_or_imp, hb0, or_false]
        at hfd hd
    obtain ⟨⟨rfl, isunit_gb⟩, hd⟩ := hd
    use fun b₁ b₂ ↦ if b₂ = b then ↑isunit_gb.unit⁻¹ else 0
    simp? [Finset.sum_insert hb, hb] says
      simp only [Finset.sum_insert hb, ite_smul, zero_smul, ↓reduceIte, Finset.sum_ite_eq', hb,
        add_zero, sPolynomial_self, smul_zero, zero_add]
    simp only [m.toSyn.injective.eq_iff] at *
    trans ∑ b' ∈ B, (g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b)
    · suffices (-(∑ i ∈ B, m.leadingCoeff (g i))) = m.leadingCoeff (g b) by
        rw [add_comm, Finset.sum_sub_distrib, sub_eq_add_neg, ← Finset.sum_smul, ← Finset.sum_mul,
          ← neg_smul, ← neg_mul, this, isunit_gb.mul_val_inv, one_smul]
      rw [← add_eq_zero_iff_neg_eq']
      trans (g b).coeff (m.degree <| g b) + ∑ i ∈ B, (g i).coeff (m.degree <| g b)
      · unfold leadingCoeff
        congr 1
        apply Finset.sum_congr rfl
        intro b' hb'
        rcases hd b' hb' with h | h <;> simp [h]
      · rw [← coeff_sum, ← coeff_add, ← notMem_support_iff]
        exact m.notMem_support_of_degree_lt hfd
    · apply Finset.sum_congr rfl
      intro b' hb'
      rw [sPolynomial]
      obtain (⟨h, -⟩ | h) := hd b' hb' <;>
        simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)

Tactic:
rw [Ne, mul_eq_zero, not_or] at h

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)
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
N : Type u_3
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn : |val b|ₘ ≤ |val a|ₘ ^ n
⊢ ∃ n, |f (val b)|ₘ ≤ |f (val a)|ₘ ^ n

Tactic:
← map_mabs,

Goal state after:
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
N : Type u_3
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn : |val b|ₘ ≤ |val a|ₘ ^ n
⊢ ∃ n, f |val b|ₘ ≤ f |val a|ₘ ^ n
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 : |a|ₘ ≤ |b|ₘ
⊢ mk b ≤ mk a

Tactic:
rw [← mk_mabs a, ← mk_mabs]

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : |a|ₘ ≤ |b|ₘ
⊢ mk |b|ₘ ≤ mk |a|ₘ
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
hab : mk a ≤ mk b
⊢ mk a ≤ mk (a / b)

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

Goal state after:
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:
ih

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 (∏ i ∈ s, a i) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
ih

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 (a (s.min' hs)) = 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:
ih

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: case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ ((∃ m, |f b|ₘ ≤ |f a|ₘ ^ m) ∧ ∃ n, |f a|ₘ ≤ |f b|ₘ ^ n) → (∃ m, |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ n, |a|ₘ ≤ |b|ₘ ^ n

Tactic:
← map_mabs,

Goal state after:
case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ ((∃ m, f |b|ₘ ≤ f |a|ₘ ^ m) ∧ ∃ n, f |a|ₘ ≤ f |b|ₘ ^ n) → (∃ m, |b|ₘ ≤ |a|ₘ ^ m) ∧ ∃ n, |a|ₘ ≤ |b|ₘ ^ n
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case 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
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B

Tactic:
induction B using ind with

Goal state after:
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)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
inst✝ : MulArchimedean M
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
⊢ mk a ha = B

Tactic:
induction B using ind with

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
inst✝ : MulArchimedean M
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
⊢ mk a ha = mk b hb
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B

Tactic:
induction B using ind with

Goal state after:
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 : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
a : M
ha : a ≠ 1
b : M
hb : b ≠ 1
hAB : mk a ha ≤ mk b hb
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ (mk b hb)
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
intro x mx

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

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.SurjOn (fun x ↦ c - ↑x) ↑(range #s) ↑(Ioc (c - ↑(#s)) c)

Tactic:
intro x mx

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

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ ∀ a ∈ range #s, c + ↑a ∈ Ico c (c + ↑(#s))

Tactic:
intro x mx

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

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.SurjOn (fun x ↦ c + ↑x) ↑(range #s) ↑(Ico c (c + ↑(#s)))

Tactic:
intro x mx

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ ∀ (a b : Interval α), a - b = a + -b

Tactic:
rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)

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⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯

Tactic:
rw [← Set.IsWF.min_union]

Goal state after:
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 ⋯ ≤ ⋯.min ⋯
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:
rw [sub_eq_add_neg, ← orderTop_neg (x := y)]

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.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
this : 1 ∈ (orderAddMonoidHom G).range
⊢ Function.Surjective ⇑(orderAddMonoidHom G)

Tactic:
obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩

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✝ : MulLeftMono M
u : Mˣ
x✝¹ x✝ : M
h : ↑u * x✝¹ ≤ ↑u * x✝
⊢ x✝¹ ≤ x✝

Tactic:
by
  simpa using mul_le_mul_right h ↑u⁻¹

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✝⁴ : 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 ≤ c * a - b * a

Tactic:
← sub_mul,

Goal state after:
Γ : 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 ≤ (c - b) * a
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case succ
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : α
n : ℕ
a✝ : f (n • a) ≤ f a
⊢ f ((n + 1) • a) ≤ f a

Tactic:
rw [add_nsmul]

Goal state after:
case succ
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : α
n : ℕ
a✝ : f (n • a) ≤ f a
⊢ f (n • a + 1 • a) ≤ f a
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case inr
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 : α
hne : f x ≠ f y
h_lt : f y < f x
⊢ f (x + y) = max (f x) (f y)

Tactic:
rw [add_eq_left_of_lt hna h_lt]

Goal state after:
case inr
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 : α
hne : f x ≠ f y
h_lt : f y < f x
⊢ f x = max (f x) (f y)
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
have hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk (f x).val) f.support := by
    intro c hc d hd h
    simp only
    rw [seed.archimedeanClassMk_of_mem_stratum (f c).prop (by simpa using! hc)]
    rw [seed.archimedeanClassMk_of_mem_stratum (f d).prop (by simpa using! hd)]
    exact h

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))