awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := Set α) (range fun (h : p) ↦ f h) ∅
have e_a : IsEmpty p
Tactic: rwa [range_eq_empty_iff, isEmpty_Prop]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
inst_1 : Decidable p
f : p → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
have pos : ∀ (H : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
Tactic: by_cases H : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompletePartialOrderSup α
p : Prop
inst_1 : Decidable p
f : p → α
pos : ∀ (H : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
have neg : ∀ (H : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), f h) (if h : p then f h else sSup ∅)
Tactic: by_cases H : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have simp : ⨆ (i : ι), f (Subtype.mk (p := p) i sorry) = iSup.{u_1, max 1 u_4} f
Tactic: simp only [hp, ciSup_unique]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ (i : ι), f (Subtype.mk (p := p) i ⋯) = iSup.{u_1, max 1 u_4} f
have simp : sSup (range fun (i : ι) ↦ f (Subtype.mk (p := p) i sorry)) = sSup (range.{u_1, max 1 u_4} f)
Tactic: simp only [iSup]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ sSup (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = sSup (range.{u_1, max 1 u_4} f)
have e_a : (range fun (i : ι) ↦ f (Subtype.mk (p := p) i sorry)) = range.{u_1, max 1 u_4} f
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = range.{u_1, max 1 u_4} f
have e_a : (range fun (i : ι) ↦ f (Subtype.mk (p := p) i sorry)) ⊆ range.{u_1, max 1 u_4} f
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
e_a : (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) ⊆ range.{u_1, max 1 u_4} f
⊢ (range fun (i : ι) ↦ f (Subtype.mk (p := p) i ⋯)) = range.{u_1, max 1 u_4} f
have e_a₁ : range.{u_1, max 1 u_4} f ⊆ range fun (i : ι) ↦ f (Subtype.mk (p := p) i sorry)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
have inl : IsEmpty ι → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
inl : IsEmpty ι → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
have inr : Nonempty ι → Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h : IsEmpty ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
have inl : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [iSup_of_empty']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : (i : ι) → p i → α
hp : ∀ (i : ι), ¬p i
h : Nonempty ι
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f i h) (sSup ∅)
have this : ∀ (i : ι), IsEmpty (p i)
Tactic: have (i : ι) : IsEmpty (p i) := ⟨hp i⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ Membership.mem (γ := Set α) (⋂ (n : β), Icc (f n) (g n)) (⨆ (n : β), f n)
have refine : ∀ (n : β), ⨆ (n : β), f n ∈ Icc (f n) (g n)
Tactic: refine mem_iInter.2 fun n => ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ ⨆ (n : β), f n ∈ Icc (f n) (g n)
have this : Nonempty β
Tactic: haveI : Nonempty β := ⟨n⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ ⨆ (n : β), f n ∈ Icc (f n) (g n)
have h₁ : ∀ (m : β), f m ≤ g n
Tactic: have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
inst_2 : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
h₁ : ∀ (m : β), f m ≤ g n
⊢ ⨆ (n : β), f n ∈ Icc (f n) (g n)
have h₂ : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
Tactic: have h₂ : Directed (· ≤ ·) f := hf.directed_le
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ Eq.{u_1 + 1} (α := Set α) (Ici (⨆ (i : ι), f i)) (⋂ (i : ι), Ici (f i))
have h : ∀ (x : α), Membership.mem (γ := Set α) (Ici (⨆ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Ici (f i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
⊢ ⨆ (x : (↑(Iic a) : Type u_2)), f (↑x : β) = f a
have hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
Tactic: have hd : Directed (· ≤ ·) (fun x : Iic a ↦ f x) := fun x y ↦ ⟨⟨a, le_refl a⟩, ⟨hf x.2, hf y.2⟩⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
⊢ ⨆ (x : (↑(Iic a) : Type u_2)), f (↑x : β) = f a
have H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))
Tactic: have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))
⊢ ⨆ (x : (↑(Iic a) : Type u_2)), f (↑x : β) = f a
have apply : ⨆ (j : (↑(Iic a) : Type u_2)), f (↑j : β) ≤
  f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a sorry : { x : β // x ∈ Iic a }) : β)
Tactic: apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))
⊢ ⨆ (j : (↑(Iic a) : Type u_2)), f (↑j : β) ≤
    f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a ⋯ : { x : β // x ∈ Iic a }) : β)
have rw : ∀ (i : (↑(Iic a) : Type u_2)),
  f (↑i : β) ≤ f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a sorry : { x : β // x ∈ Iic a }) : β)
Tactic: rw [hd.ciSup_le_iff H]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
Tactic: rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
Tactic: rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)
have rw₂ : Eq.{u_2 + 1} (α := β) (⨆ (i : ι), l (f i)) (⨆ (i : ι), l (f i))
Tactic: rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))
have this : Nonempty.{u_3 + 1} (↑s : Type u_3)
Tactic: haveI := hne.to_subtype
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))
have hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
Tactic: rw [image_eq_range] at hf
Cleared hypotheses: hf, hne, this
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompletePartialOrder.Indexed (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))
have refine : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (i : (↑s : Type u_3)) ↦ f (↑i : γ)
Tactic: refine gc.l_ciSup_of_directed ?_ hf
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hab : le a b
hbc : le b c_1
⊢ le a c_1
have rw : ∀ (hab : a ≤ b) (hbc : b ≤ c_1), a ≤ c_1
Tactic: rw [eq_le] at hab hbc ⊢
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Order.Copy (hypothesis)
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : le a b
hba : le b a
⊢ a = b
have hab₁ : a ≤ b
Tactic: simp_rw [eq_le] at hab hba
Cleared hypotheses: hab, hba
-- Lean 4 proof step from Mathlib.Order.Copy (hypothesis)
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : le a b
hba : le b a
hab₁ : a ≤ b
⊢ a = b
have hba₁ : b ≤ a
Tactic: simp_rw [eq_le] at hab hba
Cleared hypotheses: hab, hba
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : le a c_1
hbc : le b c_1
⊢ le (sup a b) c_1
have simp_rw : ∀ (hac : a ≤ c_1) (hbc : b ≤ c_1), sup a b ≤ c_1
Tactic: simp_rw [eq_le] at hac hbc ⊢
Cleared hypotheses: hac, hbc
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : le a b
hbc : le a c_1
⊢ le a (inf b c_1)
have simp_rw : ∀ (hac : a ≤ b) (hbc : a ≤ c_1), a ≤ inf b c_1
Tactic: simp_rw [eq_le] at hac hbc ⊢
Cleared hypotheses: hac, hbc
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y
have rw : ∀ (x y : α), x ≤ y ↔ le x y
Tactic: rw [← eq_le]
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y
have rw : ∀ (x y : α), x ≤ y ↔ le x y
Tactic: rw [← eq_le]
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y
have rw : ∀ (x y : α), x ≤ y ↔ le x y
Tactic: rw [← eq_le]
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ x ≤ y
have rw : ∀ (x y : α), x ≤ y ↔ le x y
Tactic: rw [← eq_le]
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)
have subst_vars : ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (SupSet.sSup s)
Tactic: subst_vars
Cleared hypotheses: le, eq_le, sup, eq_sup, inf, eq_inf, sSup, eq_sSup, sInf, eq_sInf
-- Lean 4 proof step from Mathlib.Order.Copy (goal)
Goal:
α : Type u
c : ConditionallyCompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
⊢ ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)
have subst_vars : ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (InfSet.sInf s)
Tactic: subst_vars
Cleared hypotheses: le, eq_le, sup, eq_sup, inf, eq_inf, sSup, eq_sSup, sInf, eq_sInf
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
⊢ x < y
have hx₁ : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 sorry) = x
Tactic: simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
      exists_and_left, Slt, Sgt] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
hx₁ : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = x
⊢ x < y
have hy₁ : ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 sorry) = y
Tactic: simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
      exists_and_left, Slt, Sgt] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
x y : β
hx : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = x
hy : ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = y
⊢ x < y
have obtain : ∀ (w : α) (hx : w < a) (w_1 : w ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w sorry) < y
Tactic: obtain ⟨_, hx, _, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
y : β
hy : ∃ (a_1 : α), a < a_1 ∧ ∃ (x : a_1 ∈ S), (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) a_1 ⋯) = y
w : α
hx : w < a
w_1 : w ∈ S
⊢ (f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w ⋯) < y
have obtain : ∀ (w_2 : α) (hy : a < w_2) (w_3 : w_2 ∈ S),
  LT.lt.{u_2} (α := β) ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w sorry) : β)
    ((f : (a : ↥S) → β) (Subtype.mk (p := fun (a : α) ↦ a ∈ S) w_2 sorry) : β)
Tactic: obtain ⟨_, hy, _, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)
have obtain : ∀ (b : β) (hb : ∀ x ∈ Slt, x < b) (hb' : ∀ y ∈ Sgt, b < y),
  ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) sorry))
      (⇑f : (a : ↥S) → β)
Tactic: obtain ⟨b, hb, hb'⟩ := Order.exists_between_finsets Slt Sgt (fun x hx y hy => by
    simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
      exists_and_left, Slt, Sgt] at hx hy
    obtain ⟨_, hx, _, rfl⟩ := hx
    obtain ⟨_, hy, _, rfl⟩ := hy
    exact f.strictMono (hx.trans hy))
-- Lean 4 proof step from Mathlib.Order.CountableDenseLinearOrder (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : DenselyOrdered β
inst_3 : NoMinOrder β
inst_4 : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : OrderEmbedding.{u_1, u_2} (↥S) β
a : α
Slt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | (↑x : α) < a})
Sgt : Finset β := Finset.image (⇑f : (a : ↥S) → β) ({x ∈ S.attach | a < (↑x : α)})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ ∃ (g : OrderEmbedding.{u_1, u_2} (↥(insert a S)) β),
    Eq (α := (↑(↑S : Set α) : Type u_1) → β)
      (Function.comp (β := ↥(insert a S)) (⇑g : (a : ↥(insert a S)) → β)
        (Set.inclusion (s := (↑S : Set α)) (t := (↑(insert a S) : Set α)) ⋯))
      (⇑f : (a : ↥S) → β)
have refine_1 : StrictMono.{u_1, u_2} (β := β) fun (x : ↥(insert a S)) ↦
  if hx : (↑x : α) ∈ S then (f : (a : ↥S) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ S) (↑x : α) hx) else b
Tactic: refine ⟨OrderEmbedding.ofStrictMono
    (fun (x : (insert a S : Finset α)) => if hx : x.1 ∈ S then f ⟨x.1, hx⟩ else b) ?_, ?_⟩