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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
⊢ f = g

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean β
f g : α →+*o β
x : α
⊢ f x = g x
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✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : ↑q < inducedMap α β a
⊢ ↑q < a

Tactic:
← inducedMap_rat α

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
q : ℚ
h : inducedMap α β ↑q < inducedMap α β a
⊢ ↑q < a
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0

Tactic:
rwa [ne_eq, tsub_eq_zero_iff_le, not_le]

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

Goal state before:
pp: case right
M : Type u_2
inst✝³ : LinearOrder M
inst✝² : DenselyOrdered M
x : M
inst✝¹ : CommGroup M
inst✝ : IsOrderedCancelMonoid M
hx : x < 1
n : ℕ
y : M
hy : 1 < y
hy' : y ^ n < x⁻¹
⊢ x < y⁻¹ ^ n

Tactic:
simpa [lt_inv'] using hy'

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
⊢ I = closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ I}) x}

Tactic:
ext x

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
x : M
⊢ x ∈ I ↔ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ I}) x}
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
⊢ (fst α β).comp (inl α β) = OrderMonoidWithZeroHom.id α

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
x : α
⊢ ((fst α β).comp (inl α β)) x = (OrderMonoidWithZeroHom.id α) x
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
⊢ mk (k • a) = mk a

Tactic:
obtain ⟨m, hm⟩ := Archimedean.arch 1 (show 0 < |k| by simpa using h)

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
⊢ mk (k • a) = mk a
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✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
NonemptyInterval.coe_eq_pure

Goal state after:
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
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s

Tactic:
obtain ⟨b, hs, hb⟩ := not_subset.1 h

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
b : Interval α
hs : b ∈ x✝
hb : b ∉ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = ↑g
⊢ x.coeff g ≠ 0

Tactic:
by
  have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]
  have hx : x ≠ 0 := orderTop_ne_top.1 h
  rw [orderTop_of_ne_zero hx, WithTop.coe_eq_coe] at hg
  rw [← hg]
  exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
⊢ x.coeff x.order = 0 ↔ x = 0

Tactic:
refine ⟨not_imp_not.1 fun hx ↦ ?_, by simp +contextual⟩

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : ¬x = 0
⊢ ¬x.coeff x.order = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : x.coeff g = (embDomain f y).coeff (f g)
⊢ x.coeff g = y.coeff g

Tactic:
embDomain_coeff

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ x.order < i ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
rw [← not_le, le_order_iff_forall h]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (AddOpposite.unop (addOppositeEquiv x)).orderTop = x.orderTop

Tactic:
classical
  simp only [orderTop,
    addOppositeEquiv_support]
  simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
  simp_rw [HahnSeries.ext_iff, funext_iff]
  simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

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

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
⊢ g ∈ x.support

Tactic:
· have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
    rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this
    simpa [this] using hg

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

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid E₁
inst✝⁴ : PartialOrder E₁
inst✝³ : AddCommMonoid E₂
inst✝² : PartialOrder E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
x✝¹ x✝ : E₁ →ₚ[R] E₂
h : x✝¹.toLinearMap = x✝.toLinearMap
⊢ x✝¹ = x✝

Tactic:
ext x

Goal state after:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid E₁
inst✝⁴ : PartialOrder E₁
inst✝³ : AddCommMonoid E₂
inst✝² : PartialOrder E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
x✝¹ x✝ : E₁ →ₚ[R] E₂
h : x✝¹.toLinearMap = x✝.toLinearMap
x : E₁
⊢ x✝¹ x = x✝ x
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c : M
⊢ Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)

Tactic:
ext x

Goal state after:
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ x ∈ Ico (a * c) (b * c) ↔ x ∈ map (mulRightEmbedding c) (Ico a b)
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
· have : ¬0 < a + b := by simpa using add_nonpos ha hb
      simp [ha, hb, card_Ico_zero_add, Ico_eq_empty, this]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
⊢ Ico 0 ↑b = {0}

Tactic:
ext x

Goal state after:
case h
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x ∈ Ico 0 ↑b ↔ x ∈ {0}
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
hf' : ArchimedeanClass.mk (f.sum fun x xi ↦ ↑xi) = ArchimedeanClass.mk b
⊢ a = 0

Tactic:
contrapose! hf' with h0

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
⊢ ArchimedeanClass.mk (f.sum fun x xi ↦ ↑xi) ≠ ArchimedeanClass.mk b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₁
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
⊢ (finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R) = OrderHom.id

Tactic:
ext x

Goal state after:
case h₁
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex (Γ × FiniteArchimedeanClass R)
⊢ ((finiteArchimedeanClassOrderHomLex Γ R).comp (finiteArchimedeanClassOrderHomInvLex Γ R)) x = OrderHom.id x
Module: Mathlib.RingTheory.HahnSeries.Lex

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

Tactic:
ext x

Goal state after:
case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : FiniteArchimedeanClass (Lex R⟦Γ⟧)
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R)) x) = ↑(OrderHom.id x)
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
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ↑((finiteArchimedeanClassOrderIso Γ R) (FiniteArchimedeanClass.mk x h)) = (ofLex x).orderTop

Tactic:
by
  simp [finiteArchimedeanClassOrderIso]

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✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
⊢ (single a) r * (single b) s = (single (a + b)) (r * s)

Tactic:
ext x

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff 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
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk (↑↑f x) = ArchimedeanClass.mk (↑↑f y) ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
simp_rw [← toOrderAddMonoidHom_apply, ← orderHom_mk]
  trans ArchimedeanClass.mk x = .mk y
  · exact Function.Injective.eq_iff <| orderHom_injective <| toOrderAddMonoidHom_injective _
  · simp_rw [mk_eq_mk]
    aesop

Goal state after:
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
⊢ (Set.range fun s ↦ star s * s) = Set.univ.pi fun i ↦ Set.range fun s ↦ star s * s

Tactic:
ext x

Goal state after:
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy x : (i : ι) → A i
⊢ (x ∈ Set.range fun s ↦ star s * s) ↔ x ∈ Set.univ.pi fun i ↦ Set.range fun s ↦ star s * s
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)
hyz : ¬↑z - ↑y = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M),
    ↑c < ArchimedeanClass.mk (x - ↑z) → (ofLex (f.eval x)).coeff c = (ofLex (↑↑f z)).coeff c
⊢ ∀ (c : FiniteArchimedeanClass M), ↑c < ArchimedeanClass.mk (x - ↑z) → (ofLex (↑↑f (z - y))).coeff c = 0

Tactic:
intro c hc

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)
hyz : ¬↑z - ↑y = 0
h1 :
  ∀ (c : FiniteArchimedeanClass M),
    ↑c < ArchimedeanClass.mk (x - ↑z) → (ofLex (f.eval x)).coeff c = (ofLex (↑↑f z)).coeff c
c : FiniteArchimedeanClass M
hc : ↑c < ArchimedeanClass.mk (x - ↑z)
⊢ (ofLex (↑↑f (z - y))).coeff c = 0
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ R.ofPrime (R.idealOfLE S h) = S

Tactic:
ext x

Goal state after:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
⊢ x ∈ R.ofPrime (R.idealOfLE S h) ↔ x ∈ S
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
apply ofPrime_le_of_le

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual b).asIdeal ≤ (OrderDual.ofDual a).asIdeal
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
ext x

Goal state after:
case mp
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.IsEquiv v₂
x : K
⊢ x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
⊢ f.eval x < ↑↑f y

Tactic:
rw [HahnSeries.lt_iff]

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
⊢ ∃ i,
    (∀ j < i, (ofLex (f.eval x)).coeff j = (ofLex (↑↑f y)).coeff j) ∧
      (ofLex (f.eval x)).coeff i < (ofLex (↑↑f y)).coeff i
Module: Mathlib.RingTheory.Valuation.ValuationSubring

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

Tactic:
constructor
  · intro h x hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢
    by_contra h_2; exact hx (h 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.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
q : ℚ
⊢ mk ↑q = ↑q

Tactic:
change mk (FiniteElement.mk ..) = _
  cases q with | div n d hd
  rw [← mul_left_inj' (c := ↑d) (mod_cast hd), ← map_natCast mk d, ← map_mul,
    ← FiniteElement.mk_natCast, FiniteElement.mk_mul_mk]
  simp_all

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G
this : ↑a • QuotientGroup.mk '' s = QuotientGroup.mk '' (a • s)
h : a • s = s
⊢ QuotientGroup.mk '' (a • s) = QuotientGroup.mk '' s

Tactic:
by rw [h]

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

Goal state before:
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_of_mk_ne_zero hy.ne, stdPart_of_mk_ne_zero]

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
⊢ mk (x + y) ≠ 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

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

Tactic:
by
  obtain hy | hy := le_or_gt 0 (mk y)
  · rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]
  · rw [stdPart_of_mk_ne_zero hy.ne, stdPart_of_mk_ne_zero]
    rw [mk_add_eq_mk_right (hy.trans hx)]
    exact hy.ne

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
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ↑(ball K d) ⊆ ↑(ball K c)

Tactic:
simpa using (ball_strictAnti K).antitone hdc

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
hp : P = 0
⊢ (C x * P).coeffList = List.map (fun x_1 ↦ x * x_1) P.coeffList

Tactic:
simp [hp]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ (p.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (p.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
divModByMonicAux

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : p = 0
⊢ (if p * q = 0 then 0 else ↑(Fintype.card Fq) ^ (p * q).natDegree) =
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) * if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
simp [hp]

Goal state after: