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
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has hrec =>
    simp only [Finset.prod_insert has, Finset.sum_insert has]
    rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
    exact congr_arg₂ _ rfl hrec

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

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

Tactic:
rintro rfl

Goal state after:
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_

Goal state after:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p

Tactic:
rintro rfl

Goal state after:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p

Tactic:
rintro rfl

Goal state after:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False
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 : f ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔ m.toSyn (m.degree f) < m.toSyn (m.degree g)

Tactic:
by
  simp [withBotDegree_lt_withBotDegree_iff, hf]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

Tactic:
refine sum_congr rfl fun i hi => ?_
    rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
    rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i

Tactic:
· refine sum_congr rfl fun i hi => ?_
    rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
    rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b c : ArithmeticFunction R
x✝ : ℕ
⊢ (a * (b + c)) x✝ = (a * b + a * c) x✝

Tactic:
simp [← sum_add_distrib, mul_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : R
⊢ ((algebraMap R (ArithmeticFunction S)) x) 1 = (algebraMap R S) x

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
rintro rfl

Goal state after:
p k : ℕ
hk : 0 < k
hn : Nat.factorization 0 = Finsupp.single p k
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x,
      ∏ i, Additive.toMul ((Equiv.piCongrRight fun x ↦ Additive.ofMul) x i) = ⟨n, h⟩ ∧
        (fun x_1 ↦ ↑(Additive.toMul ((Equiv.piCongrRight fun x ↦ Additive.ofMul) x x_1))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0

Tactic:
Equiv.piCongrRight_apply,

Goal state after:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x,
      ∏ x_1, Additive.toMul (Pi.map (fun a ↦ ⇑Additive.ofMul) x x_1) = ⟨n, h⟩ ∧
        (fun x_1 ↦ ↑(Additive.toMul (Pi.map (fun a ↦ ⇑Additive.ofMul) x x_1))) = f) ↔
    ∏ i, f i = n ∧ n ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.a
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
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : ↥n.primeFactors
hq : q ∈ {p_1 ∈ n.primeFactors.attach | g ↑p_1 ⋯ = f p hp✝}
⊢ ¬p = ↑q

Tactic:
rintro rfl

Goal state after:
case h.a
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
q : ↥n.primeFactors
hp✝ : ↑q ∈ n.primeFactors
hp : Prime ↑q ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ g (↑q) hp✝
hq : q ∈ {p ∈ n.primeFactors.attach | g ↑p ⋯ = f (↑q) hp✝}
⊢ False
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : 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) < a + b

Tactic:
cast_add

Goal state after:
case refine_2
α : 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 < a + b
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr
α : 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 : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑(q * q) < a * a

Tactic:
push_cast

Goal state after:
case inr
α : 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 : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q * ↑q < inducedMap α β a * inducedMap α β a
⊢ ↑q * ↑q < a * a
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case e'_3
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 : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ a✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom a✝)

Tactic:
· rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
        dsimp
        rw [inducedMap_inv_self β γ _]

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

Goal state before:
pp: case e'_4
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 : ℚ
a✝ b✝ : β
h : (inducedOrderRingHom β γ).toRingHom a✝ ≤ (inducedOrderRingHom β γ).toRingHom b✝
⊢ b✝ = inducedMap γ β ((inducedOrderRingHom β γ).toRingHom b✝)

Tactic:
· rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
        dsimp
        rw [inducedMap_inv_self β γ _]

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) + 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)

Tactic:
simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_symm_apply]

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 a + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (σ i) ≤
    f a • g a + f ((Equiv.symm σ) a) • g (σ a) + ∑ x ∈ s.erase ((Equiv.symm σ) a), f x • g ((Equiv.swap a (σ a)) (σ x))
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✝ : 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
x : ι
hx : ¬σ x = a ∧ x ∈ s
⊢ x ≠ a

Tactic:
rintro rfl

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✝ : PosSMulMono α β
f : ι → α
g : ι → β
s : Finset ι
σ : Perm ι
x : ι
has : x ∉ s
hamax : ∀ x_1 ∈ s, toLex (g x_1, f x_1) ≤ toLex (g x, f x)
hfg : MonovaryOn f g ↑(insert x s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert x s)
τ : Perm ι := Equiv.trans σ (Equiv.swap x (σ x))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap x (σ x))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : x ≠ σ x
h1s : (Equiv.symm σ) x ∈ s
hx : ¬σ x = x ∧ x ∈ s
⊢ False
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case e'_7
ι : 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
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ g = (g ∘ ⇑σ⁻¹) ∘ ⇑σ

Tactic:
comp_assoc,

Goal state after:
case e'_7
ι : 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
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ g = g ∘ ⇑σ⁻¹ ∘ ⇑σ
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case e'_6
ι : 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
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ f = (f ∘ ⇑σ) ∘ ⇑(Equiv.symm σ)

Tactic:
comp_assoc,

Goal state after:
case e'_6
ι : 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
h : MonovaryOn (f ∘ ⇑σ) g ↑s
⊢ f = f ∘ ⇑σ ∘ ⇑(Equiv.symm σ)
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
hneg : a ≤ 1
⊢ a < b

Tactic:
obtain h := mk_lt_mk.mp h 1
  rw [pow_one, mabs_lt, mabs_eq_inv_self.mpr hneg, inv_inv] at h
  exact h.1

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.Cyclic

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = Subgroup.zpowers (Subgroup.genLTOne H)
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
← one_lt_inv',

Goal state after:
case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : 1 < g⁻¹
hH : Subgroup.zpowers g = Subgroup.zpowers (Subgroup.genLTOne H)
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H
Module: Mathlib.Algebra.Order.Hom.Lattice

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
⊢ ⨆ i, v (x i) = ⨆ i, v (x ↑i)

Tactic:
obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
  have : Nonempty {j // x j ≠ 0} := .intro ⟨i, hi⟩
  have : Nonempty ι := .intro i
  refine le_antisymm (ciSup_le fun j ↦ ?_) <| ciSup_le fun ⟨j, hj⟩ ↦ le_ciSup_of_le j le_rfl
  rcases eq_or_ne (x j) 0 with h | h
  · rw [h, map_zero]
    exact le_ciSup_of_le ⟨i, hi⟩ (apply_nonneg ..)
  · exact le_ciSup_of_le ⟨j, h⟩ le_rfl

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = min ↑g ↑g

Tactic:
inf_idem

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = ↑g
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex y).orderTop < (ofLex x).orderTop
⊢ |x| < |y|

Tactic:
rw [← orderTop_abs x, ← orderTop_abs y] at h
  refine (lt_iff _ _).mpr ⟨(ofLex |y|).orderTop.untop h.ne_top, ?_, ?_⟩
  · simp +contextual [-orderTop_abs, coeff_eq_zero_of_lt_orderTop, h.trans']
  · simpa [-orderTop_abs, coeff_eq_zero_of_lt_orderTop, coeff_untop_eq_leadingCoeff, h]
      using h.ne_top

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : 0 ≤ b
⊢ (↑(addMonoidHom G)).toFun a ≤ (↑(addMonoidHom G)).toFun ((fun x ↦ a + x) b)

Tactic:
suffices 0 ≤ addMonoidHom G b by simpa

Goal state after:
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : 0 ≤ b
⊢ 0 ≤ (addMonoidHom G) b
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h.mpr
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x = 0 → 0 ≤ x ∧ x < ↑b

Tactic:
rintro rfl

Goal state after:
case h.mpr
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
⊢ 0 ≤ 0 ∧ 0 < ↑b
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inl
M : Type u_1
G : Type u_2
inst✝⁸ : AddCancelCommMonoid M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : LocallyFiniteOrder M
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a b : G
hb : 0 ≤ b
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

pp: case inr
M : Type u_1
G : Type u_2
inst✝⁸ : AddCancelCommMonoid M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : LocallyFiniteOrder M
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

Tactic:
· simp [orderAddMonoidHom, addMonoidHom, hb]

Goal state after:
case inr
M : Type u_1
G : Type u_2
inst✝⁸ : AddCancelCommMonoid M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : LocallyFiniteOrder M
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr
M : Type u_1
G : Type u_2
inst✝⁸ : AddCancelCommMonoid M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : LocallyFiniteOrder M
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

Tactic:
· simp [orderAddMonoidHom, addMonoidHom, hb]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.PNat

Goal state before:
pp: x : ↥(nonZeroDivisors ℕ)
⊢ 0 < ↑x

Tactic:
by simp [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
k : Γ'
hki : k < f i
hkmem : k ∈ Set.range ⇑f
⊢ (embDomain f (ofLex a)).coeff k = (embDomain f (ofLex b)).coeff k

Tactic:
obtain ⟨j', rfl⟩ := hkmem
          simpa using hj _ <| f.lt_iff_lt.mp hki

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

Goal state before:
pp: case mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ ⊤ + mk x = ⊤

Tactic:
rw [← mk_zero, ← mk_mul, zero_mul]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
rw [or_iff_not_imp_left, not_le]

Goal state after:
case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y
h₂ : y ≈ z
⊢ z < x → x ≈ z
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
rw [or_iff_not_imp_left, not_le]

Goal state after:
case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≈ y
h₂ : y ≤ z
⊢ z < x → x ≈ z