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

Goal state before:
pp: case mk
G : Type u_1
inst✝ : CommGroup G
q : GroupCone G
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
G : Type u_1
inst✝ : CommGroup G
q : GroupCone G
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } =
    (fun C ↦ C.carrier) q
⊢ { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ } = q
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
Module: Mathlib.Algebra.Order.Group.Cone

Goal state before:
pp: case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝

Tactic:
;

Goal state after:
case mk.mk
G : Type u_1
inst✝ : CommGroup G
toSubmonoid✝¹ : Submonoid G
eq_one_of_mem_of_inv_mem'✝¹ : ∀ {a : G}, a ∈ toSubmonoid✝¹.carrier → a⁻¹ ∈ toSubmonoid✝¹.carrier → a = 1
toSubmonoid✝ : Submonoid G
eq_one_of_mem_of_inv_mem'✝ : ∀ {a : G}, a ∈ toSubmonoid✝.carrier → a⁻¹ ∈ toSubmonoid✝.carrier → a = 1
h :
  (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝¹, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝¹ } =
    (fun C ↦ C.carrier) { toSubmonoid := toSubmonoid✝, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'✝ }
⊢ toSubmonoid✝¹ = toSubmonoid✝
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ ∃ g, Subgroup.zpowers g = Subgroup.zpowers g2

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
⊢ ∃ g, Subgroup.zpowers g = Subgroup.zpowers g2
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ Nontrivial ↥(Subgroup.zpowers g2)

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
⊢ Nontrivial ↥(Subgroup.zpowers g2)
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
h2 : Nontrivial ↥(Subgroup.zpowers g1)
⊢ IsCyclic ↥(Subgroup.zpowers g2)

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
h2 : Nontrivial ↥(Subgroup.zpowers g1)
⊢ IsCyclic ↥(Subgroup.zpowers g2)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
x : ℤ
mx : (c - ↑(#s) < x ∧ x ≤ c) ∧ x ∉ s
⊢ c - ↑(#s) ≤ x

Tactic:
;

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
x : ℤ
mx : (c - ↑(#s) < x ∧ x ≤ c) ∧ x ∉ s
⊢ c - ↑(#s) ≤ x
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
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
exists s.sup g

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
⊢ ∀ (m : ℕ), s.sup g ≤ m → f (s.sup g) = f m
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑x ∈ Ioc (c - ↑(#s)) c
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x < #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x < #s
⊢ c - ↑(#s) < c - ↑x ∧ c - ↑x ≤ c
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
my : y ∈ ↑(range #s)
h : c - ↑x = c - ↑y
⊢ x = y

Tactic:
;

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
my : y ∈ ↑(range #s)
h : c - ↑x = c - ↑y
⊢ x = y
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)

Tactic:
;

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case h
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - ↑(#s) < x ∧ x ≤ c
⊢ (c - x).toNat < #s ∧ c - ↑(c - x).toNat = x

Tactic:
;

Goal state after:
case h
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - ↑(#s) < x ∧ x ≤ c
⊢ (c - x).toNat < #s ∧ c - ↑(c - x).toNat = x
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : (c ≤ x ∧ x < c + ↑(#s)) ∧ x ∉ s
⊢ x ≤ c + ↑(#s)

Tactic:
;

Goal state after:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + ↑(#s))
x : ℤ
mx : (c ≤ x ∧ x < c + ↑(#s)) ∧ x ∉ s
⊢ x ≤ c + ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c + ↑x ∈ Ico c (c + ↑(#s))

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c + ↑x ∈ Ico c (c + ↑(#s))
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x < #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)

Tactic:
;

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x < #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
my : y ∈ ↑(range #s)
h : c + ↑x = c + ↑y
⊢ x = y

Tactic:
;

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ ↑(range #s)
y : ℕ
my : y ∈ ↑(range #s)
h : c + ↑x = c + ↑y
⊢ x = y
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)

Tactic:
;

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case h
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + ↑(#s)
⊢ (x - c).toNat < #s ∧ c + ↑(x - c).toNat = x

Tactic:
;

Goal state after:
case h
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + ↑(#s)
⊢ (x - c).toNat < #s ∧ c + ↑(x - c).toNat = x
Module: Mathlib.Algebra.Order.GroupWithZero.Bounds

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
a : α
⊢ f a ∈ {x | 0 ≤ x}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty α
inst✝² : Preorder β
inst✝¹ : Zero β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hf0 : 0 ≤ f
hg : MonotoneOn g {x | 0 ≤ x}
a : α
⊢ f a ∈ {x | 0 ≤ x}
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case mk
α : Type u_1
inst✝ : LE α
t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝ : LE α
t : NonemptyInterval α
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd = t.toProd
⊢ { toProd := toProd✝, fst_le_snd := fst_le_snd✝ } = t
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝ : LE α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.1 ≤ toProd✝¹.2
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
inst✝ : LE α
toProd✝¹ : α × α
fst_le_snd✝¹ : toProd✝¹.1 ≤ toProd✝¹.2
toProd✝ : α × α
fst_le_snd✝ : toProd✝.1 ≤ toProd✝.2
h : { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ }.toProd = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }.toProd
⊢ { toProd := toProd✝¹, fst_le_snd := fst_le_snd✝¹ } = { toProd := toProd✝, fst_le_snd := fst_le_snd✝ }
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ (- -s).toProd = s.toProd

Tactic:
;

Goal state after:
ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s✝ t : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s : NonemptyInterval α
⊢ (- -s).toProd = s.toProd
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd
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
x✝ : Γ
⊢ (map 0 f).coeff x✝ = coeff 0 x✝

Tactic:
;

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.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⟦Γ⟧
x✝ : Γ
⊢ ((truncLT c) (r • x)).coeff x✝ = (r • (truncLT c) x).coeff x✝

Tactic:
;

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
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
a : Γ
r s : R
⊢ ((single a) (r + s)).coeff = ((single a) r + (single a) s).coeff

Tactic:
;

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
a : Γ
r s : R
⊢ ((single a) (r + s)).coeff = ((single a) r + (single a) s).coeff
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✝ : Γ
⊢ ((x + y).map f).coeff x✝ = (x.map f + y.map f).coeff x✝

Tactic:
;

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:
;

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

Tactic:
;

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:
;

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

Tactic:
;

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
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : AddOpposite.unop (addOppositeEquiv x) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Tactic:
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : (fun a ↦ AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
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 x✝ : Γ
⊢ { coeff := fun i ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ }.coeff x✝ = coeff 0 x✝

Tactic:
;

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: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
;

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
;

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
;

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order

pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
;

Goal state after:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order

case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.order y.order ≤ (x + y).order
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.order y.order ≤ (x + y).order

pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
;

Goal state after:
case pos
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min x.order y.order ≤ (x + y).order

case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.order y.order ≤ (x + y).order
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✝ : Γ
⊢ ((-x).map f).coeff x✝ = (-x.map f).coeff x✝

Tactic:
;

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✝ : Γ
⊢ ((x - y).map f).coeff x✝ = (x.map f - y.map f).coeff x✝

Tactic:
;

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: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < (-y).orderTop
⊢ (x + -y).leadingCoeff = x.leadingCoeff

Tactic:
exact leadingCoeff_add_eq_left hxy

Goal state after: