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

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ coeff (m.degree f) f + 0 ≠ 0

Tactic:
add_zero,

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ coeff (m.degree f) f ≠ 0
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case calc_1
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 ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) +
      ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0))

Tactic:
gcongr ?_ + ?_

Goal state after:
case h₁
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 ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) ≤
    pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))

case h₂
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 ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    ↑(degreeOf 0 p) / ↑(#(S 0))
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
⊢ ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ∏ i, ↑(#(S i)) =
    ↑(degreeOf 0 p) * ↑(∏ i, #(S i.succ)) / (↑(#(S 0)) * ↑(∏ i, #(S i.succ)))

Tactic:
norm_cast; rw [prod_univ_succ]

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

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False

Tactic:
exact absurd this (by lia)

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
hg : ¬g = 0
⊢ m.withBotDegree (f + g) = m.withBotDegree f

Tactic:
simp only [withBotDegree_lt_withBotDegree_iff, hg, ne_eq, false_and, or_false] at h

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

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))
⊢ m.toWithBotSyn (m.withBotDegree (∑ x ∈ Finset.cons a s haA, f x)) ≤
    (Finset.cons a s haA).sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
| cons a s haA h =>

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map f (Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val)).sum =
    ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod

Tactic:
Multiset.map_map,

Goal state after:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
h0 : f = 0 ∨ g = 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝¹ : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
· (obtain rfl | rfl := h0) <;> simp

Goal state after:
σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝¹ : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ ∀ {m n : ℕ},
    m.Coprime n →
      ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 =
        (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2

Tactic:
intro m

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m : ℕ
⊢ ∀ {n : ℕ},
    m.Coprime n →
      ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 =
        (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2) =
    ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2

Tactic:
apply sum_nbij fun ((i, j), k, l) ↦ (i * k, j * l)

Goal state after:
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    (match a with
      | ((i, j), k, l) => (i * k, j * l)) ∈
      (m * n).divisorsAntidiagonal

case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.InjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal)

case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.SurjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

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
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) =
      f
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).1 *
        g
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).2
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 1).Coprime (a 2)

Tactic:
refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 1 * a 2 ∣ n
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ n.divisors ×ˢ n.divisors ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n ∧ n ≠ 0

Tactic:
Finset.mem_product

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n ∧ n ≠ 0
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
⊢ ∀ a ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal,
    f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) =
      f
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).1 *
        g
          (match a with
            | ((i, j), k, l) => (i * k, j * l)).2

Tactic:
simp only [mem_divisorsAntidiagonal, mem_product]

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
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    (a.1.1 * a.1.2 = m ∧ m ≠ 0) ∧ a.2.1 * a.2.2 = n ∧ n ≠ 0 →
      f a.1.1 * g a.1.2 * (f a.2.1 * g a.2.2) = f (a.1.1 * a.2.1) * g (a.1.2 * a.2.2)
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inl
ι : 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
⊢ f a • g (σ a) + ∑ i ∈ s, f i • g (σ i) ≤ f a • g a + ∑ i ∈ s, f i • g (τ i)

Tactic:
rw [hτ, ← hσa, swap_self, trans_refl]

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

Goal state before:
pp: case inr
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
hab : |val b|ₘ ≤ |val a|ₘ
⊢ a ≤ b ∨ b ≤ a

Tactic:
· exact .inl ⟨1, by simpa using hab⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ (x.factorization ⊓ y.factorization).support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
Finsupp.support_inf

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ x.factorization.support ∩ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → 1 (m * n) = 1 m * 1 n

Tactic:
intro m

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
m : ℕ
⊢ ∀ {n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → 1 (m * n) = 1 m * 1 n
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
⊢ i ≤ y

Tactic:
refine (lt_of_lt_of_le ?_ (Finset.min'_le _ _ hmem)).le

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 (∏ i ∈ s, a i)
y : ι
hy : y ∈ Finset.cons i s hi
hmem : y ∈ s
⊢ i < s.min' ⋯
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
⊢ (orderHom f) ⊤ = ⊤

Tactic:
← mk_one,

Goal state after:
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
⊢ (orderHom f) (mk 1) = ⊤
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
⊢ (orderHom f) (mk 1) = ⊤

Tactic:
← mk_one,

Goal state after:
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
⊢ (orderHom f) (mk 1) = mk 1
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
s : UpperSet (MulArchimedeanClass M)
a b : M
ha : a ∈ mk ⁻¹' ↑s
hb : b ∈ mk ⁻¹' ↑s
⊢ a * b ∈ mk ⁻¹' ↑s

Tactic:
rw [Set.mem_preimage] at ha hb ⊢
    obtain h | h := min_le_iff.mp (min_le_mk_mul a b)
    · exact s.upper h ha
    · exact s.upper h hb

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

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ ⌈r⌉ₑ < n ↔ r ≤ ↑n - 1

Tactic:
simpa using (le_ceil hn₀ hn).not

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

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ ⌈r⌉ₑ < n ↔ r ≤ ↑n - 1

Tactic:
by
  simpa using (le_ceil hn₀ hn).not

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

Goal state before:
pp: M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
⊢ ∃ y, y < 1 ∧ x < y ^ n

Tactic:
obtain ⟨y, hy, hy'⟩ := exists_pow_lt_of_one_lt (one_lt_inv_of_inv hx) n
  use y⁻¹, inv_lt_one_of_one_lt hy
  simpa [lt_inv'] using hy'

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
intro x mx y my (h : c + x = c + y)

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
my : y ∈ ↑(range #s)
h : c + ↑x = c + ↑y
⊢ x = y
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
by
  simpa [succ_eq_add_one] using Iio_succ_eq_Iic b

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
⊢ map 0 f = 0

Tactic:
by
  ext; simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : embDomain f x = embDomain f y
⊢ x = y

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

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x + y).map f = x.map f + y.map f

Tactic:
by
  ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : R⟦Γ⟧
⊢ (-x).map f = -x.map f

Tactic:
by
  ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x - y).map f = x.map f - y.map f

Tactic:
by
  ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
⊢ (r • x).map f = r • x.map f

Tactic:
by
  ext; simp

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

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
horder' : (ofLex x).orderTop.untop htop = i
⊢ 0 < (ofLex x).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
horder'

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
horder' : (ofLex x).orderTop.untop htop = i
⊢ 0 < (ofLex x).coeff i
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
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
⊢ (archimedeanClassOrderIsoWithTop Γ R) (ArchimedeanClass.mk x) = (ofLex x).orderTop

Tactic:
by
  unfold archimedeanClassOrderIsoWithTop
  obtain rfl | h := eq_or_ne x 0 <;>
    simp [FiniteArchimedeanClass.withTopOrderIso_symm_apply, *]

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

Goal state before:
pp: 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
u : ArchimedeanStrata K M
⊢ IsInternal u.stratum'

Tactic:
apply DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top u.iSupIndep_stratum'
  apply Submodule.map_injective_of_injective u.baseDomain.subtype_injective
  suffices ⨆ i, u.baseDomain ⊓ u.stratum i = u.baseDomain by simpa using! this
  apply iSup_congr
  intro c
  simpa using! le_iSup _ _

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

Tactic:
by
    rw [← sub_nonneg] at hbc ⊢
    rw [← mul_sub, ← leadingCoeff_nonneg_iff, ofLex_mul, leadingCoeff_mul]
    apply mul_nonneg
    · simpa
    · rwa [leadingCoeff_nonneg_iff]

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

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

Tactic:
by
    induction x with | mk x
    induction y with | mk y
    rw [← mk_mul, mul_comm, mk_mul]

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

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

Tactic:
← mk_one,

Goal state after:
case mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ mk 1 + mk x = mk x
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝⁵ : LinearOrder R
inst✝⁴ : CommRing R
inst✝³ : IsStrictOrderedRing R
S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
f : S →+o R
⊢ (orderHom f) 0 = mk (f 1)

Tactic:
← mk_one,

Goal state after:
R : Type u_1
inst✝⁵ : LinearOrder R
inst✝⁴ : CommRing R
inst✝³ : IsStrictOrderedRing R
S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
f : S →+o R
⊢ (orderHom f) (mk 1) = mk (f 1)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mp.zero
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ 0 • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

pp: case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
· simp_all [exists_zero_lt]

Goal state after:
case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r).leadingCoeff * x.leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_of_single, ne_eq, hr.left.mul_left_eq_zero_iff, leadingCoeff_eq_zero]

Goal state after: