awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_himp : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst : CompleteAtomicBooleanAlgebra β
completeBooleanAlgebra : CompleteBooleanAlgebra α := e.completeBooleanAlgebra
le : ∀ {x y : α}, LE.le.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{v} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{v + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
map_compl : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) aᶜ : β) (((e : (a : α) → β) a)ᶜ : β)
map_himp :
  ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a ⇨ b) : β) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)
map_hnot : ∀ (a : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (￢a) : β) (￢(e : (a : α) → β) a : β)
⊢ CompleteAtomicBooleanAlgebra α
have map_sdiff : ∀ (a b : α), Eq.{v + 1} (α := β) ((e : (a : α) → β) (a \ b) : β) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeAtomicBooleanAlgebra
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Type u_8
inst : SupSet α
f : ULift.{u_9, u_8} ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ULift.{u_9, u_8} ι), f i) (⨆ (i : ι), f { down := i })
have simp : Eq.{u_1 + 1} (α := α) (sSup (range fun (i : ULift.{u_9, u_8} ι) ↦ f i)) (sSup (range fun (i : ι) ↦ f { down := i }))
Tactic: simp only [iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Type u_8
inst : SupSet α
f : ULift.{u_9, u_8} ι → α
⊢ Eq.{u_1 + 1} (α := α) (sSup (range fun (i : ULift.{u_9, u_8} ι) ↦ f i)) (sSup (range fun (i : ι) ↦ f { down := i }))
have e_a : ∀ (x : α),
  Membership.mem (γ := Set α) (range fun (i : ULift.{u_9, u_8} ι) ↦ f i) x ↔
    Membership.mem (γ := Set α) (range fun (i : ι) ↦ f { down := i }) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
have rw : (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}
Tactic: rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
have rw₁ : (∀ a ∈ s, a = ⊥) ↔ s ⊆ {⊥}
Tactic: rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
rw : (∀ a ∈ s, a = ⊥) ↔ s = ∅ ∨ s = {⊥}
rw₁ : (∀ a ∈ s, a = ⊥) ↔ s ⊆ {⊥}
⊢ sSup s = ⊥ ↔ s = ∅ ∨ s = {⊥}
have rw₂ : (∀ a ∈ s, a = ⊥) ↔ ∀ y ∈ s, y = ⊥
Tactic: rw [sSup_eq_bot, ← subset_singleton_iff_eq, subset_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s = {⊥}
have rw : s.Nonempty ∧ ∀ x ∈ s, x = ⊥
Tactic: rw [Set.eq_singleton_iff_nonempty_unique_mem]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
inst : CompleteLattice α
s : Set α
h_sup : sSup s = ⊥
hne : s.Nonempty
⊢ s.Nonempty ∧ ∀ x ∈ s, x = ⊥
have h_sup₁ : ∀ a ∈ s, a = ⊥
Tactic: rw [sSup_eq_bot] at h_sup
Cleared hypotheses: h_sup, hne
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : SupSet α
s : Set α
⊢ sSup s = ⨆ (a : (↑s : Type u_1)), (↑a : α)
have rw : sSup s = sSup (range fun (a : (↑s : Type u_1)) ↦ (↑a : α))
Tactic: rw [iSup, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : SupSet α
s : Set α
rw : sSup s = sSup (range fun (a : (↑s : Type u_1)) ↦ (↑a : α))
⊢ sSup s = ⨆ (a : (↑s : Type u_1)), (↑a : α)
have rw₁ : sSup s = sSup s
Tactic: rw [iSup, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), g (f x)) (⨆ (y : ι'), g y)
have simp : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (y : ι') ↦ g y))
Tactic: simp only [iSup.eq_1]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (y : ι') ↦ g y))
have e_a : Eq.{u_1 + 1} (α := Set α) (range fun (x : ι) ↦ g (f x)) (range fun (y : ι') ↦ g y)
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := α) (⨆ (x : ι), f x) (⨆ (y : ι'), g y)
have h₁ : ∀ (x : ι), f x = g (h x)
Tactic: convert! h1.iSup_comp g
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : SupSet α
p q : Prop
f₁ : p → α
f₂ : q → α
pq : p ↔ q
f : ∀ (x : q), f₁ ⋯ = f₂ x
⊢ iSup f₁ = iSup f₂
have obtain : ∀ {f₂ : p → α} (pq : p ↔ p) (f : ∀ (x : p), f₁ sorry = f₂ x), iSup f₁ = iSup f₂
Tactic: obtain rfl := propext pq
Cleared hypotheses: q, f₂, pq, f
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
g : β → α
f : ι → β
⊢ Eq.{u_1 + 1} (α := α) (⨆ (b : (↑(range f) : Type u_2)), g (↑b : β)) (⨆ (i : ι), g (f i))
have rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (⨆ (i : ι), g (f i))
Tactic: rw [iSup, iSup, ← image_eq_range, ← range_comp']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (⨆ (i : ι), g (f i))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (b : (↑(range f) : Type u_2)), g (↑b : β)) (⨆ (i : ι), g (f i))
have rw₁ : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (sSup (range fun (i : ι) ↦ g (f i)))
Tactic: rw [iSup, iSup, ← image_eq_range, ← range_comp']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (⨆ (i : ι), g (f i))
rw₁ :
  Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β)))
    (sSup (range fun (i : ι) ↦ g (f i)))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (b : (↑(range f) : Type u_2)), g (↑b : β)) (⨆ (i : ι), g (f i))
have rw₂ : sSup (g '' range f) = sSup (range fun (i : ι) ↦ g (f i))
Tactic: rw [iSup, iSup, ← image_eq_range, ← range_comp']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β))) (⨆ (i : ι), g (f i))
rw₁ :
  Eq.{u_1 + 1} (α := α) (sSup (range fun (b : (↑(range f) : Type u_2)) ↦ g (↑b : β)))
    (sSup (range fun (i : ι) ↦ g (f i)))
rw₂ : sSup (g '' range f) = sSup (range fun (i : ι) ↦ g (f i))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (b : (↑(range f) : Type u_2)), g (↑b : β)) (⨆ (i : ι), g (f i))
have rw₃ : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : ι) ↦ g (f x))) (sSup (range fun (i : ι) ↦ g (f i)))
Tactic: rw [iSup, iSup, ← image_eq_range, ← range_comp']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ (a : (↑s : Type u_2)), f (↑a : β)
have rw : sSup (f '' s) = sSup (range fun (a : (↑s : Type u_2)) ↦ f (↑a : β))
Tactic: rw [iSup, image_eq_range]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
s : Set β
f : β → α
rw : sSup (f '' s) = sSup (range fun (a : (↑s : Type u_2)) ↦ f (↑a : β))
⊢ sSup (f '' s) = ⨆ (a : (↑s : Type u_2)), f (↑a : β)
have rw₁ : Eq.{u_1 + 1} (α := α) (sSup (range fun (x : (↑s : Type u_2)) ↦ f (↑x : β)))
  (sSup (range fun (a : (↑s : Type u_2)) ↦ f (↑a : β)))
Tactic: rw [iSup, image_eq_range]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)
have rw : ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)
Tactic: rw [sSup_eq_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
a : α
inst_1 : Nonempty ι
⊢ ⨆ (x : ι), a = a
have rw : sSup (range fun (x : ι) ↦ a) = a
Tactic: rw [iSup, range_const, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
a : α
inst_1 : Nonempty ι
rw : sSup (range fun (x : ι) ↦ a) = a
⊢ ⨆ (x : ι), a = a
have rw₁ : sSup {a} = a
Tactic: rw [iSup, range_const, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
a : α
inst_1 : Nonempty ι
rw : sSup (range fun (x : ι) ↦ a) = a
rw₁ : sSup {a} = a
⊢ ⨆ (x : ι), a = a
have rw₂ : a = a
Tactic: rw [iSup, range_const, sSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : p → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
have pos : ∀ (h : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
p : Prop
inst_1 : Decidable p
a : p → α
pos : ∀ (h : p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
have neg : ∀ (h : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (h : p), a h) (if h : p then a h else ⊥)
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
⊢ ⨆ i ∈ s, a = a
have this : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: haveI : Nonempty s := Set.nonempty_coe_sort.mpr hs
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ ⨆ i ∈ s, a = a
have rw : ⨆ (i : (↑s : Type u_2)), a = a
Tactic: rw [← iSup_subtype'', iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
rw : ⨆ (i : (↑s : Type u_2)), a = a
⊢ ⨆ i ∈ s, a = a
have rw₁ : a = a
Tactic: rw [← iSup_subtype'', iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
⊢ (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
have rw : (⨆ (x : ι), f x) ⊔ a = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), a
Tactic: rw [iSup_sup_eq, iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
rw : (⨆ (x : ι), f x) ⊔ a = (⨆ (x : ι), f x) ⊔ ⨆ (x : ι), a
⊢ (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
have rw₁ : (⨆ (x : ι), f x) ⊔ a = (⨆ (x : ι), f x) ⊔ a
Tactic: rw [iSup_sup_eq, iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x
have rw : a ⊔ ⨆ (x : ι), f x = (⨆ (x : ι), a) ⊔ ⨆ (x : ι), f x
Tactic: rw [iSup_sup_eq, iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : Nonempty ι
f : ι → α
a : α
rw : a ⊔ ⨆ (x : ι), f x = (⨆ (x : ι), a) ⊔ ⨆ (x : ι), f x
⊢ a ⊔ ⨆ (x : ι), f x = ⨆ (x : ι), a ⊔ f x
have rw₁ : a ⊔ ⨆ (x : ι), f x = a ⊔ ⨆ (x : ι), f x
Tactic: rw [iSup_sup_eq, iSup_const]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
⊢ (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
have this : Nonempty.{max 1 u_4} { i : ι // p i }
Tactic: haveI : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
this : Nonempty.{max 1 u_4} { i : ι // p i }
⊢ (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
have rw : (⨆ (x : Subtype p), f (↑x : ι) sorry) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
Tactic: rw [iSup_subtype', iSup_subtype', iSup_sup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
this : Nonempty.{max 1 u_4} { i : ι // p i }
rw : (⨆ (x : Subtype p), f (↑x : ι) ⋯) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
⊢ (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
have rw₁ : (⨆ (x : Subtype p), f (↑x : ι) sorry) ⊔ a = ⨆ (x : Subtype p), f (↑x : ι) sorry ⊔ a
Tactic: rw [iSup_subtype', iSup_subtype', iSup_sup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ (i : ι), p i
this : Nonempty.{max 1 u_4} { i : ι // p i }
rw : (⨆ (x : Subtype p), f (↑x : ι) ⋯) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
rw₁ : (⨆ (x : Subtype p), f (↑x : ι) ⋯) ⊔ a = ⨆ (x : Subtype p), f (↑x : ι) ⋯ ⊔ a
⊢ (⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ a = ⨆ (i : ι), ⨆ (h : p i), f i h ⊔ a
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (x : Subtype p), f (↑x : ι) sorry ⊔ a) (⨆ (x : Subtype p), f (↑x : ι) sorry ⊔ a)
Tactic: rw [iSup_subtype', iSup_subtype', iSup_sup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)
have a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j) (⨆ (i : ι), f i)
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j)
have a : ∀ (j : ι), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j
Tactic: refine iSup_le fun j ↦ ?_