mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ f.totalDegree = 0

Tactic:
apply Nat.eq_zero_of_le_zero

Goal state after:
case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ f.totalDegree ≤ 0
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (monomial n) a = (monomial n) 1 * C a

Tactic:
rw [mul_comm, C_mul_monomial, mul_one]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ toLex (single 0 1) + toLex (single 1 1) < toLex (single 0 2)

Tactic:
use 0

Goal state after:
case h
α : Type u_1
⊢ (∀ (j : Fin 2),
      (fun x1 x2 ↦ x1 < x2) j 0 →
        (ofLex (toLex (single 0 1) + toLex (single 1 1))) j = (ofLex (toLex (single 0 2))) j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (single 0 1) + toLex (single 1 1))) 0) ((ofLex (toLex (single 0 2))) 0)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mpr.inl
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b

Tactic:
use 0

Goal state after:
case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ 0 ≤ Finsupp.single i 1 ∧ b ∣ r ∧ p = (monomial 0) b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
hn,

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ 0) = 0
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) ≤
    ↑(#({x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i))

Tactic:
by
            gcongr with x; exact And.right

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0 ∨ g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
rcases h0 with h0 | h0

Goal state after:
case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
suffices f * g ≠ 0 by simp [withBotDegree_eq, m.degree_mul_of_left_mem_nonZeroDivisors hf, *]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f ≠ 0 ∧ g ≠ 0
⊢ f * g ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : f - m.leadingTerm f ≠ 0
⊢ m.degree f ≠ 0

Tactic:
contrapose h
  rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_zero]

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
⊢ coeff (m.degree (m.sPolynomial f g)) (m.sPolynomial f g) = 0

Tactic:
hs,

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
⊢ coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
⊢ ∏ x ∈ n.primeFactors, x = n

Tactic:
apply prod_primeFactors_of_squarefree hn

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

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = ∏ i, a i

Tactic:
Fin.prod_univ_three a

Goal state after:
n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * a 2
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i, a i = n

Tactic:
Fin.prod_univ_three a

Goal state after:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Field β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
q : ℚ
⊢ cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}

Tactic:
by
  simp_rw [cutMap, Rat.cast_lt]

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)

Tactic:
obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
q : ℚ
hq : ↑q - b < a
q₁ : ℚ
hq₁q : ↑q - b < ↑q₁
hq₁ab : ↑q₁ < a
⊢ q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑q ^ 2
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
rw [← cast_pow] at hbq

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < ↑(q ^ 2)
hqa : ↑q ^ 2 < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f n = g n

Tactic:
hn,

Goal state after:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f 0 = g 0
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case e'_8
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ ↑s = ⇑σ ⁻¹' ↑s

Tactic:
rw [σ.eq_preimage_iff_image_eq, Set.image_perm hσ]

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

Goal state before:
pp: case pos
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : x ≤ 1
⊢ ∃ n, x ≤ y ^ n

Tactic:
use 0

Goal state after:
case h
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
h : ∀ (a : M), a ≠ 1 → ∀ (b : M), b ≠ 1 → mk a = mk b
x y : M
hy : 1 < y
hx : x ≤ 1
⊢ x ≤ y ^ 0
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ StrictAnti subsemigroup

Tactic:
intro s t hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s < t
⊢ subsemigroup t < subsemigroup s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ Antitone subgroup

Tactic:
intro s t hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
⊢ subgroup t ≤ subgroup s
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁷ : Semiring α
inst✝⁶ : PartialOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : MulActionWithZero α β
inst✝² : FloorDiv α β
a : α
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β), c ≤ a • b ⌊/⌋ a ↔ c ≤ b

Tactic:
by simp [smul_le_smul_iff_of_pos_left, ha]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁷ : Semiring α
inst✝⁶ : PartialOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : MulActionWithZero α β
inst✝² : CeilDiv α β
a : α
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
b : β
⊢ ∀ (c : β), a • b ⌈/⌉ a ≤ c ↔ b ≤ c

Tactic:
by simp [smul_le_smul_iff_of_pos_left, ha]

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ MulArchimedeanClass.lift (fun b ↦ if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A ≠ ⊤

Tactic:
induction A using MulArchimedeanClass.ind with | mk a
    simpa using MulArchimedeanClass.mk_eq_top_iff.not.mp hA

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∀ a ∈ range #s, c - ↑a ∈ Ioc (c - ↑(#s)) c

Tactic:
intro x mx; rw [mem_Ioc]; rw [mem_range] at mx; lia

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.InjOn (fun x ↦ c + ↑x) ↑(range #s)

pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.SurjOn (fun x ↦ c + ↑x) ↑(range #s) ↑(Ico c (c + ↑(#s)))

Tactic:
· intro x mx y my (h : c + x = c + y); lia

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Set.SurjOn (fun x ↦ c + ↑x) ↑(range #s) ↑(Ico c (c + ↑(#s)))
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 : ∀ (a : α), f a ≤ b
⊢ b ∈ {x | 0 ≤ x}

Tactic:
exact le_trans (hf0 Classical.ofNonempty) (hb Classical.ofNonempty)

Goal state after:
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
s : NonemptyInterval α
hs : ↑s ∈ S
⊢ (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).1 ≤
    (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).2

Tactic:
exact iInf₂_le_of_le s hs (le_iSup₂_of_le s hs s.fst_le_snd)

Goal state after:
Module: Mathlib.Data.Finset.MulAntidiagonal

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

Tactic:
IsWF.le_min_iff

Goal state after:
α : Type u_1
s t : Set α
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s * t, hs.min hsn * ht.min htn ≤ b
Module: Mathlib.RingTheory.HahnSeries.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 Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝² x✝¹ : R
x✝ : V⟦Γ⟧
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by
    ext
    simp [add_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
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ (fun i ↦ ArchimedeanClass.mk ↑(f i)) x < (fun i ↦ ArchimedeanClass.mk ↑(f i)) y

Tactic:
change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
x : FiniteArchimedeanClass M
hx : x ∈ ↑f.support
y : FiniteArchimedeanClass M
hy : y ∈ ↑f.support
hxy : x < y
⊢ ArchimedeanClass.mk ↑(f x) < ArchimedeanClass.mk ↑(f y)
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
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
rw [HahnSeries.orderTop_of_ne_zero hx, HahnSeries.orderTop_of_ne_zero hhy, ← h,
      ← Set.IsWF.min_vadd]

Goal state after:
case neg
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
⊢ ↑(⋯.min ⋯) ≤ ((of R).symm (x • y)).orderTop
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 0 + mk x = mk x

Tactic:
rw [← mk_one, ← mk_mul, one_mul]

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✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
m : ℕ
hm_lt : m < n + 1
hM : f ((a + b) ^ n) ≤ f (↑(n.choose m) * (a ^ m * b ^ (n - m)))
⊢ f ((a + b) ^ n) ≤ f (a ^ m) * f (b ^ (n - m))

Tactic:
exact le_trans hM (le_trans (nmul_le hna) (map_mul_le_mul _ _ _))

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Tactic:
by_cases h : g = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : ¬g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g
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⟦Γ⟧
hyz : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ y = z

Tactic:
let : AddCancelCommMonoid R := ⟨⟩
    contrapose! hyz
    simp only [ne_eq, ← coeff_inj, funext_iff, not_forall] at ⊢ hyz
    have : Set.IsWF {a | y.coeff a ≠ z.coeff a} :=
      .mono (y.isWF_support.union z.isWF_support) (by intro; simp; grind)
    let a : Γ := this.min hyz
    have ha : y.coeff a ≠ z.coeff a := this.min_mem hyz
    refine ⟨x.order + a, ?_⟩
    rwa [coeff_mul, coeff_mul, sum_subset subset_union_left,
      sum_subset (s₁ := antidiagonal _ _ _) subset_union_right,
      sum_eq_sum_iff_single (i := (x.order, a)), mul_right_inj' (coeff_order_eq_zero.not.2 hx)]
    · simp [hx]
      grind
    · simp +contextual only [mem_union, mem_antidiagonal, mul_eq_mul_left_iff, Prod.mk.injEq,
        ne_eq, ← and_or_left, ← or_and_right, or_false, and_imp, Prod.forall, mem_support, not_and]
      rintro b c hxb - hbc hbc'
      contrapose! hbc'
      rwa [eq_comm, eq_comm (a := c), ← add_eq_add_iff_eq_and_eq (order_le_of_coeff_ne_zero hxb)
        (Set.IsWF.min_le this hyz hbc'), eq_comm]
    · simp +contextual [← and_or_left, ← or_and_right]
    · simp +contextual [← and_or_left, ← or_and_right]

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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (x - ↑z + (↑z - ↑y))

Tactic:
apply ArchimedeanClass.mk_left_le_mk_add

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
y : ↥(↑f).domain
h : f.eval x = ↑↑f y
z : ↥(↑f).domain
this : x - ↑y = x - ↑z + (↑z - ↑y)
⊢ ArchimedeanClass.mk (x - ↑z) ≤ ArchimedeanClass.mk (↑z - ↑y)
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ↑b = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
use 0

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ↑b = 0
⊢ a * 0 = b ∨ b * 0 = a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
use 0

Goal state after:
case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ a * 0 = b ∨ b * 0 = a
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: s : ℝ
⊢ 0 ≤ star s * s

Tactic:
exact mul_self_nonneg s

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
Γ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsEquiv v.valuationSubring.valuation

Tactic:
rw [isEquiv_iff_val_le_one]
  intro x
  rw [ValuationSubring.valuation_le_one_iff, mem_valuationSubring_iff]

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

Goal state before:
pp: case mk.mk.inl
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
hy : 0 < mk y
hx : mk x ≤ 0
⊢ ∃ n, mk x ≤ n • mk y

Tactic:
use 0

Goal state after:
case h
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
hy : 0 < mk y
hx : mk x ≤ 0
⊢ mk x ≤ 0 • mk y
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : FiniteResidueField K →+*o ℝ
h : 0 ≤ mk x
⊢ Classical.ofNonempty = f

Tactic:
exact Subsingleton.allEq _ _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval x (eval (C y) (C p)) = eval x p

Tactic:
eval_C

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ eval x p = eval x p