mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
x✝ : Set (Interval α)
⊢ IsLUB x✝
    (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ })

Tactic:
constructor

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

case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ∈
    lowerBounds (upperBounds x✝)
Module: Mathlib.Order.Interval.Basic

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

Tactic:
constructor

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

case neg.coe.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
h : ¬x✝ ⊆ {⊥}
a✝ : NonemptyInterval α
ha : ↑a✝ ∈ x✝
⊢ a✝.toProd.2 ≤
    { fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }.toProd.2
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 α)
⊢ IsGLB s₁
    (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥)

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ∈
    lowerBounds s₁

case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ∈
    upperBounds (lowerBounds s₁)
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt ↔ a = hs.min hns ∧ b = ht.min hnt

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt → a = hs.min hns ∧ b = ht.min hnt

case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
⊢ map 0 f = 0

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero S
f : ZeroHom R S
x✝ : Γ
⊢ (map 0 f).coeff x✝ = coeff 0 x✝
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
⊢ ↑↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2, fst_le_snd := ⋯ } = ⋂ s ∈ S, ↑s

Tactic:
ext

Goal state after:
case pos
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2
x✝ : α
⊢ x✝ ∈ ↑↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2, fst_le_snd := ⋯ } ↔
    x✝ ∈ ⋂ s ∈ S, ↑s
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 Γ'
⊢ embDomain f 0 = 0

Tactic:
ext

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x✝ : Γ'
⊢ (embDomain f 0).coeff x✝ = coeff 0 x✝
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 Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
x✝ : R
⊢ x✝ • 0 = 0

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
x✝¹ : R
x✝ : Γ
⊢ (x✝¹ • 0).coeff x✝ = coeff 0 x✝
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
⊢ (truncLT c) (r • x) = r • (truncLT c) x

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
x✝ : Γ
⊢ ((truncLT c) (r • x)).coeff x✝ = (r • (truncLT c) x).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x + y).map f = x.map f + y.map f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
x✝ : Γ
⊢ ((x + y).map f).coeff x✝ = (x.map f + y.map f).coeff x✝
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✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (Function.support fun a ↦ AddOpposite.unop (x.coeff a)) = x.support

Tactic:
ext

Goal state after:
Γ : 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✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
x✝ : Γ
⊢ (x✝ ∈ Function.support fun a ↦ AddOpposite.unop (x.coeff a)) ↔ x✝ ∈ x.support
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✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (Function.support fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) = (AddOpposite.unop x).support

Tactic:
ext

Goal state after:
Γ : 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✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
x✝ : Γ
⊢ (x✝ ∈ Function.support fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) ↔ x✝ ∈ (AddOpposite.unop x).support
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✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
⊢ AddOpposite.unop (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ }) =
    AddOpposite.unop
      (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
        AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ })

Tactic:
ext

Goal state after:
Γ : 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✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
x✝ : Γ
⊢ (AddOpposite.unop (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ })).coeff
      x✝ =
    (AddOpposite.unop
          (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
            AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ })).coeff
      x✝
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]
  simp

Goal state after:
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)).support = x.support

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
x✝ : Γ
⊢ x✝ ∈ (AddOpposite.unop (addOppositeEquiv x)).support ↔ x✝ ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
⊢ { coeff := fun i ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ } = 0

Tactic:
ext

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c x✝ : Γ
⊢ { coeff := fun i ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ }.coeff x✝ = coeff 0 x✝
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✝ : AddCommMonoid R
x y : R⟦Γ⟧
⊢ x + y = y + x

Tactic:
ext

Goal state after:
Γ : 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✝ : AddCommMonoid R
x y : R⟦Γ⟧
x✝ : Γ
⊢ (x + y).coeff x✝ = (y + x).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : R⟦Γ⟧
⊢ (-x).support = x.support

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : R⟦Γ⟧
x✝ : Γ
⊢ x✝ ∈ (-x).support ↔ x✝ ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : R⟦Γ⟧
⊢ (-x).map f = -x.map f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : R⟦Γ⟧
x✝ : Γ
⊢ ((-x).map f).coeff x✝ = (-x.map f).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x - y).map f = x.map f - y.map f

Tactic:
ext

Goal state after:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
x✝ : Γ
⊢ ((x - y).map f).coeff x✝ = (x.map f - y.map f).coeff x✝
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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝² x✝¹ : R
x✝ : V⟦Γ⟧
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝³ x✝² : R
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ ((x✝³ * x✝²) • x✝¹).coeff x✝ = (x✝³ • x✝² • x✝¹).coeff x✝
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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝ : V⟦Γ⟧
⊢ 1 • x✝ = x✝

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ (1 • x✝¹).coeff x✝ = x✝¹.coeff x✝
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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝ : R
⊢ x✝ • 0 = 0

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝¹ : R
x✝ : Γ
⊢ (x✝¹ • 0).coeff x✝ = coeff 0 x✝
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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝² : R
x✝¹ x✝ : V⟦Γ⟧
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝³ : R
x✝² x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ (x✝³ • (x✝² + x✝¹)).coeff x✝ = (x✝³ • x✝² + x✝³ • x✝¹).coeff x✝
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 Γ
V : Type u_8
inst✝⁶ : Monoid R
inst✝⁵ : AddMonoid V
inst✝⁴ : DistribMulAction R V
S : Type u_9
inst✝³ : Monoid S
inst✝² : DistribMulAction S V
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
⊢ (r • s) • a = r • s • a

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝⁶ : Monoid R
inst✝⁵ : AddMonoid V
inst✝⁴ : DistribMulAction R V
S : Type u_9
inst✝³ : Monoid S
inst✝² : DistribMulAction S V
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
x✝ : Γ
⊢ ((r • s) • a).coeff x✝ = (r • s • a).coeff x✝
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 Γ
V : Type u_8
inst✝⁵ : Monoid R
inst✝⁴ : AddMonoid V
inst✝³ : DistribMulAction R V
S : Type u_9
inst✝² : Monoid S
inst✝¹ : DistribMulAction S V
inst✝ : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
⊢ r • s • a = s • r • a

Tactic:
ext

Goal state after:
Γ : 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 Γ
V : Type u_8
inst✝⁵ : Monoid R
inst✝⁴ : AddMonoid V
inst✝³ : DistribMulAction R V
S : Type u_9
inst✝² : Monoid S
inst✝¹ : DistribMulAction S V
inst✝ : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
x✝ : Γ
⊢ (r • s • a).coeff x✝ = (s • r • a).coeff x✝
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:
ext

Goal state after:
Γ : 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✝¹).coeff x✝ = (x✝³ • x✝¹ + x✝² • x✝¹).coeff x✝
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✝ : V⟦Γ⟧
⊢ 0 • x✝ = 0

Tactic:
ext

Goal state after:
Γ : 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✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ (0 • x✝¹).coeff x✝ = coeff 0 x✝
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⟦Γ⟧
⊢ (r • x).map f = r • x.map f

Tactic:
ext

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.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✝ : Γ →₀ V
⊢ ofFinsupp (x✝¹ + x✝) = ofFinsupp x✝¹ + ofFinsupp x✝

Tactic:
ext

Goal state after:
Γ : 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✝¹ : Γ →₀ V
x✝ : Γ
⊢ (ofFinsupp (x✝² + x✝¹)).coeff x✝ = (ofFinsupp x✝² + ofFinsupp x✝¹).coeff x✝
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✝¹ : R
x✝ : Γ →₀ V
⊢ ofFinsupp (x✝¹ • x✝) = (RingHom.id R) x✝¹ • ofFinsupp x✝

Tactic:
ext

Goal state after:
Γ : 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✝² : R
x✝¹ : Γ →₀ V
x✝ : Γ
⊢ (ofFinsupp (x✝² • x✝¹)).coeff x✝ = ((RingHom.id R) x✝² • ofFinsupp x✝¹).coeff x✝
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff ↔
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i

Tactic:
constructor

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 < (ofLex x).leadingCoeff →
    ∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i

case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ (∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i) →
    0 < (ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 ≤ (ofLex x).leadingCoeff ↔ 0 ≤ x

Tactic:
constructor

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 ≤ (ofLex x).leadingCoeff → 0 ≤ x

case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ 0 ≤ x → 0 ≤ (ofLex x).leadingCoeff
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 x : M
⊢ a * c ≤ x ∧ x < b * c ↔ ∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ a * c ≤ x ∧ x < b * c → ∃ a_2, (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x

case mpr
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c
Module: Mathlib.RingTheory.HahnSeries.Lex

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

Tactic:
constructor

Goal state after:
case inr.mp
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |y| ≤ n • |x|) → ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

case inr.mpr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
⊢ (∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|
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
x : G
⊢ 0 ≤ x ∧ x < ↑b ↔ x = 0

Tactic:
constructor

Goal state after:
case h.mp
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
⊢ 0 ≤ x ∧ x < ↑b → x = 0

case h.mpr
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 = 0 → 0 ≤ x ∧ x < ↑b