mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
x✝ : Γ
⊢ ((r • x).map f).coeff x✝ = (r • x.map f).coeff x✝

Tactic:
;

Goal state after:
Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
x✝ : Γ
⊢ ((r • x).map f).coeff x✝ = (r • x.map f).coeff x✝
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 : E₁
⊢ x✝¹ x = x✝ x

Tactic:
;

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.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
d : Associates M
c : Associates M
⊢ a * c ≤ a * d * c

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
d : Associates M
c : Associates M
⊢ a * c ≤ a * d * c
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: 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✝
G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
a b : G
h : a ≤ b
this : Monotone (↑(orderMonoidHom Gˣ).toMonoidHom).toFun
⊢ (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun a ≤
    (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun b

Tactic:
;

Goal state after:
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✝
G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
a b : G
h : a ≤ b
this : Monotone (↑(orderMonoidHom Gˣ).toMonoidHom).toFun
⊢ (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun a ≤
    (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun b
Module: Mathlib.Algebra.Order.PUnit

Goal state before:
pp: a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ a✝¹ + c✝ ≤ b✝ + c✝

Tactic:
;

Goal state after:
a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ a✝¹ + c✝ ≤ b✝ + c✝
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) m✝ n₁✝) ((fun x1 x2 ↦ x1 * x2) m✝ n₂✝)

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 * x2) m✝ n₁✝) ((fun x1 x2 ↦ x1 * x2) m✝ n₂✝)
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → m✝ * n₁✝ ≤ m✝ * n₂✝

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → m✝ * n₁✝ ≤ m✝ * n₂✝
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝)

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) n₁✝ n₂✝ →
    (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝) (swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝)
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝ ≤ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_2
x y z : α
s : Set α
f : ι → α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
m✝ n₁✝ n₂✝ : α
⊢ n₁✝ ≤ n₂✝ → swap (fun x1 x2 ↦ x1 * x2) m✝ n₁✝ ≤ swap (fun x1 x2 ↦ x1 * x2) m✝ n₂✝
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: case mk
R : Type u_1
inst✝ : Ring R
q : RingCone R
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝ : Ring R
q : RingCone R
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ } = q
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
Module: Mathlib.Algebra.Order.Ring.Cone

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝ : Ring R
toSubsemiring✝¹ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝¹ : ∀ {a : R}, a ∈ toSubsemiring✝¹.carrier → -a ∈ toSubsemiring✝¹.carrier → a = 0
toSubsemiring✝ : Subsemiring R
eq_zero_of_mem_of_neg_mem'✝ : ∀ {a : R}, a ∈ toSubsemiring✝.carrier → -a ∈ toSubsemiring✝.carrier → a = 0
h :
  (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝¹, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubsemiring := toSubsemiring✝, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
;

Goal state after:
case pos
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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

Tactic:
;

Goal state after:
case pos
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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop

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
⊢ x.orderTop +ᵥ ((of R).symm y).orderTop ≤ ((of R).symm (x • y)).orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
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
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

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
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
;

Goal state after:
case pos
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
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

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
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
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 (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

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 (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
;

Goal state after:
case pos
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 (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

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 (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
by_cases! hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty

Goal state after:
case pos
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : f.support.erase (f.support.min' hsupport) = ∅
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: case mk
R : Type u_1
inst✝ : CommRing R
q : RingPreordering R
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } =
    (fun P ↦ (↑P).carrier) q
⊢ { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } = q

Tactic:
;

Goal state after:
case mk
R : Type u_1
inst✝ : CommRing R
q : RingPreordering R
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } =
    (fun P ↦ (↑P).carrier) q
⊢ { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ } = q
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹, neg_one_notMem' := neg_one_notMem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹, neg_one_notMem' := neg_one_notMem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
inst✝ : CommRing R
toSubsemiring✝¹ : Subsemiring R
mem_of_isSquare'✝¹ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝¹.carrier
neg_one_notMem'✝¹ : -1 ∉ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring R
mem_of_isSquare'✝ : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring✝.carrier
neg_one_notMem'✝ : -1 ∉ toSubsemiring✝.carrier
h :
  (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝¹, mem_of_isSquare' := mem_of_isSquare'✝¹,
        neg_one_notMem' := neg_one_notMem'✝¹ } =
    (fun P ↦ (↑P).carrier)
      { toSubsemiring := toSubsemiring✝, mem_of_isSquare' := mem_of_isSquare'✝, neg_one_notMem' := neg_one_notMem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
A B : RingPreordering R
h : ↑A = ↑B
x✝ : R
⊢ x✝ ∈ (↑A).carrier ↔ x✝ ∈ (↑B).carrier

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
A B : RingPreordering R
h : ↑A = ↑B
x✝ : R
⊢ x✝ ∈ (↑A).carrier ↔ x✝ ∈ (↑B).carrier