mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hp : p ∣ q
⊢ p ∣ X i * q

pp: case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ X i * q

Tactic:
· exact dvd_mul_of_dvd_right hp (X i)

Goal state after:
case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ X i * q
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 0 ^ 0 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
_root_.pow_zero,

Goal state after:
case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ 1 = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p

Tactic:
totalDegree_eq,

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ (((expand p) f).support.sup fun m ↦ (Finsupp.toMultiset m).card) =
    (f.support.sup fun m ↦ (Finsupp.toMultiset m).card) * p
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot (σ →₀ ℕ)
⊢ ⊥ < m.toWithBotSyn a ↔ ⊥ < a

Tactic:
by
  simp [bot_lt_iff_ne_bot]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case intro
ι : 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
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
⊢ DFinsupp.Lex r s x (single i a) → Acc (DFinsupp.Lex r s) x

Tactic:
rintro ⟨k, hr, hs⟩

Goal state after:
case intro
ι : 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
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → x j = (single i a) j
hs : s k (x k) ((single i a) k)
⊢ Acc (DFinsupp.Lex r s) x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : f = 0
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree

pp: case neg
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
rcases subsingleton_or_nontrivial (MvPolynomial σ R) with nontrivial | nontrivial
  · simp [Subsingleton.eq_zero (α := MvPolynomial σ R)]
  · classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s a_not_mem ih =>
      simp only [mem_insert, ne_eq, forall_eq_or_imp] at h
      obtain ⟨ha, hs⟩ := h
      simp [a_not_mem, not_false_eq_true, prod_insert, sum_insert, degreeOf_mul_eq ha
        (by rw [prod_ne_zero_iff]; exact hs), ih hs]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ Multiset.count s (p * q).degrees = Multiset.count s p.degrees + Multiset.count s q.degrees

Tactic:
← degreeOf_def,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ degreeOf s (p * q) = degreeOf s p + degreeOf s q
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ degree (ofDegLex (toDegLex (single 0 1 + single 1 1))) < degree (ofDegLex (toDegLex (single 0 2))) ∨
    degree (ofDegLex (toDegLex (single 0 1 + single 1 1))) = degree (ofDegLex (toDegLex (single 0 2))) ∧
      toLex (ofDegLex (toDegLex (single 0 1 + single 1 1))) < toLex (ofDegLex (toDegLex (single 0 2)))

Tactic:
ofDegLex_toDegLex

Goal state after:
α : Type u_1
⊢ degree (single 0 1 + single 1 1) < degree (ofDegLex (toDegLex (single 0 2))) ∨
    degree (single 0 1 + single 1 1) = degree (ofDegLex (toDegLex (single 0 2))) ∧
      toLex (single 0 1 + single 1 1) < toLex (ofDegLex (toDegLex (single 0 2)))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ m.toSyn 0 ↔ ∀ (x : σ), d x = 0

Tactic:
rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = 0 ↔ ∀ (x : σ), d x = 0
Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : { P // (P.sum fun x ↦ id) = n }
⊢ (↑f).extendDomain.support ⊆ s

Tactic:
simp [map_eq_image, image_subset_iff]

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
hg : m.leadingCoeff g ∈ R⁰
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

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

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
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
hg : m.leadingCoeff g ∈ R⁰
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
by_cases hf : f = 0
  · simp [hf]
  · simp only [leadingCoeff, degree_mul_of_right_mem_nonZeroDivisors hf hg, coeff_mul_of_degree_add]

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
hg : IsRegular (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

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

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f : MvPolynomial σ R
inst✝ : Decidable (f = 0)
hf : f = 0
⊢ WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max =
    if f = 0 then ⊥ else ↑(m.toSyn.symm (f.support.sup ⇑m.toSyn))

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f : MvPolynomial σ R
inst✝ : Decidable (f = 0)
hf : ¬f = 0
⊢ WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max =
    if f = 0 then ⊥ else ↑(m.toSyn.symm (f.support.sup ⇑m.toSyn))

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f : MvPolynomial σ R
inst✝ : Decidable (f = 0)
hf : ¬f = 0
⊢ WithBot.map (⇑m.toSyn.symm) (Finset.image (⇑m.toSyn) f.support).max =
    if f = 0 then ⊥ else ↑(m.toSyn.symm (f.support.sup ⇑m.toSyn))
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
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : f ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
· simp [hf]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : f ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False

Tactic:
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']

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

Goal state before:
pp: case zero
⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a

Tactic:
exact ⟨1, 0, by simp, squarefree_one⟩

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

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

Tactic:
have : Coprime (m / gcd m n) (gcd m n) :=
    coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]

Goal state after:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
this : (m / m.gcd n).Coprime (m.gcd n)
⊢ (m / m.gcd n).Coprime n
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
have : Coprime (m / gcd m n) (gcd m n) :=
    coprime_of_squarefree_mul <| by simpa [Nat.div_mul_cancel, gcd_dvd_left]
  simpa [Nat.div_mul_cancel, gcd_dvd_right] using
    (coprime_div_gcd_div_gcd (m := m) (gcd_ne_zero_right hn).bot_lt).mul_right this

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

Goal state before:
pp: R : Type u_1
inst✝ : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f l = f (l / d) * f d

Tactic:
← hf.right hl,

Goal state after:
R : Type u_1
inst✝ : GroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : (l / d).Coprime d
hd : f d ≠ 0
⊢ f l = f (l / d * d)
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : { n // IsPrimePow n }
⊢ (fun pk ↦ ⟨↑pk.1 ^ (pk.2 + 1), ⋯⟩) ((fun n ↦ (⟨(↑n).minFac, ⋯⟩, (↑n).factorization (↑n).minFac - 1)) n) = n

Tactic:
by
    ext1
    dsimp only
    rw [sub_one_add_one (Nat.factorization_minFac_ne_zero n.prop.one_lt),
      n.prop.minFac_pow_factorization_eq]

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (f * g) n = ∑ n ∈ Ioc 0 N, f n * ∑ m ∈ Ioc 0 (N / n), g m

Tactic:
rw [sum_Ioc_mul_eq_sum_prod_filter, sum_filter, sum_product]

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ (∑ x ∈ Ioc 0 N, ∑ y ∈ Ioc 0 N, if (x, y).1 * (x, y).2 ≤ N then f (x, y).1 * g (x, y).2 else 0) =
    ∑ n ∈ Ioc 0 N, f n * ∑ m ∈ Ioc 0 (N / n), g m
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : 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 : β
hb : b ∈ cutMap β (a * a)
⊢ b ≤ inducedMap α β a * inducedMap α β a

Tactic:
by
  obtain ⟨q, hb, rfl⟩ := hb
  obtain ⟨q', hq', hqq', hqa⟩ := exists_rat_pow_btwn two_ne_zero hb (mul_self_pos.2 ha.ne')
  trans (q' : β) ^ 2
  · exact mod_cast hqq'.le
  · rw [pow_two] at hqa ⊢
    exact mul_self_le_mul_self (mod_cast hq'.le)
      (le_csSup (cutMap_bddAbove β a) <|
        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)

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
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
refine ⟨0, ?_, hb⟩
    rw [← Rat.cast_zero, coe_mem_cutMap_iff, Rat.cast_zero]
    exact mul_self_pos.2 ha.ne'

Goal state after:
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:
by
  rw [degree_add_of_lt, degree_X]
  simp only [degree_C, map_zero, degree_X]
  rw [← bot_eq_zero, bot_lt_iff_ne_bot, bot_eq_zero, ← map_zero m.toSyn]
  simp

Goal state after:
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 ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
rw [lt_def, le_def, le_def]
    suffices (∀ (n : ℕ), |b.val|ₘ ^ n < |a.val|ₘ) → ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n by
      simpa using this
    intro h
    obtain h := (h 1).le
    exact ⟨1, by simpa using h⟩

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

Goal state before:
pp: case insert.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g (τ i)

Tactic:
simp only [← s.sum_erase_add _ h1s, add_comm]

Goal state after:
case insert.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f a • g (σ a) + (f ((Equiv.symm σ) a) • g (σ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (σ i)) ≤
    f a • g a + (f ((Equiv.symm σ) a) • g (τ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (τ i))
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:
· rw [mul_comm, mk_mul_eq_mk_left hlt, ih]
      congr 2
      refine le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)
      intro y hy
      obtain rfl | hmem := Finset.mem_cons.mp hy
      · apply ((hmono.lt_iff_lt hminmem (by simp)).mp ?_).le
        rw [ih] at hlt
        exact hlt
      · exact Finset.min'_le _ _ hmem

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✝ : MulArchimedean M
A B : FiniteMulArchimedeanClass M
⊢ A = B

Tactic:
induction A using ind with | mk a ha
     =>  _ 

Goal state after:
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
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
α : Type u_2
inst✝ : PartialOrder α
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ ≤ mk ↑b ⋯ → f a ≤ f b
A B : FiniteMulArchimedeanClass M
hAB : A ≤ B
⊢ lift f ⋯ A ≤ lift f ⋯ B

Tactic:
induction A using ind with | mk a ha
     =>  _ 

Goal state after:
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
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulLeftStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ b', b' > b ∧ 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.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : SetLike S G
C : S
inst✝ : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ a = b

Tactic:
simpa [div_eq_one, eq_comm] using eq_one_of_mem_of_inv_mem nab (by simpa using nba)

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ g1 = g2

Tactic:
have h1 : IsCyclic ↥(Subgroup.zpowers g2) := by
      rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]; use g2

Goal state after:
case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ g1 = g2
Module: Mathlib.Algebra.Order.Module.Basic

Goal state before:
pp: case inl.inl
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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

Goal state before:
pp: case inl.inr
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : a ≤ 0
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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

Goal state before:
pp: case inr.inl
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : b ≤ 0
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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

Goal state before:
pp: case inr.inr
R : Type u_2
M : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : IsOrderedRing R
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module R M
inst✝ : PosSMulMono R M
a : R
b : M
ha : 0 ≤ a
hb : 0 ≤ b
⊢ |a • b| = |a| • |b|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos,
      smul_nonpos_of_nonpos_of_nonneg, smul_nonneg_of_nonpos_of_nonpos]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ ¬x.coeff = 0 ↔ x ≠ 0

Tactic:
coeff_fun_eq_zero_iff

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ ¬x = 0 ↔ x ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).support ⊆ {a}

Tactic:
classical exact Pi.support_single_subset

Goal state after: