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

Goal state before:
pp: case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp

Goal state after:
case inr.succ.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp : p ∣ (monomial n') 1 * q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n') 1 * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : Finsupp.degree n' = d
⊢ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Tactic:
rw [add_eq_left]
      rw [Multiset.filter_eq_nil]
      exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ x₂ j = x j

Tactic:
Classical.not_imp

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ x.support = ∅ → (∀ i ∈ ∅, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
ht

Goal state after:
case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : x.support = ∅
⊢ (∀ i ∈ ∅, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : MvPolynomial σ R
⊢ m.degree f = 0

Tactic:
by
  rw [Subsingleton.eq_zero f, degree_zero]

Goal state after:
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 : ↥(s.finsuppAntidiag n)
⊢ (fun f ↦ ⟨(↑f).extendDomain, ⋯⟩) ((fun f ↦ ⟨subtypeDomain (fun x ↦ x ∈ s) ↑f, ⋯⟩) f) = f

Tactic:
obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop
    ext1
    exact extendDomain_subtypeDomain _ hs

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

Tactic:
rw [Multiset.prod_coe, Nat.prod_primeFactorsList n.succ_ne_zero]
      exact prod_normalizedFactors n.succ_ne_zero

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

Goal state before:
pp: case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i) = ∏ i ∈ insert a s, m.leadingCoeff (P i)

Tactic:
simp only [Finset.prod_insert has, Finset.sum_insert has]

Goal state after:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)
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 ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Tactic:
· intro i hi
    rw [(H i hi).leadingCoeff_eq_one]
    exact isRegular_one

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ AddMonoidAlgebra.leadingCoeff (⇑toLex) pₖ ≠ 0

Tactic:
AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ pₖ ≠ 0
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1) / ↑(#(S i_1))

Tactic:
Fin.sum_univ_succ,

Goal state after:
case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    ↑((Finsupp.cons p'.natDegree i) 0) / ↑(#(S 0)) + ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1.succ) / ↑(#(S i_1.succ))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_1
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
⊢ S.max' ⋯ < (b * x) ^ 2

Tactic:
convert!
      lt_mul_of_one_lt_right hlts
        (one_lt_pow two_ne_zero (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩))
    using 1
    rw [mul_pow]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
⊢ t ∈ n.primeFactors.powerset → (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f t.val.prod * g (n / t.val.prod)

Tactic:
ht

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
⊢ (∏ i ∈ t, f i) * ∏ i ∈ n.primeFactors \ t, g i = f t.val.prod * g (n / t.val.prod)
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: 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

Tactic:
Pi.map_apply,

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

Goal state before:
pp: case inl
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0

Tactic:
exact i.elim0

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
⊢ BddAbove (cutMap β a)

Tactic:
obtain ⟨q, hq⟩ := exists_rat_gt a

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
hq : a < ↑q
⊢ BddAbove (cutMap β a)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.snd.snd
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.2 = ((c1, c2), d1, d2).2.2

Tactic:
trans gcd (b1 * b2) (a2 * b2)
      · rw [gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.2.1, h.2, gcd_mul_right,
          cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]

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

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 α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i • g i

Tactic:
← card_range #s,

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 α β
s : Finset ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
σ : Perm ι
hσ : σ.IsCycleOn ↑s
hs : {x | σ x ≠ x} ⊆ ↑s
⊢ (∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ #(range #s) • ∑ i ∈ s, f i • g i
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, |val (of (f (val b)))|ₘ ≤ |val (of (f (val a)))|ₘ ^ n

Tactic:
val_of,

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (succ i) = f (succ i) \ f i

Tactic:
hf.disjointed_succ

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ f (succ i) \ f i = f (succ i) \ f i

α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ ¬IsMax i
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
hba : mk b ≤ mk a
⊢ mk b ≤ mk (a * b)

Tactic:
by
  simpa [hba] using min_le_mk_mul (a := a) (b := b)

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

Goal state before:
pp: case e'_8
ι : 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
⊢ ↑s = ⇑σ ⁻¹' ↑s

Tactic:
σ.eq_preimage_iff_image_eq,

Goal state after:
case e'_8
ι : 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
⊢ ⇑σ '' ↑s = ↑s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: 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 : MulArchimedeanClass M
⊢ (orderHom f) a = (orderHom f) b → a = b

Tactic:
induction a using ind with | mk a

Goal state after:
case 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
b : MulArchimedeanClass M
a : M
⊢ (orderHom f) (mk a) = (orderHom f) b → mk a = b
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
⊢ t ∈ Set.Iio ⊤ → s < t → subgroup t < subgroup s

Tactic:
ht

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
ht : t ∈ Set.Iio ⊤
⊢ s < t → subgroup t < subgroup s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
motive : FiniteMulArchimedeanClass M → Prop
mk : ∀ (a : M) (ha : a ≠ 1), motive (FiniteMulArchimedeanClass.mk a ha)
⊢ ∀ (x : FiniteMulArchimedeanClass M), motive x

Tactic:
by
  simpa [FiniteMulArchimedeanClass, MulArchimedeanClass.forall]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
m n : ℕ
⊢ m = ⌊↑m⌋₊

Tactic:
rw [m.floor_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case hbc
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
apply lt_floor_add_one

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

Goal state before:
pp: H : Type u_1
inst✝² : CommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedMonoid H
a✝ a : H
⊢ a ∈ (Submonoid.oneLE H).carrier → a⁻¹ ∈ (Submonoid.oneLE H).carrier → a = 1

Tactic:
by simpa using ge_antisymm

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⟦Γ⟧
hx : x.orderTop ≠ ⊤
⊢ x.coeff (x.orderTop.untop hx) = x.leadingCoeff

Tactic:
by
  rw [orderTop_ne_top] at hx
  rw [leadingCoeff_of_ne_zero hx, (WithTop.untop_eq_iff _).mpr (orderTop_of_ne_zero hx)]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬orderTop 0 < x.orderTop

Tactic:
orderTop_zero

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ f (x.orderTop.untop ⋯) ≤ f z

Tactic:
OrderEmbedding.le_iff_le,

Goal state after:
case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ x.orderTop.untop ⋯ ≤ z
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → x.coeff j = 0
h : x ≠ 0
⊢ i ≤ x.orderTop

Tactic:
by_contra! hi
      exact x.isWF_support.min_mem (support_nonempty_iff.2 h) (H _ (orderTop_of_ne_zero h ▸ hi))

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ x.order < i ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
by
  rw [← not_le, le_order_iff_forall h]
  simp

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

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : orderTop 0 = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
orderTop_zero

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : ⊤ = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mpr
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ ∃ n, |y| ≤ n • |x|

Tactic:
refine ⟨n + 1, ((lt_iff _ _).mpr ?_).le⟩

Goal state after:
case inr.mpr
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ ∃ i,
    (∀ j < i, (ofLex |y|).coeff j = (ofLex ((n + 1) • |x|)).coeff j) ∧
      (ofLex |y|).coeff i < (ofLex ((n + 1) • |x|)).coeff i