mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ⨆ c, f (b, c) ≤ c

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ⨆ c, f (b, c) ≤ c
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a✝ : WithTop (WithBot α)
⊢ (f.comp g).withTopWithBot a✝ = (f.withTopWithBot.comp g.withTopWithBot) a✝
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝ : WithTop α
⊢ x✝ ∈ range some ↔ x✝ ∈ Iio ⊤

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
x✝ : WithTop α
⊢ x✝ ∈ range some ↔ x✝ ∈ Iio ⊤
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ioi ↑a ↔ x ∈ some '' Ioi a ∪ {⊤}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ioi ↑a ↔ x ∈ some '' Ioi a ∪ {⊤}
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ici ↑a ↔ x ∈ some '' Ici a ∪ {⊤}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
x : WithTop α
⊢ x ∈ Ici ↑a ↔ x ∈ some '' Ici a ∪ {⊤}
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : ↑(Finset.cons b t hbt) ⊆ ⋃ i, f i
⊢ ∃ i, ↑(Finset.cons b t hbt) ⊆ f i

Tactic:
simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢

Goal state after:
case cons
α : Type u_1
ι : Type u_2
inst✝ : Nonempty ι
f : ι → Set α
h : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
b : α
t : Finset α
hbt : b ∉ t
iht : ↑t ⊆ ⋃ i, f i → ∃ i, ↑t ⊆ f i
hs : (∃ i, b ∈ f i) ∧ ↑t ⊆ ⋃ i, f i
⊢ ∃ i, b ∈ f i ∧ ↑t ⊆ f i
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down

Tactic:
;

Goal state after:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down
Module: Mathlib.Order.Cover

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

pp: case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b

case inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b
Module: Mathlib.Order.Cover

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

pp: case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b

case inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
Module: Mathlib.Order.Cover

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioi a = {⊤}

Tactic:
;

Goal state after:
case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioi a = {⊤}
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a ≤ b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a ≤ b

Tactic:
;

Goal state after:
⊢ ∀ {a b : Bool}, (a ≤ b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a ≤ b
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, (a < b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a < b

Tactic:
;

Goal state after:
⊢ ∀ {a b : Bool}, (a < b ∧ ∀ ⦃c : Bool⦄, a < c → ¬c < b) ↔ a < b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s ⋖ insert a s
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t

Tactic:
;

Goal state after:
α : Type u_1
t : Set α
a : α
ha : a ∈ t
⊢ t \ {a} ⋖ t
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
x y : α
⊢ x ⩿ y ↔ ReflGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
    · exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩
  · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_wcovBy_mk_iff_left.2 h
    · exact mk_wcovBy_mk_iff_right.2 h

Goal state after:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft

Tactic:
;

Goal state after:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : α
⊢ x ∈ s.preimage Sum.inl ⋯ ↔ x ∈ s.toLeft
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight

Tactic:
;

Goal state after:
α : Type u
β : Type v
s : Finset (α ⊕ β)
x : β
⊢ x ∈ s.preimage Sum.inr ⋯ ↔ x ∈ s.toRight
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s).Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ ↑s) f i

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s).Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ ↑s) f i
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ ↑s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ ↑s) b

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ ↑s
⊢ ∃ b, a ≤ b ∧ Maximal (fun x ↦ x ∈ ↑s) b
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
P : ι → Prop
f : ι → α
hP : ∃ i, P i
⊢ ∃ i, MinimalFor P f i

Tactic:
by
  simpa [not_lt_iff_le_imp_ge, InvImage]
    using! (instIsWellFoundedInvImage (· < ·) f).wf.has_min _ hP

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x

Tactic:
;

Goal state after:
α : Type u_2
P : α → Prop
x : α
inst✝ : PartialOrder α
hy : P x
hP : ∀ ⦃x_1 : α⦄, P x_1 → x ≤ x_1
⊢ Minimal P x
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case h
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∅.Subsingleton ∧ IsCofinal ∅

Tactic:
;

Goal state after:
case h
α : Type u_2
inst✝ : LinearOrder α
hs : ∅.Finite
hs' : IsCofinal ∅
⊢ ∅.Subsingleton ∧ IsCofinal ∅
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α ↪o β
⊢ Set.range ⇑f = Set.range ⇑f

Tactic:
;

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α ↪o β
⊢ Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x | Minimal P x} = {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}

case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α →o β
hf hg : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑f

Tactic:
;

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f : α →o β
hf hg : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑f
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b

Tactic:
;

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b + 1 - a) ↔ a ≤ x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b

Tactic:
;

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a ≤ x ∧ x < a + (b - a) ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b

Tactic:
;

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a) ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b

Tactic:
;

Goal state after:
a✝ b✝ c a b x : ℕ
⊢ a + 1 ≤ x ∧ x < a + 1 + (b - a - 1) ↔ a < x ∧ x < b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s

Tactic:
Nat.sInf_def h

Goal state after:
s : Set ℕ
h : s.Nonempty
⊢ Nat.find h ∈ s
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅

Tactic:
;

Goal state after:
case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m ∉ s

Tactic:
Nat.sInf_def h

Goal state after:
case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s

Tactic:
;

Goal state after:
case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ Ici 1 ↔ a✝ ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ Ici 1 ↔ a✝ ∈ univ
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n k l : ℕ
ih : Set.InjOn (fun x ↦ x % 0) ↑(Ico n (n + 0))
hk : k ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hl : l ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hkl : k % 0 = l % 0
⊢ False

Tactic:
;

Goal state after:
n k l : ℕ
ih : Set.InjOn (fun x ↦ x % 0) ↑(Ico n (n + 0))
hk : k ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hl : l ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hkl : k % 0 = l % 0
⊢ False
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)

Tactic:
by
  simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ a (n + 1)

Tactic:
change a n ⋖ if ha : IsMax (a n) then a n else _

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ if ha : IsMax (a n) then a n else next ha
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
k : ℕ
hk : 1 < k
P : M → Prop
hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)
hpow : ∀ (x : M), P (x ^ k) → P x
n : ℕ
ih : ∀ (x : M), P (x ^ (n + 1)) → P x
x : M
hx : P (x ^ n)
h : P (x ^ n * x)
⊢ P (x ^ (n + 1))

Tactic:
rwa [_root_.pow_succ]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioc a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ioc]
  exact Set.Ioo_subset_Ioc_self

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x ↦ f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x ↦ f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
⊢ WellQuasiOrdered s

Tactic:
intro seq
  have ⟨_, _, hle, hr⟩ := h (Function.surjInv hf ∘ seq)
  exact ⟨_, _, hle, by simpa [Function.surjInv_eq] using f.map_rel hr⟩

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j < b} ↔ a✝ ∈ Ioo a b

Tactic:
;

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j < b} ↔ a✝ ∈ Ioo a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j ≤ b} ↔ a✝ ∈ Ioc a b

Tactic:
;

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a < j ∧ j ≤ b} ↔ a✝ ∈ Ioc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j < b} ↔ a✝ ∈ Ico a b

Tactic:
;

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j < b} ↔ a✝ ∈ Ico a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j ≤ b} ↔ a✝ ∈ Icc a b

Tactic:
;

Goal state after:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j ↦ a ≤ j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ {j | a ≤ j ∧ j ≤ b} ↔ a✝ ∈ Icc a b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
;

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
a : α
⊢ a ∈ Ici ⊥ ↔ a ∈ univ

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
a : α
⊢ a ∈ Ici ⊥ ↔ a ∈ univ
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a

Tactic:
;

Goal state after:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iio a = ∅ ↔ IsMin a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
a : α
⊢ a ∈ Iic ⊤ ↔ a ∈ univ

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
a : α
⊢ a ∈ Iic ⊤ ↔ a ∈ univ
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ Set.Iic a

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ Set.Iic a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a < x
a✝ : α
⊢ a✝ ∈ {x | a < x} ↔ a✝ ∈ Ioi a

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a < x
a✝ : α
⊢ a✝ ∈ {x | a < x} ↔ a✝ ∈ Ioi a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a ≤ x
a✝ : α
⊢ a✝ ∈ {x | a ≤ x} ↔ a✝ ∈ Ici a

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ a ≤ x
a✝ : α
⊢ a✝ ∈ {x | a ≤ x} ↔ a✝ ∈ Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x < a
a✝ : α
⊢ a✝ ∈ {x | x < a} ↔ a✝ ∈ Iio a

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x < a
a✝ : α
⊢ a✝ ∈ {x | x < a} ↔ a✝ ∈ Iio a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x ≤ a
a✝ : α
⊢ a✝ ∈ {x | x ≤ a} ↔ a✝ ∈ Iic a

Tactic:
;

Goal state after:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x ↦ x ≤ a
a✝ : α
⊢ a✝ ∈ {x | x ≤ a} ↔ a✝ ∈ Iic a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Icc a b)
a✝ : α
⊢ a✝ ∈ (Icc a b).toFinset ↔ a✝ ∈ Finset.Icc a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ico a b)
a✝ : α
⊢ a✝ ∈ (Ico a b).toFinset ↔ a✝ ∈ Finset.Ico a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : Fintype ↑(Ioo a b)
a✝ : α
⊢ a✝ ∈ (Ioo a b).toFinset ↔ a✝ ∈ Finset.Ioo a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a

Tactic:
;

Goal state after:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ioi a)
a✝ : α
⊢ a✝ ∈ (Ioi a).toFinset ↔ a✝ ∈ Finset.Ioi a