mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
rw [le_antisymm_iff, archimedeanClassMk_le_archimedeanClassMk_iff,
    archimedeanClassMk_le_archimedeanClassMk_iff]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
⊢ ((ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff) ∧
      ((ofLex y).orderTop < (ofLex x).orderTop ∨
        (ofLex y).orderTop = (ofLex x).orderTop ∧
          ArchimedeanClass.mk (ofLex y).leadingCoeff ≤ ArchimedeanClass.mk (ofLex x).leadingCoeff) ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z

Tactic:
simp_all only [rightMulResiduation, mul_sSup_distrib, Set.mem_ofPred_eq,
      iSup_le_iff, implies_true]

Goal state after:
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✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : SMulZeroClass R V
x : R⟦Γ⟧
x✝ : Γ'
⊢ ((of R).symm (x • 0)).coeff x✝ = ((of R).symm 0).coeff x✝

Tactic:
simp [coeff_smul]

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

Goal state before:
pp: case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : FiniteArchimedeanClass (Lex R⟦Γ⟧)
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R)) x) = ↑(OrderHom.id x)

Tactic:
induction x using FiniteArchimedeanClass.ind with

Goal state after:
case h₂.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a : Lex R⟦Γ⟧
ha : a ≠ 0
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R))
        (FiniteArchimedeanClass.mk a ha)) =
    ↑(OrderHom.id (FiniteArchimedeanClass.mk a ha))
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✝ : SMulWithZero R V
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm (0 • x)).coeff x✝ = ((of R).symm 0).coeff x✝

Tactic:
simp [coeff_smul]

Goal state after:
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 x < f y
⊢ f (x + y) = f y

Tactic:
by_contra! h

Goal state after:
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 x < f y
h : f (x + y) ≠ f y
⊢ False
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
⊢ f (x + y) = f x

Tactic:
by_contra! h

Goal state after:
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
⊢ False
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✝³ x✝² x✝¹ x✝ : R
hx : mk x✝³ = mk x✝²
hy : mk x✝¹ = mk x✝
⊢ mk (x✝³ * x✝¹) = mk (x✝² * x✝)

Tactic:
by
    exact (mk_mul_le_of_le hx.le hy.le).antisymm (mk_mul_le_of_le hx.ge hy.ge)

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
⊢ mk x + mk y + z = mk x + (mk y + z)

Tactic:
induction z with | mk z

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

Goal state before:
pp: case mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
h : mk x ≤ mk y
⊢ mk x + z ≤ mk y + z

Tactic:
induction z with | mk z

Goal state after:
case mk.mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x ≤ mk y
z : R
⊢ mk x + mk z ≤ mk y + mk z
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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ seed.baseEmbedding.toFun ⟨f'.sum fun d x ↦ ↑x, ⋯⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x)))

Tactic:
apply_fun ofLex

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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (seed.baseEmbedding.toFun ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) =
    ofLex (toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))))
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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ↑seed.baseEmbedding ⟨↑x, hx'⟩ = toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩))

Tactic:
apply_fun ofLex

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
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = ofLex (toLex ((single c) ((seed.coeff c) ⟨↑x, hx⟩)))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g i : Γ
left✝¹ : i ∈ x.support
j : Γ
left✝ : j ∈ y.support
h2 : (embDomain f x).coeff (f i, f j).1 * (embDomain f y).coeff (f i, f j).2 ≠ 0
h1 : x.coeff i ≠ 0 ∧ y.coeff j ≠ 0 ∧ i + j = g
⊢ ∃ a b, (x.coeff a ≠ 0 ∧ y.coeff b ≠ 0 ∧ a + b = g) ∧ Prod.map ⇑f.toEmbedding ⇑f.toEmbedding (a, b) = (f i, f j)

Tactic:
exact ⟨i, j, h1, rfl⟩

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x * y)).coeff g = (embDomain f x * embDomain f y).coeff g

Tactic:
rw [embDomain_of_notMem_range hg, eq_comm]
    contrapose! hg
    obtain ⟨_, hi, _, hj, rfl⟩ := support_mul_subset ((mem_support _ _).2 hg)
    obtain ⟨i, _, rfl⟩ := support_embDomain_subset hi
    obtain ⟨j, _, rfl⟩ := support_embDomain_subset hj
    exact ⟨i + j, hf i j⟩

Goal state after:
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✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬∑ ij ∈ antidiagonal ⋯ ⋯ (x.order + a), x.coeff ij.1 * y.coeff ij.2 =
      ∑ ij ∈ antidiagonal ⋯ ⋯ (x.order + a), x.coeff ij.1 * z.coeff ij.2

Tactic:
sum_subset subset_union_left,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬∑ x_1 ∈ antidiagonal ⋯ ⋯ (x.order + a) ∪ ?m.138, x.coeff x_1.1 * y.coeff x_1.2 =
      ∑ ij ∈ antidiagonal ⋯ ⋯ (x.order + a), x.coeff ij.1 * z.coeff ij.2

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (x.order + a) ∪ ?m.138,
    x_1 ∉ antidiagonal ⋯ ⋯ (x.order + a) → x.coeff x_1.1 * y.coeff x_1.2 = 0

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := ⋯
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := ⋯
ha : y.coeff a ≠ z.coeff a
⊢ Finset (Γ × Γ)
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✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬∑ ij ∈ antidiagonal ⋯ ⋯ (a + x.order), y.coeff ij.1 * x.coeff ij.2 =
      ∑ ij ∈ antidiagonal ⋯ ⋯ (a + x.order), z.coeff ij.1 * x.coeff ij.2

Tactic:
sum_subset subset_union_left,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ¬∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ ?m.360, y.coeff x_1.1 * x.coeff x_1.2 =
      ∑ ij ∈ antidiagonal ⋯ ⋯ (a + x.order), z.coeff ij.1 * x.coeff ij.2

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ x_1 ∈ antidiagonal ⋯ ⋯ (a + x.order) ∪ ?m.360,
    x_1 ∉ antidiagonal ⋯ ⋯ (a + x.order) → y.coeff x_1.1 * x.coeff x_1.2 = 0

Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := ⋯
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := ⋯
ha : y.coeff a ≠ z.coeff a
⊢ Finset (Γ × Γ)
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
⊢ (Function.support (f.evalCoeff x)).IsWF

Tactic:
rw [Set.isWF_iff_no_descending_seq]
  by_contra! ⟨seq, ⟨hanti, hmem⟩⟩
  have hnonempty : ∃ y : f.val.domain, y.val - x ∈ ball K (seq 0) := by
    specialize hmem 0
    contrapose hmem with hempty
    simp [evalCoeff, dif_neg hempty]
  obtain ⟨y, hy⟩ := hnonempty
  have hmem' (n : ℕ) : seq n ∈ (ofLex (f.val y)).coeff.support := by
    specialize hmem n
    rw [Function.mem_support] at ⊢ hmem
    convert hmem
    refine (f.evalCoeff_eq ((ball_strictAnti K).antitone ?_ hy)).symm
    simpa using hanti.antitone (show 0 ≤ n by simp)
  obtain hwf := (ofLex (f.val y)).isWF_support
  contrapose! hwf
  rw [Set.isWF_iff_no_descending_seq]
  simpa using ⟨seq, hanti, hmem'⟩

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

Goal state before:
pp: case pos
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ∃ y, ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c

pp: case neg
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c

Tactic:
· obtain ⟨y, hy⟩ := h
    have heq : (k • y).val - k • x = k • (y.val - x) := by simp [smul_sub]
    have hy' : (k • y).val - k • x ∈ ball K c := by
      rw [heq]
      exact Submodule.smul_mem _ _ hy
    simp [f.evalCoeff_eq hy, f.evalCoeff_eq hy', LinearPMap.map_smul]

Goal state after:
case neg
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
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
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - ↑y
huv' : x - ↑y - v = u
hyv : ↑y + v ∈ (↑f).domain
⊢ f.eval x ≠ ↑↑f y

Tactic:
by_contra! h

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
y : ↥(↑f).domain
this : x - ↑y ≠ 0
xy : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (x - ↑y) this
u : M
hu : ∀ (h : u ≠ 0), xy < FiniteArchimedeanClass.mk u h
v : M
hv : v ∈ seed.stratum xy
huv : u + v = x - ↑y
huv' : x - ↑y - v = u
hyv : ↑y + v ∈ (↑f).domain
h : f.eval x = ↑↑f y
⊢ False
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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this : ↑z ≠ x
⊢ ArchimedeanClass.mk (↑z - x) ≠ ⊤

Tactic:
simpa [sub_eq_zero]

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
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
this✝ : ↑z ≠ x
hzy : z < y
hzyne : ↑z - ↑y ≠ 0
this : ↑y - ↑z = ↑y - x + (x - ↑z)
⊢ ArchimedeanClass.mk (↑z - x) ≠ ⊤

Tactic:
simpa [sub_eq_zero]

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

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
z : FiniteResidueField K
hz : 0 ≤ z
x y : FiniteElement K
h : mk x ≤ mk y
⊢ z * mk x ≤ z * mk y

Tactic:
induction z with | mk z

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
hz : 0 ≤ mk z
⊢ mk z * mk x ≤ mk z * mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
z : FiniteResidueField K
x y : FiniteElement K
h : mk x ≤ mk y
⊢ mk x + z ≤ mk y + z

Tactic:
induction z with | mk z

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
h : a • s = s
b : α
⊢ a • b ∈ s ↔ b ∈ s

Tactic:
rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 ≤ mk x
hy : 0 ≤ -mk y
⊢ stdPart (x / y) = stdPart x / stdPart y

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, stdPart_mul hx, stdPart_inv]
  rwa [mk_inv]

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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : 0 ≤ x
⊢ 0 = sInf {r | x < f r}

Tactic:
convert! Real.sInf_empty.symm
      rw [Set.eq_empty_iff_forall_notMem]
      exact fun r ↦ (lt_of_mk_lt_mk_of_nonneg hr h).not_gt

Goal state after: