awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
have empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
have insert : ∀ (a : ι) (s : Finset ι),
  a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((insert a s).sup f ∈ t ↔ ∀ i ∈ insert a s, f i ∈ t)
Tactic: classical
  induction s using Finset.induction_on <;> simp [*]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I_1 J_1 s t I J : Ideal P
⊢ Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}
have obtain : ∀ (w : P) (h : w ∈ (↑I : Set P) ∩ (↑J : Set P)), Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}
Tactic: obtain ⟨w, h⟩ := inter_nonempty I J
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
⊢ Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) ⊥
have rw : ∀ (i : Ideal P) (j : i ∈ S), ⊥ ∈ (↑i.toLowerSet : Set P)
Tactic: rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) a
b : P
hb : Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) b
⊢ Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) (a ⊔ b)
have rw : ∀ (ha : ∀ (i : Ideal P) (j : i ∈ S), a ∈ (↑i.toLowerSet : Set P)) (b : P)
  (hb : ∀ (i : Ideal P) (j : i ∈ S), b ∈ (↑i.toLowerSet : Set P)) (i : Ideal P) (j : i ∈ S),
  a ⊔ b ∈ (↑i.toLowerSet : Set P)
Tactic: rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂] at ha hb ⊢
Cleared hypotheses: ha, b, hb
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
have simp_rw : x ∈ (↑(sInf S) : Set P) ↔ ∀ s ∈ S, x ∈ (↑s : Set P)
Tactic: simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
simp_rw : x ∈ (↑(sInf S) : Set P) ↔ ∀ s ∈ S, x ∈ (↑s : Set P)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
have simp_rw₁ : Membership.mem (γ := Set P) (⋂ s ∈ S, (↑s : Set P)) x ↔ ∀ s ∈ S, x ∈ (↑s : Set P)
Tactic: simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ s ≤ sInf S
have rwa : (↑s : Set P) ⊆ (↑(sInf S) : Set P)
Tactic: rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
rwa : (↑s : Set P) ⊆ (↑(sInf S) : Set P)
⊢ s ≤ sInf S
have rwa₁ : (↑s : Set P) ⊆ ⋂ s ∈ S, (↑s : Set P)
Tactic: rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
rwa : (↑s : Set P) ⊆ (↑(sInf S) : Set P)
rwa₁ : (↑s : Set P) ⊆ ⋂ s ∈ S, (↑s : Set P)
⊢ s ≤ sInf S
have rwa₂ : ∀ (i : Ideal P) (j : i ∈ S), (↑s : Set P) ⊆ (↑i : Set P)
Tactic: rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
⊢ IsGLB S (sInf S)
have refine : ∀ (s : Ideal P) (hs : s ∈ S), sInf S ≤ s
Tactic: refine ⟨fun s hs ↦ ?_, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ sInf S ≤ s
have rw : ⋂ s ∈ S, (↑s : Set P) ⊆ (↑s : Set P)
Tactic: rw [← coe_subset_coe, coe_sInf]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'
have refine : x = x ⊓ i ⊔ x ⊓ j
Tactic: refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
have apply : ⊤ ∈ I
Tactic: apply hI.top_notMem
-- Lean 4 proof step from Mathlib.Order.Ideal (hypothesis)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I
have ht : x ⊔ xᶜ ∈ I
Tactic: have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I
have rwa : ∀ (ht : ⊤ ∈ I), ⊤ ∈ I
Tactic: rwa [sup_compl_eq_top] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.Ideal (hypothesis)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ x ∉ I ∨ xᶜ ∉ I
have h : xᶜ ∈ I → x ∉ I
Tactic: have h : xᶜ ∈ I → x ∉ I := hI.notMem_of_compl_mem
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I
have inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I
have inr : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₁ : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr₁ : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I
have inl₂ : ∀ (h : xᶜ ∉ I), ¬x ∉ I → xᶜ ∉ I
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₁ : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr₁ : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₂ : ∀ (h : xᶜ ∉ I), ¬x ∉ I → xᶜ ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I
have inr₂ : ∀ (h : x ∉ I), ¬x ∉ I → xᶜ ∉ I
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₁ : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr₁ : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₂ : ∀ (h : xᶜ ∉ I), ¬x ∉ I → xᶜ ∉ I
inr₂ : ∀ (h : x ∉ I), ¬x ∉ I → xᶜ ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I
have inr₃ : ∀ (h : x ∉ I), x ∈ I → xᶜ ∈ I → False
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I
have empty : ⨆ (i : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ i), f i ∈ I ↔ ∀ (i : α), Membership.mem (γ := Set α) ∅ i → f i ∈ I
Tactic: induction s, hs using Finite.induction_on with simp [↓iSup_insert, sup_mem_iff, *]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
empty :
  ⨆ (i : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ i), f i ∈ I ↔ ∀ (i : α), Membership.mem (γ := Set α) ∅ i → f i ∈ I
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I
have insert : ∀ {a : α} {s : Set α},
  a ∉ s → s.Finite → (⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I) → (⨆ i ∈ insert a s, f i ∈ I ↔ ∀ i ∈ insert a s, f i ∈ I)
Tactic: induction s, hs using Finite.induction_on with simp [↓iSup_insert, sup_mem_iff, *]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)
have hf : ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
Tactic: apply monotone_nat_of_le_succ
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
have hf : sequenceOfCofinals p 𝒟 n ≤
  match (motive := Option ι → P) Encodable.decode n with
  | none => sequenceOfCofinals p 𝒟 n
  | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
Tactic: dsimp only [sequenceOfCofinals, Nat.add]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
have hf : sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 n
Tactic: cases (Encodable.decode n : Option ι)
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
hf : sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 n
⊢ sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
have hf₁ : ∀ (val : ι),
  sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) some val with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
Tactic: cases (Encodable.decode n : Option ι)
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
have dsimp : Membership.mem (α := P) (𝒟 i)
  (match (motive := Option ι → P) Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
    P)
Tactic: dsimp only [sequenceOfCofinals, Nat.add]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ Membership.mem (α := P) (𝒟 i)
    (match (motive := Option ι → P) Encodable.decode (Encodable.encode i) with
      | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
      | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
      P)
have rw : Membership.mem (α := P) (𝒟 i)
  (match (motive := Option ι → P) some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
    P)
Tactic: rw [Encodable.encodek]
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)
have refine : ∃ s ∈ C, s.Nonempty
Tactic: refine ⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
    directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ ∃ s ∈ C, s.Nonempty
have let : ∀ (I : Set P) (hI : I ∈ C), ∃ s ∈ C, s.Nonempty
Tactic: let ⟨I, hI⟩ := hNe
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
⊢ IsCoatomic.{u_1} (Ideal P)
have h : ∀ (c : Set (Ideal P)),
  IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds c
Tactic: apply IsCoatomic.of_isChain_bounded
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S
have h : ∀ I ∈ SetLike.coe '' S, IsIdeal I
Tactic: refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
h : ∀ I ∈ SetLike.coe '' S, IsIdeal I
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S
have h₁ : ∀ (x y : Ideal P), x ≤ y → (↑x : Set P) ⊆ (↑y : Set P)
Tactic: refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
h : ∀ I ∈ SetLike.coe '' S, IsIdeal I
h₁ : ∀ (x y : Ideal P), x ≤ y → (↑x : Set P) ⊆ (↑y : Set P)
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S
have h₂ : Ne (α := Ideal P) (IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) sorry) ⊤
Tactic: refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
h : ∀ I ∈ SetLike.coe '' S, IsIdeal I
h₁ : ∀ (x y : Ideal P), x ≤ y → (↑x : Set P) ⊆ (↑y : Set P)
h₂ : Ne (α := Ideal P) (IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) ⋯) ⊤
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S
have h₃ : IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) sorry ∈ upperBounds S
Tactic: refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
hI : I.IsProper
⊢ ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal
have inl : ∀ (hI : IsProper.{u_1} (P := P) ⊤), ∃ (J : Ideal P), ⊤ ≤ J ∧ J.IsMaximal
Tactic: rcases IsCoatomic.eq_top_or_exists_le_coatom I with rfl | ⟨J, hJ, hJ'⟩
Cleared hypotheses: I, hI
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
hI : I.IsProper
inl : ∀ (hI : IsProper.{u_1} (P := P) ⊤), ∃ (J : Ideal P), ⊤ ≤ J ∧ J.IsMaximal
⊢ ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal
have inr : ∀ (J : Ideal P) (hJ : IsCoatom J) (hJ' : I ≤ J), ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal
Tactic: rcases IsCoatomic.eq_top_or_exists_le_coatom I with rfl | ⟨J, hJ, hJ'⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
⊢ ∃ (I : Ideal P), I.IsMaximal
have rcases : ∀ (a : P) (ha : a ≠ ⊤), ∃ (I : Ideal P), I.IsMaximal
Tactic: rcases exists_ne (⊤ : P) with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Order.Ideal (hypothesis)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : a ≠ ⊤
⊢ ∃ (I : Ideal P), I.IsMaximal
have ha₁ : IsProper (principal a)
Tactic: rw [← isProper_principal_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.Ideal (goal)
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : IsProper (principal a)
⊢ ∃ (I : Ideal P), I.IsMaximal
have rcases : ∀ (I : Ideal P) (hI : I.IsMaximal), ∃ (I : Ideal P), I.IsMaximal
Tactic: rcases ha.exists_le_maximal with ⟨I, -, hI⟩
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf :
  ∀ (a : α) (b : β),
    s b ((f : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
g : r ↪r s
hg :
  ∀ (a : α) (b : β),
    s b ((g : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) b
h :
  Eq (α := (a : α) → β)
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) f hf))
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) g hg))
⊢ mk (r := r) (s := s) f hf = mk (r := r) (s := s) g hg
have e_toRelEmbedding : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b ((f : (a : α) → β) a)
⊢ ∃ (a' : α), (f : (a : α) → β) a' = b ∧ r a' a
have rcases : ∀ (a' : α) (h : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)),
  ∃ (a'_1 : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a'_1 : β) ((f : (a : α) → β) a' : β) ∧ r a'_1 a
Tactic: rcases f.mem_range_of_rel h with ⟨a', rfl⟩
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h :
  t c
    ((f.toRelEmbedding (r := r) (s := s).trans (r := r) (s := s) (t := t) (g.toRelEmbedding (r := s) (s := t)) :
        (a : α) → γ)
      a)
⊢ Membership.mem (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (⇑(f.toRelEmbedding (r := r) (s := s).trans (r := r) (s := s) (t := t) (g.toRelEmbedding (r := s) (s := t))) :
        (a : α) → γ))
    c
have simp : Membership.mem (γ := Set γ)
  (Set.range.{u_3, u_1 + 1} (ι := α) (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
  c
Tactic: simp only [RelEmbedding.coe_trans, coe_coe_fn, comp_apply] at h ⊢
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
⊢ Membership.mem (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    c
have rcases : ∀ (b : β) (h : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))),
  Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b : γ)
Tactic: rcases g.2 _ _ h with ⟨b, rfl⟩
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
⊢ Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b : γ)
have h₁ : s b ((f : (a : α) → β) a)
Tactic: have h := g.map_rel_iff.1 h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h_1 : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
h : s b ((f : (a : α) → β) a)
⊢ Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b : γ)
have rcases : ∀ (a' : α)
  (h :
    t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β))
      ((g : (a : β) → γ) ((f : (a : α) → β) a : β)))
  (h : s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a') ((f : (a : α) → β) a)),
  Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β) : γ)
Tactic: rcases f.2 _ _ h with ⟨a', rfl⟩
Cleared hypotheses: b, h_1, h
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
⊢ f = g
have h : ∀ (a : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
have h : ∀ (b : α) (IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)) (x : β),
  s x ((f : (a : α) → β) b) ↔ s x ((g : (a : α) → β) b)
Tactic: refine IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)
x : β
⊢ s x ((f : (a : α) → β) b) ↔ s x ((g : (a : α) → β) b)
have h : (∃ (a' : α), (f : (a : α) → β) a' = x ∧ r a' b) ↔ ∃ (a' : α), (g : (a : α) → β) a' = x ∧ r a' b
Tactic: rw [f.exists_eq_iff_rel, g.exists_eq_iff_rel]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f g : r ≼i s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
have rw : Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
Tactic: rw [Subsingleton.elim f g]
-- Lean 4 proof step from Mathlib.Order.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) ∨
    ∃ (b : β), ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b
have apply : (¬∃ (b : β), ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b) →
  Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
Tactic: apply or_iff_not_imp_right.2