mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s

Tactic:
simp_rw [mk, Ne, ← MulArchimedeanClass.mk_eq_top_iff]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : b ∈ upperBounds (range f)
⊢ b ∈ {x | 0 ≤ x}

Tactic:
simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hb

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
b : β
hb : ∀ (a : α), f a ≤ b
⊢ b ∈ {x | 0 ≤ x}
Module: Mathlib.Algebra.Order.Hom.Lattice

Goal state before:
pp: case inl
ι : 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 : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
h : x j = 0
⊢ v (x j) ≤ ⨆ i, v (x ↑i)

Tactic:
h,

Goal state after:
case inl
ι : 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 : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
j : ι
h : x j = 0
⊢ v 0 ≤ ⨆ i, v (x ↑i)
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t : NonemptyInterval α
hb : ↑s ≤ ↑t
c : NonemptyInterval α
hc : ↑s ≤ ↑c
⊢ ↑s ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
    else ⊥

Tactic:
simp only [Interval.coe_le_coe] at hb hc ⊢

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ ↑s ≤
    if h : t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }
    else ⊥
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b c : α
h : b * c = 1
⊢ pure (b * c) = 1

Tactic:
h,

Goal state after:
case refine_2
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b c : α
h : b * c = 1
⊢ pure 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
h,

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ leadingCoeff 0 = coeff 0 (order 0)
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 ∉ ⇑f '' x.support
⊢ g ∉ (embDomain f x).support

Tactic:
mem_support,

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
⊢ ¬(embDomain f x).coeff g ≠ 0
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 : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
h,

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 : orderTop 0 = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
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 : ⊤ = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
h,

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
⊢ leadingCoeff 0 = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V✝ : Type u_6
α : Type u_7
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝² x✝¹ : R
x✝ : V⟦Γ⟧
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by
    ext
    simp [mul_smul]

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
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
h0 : a ≠ 0
⊢ ArchimedeanClass.mk a = ↑c

Tactic:
apply le_antisymm
  · contrapose! h0 with hlt
    have ha' : a ∈ ball K c := (mem_ball_iff K).mpr fun _ ↦ hlt
    exact (Submodule.disjoint_def.mp (u.disjoint_ball_stratum _)) _ ha' ha
  · apply (mem_closedBall_iff K).mp _ h0
    rw [← u.ball_sup_stratum_eq c]
    exact Submodule.mem_sup_right ha

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✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (match ⟨a, ha⟩ with
    | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯)) ≤
    match ⟨b, hb⟩ with
    | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯)

Tactic:
Prod.Lex.le_iff

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex
          (match ⟨a, ha⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 <
      (ofLex
          (match ⟨b, hb⟩ with
          | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∨
    (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 =
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).1 ∧
      (ofLex
            (match ⟨a, ha⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2 ≤
        (ofLex
            (match ⟨b, hb⟩ with
            | ⟨x, hx⟩ => toLex ((ofLex x).orderTop.untop ⋯, FiniteArchimedeanClass.mk (ofLex x).leadingCoeff ⋯))).2
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha : a ∈ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0}
⊢ (VAddAntidiagonal a ⋯).Nonempty

Tactic:
contrapose! ha

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : SMul R V
inst✝⁴ : PartialOrder Γ'
inst✝³ : VAdd Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : Zero R
inst✝ : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha : VAddAntidiagonal a ⋯ = ∅
⊢ a ∉ {a | ∑ ij ∈ VAddAntidiagonal a ⋯, x.coeff ij.1 • ((of R).symm y).coeff ij.2 ≠ 0}
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal k ⋯, x.coeff ij.1 • ((of R).symm (y + z)).coeff ij.2 = ((of R).symm (x • y + x • z)).coeff k

pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (y + z)).support ⊆ ((of R).symm y).support ∪ ((of R).symm z).support

Tactic:
of_symm_add

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal k ⋯, x.coeff ij.1 • ((of R).symm y + (of R).symm z).coeff ij.2 =
    ((of R).symm (x • y + x • z)).coeff k

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k : Γ'
hwf : (((of R).symm y).support ∪ ((of R).symm z).support).IsPWO
⊢ ((of R).symm (y + z)).support ⊆ ((of R).symm y).support ∪ ((of R).symm z).support
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, (x.coeff + y.coeff) ij.1 • ((of R).symm z).coeff ij.2 =
    ((of R).symm (x • z + y • z)).coeff a

pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ (x + y).support ⊆ x.support ∪ y.support

Tactic:
of_symm_add

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ ∑ ij ∈ VAddAntidiagonal a ⋯, (x.coeff + y.coeff) ij.1 • ((of R).symm z).coeff ij.2 =
    ((of R).symm (x • z) + (of R).symm (y • z)).coeff a

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : AddCommMonoid R
inst✝ : SMulWithZero R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u
a : Γ'
hwf : (x.support ∪ y.support).IsPWO
⊢ (x + y).support ⊆ x.support ∪ y.support
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: case succ
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : α
n : ℕ
a✝ : f (n • a) ≤ f a
⊢ f (n • a + 1 • a) ≤ f a

Tactic:
apply le_trans <| hna (n • a) (1 • a)

Goal state after:
case succ
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : AddMonoid α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : α
n : ℕ
a✝ : f (n • a) ≤ f a
⊢ max (f (n • a)) (f (1 • a)) ≤ f a
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (ofLex 0).coeff (f.support.min' hsupport) < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))

Tactic:
suffices (seed.coeff (f.support.min' hsupport)) 0 <
      (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport)) by
    simpa using! this

Goal state after:
case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ (seed.coeff (f.support.min' hsupport)) 0 < (seed.coeff (f.support.min' hsupport)) (f (f.support.min' hsupport))
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (↑(f (f.support.min' hsupport)) - f.sum fun x x_1 ↦ ↑x_1)

Tactic:
rw [ArchimedeanClass.mk_sub_comm]

Goal state after:
case refine_2
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk ((f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)))
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
inst✝ : IsOrderedAddMonoid R
⊢ StrictMono ↑seed.baseEmbedding

Tactic:
by
  intro x y h
  apply lt_of_sub_pos
  rw [← LinearPMap.map_sub]
  exact baseEmbedding_pos _ <| by simpa using h

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
h,

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ ((single a) r * (single b) s).coeff (a + b) = ((single (a + b)) (r * s)).coeff (a + b)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C r).order = 0

Tactic:
h,

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C 0).order = 0
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ (C r).order = 0

Tactic:
exact order_single h

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ (A.valuation ↑a)⁻¹ ≤ 1

Tactic:
h,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ 1⁻¹ ≤ 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
⊢ A = B

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : A = B
⊢ A = B

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : B = ⊤
⊢ A = B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
⊢ B = ⊤

Tactic:
obtain h | h := eq_self_or_eq_top_of_le hle

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : A = B
⊢ B = ⊤

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : B = ⊤
⊢ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
· simp only [h_1, zero_mem]

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
· simp only [h_1, zero_mem]

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.nonunits ≤ A.nonunits
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

pp: case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
· simp only [h_1, zero_mem]

Goal state after:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B
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
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑((↑f).supSpanSingleton x (f.eval x) hx) ⟨a + k • x, ⋯⟩))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range

Tactic:
LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ ha

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
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩ + (RingHom.id K) k • f.eval x))) ∈
    ((↑f).supSpanSingleton x (f.eval x) hx).toFun.range
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 2 ↔ ∃ a b, f = X ^ 2 + C a * X + C b

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_add_add_two a b⟩

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ ∃ a b, f = X ^ 2 + C a * X + C b