awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
⊢ p ((lfp : (a : α →o α) → α) f)
have suffices : sSup s = (lfp : (a : α →o α) → α) f
Tactic: suffices sSup s = f.lfp from this ▸ hSup
-- Lean 4 proof step from Mathlib.Order.FixedPoints (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = (lfp : (a : α →o α) → α) f
have h : sSup s ≤ (lfp : (a : α →o α) → α) f
Tactic: have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
-- Lean 4 proof step from Mathlib.Order.FixedPoints (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ (lfp : (a : α →o α) → α) f → p ((f : (a : α) → α) a)
s : Set α := {a : α | a ≤ (lfp : (a : α →o α) → α) f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ (lfp : (a : α →o α) → α) f
⊢ sSup s = (lfp : (a : α →o α) → α) f
have hmem : Membership.mem (α := α) s ((f : (a : α) → α) (sSup s) : α)
Tactic: have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) ((lfp : (a : α →o α) → α) h.onDiag : α)
have refine_1 : LE.le (α := α) ((comp lfp h : (a : α) → α) ((lfp : (a : α →o α) → α) h.onDiag : α) : α)
  ((lfp : (a : α →o α) → α) h.onDiag : α)
Tactic: refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
refine_1 :
  LE.le (α := α) ((comp lfp h : (a : α) → α) ((lfp : (a : α →o α) → α) h.onDiag : α) : α)
    ((lfp : (a : α →o α) → α) h.onDiag : α)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) ((lfp : (a : α →o α) → α) h.onDiag : α)
have refine_2 : Eq (α := α) ((h.onDiag : (a : α) → α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) : α)
  ((lfp : (a : α →o α) → α) (comp lfp h) : α)
Tactic: refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))
-- Lean 4 proof step from Mathlib.Order.FixedPoints (hypothesis)
Goal:
α : Type u
inst : CompleteLattice α
h : α →o α →o α
a : α := (lfp : (a : α →o α) → α) (comp lfp h)
⊢ Eq (α := α) ((h.onDiag : (a : α) → α) ((lfp : (a : α →o α) → α) (comp lfp h) : α) : α)
    ((lfp : (a : α →o α) → α) (comp lfp h) : α)
have ha : Function.comp (β := α →o α) (⇑lfp : (a : α →o α) → α) (⇑h : (a : α) → α →o α) a = a
Tactic: have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
have a : LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
a : LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
⊢ Eq (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
have a₁ : LE.le (α := α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α) ((lfp : (a : α →o α) → α) f : α)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
⊢ LE.le (α := α) ((lfp : (a : α →o α) → α) f : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
have a : Eq (α := α) ((f : (a : α) → α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥) : α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α)
Tactic: apply lfp_le_fixed
-- Lean 4 proof step from Mathlib.Order.FixedPoints (goal)
Goal:
α : Type u
inst : CompleteLattice α
f : α →o α
h : ωScottContinuous (α := α) (β := α) (⇑f : (a : α) → α)
⊢ LE.le (α := α) (⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ : α) ((lfp : (a : α →o α) → α) f : α)
have a : ∀ (b : α), (f : (a : α) → α) b ≤ b → ⨆ (n : ℕ), (⇑f : (a : α) → α)^[n] ⊥ ≤ b
Tactic: apply le_lfp
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
h : BddAbove (l '' s)
x : β
hx : x ∈ upperBounds (l '' s)
⊢ u x ∈ upperBounds s
have rwa : ∀ (hx : x ∈ u ⁻¹' upperBounds s), u x ∈ upperBounds s
Tactic: rwa [gc.upperBounds_l_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s
have rwa : ∀ (hb : b ∈ u ⁻¹' upperBounds s), u b ∈ upperBounds s
Tactic: rwa [gc.upperBounds_l_image] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
⊢ IsLUB (range (l ∘ f)) (l (iSup f))
have rw : IsLUB (l '' range f) (l (sSup (range f)))
Tactic: rw [range_comp, ← sSup_range]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b
have dsimp : (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
have rw : (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ
Tactic: rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
rw : (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
have rw₁ : (u aᶜ)ᶜ ≤ b ↔ bᶜ ≤ u aᶜ
Tactic: rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
rw : (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ
rw₁ : (u aᶜ)ᶜ ≤ b ↔ bᶜ ≤ u aᶜ
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
have rw₂ : bᶜ ≤ u aᶜ ↔ bᶜ ≤ u aᶜ
Tactic: rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have ha₁ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀
Cleared hypotheses: ha₀, hb₀
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
ha₁ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have hb₁ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀
Cleared hypotheses: ha₀, hb₀
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₄ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
simp_rw₄ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₅ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
simp_rw₄ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
simp_rw₅ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₆ : ∀ (b : γ), a₀ ≤ u₁ b₀ b ↔ ∀ x ∈ s, x ≤ u₁ b₀ b
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap (φ := fun (x : α) (y : β) ↦ γ) l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
simp_rw : ∀ (b : γ), l a₀ b₀ ≤ b ↔ b ∈ upperBounds (image2 l s t)
simp_rw₁ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b
simp_rw₂ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
simp_rw₃ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, ∀ y ∈ t, y ≤ u₂ x b
simp_rw₄ : ∀ (b : γ), b₀ ≤ u₂ a₀ b ↔ ∀ x ∈ s, b₀ ≤ u₂ x b
simp_rw₅ : ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, l x b₀ ≤ b
simp_rw₆ : ∀ (b : γ), a₀ ≤ u₁ b₀ b ↔ ∀ x ∈ s, x ≤ u₁ b₀ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
have simp_rw₇ : ∀ (b : γ), True
Tactic: simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove.{u} (α := α) ((⇑e : (a : α) → β) ⁻¹' s) ↔ BddAbove s
have rw : BddAbove.{v} (α := β) (image.{u, v} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s)) ↔ BddAbove s
Tactic: rw [← e.bddAbove_image, e.image_preimage]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set β
rw : BddAbove.{v} (α := β) (image.{u, v} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s)) ↔ BddAbove s
⊢ BddAbove.{u} (α := α) ((⇑e : (a : α) → β) ⁻¹' s) ↔ BddAbove s
have rw₁ : BddAbove s ↔ BddAbove s
Tactic: rw [← e.bddAbove_image, e.image_preimage]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sSup (u '' s)) = sSup s
have rw : l (⨆ a ∈ s, u a) = sSup s
Tactic: rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
rw : l (⨆ a ∈ s, u a) = sSup s
⊢ l (sSup (u '' s)) = sSup s
have rw₁ : ⨆ i ∈ s, i = sSup s
Tactic: rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
rw : l (⨆ a ∈ s, u a) = sSup s
rw₁ : ⨆ i ∈ s, i = sSup s
⊢ l (sSup (u '' s)) = sSup s
have rw₂ : Eq.{v + 1} (α := β) (⨆ i ∈ s, i) (⨆ a ∈ s, a)
Tactic: rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (sInf (u '' s)) = sInf s
have rw : l (⨅ a ∈ s, u a) = sInf s
Tactic: rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
rw : l (⨅ a ∈ s, u a) = sInf s
⊢ l (sInf (u '' s)) = sInf s
have rw₁ : ⨅ i ∈ s, i = sInf s
Tactic: rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
rw : l (⨅ a ∈ s, u a) = sInf s
rw₁ : ⨅ i ∈ s, i = sInf s
⊢ l (sInf (u '' s)) = sInf s
have rw₂ : Eq.{v + 1} (α := β) (⨅ i ∈ s, i) (⨅ a ∈ s, a)
Tactic: rw [sInf_image, gi.l_biInf_u, sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
l : α → β
u : β → α
inst : CompleteLattice α
inst_1 : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ (i : ι), ⨅ (hi : p i), f i hi) = ⨅ (i : ι), ⨅ (hi : p i), l (f i hi)
have rw : l (⨅ (x : Subtype p), f (↑x : ι) sorry) = ⨅ (x : Subtype p), l (f (↑x : ι) sorry)
Tactic: rw [iInf_subtype', iInf_subtype']
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ a
have simp : ∀ (a b : β), l (u a ⊓ u b) ≤ a
Tactic: simp only [gi.choice_eq]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b : β), gi.choice (u a ⊓ u b) ⋯ ≤ b
have simp : ∀ (a b : β), l (u a ⊓ u b) ≤ b
Tactic: simp only [gi.choice_eq]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : SemilatticeInf α
gi : GaloisInsertion l u
⊢ ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ gi.choice (u b ⊓ u c) ⋯
have simp : ∀ (a b c : β), a ≤ b → a ≤ c → a ≤ l (u b ⊓ u c)
Tactic: simp only [gi.choice_eq]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : Preorder α
inst_2 : OrderTop α
gi : GaloisInsertion l u
⊢ ∀ (a : β), a ≤ gi.choice ⊤ ⋯
have simp : ∀ (a : β), a ≤ l ⊤
Tactic: simp only [gi.choice_eq]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort u_1
a₁ a₂ : α
b₁ b₂ : β
l : α → β
u : β → α
inst : PartialOrder β
inst_1 : CompleteLattice α
gi : GaloisInsertion l u
x : Set β
⊢ IsGLB x (gi.choice (sInf (u '' x)) ⋯)
have rw : IsGLB x (l (sInf (u '' x)))
Tactic: rw [gi.choice_eq]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Defs (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
l : α → β
u : β → α
⊢ Eq (α := Prop) (∀ (a : β) (b : α), u a ≤ b ↔ a ≤ l b) (∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a)
have rw : Eq (α := Prop) (∀ (b : α) (a : β), u a ≤ b ↔ a ≤ l b) (∀ (a : α) (b : β), b ≤ l a ↔ u b ≤ a)
Tactic: rw [forall_comm]
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
have mp : u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.GaloisConnection.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PartialOrder α
inst_1 : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
mp : u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
have mpr : (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
have mp : GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
mp : GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1
have mpr : rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
have mpr : ∀ {x y : α × β}, rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
Tactic: revert x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
have rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
Tactic: rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.GameAdd (goal)
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x x_1 : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
rw : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
have rw₁ : GameAdd rβ rα ((a₁, b₁).2, (a₁, b₁).1) ((a₂, b₂).2, (a₂, b₂).1) ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)
Tactic: rw [Prod.swap, Prod.swap, gameAdd_mk_iff, gameAdd_mk_iff, or_comm]