awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
h : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : Equiv.{u, u} (mk β B) (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A
have rw : ∀ (e : Equiv.{u, u} (mk β B) (mk (A a).Type (A a).Func)) (b : (mk β B).Type) (yb : y.Equiv ((mk β B).Func b)),
  y ∈ ⋃₀ mk α A
Tactic: rw [← eta (A a)] at e
Cleared hypotheses: e, b, yb
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
x : PSet.{u}
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)
have h : ∀ (x_1 : PSet.{u}), x_1 ∈ (⋃₀ x).toSet ↔ x_1 ∈ ⋃₀ (toSet '' x.toSet)
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
⊢ (mk α A).rank = (mk α_1 A_1).rank
have apply : Eq.{u_1 + 2} (α := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank)
  (Set.range fun (a : α_1) ↦ succ (A_1 a).rank)
Tactic: apply congr_arg sSup
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
⊢ Eq.{u_1 + 2} (α := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank)
    (Set.range fun (a : α_1) ↦ succ (A_1 a).rank)
have h : ∀ (x : Ordinal.{u_1}),
  Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
have h : Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x →
  Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
h :
  Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x →
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
have h₁ : Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x →
  Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x →
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x
have h : ∀ (x_1 : α) (h : succ (A x_1).rank = x), ∃ (y : α_1), succ (A_1 y).rank = x
Tactic: simp only [Set.mem_range, forall_exists_index]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α_1) ↦ succ (A_1 a).rank) x →
    Membership.mem (γ := Set Ordinal.{u_1}) (Set.range fun (a : α) ↦ succ (A a).rank) x
have h : ∀ (x_1 : α_1) (h : succ (A_1 x_1).rank = x), ∃ (y : α), succ (A y).rank = x
Tactic: simp only [Set.mem_range, forall_exists_index]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α
h : succ (A a).rank = x
⊢ ∃ (y : α_1), succ (A_1 y).rank = x
have h₁ : ∀ (b : α_1) (h' : Equiv.{u_1, u_1} (A a) (A_1 b)), ∃ (y : α_1), succ (A_1 y).rank = x
Tactic: obtain ⟨b, h'⟩ := αβ a
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α
h : succ (A a).rank = x
b : α_1
h' : Equiv.{u_1, u_1} (A a) (A_1 b)
⊢ ∃ (y : α_1), succ (A_1 y).rank = x
have h₁ : succ (A_1 b).rank = x
Tactic: exists b
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α
h : succ (A a).rank = x
b : α_1
h' : Equiv.{u_1, u_1} (A a) (A_1 b)
⊢ succ (A_1 b).rank = x
have h₁ : succ (A_1 b).rank = succ (A a).rank
Tactic: rw [← h, rank_congr h']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α
h : succ (A a).rank = x
b : α_1
h' : Equiv.{u_1, u_1} (A a) (A_1 b)
h₁ : succ (A_1 b).rank = succ (A a).rank
⊢ succ (A_1 b).rank = x
have h₂ : succ (A_1 b).rank = succ (A_1 b).rank
Tactic: rw [← h, rank_congr h']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α_1
h : succ (A_1 a).rank = x
⊢ ∃ (y : α), succ (A y).rank = x
have h₁ : ∀ (b : α) (h' : Equiv.{u_1, u_1} (A b) (A_1 a)), ∃ (y : α), succ (A y).rank = x
Tactic: obtain ⟨b, h'⟩ := βα a
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α_1
h : succ (A_1 a).rank = x
b : α
h' : Equiv.{u_1, u_1} (A b) (A_1 a)
⊢ ∃ (y : α), succ (A y).rank = x
have h₁ : succ (A b).rank = x
Tactic: exists b
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α_1
h : succ (A_1 a).rank = x
b : α
h' : Equiv.{u_1, u_1} (A b) (A_1 a)
⊢ succ (A b).rank = x
have h₁ : succ (A b).rank = succ (A_1 a).rank
Tactic: rw [← h, rank_congr h']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
α_1 : Type u_1
A_1 : α_1 → PSet.{u_1}
αβ : ∀ (a : α), ∃ (b : α_1), Equiv.{u_1, u_1} (A a) (A_1 b)
βα : ∀ (b : α_1), ∃ (a : α), Equiv.{u_1, u_1} (A a) (A_1 b)
x : Ordinal.{u_1}
a : α_1
h : succ (A_1 a).rank = x
b : α
h' : Equiv.{u_1, u_1} (A b) (A_1 a)
h₁ : succ (A b).rank = succ (A_1 a).rank
⊢ succ (A b).rank = x
have h₂ : succ (A_1 a).rank = succ (A_1 a).rank
Tactic: rw [← h, rank_congr h']
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
A : α → PSet.{u_1}
x : PSet.{u_1}
w : (mk α A).Type
h : x.Equiv ((mk α A).Func w)
⊢ x.rank < (mk α A).rank
have rw : succ ((mk α A).Func w).rank ≤ (mk α A).rank
Tactic: rw [rank_congr h, ← succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
⊢ (mk α A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o
have refine : ∀ (h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o) (a : α), succ (A a).rank ≤ o
Tactic: refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o
a : α
⊢ succ (A a).rank ≤ o
have rw : (A a).rank < o
Tactic: rw [succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
have contrapose! : x.rank ≤ o ↔ ∀ (y : PSet.{u_1}) (_ : y ∈ x), y.rank < o
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
⊢ (insert x y).rank = max (succ x.rank) y.rank
have a : (insert x y).rank ≤ max (succ x.rank) y.rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
a : (insert x y).rank ≤ max (succ x.rank) y.rank
⊢ (insert x y).rank = max (succ x.rank) y.rank
have a₁ : max (succ x.rank) y.rank ≤ (insert x y).rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
⊢ (insert x y).rank ≤ max (succ x.rank) y.rank
have a : ∀ ⦃y_1 : PSet.{u_1}⦄, y_1.Equiv x ∨ y_1 ∈ y → y_1.rank < max (succ x.rank) y.rank
Tactic: simp_rw [rank_le_iff, mem_insert_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank
have a : succ x.rank ≤ (insert x y).rank
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
a : succ x.rank ≤ (insert x y).rank
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank
have a₁ : y.rank ≤ (insert x y).rank
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x.powerset.rank = succ x.rank
have a : x.powerset.rank ≤ succ x.rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
a : x.powerset.rank ≤ succ x.rank
⊢ x.powerset.rank = succ x.rank
have a₁ : succ x.rank ≤ x.powerset.rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank
have a : ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank
Tactic: simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ succ x.rank ≤ x.powerset.rank
have a : x.rank < x.powerset.rank
Tactic: rw [succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank
have a : x ∈ x.powerset
Tactic: apply rank_lt_of_mem
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank
have simp_rw : ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank
Tactic: simp_rw [rank_le_iff, mem_sUnion]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : PSet.{u_1}
⊢ (∃ z ∈ x, y ∈ z) → y.rank < x.rank
have this : ∀ w ∈ x, y ∈ w → y.rank < x.rank
Tactic: ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ y.rank < x.rank
have trans : y.rank < w.rank
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
⊢ y.rank < x.rank
have trans₁ : w.rank < x.rank
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
trans₁ : w.rank < x.rank
⊢ y.rank < x.rank
have trans₂ : Ordinal.{u_1}
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank
have rw : x.rank ≤ (⋃₀ x).powerset.rank
Tactic: rw [← rank_powerset]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
have h : x ⊆ (⋃₀ x).powerset
Tactic: apply rank_mono
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u_1}
⊢ x ⊆ (⋃₀ x).powerset
have h : ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset
Tactic: rw [subset_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : PSet.{u_1}
h : z ∈ x
⊢ z ∈ (⋃₀ x).powerset
have h : ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x
Tactic: rw [mem_powerset, subset_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : PSet.{u_1}
h : z ∈ x
z_1 : PSet.{u_1}
h_1 : z_1 ∈ z
⊢ z_1 ∈ ⋃₀ x
have h : ∃ z ∈ x, z_1 ∈ z
Tactic: rw [mem_sUnion]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : PSet.{u_1}
h : z ∈ x
z_1 : PSet.{u_1}
h_1 : z_1 ∈ z
⊢ ∃ z ∈ x, z_1 ∈ z
have h : z ∈ x ∧ z_1 ∈ z
Tactic: exists z
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : PSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) x
have h : ∀ (x : PSet.{u}) (ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y),
  lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) x
Tactic: induction x using mem_wf.induction with | _ x ih
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) x
have h : lift.{u + 1, u} x.rank =
  ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (↑b : PSet.{u}))
Tactic: rw [IsWellFounded.rank_eq]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank =
    ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (↑b : PSet.{u}))
have h : lift.{u + 1, u} x.rank = ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑b : PSet.{u}).rank)
Tactic: simp_rw [← fun y : { y // y ∈ x } => ih y y.2]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑b : PSet.{u}).rank)
have apply : ∀ c < lift.{u + 1, u} x.rank, c < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)
Tactic: apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y
apply : ∀ c < lift.{u + 1, u} x.rank, c < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)
⊢ lift.{u + 1, u} x.rank = ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑b : PSet.{u}).rank)
have apply₁ : ∀ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank) ≤ lift.{u + 1, u} x.rank
Tactic: apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)
have rw : (∃ a' < x.rank, lift.{u + 1, u} a' = h) →
  h < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)
Tactic: rw [lt_lift_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
have contrapose! : x.rank ≤ o ↔ ∀ (y : ZFSet.{u}) (_ : y ∈ x), y.rank < o
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank = max x.rank y.rank
have a : (x ∪ y).rank ≤ max x.rank y.rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
a : (x ∪ y).rank ≤ max x.rank y.rank
⊢ (x ∪ y).rank = max x.rank y.rank
have a₁ : max x.rank y.rank ≤ (x ∪ y).rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank
have a : ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
Tactic: simp_rw [rank_le_iff, mem_union, lt_max_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y y_1 : ZFSet.{u_1}
⊢ y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
have a : y_1 ∈ x → y_1.rank < x.rank
Tactic: apply Or.imp
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y y_1 : ZFSet.{u_1}
a : y_1 ∈ x → y_1.rank < x.rank
⊢ y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
have a₁ : y_1 ∈ y → y_1.rank < y.rank
Tactic: apply Or.imp
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank
have a : x.rank ≤ (x ∪ y).rank
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
a : x.rank ≤ (x ∪ y).rank
⊢ max x.rank y.rank ≤ (x ∪ y).rank
have a₁ : y.rank ≤ (x ∪ y).rank
Tactic: apply max_le
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ x.rank ≤ (x ∪ y).rank
have a : x ⊆ x ∪ y
Tactic: apply rank_mono
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ y.rank ≤ (x ∪ y).rank
have a : y ⊆ x ∪ y
Tactic: apply rank_mono
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : ZFSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank
have simp_rw : ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank
Tactic: simp_rw [rank_le_iff, mem_sUnion]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y : ZFSet.{u_1}
⊢ (∃ z ∈ x, y ∈ z) → y.rank < x.rank
have this : ∀ w ∈ x, y ∈ w → y.rank < x.rank
Tactic: ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ y.rank < x.rank
have trans : y.rank < w.rank
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
⊢ y.rank < x.rank
have trans₁ : w.rank < x.rank
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
trans₁ : w.rank < x.rank
⊢ y.rank < x.rank
have trans₂ : Ordinal.{u_1}
Tactic: trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank
have rw : x.rank ≤ (⋃₀ x).powerset.rank
Tactic: rw [← rank_powerset]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : ZFSet.{u_1}
⊢ x.rank ≤ (⋃₀ x).powerset.rank
have h : x ⊆ (⋃₀ x).powerset
Tactic: apply rank_mono
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : ZFSet.{u_1}
h : z ∈ x
⊢ z ∈ (⋃₀ x).powerset
have h : z ⊆ ⋃₀ x
Tactic: rw [mem_powerset]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : ZFSet.{u_1}
h : z ∈ x
z_1 : ZFSet.{u_1}
h_1 : z_1 ∈ z
⊢ z_1 ∈ ⋃₀ x
have h : ∃ z ∈ x, z_1 ∈ z
Tactic: rw [mem_sUnion]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x z : ZFSet.{u_1}
h : z ∈ x
z_1 : ZFSet.{u_1}
h_1 : z_1 ∈ z
⊢ ∃ z ∈ x, z_1 ∈ z
have h : z ∈ x ∧ z_1 ∈ z
Tactic: exists z
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank = ⨆ (i : α), succ (f i).rank
have apply : (range f).rank ≤ ⨆ (i : α), succ (f i).rank
Tactic: apply (Ordinal.iSup_le _).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
apply : (range f).rank ≤ ⨆ (i : α), succ (f i).rank
⊢ (range f).rank = ⨆ (i : α), succ (f i).rank
have apply₁ : ∀ (i : α), succ (f i).rank ≤ (range f).rank
Tactic: apply (Ordinal.iSup_le _).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank = ⨆ (i : α), (f i).rank
have a : (⋃ (i : α), f i).rank ≤ ⨆ (i : α), (f i).rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
a : (⋃ (i : α), f i).rank ≤ ⨆ (i : α), (f i).rank
⊢ (⋃ (i : α), f i).rank = ⨆ (i : α), (f i).rank
have a₁ : ⨆ (i : α), (f i).rank ≤ (⋃ (i : α), f i).rank
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (⋃ (i : α), f i).rank ≤ ⨆ (i : α), (f i).rank
have a : ∀ ⦃y : ZFSet.{u}⦄, (∃ (i : α), y ∈ f i) → y.rank < ⨆ (i : α), (f i).rank
Tactic: simp_rw [rank_le_iff, mem_iUnion]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
y : ZFSet.{u}
⊢ (∃ (i : α), y ∈ f i) → y.rank < ⨆ (i : α), (f i).rank
have a : ∀ (i : α) (hy : y ∈ f i), y.rank < ⨆ (i : α), (f i).rank
Tactic: ⟨i, hy⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x : ZFSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x
have h : ∀ (x : ZFSet.{u}) (ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y),
  lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x
Tactic: induction x using inductionOn with | _ x ih
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x
have h : lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (↑b : ZFSet.{u}))
Tactic: rw [IsWellFounded.rank_eq]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (↑b : ZFSet.{u}))
have h : lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (lift.{u + 1, u} (↑b : ZFSet.{u}).rank)
Tactic: simp_rw [← fun y : { y // y ∈ x } => ih y y.2]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (lift.{u + 1, u} (↑b : ZFSet.{u}).rank)
have apply : ∀ c < lift.{u + 1, u} x.rank, c < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
Tactic: apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Rank (goal)
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
apply : ∀ c < lift.{u + 1, u} x.rank, c < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
⊢ lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (lift.{u + 1, u} (↑b : ZFSet.{u}).rank)
have apply₁ : ∀ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank) ≤ lift.{u + 1, u} x.rank
Tactic: apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)