mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inl.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, b)

pp: case intro.intro.h.inl.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(a, d)

pp: case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(b, d)

pp: case intro.intro.h.inr.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, a)

Tactic:
· exact iha c rc ⟨b, hb⟩

Goal state after:
case intro.intro.h.inl.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(a, d)

case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(b, d)

case intro.intro.h.inr.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(c, a)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

Tactic:
by_cases h : r j i

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
h : r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))

case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → Acc (DFinsupp.Lex r s) (single i y)
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → x j = (single i a) j
hs : s i (x i) (Eq.recOn ⋯ a)
j : ι
hj : j ∈ x.support
hij : j ≠ i
h : ¬r j i
⊢ Acc (DFinsupp.Lex r s) (single j (x j))
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
x_pivot : α p
x_remove : (i : Fin n) → α (p.succAbove i)
s_pivot : Finset (α p)
s_remove : (i : Fin n) → Finset (α (p.succAbove i))
⊢ p.insertNth x_pivot x_remove ∈ piFinset (p.insertNth s_pivot s_remove) ↔
    x_pivot ∈ s_pivot ∧ x_remove ∈ piFinset s_remove

Tactic:
by
  simp [mem_piFinset_iff_pivot_removeNth p]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : j = i
⊢ m j ≤ 0

pp: case neg
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : ¬j = i
⊢ m j ≤ 0

Tactic:
· rw [← hm, hj]

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : ¬j = i
⊢ m j ≤ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.degree 1 = 0

Tactic:
by
  nontriviality R
  classical rw [MvPolynomial.one_def, degree_monomial]
  simp

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LeftPreLieRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
by
    have assoc_xyz := LeftPreLieRing.assoc_symm' x y z
    have assoc_zxy := LeftPreLieRing.assoc_symm' z x y
    have assoc_yzx := LeftPreLieRing.assoc_symm' y z x
    grind

Goal state after:
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:
set S := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}

Goal state after:
n : ℕ
hn : 0 < n
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
x✝ : ℕ
⊢ (0 • r) x✝ = 0 x✝

Tactic:
simp only [smul_apply, sum_const_zero, zero_smul, zero_apply]

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

Goal state before:
pp: k k' n : ℕ
hk : k ≤ k'
⊢ (σ k) n ≤ (σ k') n

Tactic:
simp_rw [sigma_apply]

Goal state after:
k k' n : ℕ
hk : k ≤ k'
⊢ ∑ d ∈ n.divisors, d ^ k ≤ ∑ d ∈ n.divisors, d ^ k'
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 1 ↔ n = 1

Tactic:
by_cases hn0 : n = 0
  · aesop
  constructor
  · intro h
    rw [← sigma_zero_eq_one_iff]
    have zero_lt_sigma := sigma_pos 0 n hn0
    have sigma_zero_le_sigma := sigma_mono 0 k n k.zero_le
    lia
  · simp +contextual

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k

Tactic:
rw [← sigma_one_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
  exact prod_congr n.support_factorization fun _ h =>
    sigma_one_apply_prime_pow <| prime_of_mem_primeFactors h

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

Goal state before:
pp: case succ
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime (n + 1).primeFactorsList.prod

Tactic:
hx,

Goal state after:
case succ
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime [x].prod
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case succ.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ primeFactorsList ?succ.n

pp: case succ.n
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ ℕ

Tactic:
hx,

Goal state after:
case succ.a
n : ℕ
h : Ω (n + 1) = 1
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ x ∈ [x]
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]
    rw [sum_comm]
    exact sum_congr rfl fun _ _ ↦ (by simp_all)

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Tendsto

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
hU : U ∈ F
i : M × M
hx : (antidiagonal (i.1 + i.2)).sup' ⋯ f ∉ U
hi : i ∈ antidiagonal (i.1 + i.2)
e : (antidiagonal (i.1 + i.2)).sup' ⋯ f = f i
⊢ i.1 ∈ Prod.fst '' (f ⁻¹' U)ᶜ

Tactic:
simpa using ⟨i.2, e ▸ hx⟩

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

Tactic:
by
  wlog! +distrib H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, leadingTerm, sPolynomial_monomial_mul, degree_mul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < a ↔ ↑q < inducedMap α γ a

Tactic:
Iff.comm,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
q : ℚ
⊢ ↑q < inducedMap α γ a ↔ ↑q < a
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
this : i + 1 = i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]

Goal state after:
case pos
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
this : i + 1 = i
⊢ f i ≤ (Finset.Iio i).sup f ⊔ (partialSups f) i
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: ⊢ ⌈0⌉ₑ = 0

Tactic:
simpa using ceil_natCast 0

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

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

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
s t : Interval α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
classical
    rw [disjoint_iff_inf_le, disjoint_iff_inf_le, ← coe_subset_coe, coe_inf]
    rfl

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

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ a✝¹ * a✝ = 1 ↔ ∃ a b, a✝¹ = NonemptyInterval.pure a ∧ a✝ = NonemptyInterval.pure b ∧ a * b = 1

Tactic:
exact NonemptyInterval.mul_eq_one_iff

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : Zero Γ
x y : R⟦Γ⟧
hy : y ≠ 0
h : x = 0
hxy : 0 = y
⊢ False

Tactic:
exact hy hxy.symm

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

Goal state before:
pp: case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|

Tactic:
obtain ⟨j, hj, hi⟩ := (lt_iff _ _).mp hn'

Goal state after:
case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |y| ≤ n • |x|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (ofLex ((n + 1) • |x|)).coeff j_1
hi : (ofLex |y|).coeff j < (ofLex ((n + 1) • |x|)).coeff j
⊢ |(ofLex y).leadingCoeff| ≤ (n + 1) • |(ofLex x).leadingCoeff|
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a b : M
u : Mˣ
⊢ a * ↑u ≤ b * ↑u⁻¹ * ↑u ↔ a * ↑u ≤ b

Tactic:
inv_mul_cancel_right

Goal state after:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a b : M
u : Mˣ
⊢ a * ↑u ≤ b ↔ a * ↑u ≤ b
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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
j : Γ
hj : j < (ofLex x).orderTop.untop ⋯
⊢ 0 = (ofLex ((n + 1) • |x|)).coeff j

Tactic:
suffices (ofLex |x|).coeff j = 0 by simp [this]
        apply coeff_eq_zero_of_lt_orderTop
        simpa using hj

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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseEmbedding.domain
⊢ 0 < ↑seed.baseEmbedding x

Tactic:
simp_rw [seed.domain_baseEmbedding] at hmem

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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
⊢ 0 < ↑seed.baseEmbedding x
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (⋯.min ⋯ + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
HahnSeries.order_of_ne hy,

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (⋯.min ⋯ + ⋯.min ⋯) = x.leadingCoeff • ((of R).symm y).leadingCoeff
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✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ x * (y + z) = x * y + x * z

Tactic:
by
    simp only [← of_symm_smul_of_eq_mul]
    exact HahnModule.smul_add x y z

Goal state after:
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
⊢ ⋯.min ⋯ + y.order ≤ (x * y).order

Tactic:
HahnSeries.order_of_ne hy,

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
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ (x * 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⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff

Tactic:
by
  simp only [leadingCoeff_eq, order_mul_of_ne_zero h, coeff_mul_order_add_order]

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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseEmbedding.domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range

Tactic:
simp_rw [seed.domain_baseEmbedding] at hmem

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
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))) ∈ seed.baseEmbedding.toFun.range
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ (n + 1)).order = (n + 1) • x.order

Tactic:
by
    obtain rfl | hx := eq_or_ne x 0 <;> simp [pow_succ, succ_nsmul, order_pow, pow_ne_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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - k • x ∈ ball K c
⊢ ∃ y, ↑y - x ∈ ball K c

Tactic:
use k⁻¹ • y

Goal state after:
case h
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
y : ↥(↑f).domain
hy : ↑y - k • x ∈ ball K c
⊢ ↑(k⁻¹ • y) - x ∈ ball K c
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
ha' : (↑a)⁻¹ ∈ A
⊢ IsUnit a

Tactic:
refine .of_mul_eq_one ⟨a⁻¹, ha'⟩ ?_

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
ha' : (↑a)⁻¹ ∈ A
⊢ a * ⟨(↑a)⁻¹, ha'⟩ = 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl

Tactic:
← IsLocalization.AtPrime.isUnit_to_map_iff (A.ofPrime P) P x,

Goal state after:
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
⊢ (A.ofPrime P).valuation ↑x = 1 ↔ IsUnit ((algebraMap ↥A ↥(A.ofPrime P)) x)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual a) ≤
    (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual b)
⊢ OrderDual.toDual a ≤ OrderDual.toDual b

Tactic:
simp only [OrderDual.toDual_le_toDual]

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a✝ b✝ : (PrimeSpectrum ↥A)ᵒᵈ
a b : PrimeSpectrum ↥A
h :
  (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual a) ≤
    (OrderDual.ofDual.trans A.primeSpectrumEquiv) (OrderDual.toDual b)
⊢ b ≤ a
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 : FiniteElement K
⊢ mk x < mk y ↔ x < y ∧ mk x ≠ mk y

Tactic:
refine (Quotient.mk_lt_mk (H := ordConnected_preimage_mk')).trans ?_
  rw [← Quotient.eq_iff_equiv]
  rfl

Goal state after: