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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ ∏ x ∈ Ico a b, f x = ∏ x ∈ Ico a b, f x

Tactic:
]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j ↦ ⊥) = ⊥

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j ↦ ⊥) = ⊥
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (fun h ↦ c + h) (Icc a b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
⊢ IsGLB (Set.Ioc i j) i
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = f b * ∏ x ∈ Ioo a b, f x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (fun h ↦ c + h) (Ico a b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h : IsGLB (Set.Ioi i) i
⊢ IsGLB (Set.Ioc i j) i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (f i \ (Iio i).sup f)

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
⊢ p (f i \ (Iio i).sup f)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (fun h ↦ c + h) (Ioc a b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ ∏ x ∈ Ioc a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (fun h ↦ c + h) (Ioo a b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
hi_mem : i < i ∧ i ≤ j
⊢ False
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Icc a b) = image (fun h ↦ h + c) (Icc a b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = image (fun h ↦ h + c) (Ico a b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : (∀ x ∈ Set.Ioi i, succFn i ≤ x) ∧ succFn i ∈ upperBounds (lowerBounds (Set.Ioi i))
⊢ succFn i ≤ j
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioc a b) = image (fun h ↦ h + c) (Ioc a b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = ∏ x ∈ Ico a b, f x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioo a b) = image (fun h ↦ h + c) (Ioo a b)

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p ((f i \ s✝.sup f) \ f a✝)

Tactic:
]

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p ((f i \ s✝.sup f) \ f a✝)
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x > a, f x = f a * ∏ x > a, f x

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
j i k : ι
hk_lb : ∀ x ∈ Set.Ioi i, k ≤ x
hk : j < k
⊢ j ≤ i
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ ∏ x ≥ a, f x = ∏ x ≥ a, f x

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ f a * ∏ x < a, f x = f a * ∏ x < a, f x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ ∏ x ≤ a, f x = ∏ x ≤ a, f x

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j

Tactic:
]

Goal state after:
case succ
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
n : ℕ
hn : succ^[n] i < j
⊢ succ (succ^[n] i) ≤ j
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
a b : α
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
hab : a ≤ b
f : α → M
⊢ f b * ∏ x ∈ Ico a b, f x = f b * ∏ x ∈ Ico a b, f x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst

Tactic:
]

Goal state after:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x ∈ univ.sigma Ioi, f x.fst x.snd = ∏ x ∈ univ.sigma Iio, f x.snd x.fst
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x ↦ disjointed f x) = (partialSups f) a

Tactic:
]

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ disjointed f i ⊔ (Iio i).sup ⇑(partialSups f) = (partialSups f) i

case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x ↦ disjointed f x) = (partialSups f) a
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ ↑(Nat.find ⋯) = 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ ↑(Nat.find ⋯) = 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ ≤ 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ Nat.find ⋯ ≤ 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ i0 = i0

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find ⋯] i0 = i

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find ⋯] i0 = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ -↑(Nat.find ⋯) ≤ 0

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ -↑(Nat.find ⋯) ≤ 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[(-0).toNat] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : pred^[(-0).toNat] i0 < i0
h : toZ i0 i = 0
h_eq : pred^[(-toZ i0 i).toNat] i0 = i
⊢ False
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n k : ℕ
⊢ s k = s k

Tactic:
]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0

Tactic:
by_contra h
    have h_eq := iterate_pred_toZ i hi
    rw [← h_eq, h] at hi
    simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ ↑(Nat.find ⋯) ≤ ↑n

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ ↑(Nat.find ⋯) ≤ ↑n
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)

Tactic:
]

Goal state after:
case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iio i)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ 0

Tactic:
]

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : i0 ≤ pred^[n] i0
h_eq : pred^[n] i0 = i0
⊢ -↑n ≤ 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ -↑(Nat.find ⋯)

Tactic:
]

Goal state after:
case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ -↑(Nat.find ⋯)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m

Tactic:
]

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)

Tactic:
]

Goal state after:
α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ ↑(Nat.find ⋯) = ↑(Nat.find ⋯)

pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find ⋯)

Tactic:
]

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case a
α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (x✝ + c) = f (x✝ + c)

Tactic:
]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ univ.sup ?m.83 = univ.sup fun x ↦ (Iic x).sup f

pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
⊢ ι → α

pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = ?m.83 i

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup (disjointed f) = (Iic i).sup f
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (Iic i).sup' ⋯ (disjointed f) = (Iic i).sup' ⋯ f

Tactic:
← partialSups_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (partialSups (disjointed f)) i = (Iic i).sup' ⋯ f
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ (∏ x ∈ Ico a b, f x) * f b = (∏ k ∈ Ico a b, f k) * f b

Tactic:
]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (partialSups (disjointed f)) i = (Iic i).sup' ⋯ f

Tactic:
← partialSups_apply,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : Fintype ι
f : ι → α
hun : univ.biUnion Iic = univ
i : ι
x✝ : i ∈ univ
⊢ (partialSups (disjointed f)) i = (partialSups f) i