awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.PSet
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) (mk (A a).Type (A a).Func)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
let ⟨βt, _⟩ := e
        let ⟨c, bc⟩ := βt b
        ⟨⟨a, c⟩, yb.trans bc⟩

Premises used: Membership.mem, PSet.mk, _private.0.PSet.mem_sUnion.match_3, PSet.sUnion, PSet.Equiv.trans, Exists.intro, _private.0.PSet.mem_sUnion.match_4, Sigma.mk
-- Module: Mathlib.SetTheory.ZFC.PSet
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) (mk (A a).Type (A a).Func)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
exact
        let ⟨βt, _⟩ := e
        let ⟨c, bc⟩ := βt b
        ⟨⟨a, c⟩, yb.trans bc⟩
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x : PSet.{u}
h : ∀ (x_1 : PSet.{u}), x_1 ∈ (⋃₀ x).toSet ↔ x_1 ∈ ⋃₀ (toSet '' x.toSet)
⊢ (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet)

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
x x_1 : PSet.{u}
⊢ x_1 ∈ (⋃₀ x).toSet ↔ x_1 ∈ ⋃₀ (toSet '' x.toSet)

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.PSet
Goal:
⊢ ∀ (x : PSet.{u}), x.Lift ∈ embed

Tactic:
fun x =>
  ⟨⟨x⟩, Equiv.rfl⟩

Premises used: PSet.Mem, PSet.Equiv.rfl, Exists.intro, ULift.up
-- Module: Mathlib.SetTheory.ZFC.Rank
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)
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)
⊢ (mk α A).rank = (mk α_1 A_1).rank

Tactic:
apply congr_arg sSup

Premises used: congr_arg, SupSet.sSup
-- Module: Mathlib.SetTheory.ZFC.Rank
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)
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
⊢ 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:
ext
-- Module: Mathlib.SetTheory.ZFC.Rank
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
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
⊢ 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
-- Module: Mathlib.SetTheory.ZFC.Rank
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 : ∀ (x_1 : α) (h : succ (A x_1).rank = x), ∃ (y : α_1), succ (A_1 y).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

Tactic:
simp only [Set.mem_range, forall_exists_index]

Premises used: Set.mem_range, forall_exists_index
-- Module: Mathlib.SetTheory.ZFC.Rank
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 : ∀ (x_1 : α_1) (h : succ (A_1 x_1).rank = x), ∃ (y : α), succ (A y).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

Tactic:
simp only [Set.mem_range, forall_exists_index]

Premises used: Set.mem_range, forall_exists_index
-- Module: Mathlib.SetTheory.ZFC.Rank
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
h₁ : ∀ (b : α_1) (h' : Equiv.{u_1, u_1} (A a) (A_1 b)), ∃ (y : α_1), succ (A_1 y).rank = x
⊢ ∃ (y : α_1), succ (A_1 y).rank = x

Tactic:
obtain ⟨b, h'⟩ := αβ a
-- Module: Mathlib.SetTheory.ZFC.Rank
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 = x
⊢ ∃ (y : α_1), succ (A_1 y).rank = x

Tactic:
exists b
-- Module: Mathlib.SetTheory.ZFC.Rank
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
h₂ h₃ : succ (A_1 b).rank = succ (A_1 b).rank
⊢ succ (A_1 b).rank = x

Tactic:
rw [← h, rank_congr h']
-- Module: Mathlib.SetTheory.ZFC.Rank
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
h₁ : ∀ (b : α) (h' : Equiv.{u_1, u_1} (A b) (A_1 a)), ∃ (y : α), succ (A y).rank = x
⊢ ∃ (y : α), succ (A y).rank = x

Tactic:
obtain ⟨b, h'⟩ := βα a
-- Module: Mathlib.SetTheory.ZFC.Rank
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 = x
⊢ ∃ (y : α), succ (A y).rank = x

Tactic:
exists b
-- Module: Mathlib.SetTheory.ZFC.Rank
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
h₂ h₃ : succ (A_1 a).rank = succ (A_1 a).rank
⊢ succ (A b).rank = x

Tactic:
rw [← h, rank_congr h']
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
A : α → PSet.{u_1}
x : PSet.{u_1}
w : (mk α A).Type
h : x.Equiv ((mk α A).Func w)
rw : succ ((mk α A).Func w).rank ≤ (mk α A).rank
⊢ x.rank < (mk α A).rank

Tactic:
rw [rank_congr h, ← succ_le_iff]

Premises used: Order.succ_le_iff, PSet.rank_congr
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
A : α → PSet.{u_1}
x : PSet.{u_1}
w : (mk α A).Type
h : x.Equiv ((mk α A).Func w)
⊢ succ ((mk α A).Func w).rank ≤ (mk α A).rank

Tactic:
apply Ordinal.le_iSup

Premises used: Ordinal.le_iSup
-- Module: Mathlib.SetTheory.ZFC.Rank
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

Tactic:
⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩

Premises used: Ordinal.iSup_le, PSet.rank_lt_of_mem, LT.lt.trans_le, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
refine : ∀ (h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o) (a : α), succ (A a).rank ≤ o
⊢ (mk α A).rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o

Tactic:
refine ⟨fun h _ h' => (rank_lt_of_mem h').trans_le h, fun h ↦ Ordinal.iSup_le fun a ↦ ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o
a : α
rw : (A a).rank < o
⊢ succ (A a).rank ≤ o

Tactic:
rw [succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o
a : α
⊢ (A a).rank < o

Tactic:
h (Mem.mk A a)

Premises used: PSet.Mem.mk
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
α : Type u_1
A : α → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α A → y.rank < o
a : α
⊢ (A a).rank < o

Tactic:
exact h (Mem.mk A a)

Premises used: PSet.Mem.mk
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
contrapose! : x.rank ≤ o ↔ ∀ (y : PSet.{u_1}) (_ : y ∈ x), y.rank < o
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x.rank ≤ o ↔ ∀ (y : PSet.{u_1}) (_ : y ∈ x), y.rank < o

Tactic:
rank_le_iff

Premises used: PSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x.rank ≤ o ↔ ∀ (y : PSet.{u_1}) (_ : y ∈ x), y.rank < o

Tactic:
exact rank_le_iff

Premises used: PSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u}
h : x ⊆ y
⊢ x.rank ≤ y.rank

Tactic:
rank_le_iff.2 fun _ h₁ => rank_lt_of_mem (mem_of_subset h h₁)

Premises used: PSet.rank_le_iff, Iff.mpr, PSet.mem_of_subset, PSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
⊢ rank ∅ = 0

Tactic:
simp [empty_def, rank]

Premises used: PSet.rank, PSet.empty_def
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
a : (insert x y).rank ≤ max (succ x.rank) y.rank
a₁ : max (succ x.rank) y.rank ≤ (insert x y).rank
⊢ (insert x y).rank = max (succ x.rank) y.rank

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
a : ∀ ⦃y_1 : PSet.{u_1}⦄, y_1.Equiv x ∨ y_1 ∈ y → y_1.rank < max (succ x.rank) y.rank
⊢ (insert x y).rank ≤ max (succ x.rank) y.rank

Tactic:
simp_rw [rank_le_iff, mem_insert_iff]

Premises used: PSet.rank_le_iff, PSet.mem_insert_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y y_1 : PSet.{u_1}
h : y_1.Equiv x
⊢ y_1.rank < max (succ x.rank) y.rank

Tactic:
simp [rank_congr h]

Premises used: PSet.rank_congr
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y y_1 : PSet.{u_1}
h : y_1 ∈ y
⊢ y_1.rank < max (succ x.rank) y.rank

Tactic:
simp [rank_lt_of_mem h]

Premises used: PSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
a : succ x.rank ≤ (insert x y).rank
a₁ : y.rank ≤ (insert x y).rank
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

Tactic:
(rank_lt_of_mem (mem_insert x y)).succ_le

Premises used: PSet.rank_lt_of_mem, LT.lt.succ_le, PSet.mem_insert
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

Tactic:
exact (rank_lt_of_mem (mem_insert x y)).succ_le

Premises used: PSet.rank_lt_of_mem, LT.lt.succ_le, PSet.mem_insert
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank

Tactic:
rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

Premises used: Iff.mpr, PSet.rank_mono, PSet.mem_insert_of_mem, PSet.subset_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank

Tactic:
exact rank_mono (subset_iff.2 fun z => mem_insert_of_mem x)

Premises used: Iff.mpr, PSet.rank_mono, PSet.mem_insert_of_mem, PSet.subset_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
⊢ max (succ x.rank) (rank ∅) = succ x.rank

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ rank {x, y} = max (succ x.rank) (succ y.rank)

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
a : x.powerset.rank ≤ succ x.rank
a₁ : succ x.rank ≤ x.powerset.rank
⊢ x.powerset.rank = succ x.rank

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
a : ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank
⊢ x.powerset.rank ≤ succ x.rank

Tactic:
simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]

Premises used: PSet.rank_le_iff, PSet.mem_powerset, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ y ⊆ x → y.rank ≤ x.rank

Tactic:
rank_mono

Premises used: PSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
⊢ y ⊆ x → y.rank ≤ x.rank

Tactic:
exact rank_mono

Premises used: PSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
a : x.rank < x.powerset.rank
⊢ succ x.rank ≤ x.powerset.rank

Tactic:
rw [succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
a : x ∈ x.powerset
⊢ x.rank < x.powerset.rank

Tactic:
apply rank_lt_of_mem

Premises used: PSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
⊢ x ∈ x.powerset

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
simp_rw : ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
simp_rw [rank_le_iff, mem_sUnion]

Premises used: PSet.rank_le_iff, PSet.mem_sUnion
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : PSet.{u_1}
this : ∀ w ∈ x, y ∈ w → y.rank < x.rank
⊢ (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
⟨_, _, _⟩
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
trans₁ : w.rank < x.rank
trans₂ : Ordinal.{u_1}
⊢ y.rank < x.rank

Tactic:
trans
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right a : y ∈ w
x₁ : PSet.{u_1}
⊢ y.rank < w.rank

Tactic:
apply rank_lt_of_mem

Premises used: PSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
a : w ∈ x
⊢ w.rank < x.rank

Tactic:
apply rank_lt_of_mem

Premises used: PSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ y ∈ w

Tactic:
assumption
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : PSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ w ∈ x

Tactic:
assumption
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
rw : x.rank ≤ (⋃₀ x).powerset.rank
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Premises used: PSet.rank_powerset
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
h : x ⊆ (⋃₀ x).powerset
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Tactic:
apply rank_mono

Premises used: PSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
h : ∀ ⦃z : PSet.{u_1}⦄, z ∈ x → z ∈ (⋃₀ x).powerset
⊢ x ⊆ (⋃₀ x).powerset

Tactic:
rw [subset_iff]

Premises used: PSet.subset_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : PSet.{u_1}
h : z ∈ x → z ∈ (⋃₀ x).powerset
⊢ z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
_
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : PSet.{u_1}
h_1 : z ∈ x
h : ∀ ⦃z_1 : PSet.{u_1}⦄, z_1 ∈ z → z_1 ∈ ⋃₀ x
⊢ z ∈ (⋃₀ x).powerset

Tactic:
rw [mem_powerset, subset_iff]

Premises used: PSet.subset_iff, PSet.mem_powerset
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : PSet.{u_1}
h_1 : z ∈ x
z_1 : PSet.{u_1}
h : z_1 ∈ z → z_1 ∈ ⋃₀ x
⊢ z_1 ∈ z → z_1 ∈ ⋃₀ x

Tactic:
_
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : PSet.{u_1}
h_1 : z ∈ x
z_1 : PSet.{u_1}
h_2 : z_1 ∈ z
h : ∃ z ∈ x, z_1 ∈ z
⊢ z_1 ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Premises used: PSet.mem_sUnion
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : PSet.{u_1}
h_1 : z ∈ x
z_1 : PSet.{u_1}
h_2 : z_1 ∈ z
h h₁ : z ∈ x ∧ z_1 ∈ z
⊢ ∃ z ∈ x, z_1 ∈ z

Tactic:
exists z
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u}
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
⊢ 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

Premises used: PSet.mem_wf, WellFounded.induction
-- Module: Mathlib.SetTheory.ZFC.Rank
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 :
  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}))
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) x

Tactic:
rw [IsWellFounded.rank_eq]

Premises used: IsWellFounded.rank_eq
-- Module: Mathlib.SetTheory.ZFC.Rank
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 : lift.{u + 1, u} x.rank = ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑b : PSet.{u}).rank)
⊢ 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:
simp_rw [← fun y : { y // y ∈ x } => ih y y.2]

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Rank
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)
apply₁ : ∀ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank) ≤ lift.{u + 1, u} x.rank
⊢ lift.{u + 1, u} x.rank = ⨆ (b : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑b : PSet.{u}).rank)

Tactic:
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)

Premises used: Ordinal.iSup_le, LE.le.antisymm, le_of_forall_lt
-- Module: Mathlib.SetTheory.ZFC.Rank
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}
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)
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)

Tactic:
rw [lt_lift_iff]

Premises used: Ordinal.lt_lift_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
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
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ (i : { b : PSet.{u} // b ∈ x }), succ (lift.{u + 1, u} (↑i : PSet.{u}).rank)

Tactic:
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h

Premises used: Ordinal.lt_iSup_iff, Iff.mp, PSet.lt_rank_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
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 : { b : PSet.{u} // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h : PSet.{u}).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
simpa using rank_lt_of_mem h.2

Premises used: PSet.rank_lt_of_mem, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : PSet.{u_1}
⊢ (mk x).rank = x.rank

Tactic:
rfl

Premises used: ZFSet.rank, rfl
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u}
⊢ y ∈ x → y.rank < x.rank

Tactic:
Quotient.inductionOn₂ x y fun _ _ => PSet.rank_lt_of_mem

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ x.rank ≤ o ↔ ∀ ⦃y : ZFSet.{u}⦄, y ∈ x → y.rank < o

Tactic:
⟨fun h _ h' => (rank_lt_of_mem h').trans_le h,
    Quotient.inductionOn x fun _ h =>
      PSet.rank_le_iff.2 fun y h' => @h ⟦y⟧ h'⟩

Premises used: Quotient.inductionOn, LT.lt.trans_le, Iff.intro, ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u}
o : Ordinal.{u}
contrapose! : x.rank ≤ o ↔ ∀ (y : ZFSet.{u}) (_ : y ∈ x), y.rank < o
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
contrapose!
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ x.rank ≤ o ↔ ∀ (y : ZFSet.{u}) (_ : y ∈ x), y.rank < o

Tactic:
rank_le_iff

Premises used: ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ x.rank ≤ o ↔ ∀ (y : ZFSet.{u}) (_ : y ∈ x), y.rank < o

Tactic:
exact rank_le_iff

Premises used: ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u}
h : x ⊆ y
⊢ x.rank ≤ y.rank

Tactic:
rank_le_iff.2 fun _ h₁ => rank_lt_of_mem (h h₁)

Premises used: Iff.mpr, ZFSet.rank_le_iff, ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
⊢ rank ∅ = 0

Tactic:
PSet.rank_empty

Premises used: ZFSet.rank, PSet.rank_empty
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
⊢ (insert x y).rank = max (succ x.rank) y.rank

Tactic:
Quotient.inductionOn₂ x y PSet.rank_insert

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u_1}
⊢ max (succ x.rank) (rank ∅) = succ x.rank

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
⊢ rank {x, y} = max (succ x.rank) (succ y.rank)

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
a : (x ∪ y).rank ≤ max x.rank y.rank
a₁ : max x.rank y.rank ≤ (x ∪ y).rank
⊢ (x ∪ y).rank = max x.rank y.rank

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
a : ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
⊢ (x ∪ y).rank ≤ max x.rank y.rank

Tactic:
simp_rw [rank_le_iff, mem_union, lt_max_iff]

Premises used: ZFSet.rank_le_iff, lt_max_iff, ZFSet.mem_union
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y y_1 : ZFSet.{u_1}
a : y_1 ∈ x → y_1.rank < x.rank
a₁ : y_1 ∈ y → y_1.rank < y.rank
⊢ y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank

Tactic:
apply Or.imp

Premises used: Or.imp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y y_1 : ZFSet.{u_1}
⊢ y_1 ∈ x → y_1.rank < x.rank

Tactic:
apply rank_lt_of_mem

Premises used: ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y y_1 : ZFSet.{u_1}
⊢ y_1 ∈ y → y_1.rank < y.rank

Tactic:
apply rank_lt_of_mem

Premises used: ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
a : x.rank ≤ (x ∪ y).rank
a₁ : y.rank ≤ (x ∪ y).rank
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
a : x ⊆ x ∪ y
⊢ x.rank ≤ (x ∪ y).rank

Tactic:
apply rank_mono

Premises used: ZFSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
a : y ⊆ x ∪ y
⊢ y.rank ≤ (x ∪ y).rank

Tactic:
apply rank_mono

Premises used: ZFSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y z : ZFSet.{u_1}
h : z ∈ x
⊢ z ∈ x ∪ y

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y z : ZFSet.{u_1}
h : z ∈ y
⊢ z ∈ x ∪ y

Tactic:
simp [h]
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u_1}
⊢ x.powerset.rank = succ x.rank

Tactic:
Quotient.inductionOn x PSet.rank_powerset

Premises used: Quotient.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u_1}
simp_rw : ∀ ⦃y : ZFSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
simp_rw [rank_le_iff, mem_sUnion]

Premises used: ZFSet.mem_sUnion, ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y : ZFSet.{u_1}
this : ∀ w ∈ x, y ∈ w → y.rank < x.rank
⊢ (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
⟨_, _, _⟩
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
trans : y.rank < w.rank
trans₁ : w.rank < x.rank
trans₂ : Ordinal.{u_1}
⊢ y.rank < x.rank

Tactic:
trans
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right a : y ∈ w
x₁ : ZFSet.{u_1}
⊢ y.rank < w.rank

Tactic:
apply rank_lt_of_mem

Premises used: ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
a : w ∈ x
⊢ w.rank < x.rank

Tactic:
apply rank_lt_of_mem

Premises used: ZFSet.rank_lt_of_mem