awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sSup {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨆ N ∈ S, (↑N : α))
rw₁ : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨆ N ∈ S, (↑N : α)
⊢ (↑(sSup S) : α) = ⨆ N ∈ S, (↑N : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ S, (↑a : α)) (⨆ N ∈ S, (↑N : α))
Tactic: rw [coe_sSup, ← Set.image, sSup_image]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ (↑(sInf S) : α) = ⨅ N ∈ S, (↑N : α)
have rw : Eq.{u_1 + 1} (α := α) (sInf {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨅ N ∈ S, (↑N : α))
Tactic: rw [coe_sInf, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sInf {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨅ N ∈ S, (↑N : α))
⊢ (↑(sInf S) : α) = ⨅ N ∈ S, (↑N : α)
have rw₁ : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨅ N ∈ S, (↑N : α)
Tactic: rw [coe_sInf, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sInf {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨅ N ∈ S, (↑N : α))
rw₁ : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨅ N ∈ S, (↑N : α)
⊢ (↑(sInf S) : α) = ⨅ N ∈ S, (↑N : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (⨅ a ∈ S, (↑a : α)) (⨅ N ∈ S, (↑N : α))
Tactic: rw [coe_sInf, ← Set.image, sInf_image]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ (↑(iSup f) : α) = ⨆ (i : ι), (↑(f i) : α)
have rw : (↑(sSup (range f)) : α) = ⨆ (i : ι), (↑(f i) : α)
Tactic: rw [iSup, coe_sSup', iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sSup (range f)) : α) = ⨆ (i : ι), (↑(f i) : α)
⊢ (↑(iSup f) : α) = ⨆ (i : ι), (↑(f i) : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ N ∈ range f, (↑N : α)) (⨆ (i : ι), (↑(f i) : α))
Tactic: rw [iSup, coe_sSup', iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sSup (range f)) : α) = ⨆ (i : ι), (↑(f i) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ N ∈ range f, (↑N : α)) (⨆ (i : ι), (↑(f i) : α))
⊢ (↑(iSup f) : α) = ⨆ (i : ι), (↑(f i) : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), (↑(f i) : α)) (⨆ (i : ι), (↑(f i) : α))
Tactic: rw [iSup, coe_sSup', iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ (↑(iInf f) : α) = ⨅ (i : ι), (↑(f i) : α)
have rw : (↑(sInf (range f)) : α) = ⨅ (i : ι), (↑(f i) : α)
Tactic: rw [iInf, coe_sInf', iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sInf (range f)) : α) = ⨅ (i : ι), (↑(f i) : α)
⊢ (↑(iInf f) : α) = ⨅ (i : ι), (↑(f i) : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (⨅ N ∈ range f, (↑N : α)) (⨅ (i : ι), (↑(f i) : α))
Tactic: rw [iInf, coe_sInf', iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
rw : (↑(sInf (range f)) : α) = ⨅ (i : ι), (↑(f i) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (⨅ N ∈ range f, (↑N : α)) (⨅ (i : ι), (↑(f i) : α))
⊢ (↑(iInf f) : α) = ⨅ (i : ι), (↑(f i) : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (⨅ (i : ι), (↑(f i) : α)) (⨅ (i : ι), (↑(f i) : α))
Tactic: rw [iInf, coe_sInf', iInf_range]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
s : Set β
hs : s ⊆ (⇑f : (a : α) → β) '' (↑L : Set α)
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup s)
have obtain : ∀ (t : Set α) (ht : t ⊆ (↑L : Set α))
  (hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))),
  Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup ((⇑f : (a : α) → β) '' t))
Tactic: obtain ⟨t, ht, rfl⟩ := subset_image_iff.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sSup ((⇑f : (a : α) → β) '' t))
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sSup t) : β)
Tactic: rw [← map_sSup]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
s : Set β
hs : s ⊆ (⇑f : (a : α) → β) '' (↑L : Set α)
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf s)
have obtain : ∀ (t : Set α) (ht : t ⊆ (↑L : Set α))
  (hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))),
  Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf ((⇑f : (a : α) → β) '' t))
Tactic: obtain ⟨t, ht, rfl⟩ := subset_image_iff.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L : CompleteSublattice α
t : Set α
ht : t ⊆ (↑L : Set α)
hs : Subset.{u_2} (α := Set β) ((⇑f : (a : α) → β) '' t) ((⇑f : (a : α) → β) '' (↑L : Set α))
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) (sInf ((⇑f : (a : α) → β) '' t))
have rw : Membership.mem.{u_2, u_2} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' (↑L : Set α)) ((f : (a : α) → β) (sInf t) : β)
Tactic: rw [← map_sInf]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
Tactic: rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw₁ : a ⊓ b = ⊥ ↔ (↑a : α) ⊓ (↑b : α) = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
rw₁ : a ⊓ b = ⊥ ↔ (↑a : α) ⊓ (↑b : α) = ⊥
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw₂ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
rw₁ : a ⊓ b = ⊥ ↔ (↑a : α) ⊓ (↑b : α) = ⊥
rw₂ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = ⊥
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw₃ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)
Tactic: rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊓ b = ⊥ ↔ Disjoint (↑a : α) (↑b : α)
rw₁ : a ⊓ b = ⊥ ↔ (↑a : α) ⊓ (↑b : α) = ⊥
rw₂ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = ⊥
rw₃ : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw₄ : a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)
have rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
Tactic: rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)
have rw₁ : a ⊔ b = ⊤ ↔ (↑a : α) ⊔ (↑b : α) = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
rw₁ : a ⊔ b = ⊤ ↔ (↑a : α) ⊔ (↑b : α) = ⊤
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)
have rw₂ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
rw₁ : a ⊔ b = ⊤ ↔ (↑a : α) ⊔ (↑b : α) = ⊤
rw₂ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = ⊤
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)
have rw₃ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = (↑⊤ : α)
Tactic: rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : a ⊔ b = ⊤ ↔ Codisjoint (↑a : α) (↑b : α)
rw₁ : a ⊔ b = ⊤ ↔ (↑a : α) ⊔ (↑b : α) = ⊤
rw₂ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = ⊤
rw₃ : a ⊔ b = ⊤ ↔ (↑(a ⊔ b) : α) = (↑⊤ : α)
⊢ Codisjoint a b ↔ Codisjoint (↑a : α) (↑b : α)
have rw₄ : a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ IsCompl a b ↔ IsCompl (↑a : α) (↑b : α)
have rw : Disjoint a b ∧ Codisjoint a b ↔ IsCompl (↑a : α) (↑b : α)
Tactic: rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : Disjoint a b ∧ Codisjoint a b ↔ IsCompl (↑a : α) (↑b : α)
⊢ IsCompl a b ↔ IsCompl (↑a : α) (↑b : α)
have rw₁ : Disjoint a b ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
Tactic: rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : Disjoint a b ∧ Codisjoint a b ↔ IsCompl (↑a : α) (↑b : α)
rw₁ : Disjoint a b ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
⊢ IsCompl a b ↔ IsCompl (↑a : α) (↑b : α)
have rw₂ : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
Tactic: rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
rw : Disjoint a b ∧ Codisjoint a b ↔ IsCompl (↑a : α) (↑b : α)
rw₁ : Disjoint a b ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
rw₂ : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint a b ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
⊢ IsCompl a b ↔ IsCompl (↑a : α) (↑b : α)
have rw₃ : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α)
Tactic: rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
⊢ ComplementedLattice.{u_1} ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
have refine_1 : ComplementedLattice.{u_1} ↥L → ∀ (a : α) (ha : a ∈ L) (h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b), ∃ b ∈ L, IsCompl a b
Tactic: refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
refine_1 :
  ComplementedLattice.{u_1} ↥L → ∀ (a : α) (ha : a ∈ L) (h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b), ∃ b ∈ L, IsCompl a b
⊢ ComplementedLattice.{u_1} ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
have refine_2 : ∀ (h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b) (x : ↥L) (a : α) (ha : a ∈ L),
  ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
Tactic: refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h_1 : ComplementedLattice.{u_1} ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ (b : ↥L), IsCompl a b
⊢ ∃ b ∈ L, IsCompl a b
have refine_1 : ∀ (b : ↥L) (hb : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b), ∃ b ∈ L, IsCompl a b
Tactic: obtain ⟨b, hb⟩ := h ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x : ↥L
a : α
ha : a ∈ L
⊢ ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
have refine_2 : ∀ (b : α) (hb : b ∈ L) (hb' : IsCompl a b), ∃ (b : ↥L), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ L) a ha) b
Tactic: obtain ⟨b, hb, hb'⟩ := h a ha
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ Iic a = extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
have h : ∀ (x : α), x ∈ Iic a ↔ x ∈ extent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
⊢ Ici a = intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)
have h : ∀ (x : α),
  x ∈ Ici a ↔
    Membership.mem (γ := Set α) (intent (r := fun (x1 x2 : α) ↦ x1 ≤ x2) (ofObject (fun (x1 x2 : α) ↦ x1 ≤ x2) a)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := Concept α α fun (x1 x2 : α) ↦ x1 ≤ x2) (ofAttribute (fun (x1 x2 : α) ↦ x1 ≤ x2) a) (principal a)
have h : ∀ (x : α), x ∈ left (ofAttribute (fun (x1 x2 : α) ↦ x1 ≤ x2) a) ↔ x ∈ left (principal a)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
⊢ principal (sSup A.left) = A
have h : right (principal (sSup A.left)) = A.right
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
⊢ right (principal (sSup A.left)) = A.right
have h : ∀ (x : α), x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
have h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
Tactic: rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
have h₁ : sSup A.left ≤ x ↔ x ∈ A.right
Tactic: rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
h₁ : sSup A.left ≤ x ↔ x ∈ A.right
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
have h₂ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ A.right
Tactic: rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
h₁ : sSup A.left ≤ x ↔ x ∈ A.right
h₂ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ A.right
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
have h₃ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ upperBounds A.left
Tactic: rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Ici (sSup A.left) ↔ x ∈ A.right
h₁ : sSup A.left ≤ x ↔ x ∈ A.right
h₂ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ A.right
h₃ : (∀ b ∈ A.left, b ≤ x) ↔ x ∈ upperBounds A.left
⊢ x ∈ right (principal (sSup A.left)) ↔ x ∈ A.right
have h₄ : (∀ b ∈ A.left, b ≤ x) ↔ ∀ x_1 ∈ A.left, x_1 ≤ x
Tactic: rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
⊢ principal (sInf A.right) = A
have h : ∀ (x : α), x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
have h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
Tactic: rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
have h₁ : x ≤ sInf A.right ↔ x ∈ A.left
Tactic: rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
h₁ : x ≤ sInf A.right ↔ x ∈ A.left
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
have h₂ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ A.left
Tactic: rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
h₁ : x ≤ sInf A.right ↔ x ∈ A.left
h₂ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ A.left
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
have h₃ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ lowerBounds A.right
Tactic: rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
A : DedekindCut α
x : α
h : x ∈ Iic (sInf A.right) ↔ x ∈ A.left
h₁ : x ≤ sInf A.right ↔ x ∈ A.left
h₂ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ A.left
h₃ : (∀ b ∈ A.right, x ≤ b) ↔ x ∈ lowerBounds A.right
⊢ x ∈ left (principal (sInf A.right)) ↔ x ∈ A.left
have h₄ : (∀ b ∈ A.right, x ≤ b) ↔ ∀ x_1 ∈ A.right, x ≤ x_1
Tactic: rw [left_principal, mem_Iic, le_sInf_iff, ← lowerBounds_right, mem_lowerBounds]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
⊢ ∀ (a b : DedekindCut β),
    LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) a)
        ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) b) ↔
      a ≤ b
have refine : ∀ (A B : DedekindCut β)
  (h :
    LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
      ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B))
  (x : β) (hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)), x ∈ B.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
Tactic: refine fun A B ↦ ⟨fun h x hx ↦ ?_, fun h ↦ sSup_le_sSup (image_mono h)⟩
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h :
  LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
    ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B)
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
⊢ x ∈ B.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
have simp_rw : x ∈ lowerBounds B.right
Tactic: simp_rw [← lowerBounds_right]
-- Lean 4 proof step from Mathlib.Order.Completion (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
h :
  LE.le.{u_1} (α := α) ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) A)
    ((fun (A : DedekindCut β) ↦ (sSup ((⇑f : (a : β) → α) '' A.left) : α)) B)
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
⊢ x ∈ lowerBounds B.right
have h₁ : ∀ (b : α),
  Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
    ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b
Tactic: simp_rw [le_sSup_iff, sSup_le_iff, forall_mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
A B : DedekindCut β
x : β
hx : x ∈ A.extent (r := fun (x1 x2 : β) ↦ x1 ≤ x2)
h :
  ∀ (b : α),
    Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' B.left)) b →
      ∀ ⦃x : β⦄, x ∈ A.left → (f : (a : β) → α) x ≤ b
y : β
hy : y ∈ B.right
⊢ x ≤ y
have rw : LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) ((f : (a : β) → α) y : α)
Tactic: rw [← f.le_iff_le]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ Eq.{u_1 + 1} (α := α) ((factorEmbedding f : (a : DedekindCut β) → α) (principal x) : α) ((f : (a : β) → α) x : α)
have rw : Eq.{u_1 + 1} (α := α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α) ((f : (a : β) → α) x : α)
Tactic: rw [factorEmbedding_apply]
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ Eq.{u_1 + 1} (α := α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α) ((f : (a : β) → α) x : α)
have apply : LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α)
Tactic: apply le_antisymm (by simp)
-- Lean 4 proof step from Mathlib.Order.Completion (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : PartialOrder β
f : β ↪o α
x : β
⊢ LE.le.{u_1} (α := α) ((f : (a : β) → α) x : α) (sSup ((⇑f : (a : β) → α) '' left (principal x)) : α)
have rw : ∀ (b : α),
  Membership.mem (γ := Set α) (upperBounds ((⇑f : (a : β) → α) '' left (principal x))) b → (f : (a : β) → α) x ≤ b
Tactic: rw [le_sSup_iff]