awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ IsLUB (α := β) ((fun (b : β × β) ↦ b.1 ⊔ b.2) '' d) ((fun (b : β × β) ↦ b.1 ⊔ b.2) (p₁, p₂))
have hdp₁ : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
  Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
Tactic: simp only [IsLUB, IsLeast, upperBounds, Prod.forall, mem_setOf_eq, Prod.mk_le_mk] at hdp
Cleared hypotheses: hdp
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
⊢ IsLUB (α := β) ((fun (b : β × β) ↦ b.1 ⊔ b.2) '' d) ((fun (b : β × β) ↦ b.1 ⊔ b.2) (p₁, p₂))
have simp : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
  Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
    (p₁ ⊔ p₂)
Tactic: simp only [IsLUB, IsLeast, upperBounds, mem_image, Prod.exists, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)
have e1 : Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}) (p₁, p₂)
Tactic: have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (hypothesis)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}) (p₁, p₂)
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)
have e1₁ : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
Tactic: simp only [lowerBounds, mem_setOf_eq, Prod.forall, Prod.mk_le_mk] at e1
Cleared hypotheses: e1
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)
have refine_1 : ∀ (a b₁ b₂ : β) (hbd : (b₁, b₂) ∈ d) (hba : b₁ ⊔ b₂ = a), a ≤ p₁ ⊔ p₂
Tactic: refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
refine_1 : ∀ (a b₁ b₂ : β) (hbd : (b₁, b₂) ∈ d) (hba : b₁ ⊔ b₂ = a), a ≤ p₁ ⊔ p₂
⊢ Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} (p₁ ⊔ p₂) ∧
    Membership.mem (γ := Set β) (lowerBounds {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x})
      (p₁ ⊔ p₂)
have refine_2 : ∀ (b : β)
  (hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b),
  p₁ ⊔ p₂ ≤ b
Tactic: refine ⟨fun a b₁ b₂ hbd hba => ?_,fun b hb => ?_⟩
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ a ≤ p₁ ⊔ p₂
have refine_1 : b₁ ⊔ b₂ ≤ p₁ ⊔ p₂
Tactic: rw [← hba]
-- Lean 4 proof step from Mathlib.Order.ScottContinuity (goal)
Goal:
β : Type u_2
inst : SemilatticeSup β
d : Set (β × β)
h : d.Nonempty
h_1 : DirectedOn (fun (x1 x2 : β × β) ↦ x1 ≤ x2) d
x : β × β
p₁ p₂ : β
hdp :
  (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧
    Membership.mem (γ := Set (β × β)) (lowerBounds {x : β × β | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}) (p₁, p₂)
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : Membership.mem (γ := Set β) {x : β | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x} b
⊢ p₁ ⊔ p₂ ≤ b
have refine_2 : p₁ ≤ b ∧ p₂ ≤ b
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB.{u_3} (α := γ) {x : γ | (f ∘ (⇑e : (a : γ) → α)) x ≤ y} (((⇑e.symm : (a : α) → γ) ∘ g) y)
have change : IsLUB.{u_3} (α := γ) (preimage.{u_3, u_1} (β := α) (⇑e : (a : γ) → α) {x : α | f x ≤ y} : Set γ)
  ((e.symm : (a : α) → γ) (g y) : γ)
Tactic: change IsLUB (e ⁻¹' { x | f x ≤ y }) (e.symm (g y))
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
f : α → β
g : β → α
h : IsOrderRightAdjoint f g
e : γ ≃o α
y : β
⊢ IsLUB.{u_3} (α := γ) (preimage.{u_3, u_1} (β := α) (⇑e : (a : γ) → α) {x : α | f x ≤ y} : Set γ)
    ((e.symm : (a : α) → γ) (g y) : γ)
have rw : IsLUB {x : α | f x ≤ y} (g y)
Tactic: rw [e.isLUB_preimage, e.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
⊢ Semiconj g' (⇑fb : (a : β) → β) (⇑fa : (a : α) → α)
have refine : ∀ (y : β), IsLUB (α := α) ({x : α | g x ≤ (fb : (a : β) → β) y} : Set α) ((fa : (a : α) → α) (g' y) : α)
Tactic: refine fun y => (hg' _).unique ?_
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : Preorder β
fa : α ≃o α
fb : β ↪o β
g : α → β
h : Semiconj g (⇑fa : (a : α) → α) (⇑fb : (a : β) → β)
g' : β → α
hg' : IsOrderRightAdjoint g g'
y : β
⊢ IsLUB (α := α) ({x : α | g x ≤ (fb : (a : β) → β) y} : Set α) ((fa : (a : α) → α) (g' y) : α)
have rw : IsLUB (α := α) (image (α := α) (⇑fa : (a : α) → α) {a : α | g ((fa : (a : α) → α) a) ≤ (fb : (a : β) → β) y} : Set α)
  ((fa : (a : α) → α) (g' y) : α)
Tactic: rw [← fa.surjective.image_preimage { x | g x ≤ fb y }, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (goal)
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
⊢ Semiconj h (⇑((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)
have refine : ∀ (y : α),
  IsLUB (α := α)
    (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) y : α) :
            α) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
Tactic: refine fun y => (H _).unique ?_
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (hypothesis)
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
y : α
⊢ IsLUB (α := α)
    (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) y : α) :
            α) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
have this : IsLUB (α := α)
  (image (α := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α)) :
    Set α)
  ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
Tactic: have := (f₁ g).leftOrdContinuous (H y)
-- Lean 4 proof step from Mathlib.Order.SemiconjSup (hypothesis)
Goal:
α : Type u_1
G : Type u_4
inst : PartialOrder α
inst_1 : Group G
f₁ f₂ : MonoidHom.{u_4, u_1} G (α ≃o α)
h : α → α
H :
  ∀ (x : α),
    IsLUB
      (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) x : α))
      (h x)
g : G
y : α
this :
  IsLUB (α := α)
    (image (α := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α)
        (range fun (g' : G) ↦
          ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
            ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α)) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
⊢ IsLUB (α := α)
    (range fun (g' : G) ↦
        ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
          ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α)
              ((((f₂ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) y : α) :
            α) :
      Set α)
    ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
have this₁ : IsLUB (α := α)
  (range (ι := G)
      (comp (β := G)
        (comp (β := α) (⇑((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) fun (g' : G) ↦
          ((((f₁ : (a : G) → α ≃o α) g')⁻¹ : α ≃o α) : (a : α) → α)
            ((((f₂ : (a : G) → α ≃o α) g' : α ≃o α) : (a : α) → α) y : α))
        (⇑(Equiv.mulRight g) : (a : G) → G)) :
    Set α)
  ((((f₁ : (a : G) → α ≃o α) g : α ≃o α) : (a : α) → α) (h y) : α)
Tactic: rw [← range_comp, ← (Equiv.mulRight g).surjective.range_comp _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Shrink (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a b : α
⊢ LE.le.{u} (α := Shrink.{u, u_1} α) ((equivShrink α : (a : α) → Shrink.{u, u_1} α) a : Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
    a ≤ b
have obtain : ∀ (a : Shrink.{u, u_1} α),
  LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
    (Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a ≤ b
Tactic: obtain ⟨a, rfl⟩ := (equivShrink.{u} α).symm.surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Shrink (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
b : α
a : Shrink.{u, u_1} α
⊢ LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α) b : Shrink.{u, u_1} α) ↔
    (Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a ≤ b
have obtain : ∀ (b : Shrink.{u, u_1} α),
  LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α) :
        Shrink.{u, u_1} α) ↔
    LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)
Tactic: obtain ⟨b, rfl⟩ := (equivShrink.{u} α).symm.surjective b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Shrink (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
inst_1 : Preorder α
a b : Shrink.{u, u_1} α
⊢ LE.le.{u} (α := Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α) :
        Shrink.{u, u_1} α)
      ((equivShrink α : (a : α) → Shrink.{u, u_1} α)
          ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α) :
        Shrink.{u, u_1} α) ↔
    LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
      ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)
have simp : a ≤ b ↔
  LE.le.{u_1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) a : α)
    ((Equiv.symm (equivShrink α) : (a : Shrink.{u, u_1} α) → α) b : α)
Tactic: simp only [Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
L_1 M_1 : Sublattice α
f : LatticeHom α β
s t : Set α
a b : α
L M : Sublattice α
h : Eq.{u_2 + 1} (α := Set α) ((fun (L : Sublattice α) ↦ L.carrier) L) ((fun (L : Sublattice α) ↦ L.carrier) M)
⊢ L = M
have mk : ∀ (carrier : Set α) (supClosed' : SupClosed carrier) (infClosed' : InfClosed carrier)
  (h :
    Eq.{u_2 + 1} (α := Set α)
      ((fun (L : Sublattice α) ↦ L.carrier) { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' })
      ((fun (L : Sublattice α) ↦ L.carrier) M)),
  { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α } = M
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ (↑L : Set α) = univ ↔ L = ⊤
have rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
Tactic: rw [← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
⊢ (↑L : Set α) = univ ↔ L = ⊤
have rw₁ : L = ⊤ ↔ L = ⊤
Tactic: rw [← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
⊢ (↑L : Set α) = ∅ ↔ L = ⊥
have rw : (↑L : Set α) = (↑⊥ : Set α) ↔ L = ⊥
Tactic: rw [← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
inst : Lattice α
L : Sublattice α
rw : (↑L : Set α) = (↑⊥ : Set α) ↔ L = ⊥
⊢ (↑L : Set α) = ∅ ↔ L = ⊥
have rw₁ : L = ⊥ ↔ L = ⊥
Tactic: rw [← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ map { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ } L = M ↔
    L = map { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ } M
have simp_rw : (↑(map { toFun := (⇑e.symm : (a : α) → β), map_sup' := sorry, map_inf' := sorry : LatticeHom α β } L) : Set β) = (↑M : Set β) ↔
  (↑L : Set α) = (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := sorry, map_inf' := sorry } M) : Set α)
Tactic: simp_rw [← coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ map f (L ⊓ M) = map f L ⊓ map f M
have rw : (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)
Tactic: rw [← SetLike.coe_set_eq]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi (π := π) s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom (α := π) i) (L i)
have simp : (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i
Tactic: simp [SetLike.le_def]
-- Lean 4 proof step from Mathlib.Order.Sublattice (goal)
Goal:
κ : Type u_5
π : κ → Type u_6
inst : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi (π := π) univ L = ⊥ ↔ ∃ (i : κ), L i = ⊥
have simp_rw : (↑(pi (π := π) univ L) : Set ((i : κ) → π i)) = (↑⊥ : Set ((i : κ) → π i)) ↔
  ∃ (i : κ), (↑(L i) : Set (π i)) = (↑⊥ : Set (π i))
Tactic: simp_rw [← coe_inj]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s1 s2 : Sublocale X
h : Eq.{u_1 + 1} (α := Set X) ((fun (x : Sublocale X) ↦ x.carrier) s1) ((fun (x : Sublocale X) ↦ x.carrier) s2)
⊢ s1 = s2
have mk : ∀ (carrier : Set X) (sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier)
  (himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier)
  (h :
    Eq.{u_1 + 1} (α := Set X)
      ((fun (x : Sublocale X) ↦ x.carrier) { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' })
      ((fun (x : Sublocale X) ↦ x.carrier) s2)),
  { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' : Sublocale X } = s2
Tactic: cases s1
Cleared hypotheses: s1, h
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
S : Sublocale X
a : X
ha : a ∈ (↑S : Set X)
b : X
hb : b ∈ (↑S : Set X)
⊢ a ⊓ b ∈ (↑S : Set X)
have rw : sInf {a, b} ∈ (↑S : Set X)
Tactic: rw [← sInf_pair]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
x : Set ↥S
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ S) '' x ⊆ S.carrier
have simp_rw : ∀ x_1 ∈ x, Membership.mem (γ := Set ↥S) (Subtype.val (p := fun (x : X) ↦ x ∈ S) ⁻¹' S.carrier) x_1
Tactic: simp_rw [image_subset_iff, subset_def]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : (↑(S.restrictAux x) : X) ≤ x
⊢ x ∈ S
have rw : (↑(S.restrictAux x) : X) ∈ S
Tactic: rw [le_antisymm le_restrictAux hx]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
⊢ S.restrictAux a ≤ b ↔ a ≤ (↑b : X)
have mp : S.restrictAux a ≤ b → a ≤ (↑b : X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a : X
b : ↥S
mp : S.restrictAux a ≤ b → a ≤ (↑b : X)
⊢ S.restrictAux a ≤ b ↔ a ≤ (↑b : X)
have mpr : a ≤ (↑b : X) → S.restrictAux a ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
⊢ Eq.{u_1 + 1} (α := ↥S) (sInf {s : ↥S | a ⊓ b ≤ (↑s : X)})
    (sInf {s : ↥S | a ≤ (↑s : X)} ⊓ sInf {s : ↥S | b ≤ (↑s : X)})
have change : S.restrictAux (a ⊓ b) = S.restrictAux a ⊓ S.restrictAux b
Tactic: change Sublocale.restrictAux S (a ⊓ b) = Sublocale.restrictAux S a ⊓ Sublocale.restrictAux S b
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
⊢ S.restrictAux (a ⊓ b) = S.restrictAux a ⊓ S.restrictAux b
have refine : ∀ (s : ↥S), S.restrictAux a ⊓ S.restrictAux b ≤ s ↔ S.restrictAux (a ⊓ b) ≤ s
Tactic: refine eq_of_forall_ge_iff (fun s ↦ Iff.symm ?_)
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
⊢ S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
have rw : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
Tactic: rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
rw : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
⊢ S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
have rw₁ : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X)
Tactic: rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
rw : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
rw₁ : a ≤ (↑(S.restrictAux b ⇨ s) : X) ↔ a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X)
⊢ S.restrictAux a ≤ S.restrictAux b ⇨ s ↔ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X)
have rw₂ : a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X) ↔ a ≤ (↑(S.restrictAux b) : X) ⇨ (↑s : X)
Tactic: rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
c : ↥S := Subtype.mk (p := fun (x : X) ↦ x ∈ S) (a ⇨ (↑s : X)) ⋯
⊢ (↑(S.restrictAux b) : X) ≤ a ⇨ (↑s : X) ↔ b ≤ a ⇨ (↑s : X)
have change : (↑(S.restrictAux b) : X) ≤ (↑c : X) ↔ b ≤ (↑c : X)
Tactic: change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
-- Lean 4 proof step from Mathlib.Order.Sublocale (goal)
Goal:
X : Type u_1
inst : Order.Frame X
ι : Sort u_2
S_1 T : Sublocale X
s_1 : Set X
f : ι → X
a_1 b_1 : X
S : Sublocale X
a b : X
s : ↥S
c : ↥S := Subtype.mk (p := fun (x : X) ↦ x ∈ S) (a ⇨ (↑s : X)) ⋯
⊢ (↑(S.restrictAux b) : X) ≤ (↑c : X) ↔ b ≤ (↑c : X)
have rw : S.restrictAux b ≤ c ↔ b ≤ (↑c : X)
Tactic: rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]