mathlib-initiative/mathlib-tactics huggingface dataset:
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Nonempty (ArchimedeanStrata K M)

Tactic:
have hstratum (c : FiniteArchimedeanClass M) :
      ∃ G : Submodule K M, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c :=
    IsModularLattice.exists_disjoint_and_sup_eq (ball_lt_closedBall _).le

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
hstratum : ∀ (c : FiniteArchimedeanClass M), ∃ G, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c
⊢ Nonempty (ArchimedeanStrata K M)
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⟦Γ⟧
⊢ ((ofLex x).orderTop < (ofLex y).orderTop ∨
        (ofLex x).orderTop = (ofLex y).orderTop ∧
          ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff) ∧
      ArchimedeanClass.mk y ≤ ArchimedeanClass.mk x ↔
    (ofLex x).orderTop = (ofLex y).orderTop ∧
      ArchimedeanClass.mk (ofLex x).leadingCoeff = ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
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.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 : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ ArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨a, ha⟩)) ≤
    ArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))

Tactic:
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 : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ x✝ : { a // a ≠ 0 }
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h : FiniteArchimedeanClass.mk ↑⟨a, ha⟩ ⋯ ≤ FiniteArchimedeanClass.mk ↑⟨b, hb⟩ ⋯
⊢ (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop < (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∨
    (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).orderTop =
        (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).orderTop ∧
      ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨a, ha⟩))).leadingCoeff ≤
        ArchimedeanClass.mk (ofLex (toLex ((single (ofLex x).1) ↑⟨b, hb⟩))).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ ArchimedeanClass.mk (toLex ((single ao) a)) ≤ ArchimedeanClass.mk (toLex ((single bo) b))

Tactic:
archimedeanClassMk_le_archimedeanClassMk_iff

Goal state after:
case inl.mk.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b✝ : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
a : R
ha : a ≠ 0
b : R
hb : b ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, FiniteArchimedeanClass.mk b hb)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, FiniteArchimedeanClass.mk b hb))).1
⊢ (ofLex (toLex ((single ao) a))).orderTop < (ofLex (toLex ((single bo) b))).orderTop ∨
    (ofLex (toLex ((single ao) a))).orderTop = (ofLex (toLex ((single bo) b))).orderTop ∧
      ArchimedeanClass.mk (ofLex (toLex ((single ao) a))).leadingCoeff ≤
        ArchimedeanClass.mk (ofLex (toLex ((single bo) b))).leadingCoeff
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
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
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ ↑(f.support.min' hsupport) ≤ ↑j

Tactic:
exact Finset.min'_le f.support _ hj

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
h : f (x + y) ≠ f y
h1 : f (x + y) ≤ f y
⊢ max (f (-x)) (f (x + y)) < f y

Tactic:
map_neg_eq_map

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
h1 : f (x + y) ≤ f y
⊢ max (f x) (f (x + y)) < f y
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:
map_neg_eq_map

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
h1 : f (x + y) ≤ f x
⊢ max (f (x + y)) (f y) < f 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
inst✝ : Archimedean S
f : S →+*o R
x : R
r s : S
hr : f r ≤ x
hs : x ≤ f s
⊢ 0 ≤ mk x

Tactic:
apply (min_le_mk_of_le_of_le hr hs).trans'

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
inst✝ : Archimedean S
f : S →+*o R
x : R
r s : S
hr : f r ≤ x
hs : x ≤ f s
⊢ 0 ≤ min (mk (f r)) (mk (f s))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
⊢ x * y * z = x * (y * z)

Tactic:
ext b
  rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset,
    coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset]
  simp only [coeff_mul, sum_mul, mul_sum, sum_sigma']
  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
    aesop (add safe Set.add_mem_add) (add simp [add_assoc, mul_assoc])

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
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : x ∈ {x | 0 < (↑x - 1).orderTop}
hy : y ∈ {x | 0 < (↑x - 1).orderTop}
⊢ x * y ∈ {x | 0 < (↑x - 1).orderTop}

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial R

Goal state after:
case inl
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : x ∈ {x | 0 < (↑x - 1).orderTop}
hy : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Subsingleton R
⊢ x * y ∈ {x | 0 < (↑x - 1).orderTop}

case inr
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧ˣ
hx : x ∈ {x | 0 < (↑x - 1).orderTop}
hy : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
⊢ x * y ∈ {x | 0 < (↑x - 1).orderTop}
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
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
⊢ 0 < (y.inv - 1).orderTop

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial R

Goal state after:
case inl
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Subsingleton R
⊢ 0 < (y.inv - 1).orderTop

case inr
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
⊢ 0 < (y.inv - 1).orderTop
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
h₂ : ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ = ⟦y⟧

Tactic:
rw [mk_le_mk] at h₁ h₂

Goal state after:
case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ x ∨ y ≈ x
⊢ ⟦x⟧ = ⟦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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hmem : seq 0 ∈ Function.support (f.evalCoeff x)
⊢ ∃ y, ↑y - x ∈ ball K (seq 0)

Tactic:
contrapose hmem with hempty

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
seq : ℕ → FiniteArchimedeanClass M
hanti : StrictAnti seq
hempty : ¬∃ y, ↑y - x ∈ ball K (seq 0)
⊢ seq 0 ∉ Function.support (f.evalCoeff 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
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
⊢ (Function.support (f.evalCoeff x)).IsWF

Tactic:
by
  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.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case mp.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
· exact h a.2

Goal state after:
case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
⊢ v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring

Tactic:
constructor
  · intro h; ext x; specialize h x 1; simpa using h
  · intro h; apply isEquiv_of_val_le_one
    intro x
    have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]
    simpa using this

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B

Tactic:
by
  constructor
  · intro h x hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    by_cases h_2 : x⁻¹ + 1 = 0
    · rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2
      simpa only [h_2] using B.neg_mem _ B.one_mem
    · rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1,
        ← add_sub_cancel_right x⁻¹, ← Units.val_mk0 h_2, ← mem_principalUnitGroup_iff] at hx ⊢
      simpa only [hx] using @h (Units.mk0 (x⁻¹ + 1) h_2)
  · intro h x hx
    by_contra h_1; exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

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
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
habpos : 0 < a + b
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩

Tactic:
obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb

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
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
habpos : 0 < a + b
c : K
hc : c • x = b
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩
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
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯) = 1

Tactic:
this,

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) 1 = 1
Module: Mathlib.Algebra.Order.Ring.StandardPart

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

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ stdPart (x + y) = stdPart y

Tactic:
· rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : K
hx : 0 < mk x
hy : mk y < 0
⊢ stdPart (x + y) = stdPart y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr.inr
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 : x < 0
⊢ 0 = sInf {r | x < f r}

Tactic:
· convert! Real.sInf_univ.symm
      rw [Set.eq_univ_iff_forall]
      exact fun r ↦ lt_of_mk_lt_mk_of_nonpos hr h.le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
n : ℕ
a : R[X]
⊢ (aeval (C x)) ((monomial n) a) = (mapAlgHom (aeval x)) (swap ((monomial n) a))

Tactic:
simp
      induction a using Polynomial.induction_on'
        <;> aesop (add norm [add_mul, C_mul_X_pow_eq_monomial])

Goal state after:
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |↑ev|

Tactic:
← Int.cast_abs,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑|ev|
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  0 =
    (algebraMap ℤ K) b ^ f.natDegree *
      eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
zero_eq_mul

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) b ^ f.natDegree = 0 ∨
    eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ((monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

Tactic:
by
  rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]
  · simp
  · aesop (add simp coeff_monomial)
  · simp [h]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
· simpa [destutter_cons_cons, hab] using! hl₁.length_le_length_destutter (hl.cons_cons _)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p : R[X]
x : S
⊢ (-p).smeval x + p.smeval x = 0

Tactic:
← smeval_add,

Goal state after:
R : Type u_1
inst✝³ : Ring R
S : Type u_2
inst✝² : AddCommGroup S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
p : R[X]
x : S
⊢ (-p + p).smeval x = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).coeff n ≠ 0

Tactic:
trinomial_leading_coeff' hkm hmn

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ w ≠ 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).coeff n = w

Tactic:
trinomial_leading_coeff' hkm hmn

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ w = w
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ ↑w = (trinomial k m k✝ ↑u ↑v ↑w).coeff k✝

Tactic:
trinomial_leading_coeff' hkm hmn

Goal state after:
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ ↑w = ↑w