mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ?m.84 ≠ 0

Tactic:
prod_ne_zero_iff

Goal state after:
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ∀ a ∈ ?m.91, ?m.90 a ≠ 0

R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ Type ?u.76

R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ?m.87 → MvPolynomial σ R

R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ Finset ?m.87
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hbc :
  degree (ofDegLex b) < degree (ofDegLex c) ∨
    degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) < toLex (ofDegLex c)
hab : degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
⊢ degree (ofDegLex a) < degree (ofDegLex c) ∨
    degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

Tactic:
· rcases hbc with (hbc | hbc)
      · left; exact lt_of_eq_of_lt hab.1 hbc
      · right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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

Goal state before:
pp: case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : Decidable (p = 0)
⊢ (m.leadingTerm p).support = if p = 0 then ∅ else {m.degree p}

Tactic:
simp [leadingTerm, support_monomial]

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ m.toSyn (m.toSyn.symm (p.support.sup ⇑m.toSyn)) ≤ m.toSyn (m.toSyn.symm (q.support.sup ⇑m.toSyn))

Tactic:
m.toSyn.apply_symm_apply

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ p.support.sup ⇑m.toSyn ≤ q.support.sup ⇑m.toSyn
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ (f.ppow k) x = f x ^ k

Tactic:
rw [ppow, dif_neg (Nat.ne_of_gt kpos), coe_mk]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ dirichletInverseFun f hf 0 = 0

Tactic:
dirichletInverseFun,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ (if 0 = 0 then 0
    else
      if 0 = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (0 / ↑d) * dirichletInverseFun f hf ↑d) =
    0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ dirichletInverseFun f hf 1 = ⅟(f 1)

Tactic:
dirichletInverseFun,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ (if 1 = 0 then 0
    else
      if 1 = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (1 / ↑d) * dirichletInverseFun f hf ↑d) =
    ⅟(f 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ dirichletInverseFun f hf n = -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
dirichletInverseFun,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (if n = 0 then 0
    else
      if n = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
classical
  set S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
  have hSne : S.Nonempty := by
    use 1
    have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
    simp [S, h1]
  let s := Finset.max' S hSne
  have hs : s ∈ S := Finset.max'_mem S hSne
  simp only [S, Finset.mem_filter, Finset.mem_range] at hs
  obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
  rw [hsa] at hn
  obtain ⟨hlts, hlta⟩ := CanonicallyOrderedAdd.mul_pos.mp hn
  rw [hsb] at hsa hn hlts
  refine ⟨a, b, hlta, (pow_pos_iff two_ne_zero).mp hlts, hsa.symm, ?_⟩
  rintro x ⟨y, hy⟩
  rw [Nat.isUnit_iff]
  by_contra hx
  refine Nat.lt_le_asymm ?_ (Finset.le_max' S ((b * x) ^ 2) ?_)
  · 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]
  · simp_rw [S, hsa, Finset.mem_filter, Finset.mem_range]
    refine ⟨Nat.lt_succ_iff.mpr (le_of_dvd hn ?_), ?_, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring

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

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
hab : a.Coprime 0
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}

Tactic:
simp only [Nat.coprime_zero_right] at hab

Goal state after:
case inr.inl
a : ℕ
ha : a ≠ 0
hab : a = 1
⊢ {d ∈ (a * 0).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ divisors 0 | IsPrimePow d}
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
by simp [h.2 cop]

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

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
by simp [h.2 cop]

Goal state after:
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 * 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:
rw [sum_mul_sum, ← sum_product']

Goal state after:
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 * n).divisorsAntidiagonal, f x.1 * g x.2 =
    ∑ x ∈ m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal, f x.1.1 * g x.1.2 * (f x.2.1 * g x.2.2)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case neg.mp
k n : ℕ
hn0 : ¬n = 0
h : (σ k) n = 1
⊢ n = 1

Tactic:
← sigma_zero_eq_one_iff

Goal state after:
case neg.mp
k n : ℕ
hn0 : ¬n = 0
h : (σ k) n = 1
⊢ (σ 0) n = 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k

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

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

Tactic:
simp_rw [sum_filter]

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ (∑ x ∈ Ioc 0 N, ∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N, if a.1 * a.2 = x then f a.1 * g a.2 else 0) =
    ∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N, if a.1 * a.2 ≤ N then f a.1 * g a.2 else 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s.mpr
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
hm : a✝¹ ≤ N / n
⊢ N / n ≤ N ∧ n * (N / n) ≤ N

Tactic:
simp [mul_div_le, div_le_self]

Goal state after:
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 : ι → β
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

Tactic:
exact has hx.2

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

Tactic:
by
  classical
  induction s using induction_on_max_value fun i ↦ toLex (g i, f i) generalizing σ with
  | empty => simp only [le_rfl, Finset.sum_empty]
  | insert a s has hamax hind => ?_
  set τ : Perm ι := σ.trans (swap a (σ a)) with hτ
  have hτs : {x | τ x ≠ x} ⊆ s := by
    intro x hx
    simp only [τ, Ne, Set.mem_ofPred_eq, Equiv.swap_comp_apply] at hx
    split_ifs at hx with h₁ h₂
    · obtain rfl | hax := eq_or_ne x a
      · contradiction
      · exact mem_of_mem_insert_of_ne (hσ fun h ↦ hax <| h.symm.trans h₁) hax
    · exact (hx <| σ.injective h₂.symm).elim
    · exact mem_of_mem_insert_of_ne (hσ hx) (ne_of_apply_ne _ h₂)
  specialize hind (hfg.subset <| subset_insert _ _) hτs
  simp_rw [sum_insert has]
  grw [← hind]
  obtain hσa | hσa := eq_or_ne a (σ a)
  · rw [hτ, ← hσa, swap_self, trans_refl]
  have h1s : σ.symm a ∈ s := by
    rw [Ne, ← inv_eq_iff_eq] at hσa
    refine mem_of_mem_insert_of_ne (hσ fun h ↦ hσa ?_) hσa
    rwa [apply_symm_apply, eq_comm] at h
  simp only [← s.sum_erase_add _ h1s, add_comm]
  rw [← add_assoc, ← add_assoc]
  simp only [hτ, swap_apply_left, Function.comp_apply, Equiv.coe_trans, apply_symm_apply]
  refine add_le_add (smul_add_smul_le_smul_add_smul' ?_ ?_) (sum_congr rfl fun x hx ↦ ?_).le
  · specialize hamax (σ.symm a) h1s
    rw [Prod.Lex.toLex_le_toLex] at hamax
    rcases hamax with hamax | hamax
    · exact hfg (mem_insert_of_mem h1s) (mem_insert_self _ _) hamax
    · exact hamax.2
  · specialize hamax (σ a) (mem_of_mem_insert_of_ne (hσ <| σ.injective.ne hσa.symm) hσa.symm)
    rw [Prod.Lex.toLex_le_toLex] at hamax
    rcases hamax with hamax | hamax
    · exact hamax.le
    · exact hamax.1.le
  · rw [mem_erase, Ne, eq_symm_apply] at hx
    rw [swap_apply_of_ne_of_ne hx.1 (σ.injective.ne _)]
    rintro rfl
    exact has hx.2

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✝ : Nontrivial M
⊢ Nonempty (FiniteMulArchimedeanClass M)

Tactic:
obtain ⟨x, hx⟩ := exists_ne (1 : M)
  exact ⟨mk x hx, by simpa using hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ⊆ ⊥ ↔ ↑(s ⊓ t) ⊆ ↑⊥

Tactic:
coe_inf

Goal state after:
α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ ↑s ⊓ ↑t ⊆ ⊥ ↔ ↑s ∩ ↑t ⊆ ↑⊥
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn * ht.min htn ≤ ⋯.min ⋯

Tactic:
rw [IsWF.le_min_iff]

Goal state after:
α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s * t, hs.min hsn * ht.min htn ≤ b
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 : R⟦Γ⟧
g : Γ'
hg : g ∈ (embDomain f x).support
⊢ g ∈ ⇑f '' x.support

Tactic:
contrapose hg

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∉ ⇑f '' x.support
⊢ g ∉ (embDomain f x).support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mp
Γ : 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,
        (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j) ∧
          (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i) ∨
      embDomain f (ofLex a) = embDomain f (ofLex b) →
    (∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b

pp: case mpr
Γ : 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, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b →
    (∃ i,
        (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j) ∧
          (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i) ∨
      embDomain f (ofLex a) = embDomain f (ofLex b)

Tactic:
· rintro (⟨i, hj, hi⟩ | heq)
      · have himem : i ∈ Set.range f := by
          contrapose hi
          simp [embDomain_of_notMem_range hi]
        obtain ⟨k, rfl⟩ := himem
        refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
        simpa using hj (f j) (f.lt_iff_lt.mpr hjk)
      · exact Or.inr <| embDomain_injective.comp (ofLex.injective) heq

Goal state after:
case mpr
Γ : 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, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i) ∨ a = b →
    (∃ i,
        (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j) ∧
          (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i) ∨
      embDomain f (ofLex a) = embDomain f (ofLex b)
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
h : f (x + y) ≠ f x
h1 : f (x + y) ≤ f x
⊢ max (f (x + y)) (f y) < f x

Tactic:
apply max_lt (lt_of_le_of_ne h1 h) h_lt

Goal state after:
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
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y < x

Tactic:
apply lt_of_mk_lt_mk_of_nonpos

Goal state after:
case h
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
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ mk (f y) < mk x

case hneg
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
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : y < 0
⊢ f y ≤ 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ↑(x * y).order = ↑x.order + ↑y.order

Tactic:
← WithTop.coe_add,

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ↑(x * y).order = ↑(x.order + y.order)
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
x y : R⟦Γ⟧
⊢ x.orderTop + y.orderTop ≤ (x • y).orderTop

Tactic:
exact HahnModule.orderTop_vAdd_le_orderTop_smul fun i j ↦ rfl

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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : ↑(z - y) ∈ (f.extendFun hx).domain
⊢ 0 < ↑(f.extendFun hx) (z - y)

Tactic:
extendFun,

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : ↑(z - y) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain
⊢ 0 < ↑(f.extendFun hx) (z - y)
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
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈ (f.extendFun hx).toFun.range

Tactic:
extendFun,

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
⊢ toLex ((truncLTLinearMap K c) (ofLex (f.eval x))) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : r < stdPart x
⊢ f (r - stdPart x) < x - f (stdPart x)

Tactic:
apply lt_of_mk_lt_mk_of_nonpos

Goal state after:
case h
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : r < stdPart x
⊢ mk (f (r - stdPart x)) < mk (x - f (stdPart x))

case hneg
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : r < stdPart x
⊢ f (r - stdPart x) ≤ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
⊢ stdPart x = r

Tactic:
obtain h | rfl | h := lt_trichotomy (stdPart x) r

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : stdPart x < r
⊢ stdPart x = r

case inr.inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : 0 ≤ mk x
hl : ∀ s < stdPart x, f s ≤ x
hr : ∀ s > stdPart x, x ≤ f s
⊢ stdPart x = stdPart x

case inr.inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : r < stdPart x
⊢ stdPart x = r