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

Goal state before:
pp: case insert.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f a • g (σ a) + f ((Equiv.symm σ) a) • g (σ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (σ i) ≤
    f a • g a + (f ((Equiv.symm σ) a) • g (τ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (τ i))

Tactic:
← add_assoc

Goal state after:
case insert.inr
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
⊢ f a • g (σ a) + f ((Equiv.symm σ) a) • g (σ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (σ i) ≤
    f a • g a + f ((Equiv.symm σ) a) • g (τ ((Equiv.symm σ) a)) + ∑ i ∈ s.erase ((Equiv.symm σ) a), f i • g (τ i)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case cons
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
⊢ mk (∏ i ∈ Finset.cons i s hi, a i) = mk (a ((Finset.cons i s hi).min' ⋯))

Tactic:
rw [Finset.prod_cons]

Goal state after:
case cons
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
⊢ mk (a i * ∏ x ∈ s, a x) = mk (a ((Finset.cons i s hi).min' ⋯))
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (f i).IsMultiplicative) → (∏ i ∈ s, f i).IsMultiplicative
hf : ∀ i ∈ cons a s ha, (f i).IsMultiplicative
⊢ (∏ i ∈ cons a s ha, f i).IsMultiplicative

Tactic:
rw [Finset.prod_cons]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
f : ι → ArithmeticFunction R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, (f i).IsMultiplicative) → (∏ i ∈ s, f i).IsMultiplicative
hf : ∀ i ∈ cons a s ha, (f i).IsMultiplicative
⊢ (f a * ∏ x ∈ s, f x).IsMultiplicative
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : mk a < mk b
hpos : 1 ≤ a
⊢ b < a

Tactic:
obtain h := mk_lt_mk.mp h 1
  rw [pow_one, mabs_lt, mabs_eq_self.mpr hpos] at h
  exact h.2

Goal state after:
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: S : Type u_1
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : SetLike S G
C : S
inst✝² : GroupConeClass S G
inst✝¹ : HasMemOrInvMem C
inst✝ : DecidablePred fun x ↦ x ∈ C
a b : G
⊢ a ≤ b ∨ b ≤ a

Tactic:
simpa using mem_or_inv_mem C (b / a)

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(ofClass WithZero.withZeroUnitsEquiv.symm)

Tactic:
intro x y

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ Monotone ⇑(ofClass WithZero.withZeroUnitsEquiv.symm)

Tactic:
intro x y

Goal state after:
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀
⊢ x ≤ y → (ofClass WithZero.withZeroUnitsEquiv.symm) x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) y
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ Monotone (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun

Tactic:
intro x y

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
x y : WithZero (Lex (αˣ × βˣ))
⊢ x ≤ y →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun x ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun y
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : ↑s ∈ lowerBounds s₁
h : ¬∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ ↑s ≤ ⊥

Tactic:
cases h fun b hb c hc ↦ (WithBot.coe_le_coe.1 <| ha hb).1.trans
              (s.fst_le_snd.trans (WithBot.coe_le_coe.1 <| ha hc).2)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx : x.orderTop ≠ ⊤
⊢ x.coeff (x.orderTop.untop hx) = x.leadingCoeff

Tactic:
orderTop_ne_top

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx✝ : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff (x.orderTop.untop hx✝) = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)

Tactic:
coeff_add

Goal state after:
case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.coeff (x.orderTop.untop ⋯) + y.coeff (x.orderTop.untop ⋯) = x.coeff (x.orderTop.untop ⋯)
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
⊢ 1 ∈ (orderAddMonoidHom G).range

Tactic:
have ⟨a, ha⟩ := exists_zero_lt (α := G)

Goal state after:
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
⊢ 1 ∈ (orderAddMonoidHom G).range
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
hstratum : ∀ (c : FiniteArchimedeanClass M), ∃ G, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c
⊢ Nonempty (ArchimedeanStrata K M)

Tactic:
choose g h1 h2 using hstratum

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
g : FiniteArchimedeanClass M → Submodule K M
h1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (ball K c) (g c)
h2 : ∀ (c : FiniteArchimedeanClass M), ball K c ⊔ g c = closedBall K c
⊢ Nonempty (ArchimedeanStrata K M)
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
⊢ ∑ ij ∈ {(⋯.min ⋯, ⋯.min ⋯)}, x.coeff ij.1 • ((of R).symm y).coeff ij.2 =
    x.coeff (x.orderTop.untop ⋯) • ((of R).symm y).coeff (((of R).symm y).orderTop.untop ⋯)

Tactic:
Finset.sum_singleton

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
⊢ x.coeff (⋯.min ⋯, ⋯.min ⋯).1 • ((of R).symm y).coeff (⋯.min ⋯, ⋯.min ⋯).2 =
    x.coeff (x.orderTop.untop ⋯) • ((of R).symm y).coeff (((of R).symm y).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

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

Tactic:
rw [← of_symm_smul_of_eq_mul, add_comm, ← vadd_eq_add]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
⊢ ((HahnModule.of R).symm ((single b) r • (HahnModule.of R) x)).coeff (b +ᵥ a) = r * x.coeff a
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|

Tactic:
obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)

Goal state after:
case mp.succ
R : Type u_1
S : Type u_2
inst✝⁷ : LinearOrder R
inst✝⁶ : LinearOrder S
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : Ring S
inst✝² : IsStrictOrderedRing S
inst✝¹ : DenselyOrdered R
inst✝ : Archimedean R
x y : S
f : R →+* S
hf : StrictMono ⇑f
H : ∀ {q : R}, 0 < f q ↔ 0 < q
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y)| ≤ (n + 1) • |ArchimedeanOrder.val (ArchimedeanOrder.of x)|
q : R
hq₀ : 0 < q
hq : (n + 1) • q < 1
⊢ ∃ q, 0 < f q ∧ f q * |y| ≤ |x|
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
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
have hxy : x * y ≠ 0 := fun h ↦ (by simp [h] at this)

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
⊢ (x * y).orderTop = x.orderTop + y.orderTop
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ ↑n.succ) = ↑n • mk x + mk x

Tactic:
Nat.cast_succ

Goal state after:
case mk
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : Field R
inst✝ : IsOrderedRing R
n : ℕ
x : R
⊢ mk (x ^ (↑n + 1)) = ↑n • mk x + mk x
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
x : Quotient s
⊢ x ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝ : LE α
x : α
⊢ ⟦x⟧ ≤ ⟦x⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
x y z : Quotient s
h₁ : x ≤ y
h₂ : y ≤ z
⊢ x ≤ z

Tactic:
induction x using Quotient.inductionOn with | h x

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝ : LE α
y z : Quotient s
h₂ : y ≤ z
x : α
h₁ : ⟦x⟧ ≤ y
⊢ ⟦x⟧ ≤ z
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : Quotient s
⊢ x ≤ y ∨ y ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x

Goal state after:
case h
α : Type u_1
s : Setoid α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : Quotient s
x : α
⊢ ⟦x⟧ ≤ y ∨ y ≤ ⟦x⟧
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
x y : Quotient s
h : x ≤ y
⊢ Quotient.lift f H x ≤ Quotient.lift f H y

Tactic:
induction x using Quotient.inductionOn with | h x

Goal state after:
case h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
y : Quotient s
x : α
h : ⟦x⟧ ≤ y
⊢ Quotient.lift f H ⟦x⟧ ≤ Quotient.lift f H y
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬(y, z).1 + (y, z).2 = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

Tactic:
rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬a + b = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : 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 : Quotient s
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x = y

Tactic:
induction x using Quotient.inductionOn with | h x

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

Goal state before:
pp: α : 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 : Quotient s
h₁ : x ≤ y
h₂ : y ≤ x
⊢ x = y

Tactic:
induction x using Quotient.inductionOn with | h x
    induction y using Quotient.inductionOn with | h y
    rw [mk_le_mk] at h₁ h₂
    cases h₁ with
    | inr h => exact Quotient.sound h
    | inl h₁ =>
      cases h₂ with
      | inr h => exact (Quotient.sound h).symm
      | inl h₂ => exact congrArg _ (h₁.antisymm h₂)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
⊢ r = s

Tactic:
have h := rs 0

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (x : Γ), (C r).coeff x = (C s).coeff x
h : (C r).coeff 0 = (C s).coeff 0
⊢ r = s
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ ⟦x⟧ < ⟦y⟧ ↔ x < y ∧ ¬x ≈ y

Tactic:
contrapose! +distrib
  rw [mk_le_mk, comm_of (· ≈ ·)]

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✝ : NoZeroDivisors R
x✝ y✝ x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
⊢ x * y ≠ 0

Tactic:
simp only [ne_eq, HahnSeries.ext_iff, funext_iff, not_forall]

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✝ : NoZeroDivisors R
x✝ y✝ x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ∃ x_1, ¬(x * y).coeff x_1 = coeff 0 x_1
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
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
⊢ { coeff := f.evalCoeff (k • x), isPWO_support' := ⋯ }.coeff c =
    (k • { coeff := f.evalCoeff x, isPWO_support' := ⋯ }).coeff c

Tactic:
suffices f.evalCoeff (k • x) c = k • f.evalCoeff x c by simpa using this

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
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : (R.mapOfLE S h) 1 ≤ (R.mapOfLE S h) (R.valuation ↑((A.inclusion R hR) x))
⊢ False

Tactic:
rw [(mapOfLE _ _ _).map_one, mapOfLE_valuation_apply] at c

Goal state after:
K : Type u
inst✝ : Field K
A R S : ValuationSubring K
hR : A ≤ R
hS : A ≤ S
h : R ≤ S
x : ↥A
hx : x ∈ A.idealOfLE S hS
c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)
⊢ False
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
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
⊢ ∀ j < FiniteArchimedeanClass.mk (↑y - x) hxy0, (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j

Tactic:
intro j hj
    apply evalCoeff_eq
    simpa [j.prop] using! fun _ ↦ hj

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
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ 0 < mk ↑(z - x)

Tactic:
apply hy.trans_le (mk_antitoneOn _ _ _) <;> simpa

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 : K
f : ℝ →+*o K
hx : 0 ≤ mk x
⊢ ((FiniteResidueField.ofArchimedean f).comp Classical.ofNonempty) (FiniteResidueField.mk (FiniteElement.mk x hx)) =
    FiniteResidueField.mk (FiniteElement.mk x hx)

Tactic:
OrderRingHom.apply_eq_self

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : 0 ≤ mk x
⊢ FiniteResidueField.mk (FiniteElement.mk x hx) = FiniteResidueField.mk (FiniteElement.mk x hx)