[GOAL]
x : PSet
y : PSet
inst✝¹ : IsEmpty (Type x)
inst✝ : IsEmpty (Type y)
⊢ (∀ (i : Type x), ∃ j, Equiv (Func x i) (Func y j)) ∧ ∀ (j : Type y), ∃ i, Equiv (Func x i) (Func y j)
[PROOFSTEP]
simp
[GOAL]
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
cases' hxy a with b hb
[GOAL]
case intro
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
b : Type y
hb : Equiv (Func x a) (Func y b)
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
cases' hyz b with c hc
[GOAL]
case intro.intro
x y z : PSet
hxy : x ⊆ y
hyz : y ⊆ z
a : Type x
b : Type y
hb : Equiv (Func x a) (Func y b)
c : Type z
hc : Equiv (Func y b) (Func z c)
⊢ ∃ b, Equiv (Func x a) (Func z b)
[PROOFSTEP]
exact ⟨c, hb.trans hc⟩
[GOAL]
x : PSet
i : Type x
⊢ Func x i ∈ x
[PROOFSTEP]
cases x
[GOAL]
case mk
α✝ : Type u_1
A✝ : α✝ → PSet
i : Type (mk α✝ A✝)
⊢ Func (mk α✝ A✝) i ∈ mk α✝ A✝
[PROOFSTEP]
apply Mem.mk
[GOAL]
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
⊢ ∀ (y : PSet), y ∈ mk β B → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro ⟨γ, C⟩ ⟨b, hc⟩
[GOAL]
case mk.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
cases' H.exists_right b with a ha
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
have H := ha.trans hc.symm
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (Func (mk α A) a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
rw [mk_func] at H
[GOAL]
case mk.intro.intro
α : Type u
A : α → PSet
β : Type u
B : β → PSet
H✝ : Equiv (mk α A) (mk β B)
γ : Type u
C : γ → PSet
b : Type (mk β B)
hc : Equiv (mk γ C) (Func (mk β B) b)
a : Type (mk α A)
ha : Equiv (Func (mk α A) a) (Func (mk β B) b)
H : Equiv (A a) (mk γ C)
⊢ Acc (fun x x_1 => x ∈ x_1) (mk γ C)
[PROOFSTEP]
exact mem_wf_aux H
[GOAL]
⊢ toSet ∅ = ∅
[PROOFSTEP]
simp [toSet]
[GOAL]
⊢ ¬PSet.Nonempty ∅
[PROOFSTEP]
simp [PSet.Nonempty]
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : y ∈ ⋃₀ mk α A
a : Type (mk α A)
c : Type (Func (mk α A) a)
e : Equiv y (Func (A a) c)
this : Func (A a) c ∈ mk (Type (A a)) (Func (A a))
⊢ Func (A a) c ∈ A (?m.26421 α A y x✝ a c e this)
[PROOFSTEP]
rwa [eta] at this
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (A a)
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
[PROOFSTEP]
rw [← eta (A a)] at e
[GOAL]
α : Type u
A : α → PSet
y : PSet
x✝ : ∃ z, z ∈ mk α A ∧ y ∈ z
β : Type u
B : β → PSet
a : Type (mk α A)
e : Equiv (mk β B) (mk (Type (A a)) (Func (A a)))
b : Type (mk β B)
yb : Equiv y (Func (mk β B) b)
⊢ y ∈ ⋃₀ mk α A
[PROOFSTEP]
exact
  let ⟨βt, _⟩ := e
  let ⟨c, bc⟩ := βt b
  ⟨⟨a, c⟩, yb.trans bc⟩
[GOAL]
x : PSet
⊢ toSet (⋃₀ x) = ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : PSet
⊢ x✝ ∈ toSet (⋃₀ x) ↔ x✝ ∈ ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
F : Arity ZFSet (n + 1)
⊢ Definable (n + 1) F
[PROOFSTEP]
have I := fun x => allDefinable (F x)
[GOAL]
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Definable (n + 1) F
[PROOFSTEP]
refine' @Definable.EqMk (n + 1) ⟨fun x : PSet => (@Definable.Resp _ _ (I ⟦x⟧)).1, _⟩ _ _
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
    ↑(Definable.Resp (F (Quotient.mk setoid x)))
[PROOFSTEP]
dsimp [Arity.Equiv]
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ ∀ (x y : PSet),
    PSet.Equiv x y →
      Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid x))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
intro x y h
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
x y : PSet
h : PSet.Equiv x y
⊢ Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid x))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
rw [@Quotient.sound PSet _ _ _ h]
[GOAL]
case refine'_1
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
x y : PSet
h : PSet.Equiv x y
⊢ Arity.Equiv ↑(Definable.Resp (F (Quotient.mk setoid y))) ↑(Definable.Resp (F (Quotient.mk setoid y)))
[PROOFSTEP]
exact (Definable.Resp (F ⟦y⟧)).2
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
⊢ Resp.eval (n + 1)
      { val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
              ↑(Definable.Resp (F (Quotient.mk setoid x)))) } =
    F
[PROOFSTEP]
refine' funext fun q => Quotient.inductionOn q fun x => _
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
q : ZFSet
x : PSet
⊢ Resp.eval (n + 1)
      { val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
              ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
      (Quotient.mk setoid x) =
    F (Quotient.mk setoid x)
[PROOFSTEP]
simp_rw [Resp.eval_val, Resp.f]
[GOAL]
case refine'_2
n : ℕ
F : Arity ZFSet (n + 1)
I : (x : ZFSet) → Definable (Nat.add n 0) (F x)
q : ZFSet
x : PSet
⊢ Resp.eval n
      { val := ↑(Definable.Resp (F (Quotient.mk setoid x))),
        property :=
          (_ :
            Arity.Equiv
              (↑{ val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
                    property :=
                      (_ :
                        Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
                          ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
                x)
              (↑{ val := fun x => ↑(Definable.Resp (F (Quotient.mk setoid x))),
                    property :=
                      (_ :
                        Arity.Equiv (fun x => ↑(Definable.Resp (F (Quotient.mk setoid x)))) fun x =>
                          ↑(Definable.Resp (F (Quotient.mk setoid x)))) }
                x)) } =
    F (Quotient.mk setoid x)
[PROOFSTEP]
exact @Definable.eq _ (F ⟦x⟧) (I ⟦x⟧)
[GOAL]
x : ZFSet
a : PSet
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
let f : a.Type → (mk a).toSet := fun i => ⟨mk <| a.Func i, func_mem a i⟩
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
suffices Function.Surjective f by exact small_of_surjective this
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
this : Function.Surjective f
⊢ Small.{u, u + 1} ↑(toSet (Quotient.mk setoid a))
[PROOFSTEP]
exact small_of_surjective this
[GOAL]
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
⊢ Function.Surjective f
[PROOFSTEP]
rintro ⟨y, hb⟩
[GOAL]
case mk
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
y : ZFSet
hb : y ∈ toSet (mk a)
⊢ ∃ a_1, f a_1 = { val := y, property := hb }
[PROOFSTEP]
induction y using Quotient.inductionOn
[GOAL]
case mk.h
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
a✝ : PSet
hb : Quotient.mk setoid a✝ ∈ toSet (mk a)
⊢ ∃ a_1, f a_1 = { val := Quotient.mk setoid a✝, property := hb }
[PROOFSTEP]
cases' hb with i h
[GOAL]
case mk.h.intro
x : ZFSet
a : PSet
f : Type a → ↑(toSet (mk a)) := fun i => { val := mk (Func a i), property := (_ : Func a i ∈ a) }
a✝ : PSet
i : Type a
h : PSet.Equiv a✝ (Func a i)
⊢ ∃ a_1, f a_1 = { val := Quotient.mk setoid a✝, property := (_ : ∃ b, PSet.Equiv a✝ (Func a b)) }
[PROOFSTEP]
exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩
[GOAL]
x y : ZFSet
⊢ toSet x ⊆ toSet y ↔ x ⊆ y
[PROOFSTEP]
simp [subset_def, Set.subset_def]
[GOAL]
x y : ZFSet
h : x = y
⊢ ∀ (z : ZFSet), z ∈ x ↔ z ∈ y
[PROOFSTEP]
simp [h]
[GOAL]
⊢ toSet ∅ = ∅
[PROOFSTEP]
simp [toSet]
[GOAL]
⊢ ¬ZFSet.Nonempty ∅
[PROOFSTEP]
simp [ZFSet.Nonempty]
[GOAL]
x : PSet
⊢ ZFSet.Nonempty (mk x) ↔ PSet.Nonempty x
[PROOFSTEP]
refine' ⟨_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
[GOAL]
x : PSet
⊢ ZFSet.Nonempty (mk x) → PSet.Nonempty x
[PROOFSTEP]
rintro ⟨a, h⟩
[GOAL]
case intro
x : PSet
a : ZFSet
h : a ∈ toSet (mk x)
⊢ PSet.Nonempty x
[PROOFSTEP]
induction a using Quotient.inductionOn
[GOAL]
case intro.h
x a✝ : PSet
h : Quotient.mk setoid a✝ ∈ toSet (mk x)
⊢ PSet.Nonempty x
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
x : ZFSet
⊢ x = ∅ ↔ ∀ (y : ZFSet), ¬y ∈ x
[PROOFSTEP]
rw [ext_iff]
[GOAL]
x : ZFSet
⊢ (∀ (z : ZFSet), z ∈ x ↔ z ∈ ∅) ↔ ∀ (y : ZFSet), ¬y ∈ x
[PROOFSTEP]
simp
[GOAL]
u : ZFSet
⊢ u = ∅ ∨ ZFSet.Nonempty u
[PROOFSTEP]
rw [eq_empty, ← not_exists]
[GOAL]
u : ZFSet
⊢ (¬∃ x, x ∈ u) ∨ ZFSet.Nonempty u
[PROOFSTEP]
apply em'
[GOAL]
x y : ZFSet
⊢ toSet (insert x y) = insert x (toSet y)
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (insert x y) ↔ x✝ ∈ insert x (toSet y)
[PROOFSTEP]
simp
[GOAL]
x : ZFSet
⊢ toSet {x} = {x}
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : ZFSet
⊢ x✝ ∈ toSet {x} ↔ x✝ ∈ {x}
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
⊢ x ∈ {y, z} ↔ x = y ∨ x = z
[PROOFSTEP]
simp
[GOAL]
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))
[PROOFSTEP]
rw [ZFSet.sound h]
[GOAL]
n✝ : ZFSet
x : PSet
x✝ : Quotient.mk setoid x ∈ omega
n : ℕ
h : PSet.Equiv x (Func PSet.omega { down := n })
⊢ insert (mk (Func PSet.omega { down := n })) (mk (Func PSet.omega { down := n })) =
    insert (mk (ofNat n)) (mk (ofNat n))
[PROOFSTEP]
rfl
[GOAL]
p : ZFSet → Prop
x✝³ x✝² : PSet
α : Type ?u.55373
A : α → PSet
β : Type ?u.55373
B : β → PSet
x✝¹ : PSet.Equiv (PSet.mk α A) (PSet.mk β B)
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
βα : ∀ (b : β), ∃ a, PSet.Equiv (A a) (B b)
x✝ : { a // (fun y => p (mk y)) (Func (PSet.mk α A) a) }
a : Type (PSet.mk α A)
pa : (fun y => p (mk y)) (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
⊢ (fun y => p (mk y)) (Func (PSet.mk β B) b)
[PROOFSTEP]
simpa only [mk_func, ← ZFSet.sound hb]
[GOAL]
p : ZFSet → Prop
x✝³ x✝² : PSet
α : Type ?u.55373
A : α → PSet
β : Type ?u.55373
B : β → PSet
x✝¹ : PSet.Equiv (PSet.mk α A) (PSet.mk β B)
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
βα : ∀ (b : β), ∃ a, PSet.Equiv (A a) (B b)
x✝ : { a // (fun y => p (mk y)) (Func (PSet.mk β B) a) }
b : Type (PSet.mk β B)
pb : (fun y => p (mk y)) (Func (PSet.mk β B) b)
a : α
ha : PSet.Equiv (A a) (B b)
⊢ (fun y => p (mk y)) (Func (PSet.mk α A) a)
[PROOFSTEP]
simpa only [mk_func, ZFSet.sound ha]
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ ZFSet.sep p (Quotient.mk setoid (PSet.mk α A))
a : Type (PSet.mk α A)
pa : (fun y => p (mk y)) (Func (PSet.mk α A) a)
h :
  PSet.Equiv y
    (Func
      ↑(Resp.f
          { val := PSet.sep fun y => p (mk y),
            property :=
              (_ :
                ∀ (x x_1 : PSet),
                  PSet.Equiv x x_1 → Arity.Equiv (PSet.sep (fun y => p (mk y)) x) (PSet.sep (fun y => p (mk y)) x_1)) }
          (PSet.mk α A))
      { val := a, property := pa })
⊢ p (Quotient.mk setoid y)
[PROOFSTEP]
rwa [@Quotient.sound PSet _ _ _ h]
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (Func (PSet.mk α A) a)
pa : p (Quotient.mk setoid y)
⊢ (fun y => p (mk y)) (Func (PSet.mk α A) a)
[PROOFSTEP]
rw [mk_func] at h
[GOAL]
p : ZFSet → Prop
x y✝ : ZFSet
x✝¹ y : PSet
α : Type u
A : α → PSet
x✝ : Quotient.mk setoid y ∈ Quotient.mk setoid (PSet.mk α A) ∧ p (Quotient.mk setoid y)
a : Type (PSet.mk α A)
h : PSet.Equiv y (A a)
pa : p (Quotient.mk setoid y)
⊢ p (mk (Func (PSet.mk α A) a))
[PROOFSTEP]
rwa [mk_func, ← ZFSet.sound h]
[GOAL]
a : ZFSet
p : ZFSet → Prop
⊢ toSet (ZFSet.sep p a) = {x | x ∈ toSet a ∧ p x}
[PROOFSTEP]
ext
[GOAL]
case h
a : ZFSet
p : ZFSet → Prop
x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep p a) ↔ x✝ ∈ {x | x ∈ toSet a ∧ p x}
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
x✝¹ x✝ : PSet
α : Type u
A : α → PSet
β : Type u
B : β → PSet
⊢ PSet.mk β B ∈ PSet.powerset (PSet.mk α A) ↔ Quotient.mk setoid (PSet.mk β B) ⊆ Quotient.mk setoid (PSet.mk α A)
[PROOFSTEP]
simp [mem_powerset, subset_iff]
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let ⟨b, hb⟩ := αβ a
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
induction' ea : A a with γ Γ
[GOAL]
case mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
x✝ : PSet
ea✝ : A a = x✝
γ : Type u
Γ : γ → PSet
A_ih✝ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
induction' eb : B b with δ Δ
[GOAL]
case mk.mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
hb : PSet.Equiv (A a) (B b)
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
rw [ea, eb] at hb
[GOAL]
case mk.mk
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
hb : PSet.Equiv (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
cases' hb with γδ δγ
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let c : (A a).Type := c
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
let ⟨d, hd⟩ := γδ (by rwa [ea] at c )
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
⊢ γ
[PROOFSTEP]
rwa [ea] at c
[GOAL]
case mk.mk.intro
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
[PROOFSTEP]
use⟨b, Eq.ndrec d (Eq.symm eb)⟩
[GOAL]
case h
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ })
    (Func (⋃₀ PSet.mk β B) { fst := b, snd := (_ : PSet.mk δ Δ = Func (PSet.mk β B) b) ▸ d })
[PROOFSTEP]
change PSet.Equiv ((A a).Func c) ((B b).Func (Eq.ndrec d eb.symm))
[GOAL]
case h
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝¹ : PSet
ea✝ : A a = x✝¹
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝ : PSet
eb✝ : B b = x✝
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
⊢ PSet.Equiv (Func (A a) c) (Func (B b) ((_ : PSet.mk δ Δ = B b) ▸ d))
[PROOFSTEP]
match A a, B b, ea, eb, c, d, hd with
| _, _, rfl, rfl, _, _, hd => exact hd
[GOAL]
α β : Type u
A : α → PSet
B : β → PSet
αβ : ∀ (a : α), ∃ b, PSet.Equiv (A a) (B b)
a : Type (PSet.mk α A)
c✝ : Type (Func (PSet.mk α A) a)
b : β
x✝³ : PSet
ea✝ : A a = x✝³
γ : Type u
Γ : γ → PSet
A_ih✝¹ :
  ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
ea : A a = PSet.mk γ Γ
x✝² : PSet
eb✝ : B b = x✝²
δ : Type u
Δ : δ → PSet
A_ih✝ :
  ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, PSet.Equiv (Func (⋃₀ PSet.mk α A) { fst := a, snd := c✝ }) (Func (⋃₀ PSet.mk β B) b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, PSet.Equiv (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ a, PSet.Equiv (Γ a) (Δ b)
c : Type (A a) := c✝
d : δ
hd✝ : PSet.Equiv (Γ (Eq.mp (_ : Type (A a) = Type (PSet.mk γ Γ)) c)) (Δ d)
x✝¹ : Type (PSet.mk γ Γ)
x✝ : δ
hd : PSet.Equiv (Γ (Eq.mp (_ : Type (PSet.mk γ Γ) = Type (PSet.mk γ Γ)) x✝¹)) (Δ x✝)
⊢ PSet.Equiv (Func (PSet.mk γ Γ) x✝¹) (Func (PSet.mk δ Δ) ((_ : PSet.mk δ Δ = PSet.mk δ Δ) ▸ x✝))
[PROOFSTEP]
exact hd
[GOAL]
x : ZFSet
⊢ ZFSet
[PROOFSTEP]
classical exact if h : x.Nonempty then ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) h.some else ∅
[GOAL]
x : ZFSet
⊢ ZFSet
[PROOFSTEP]
exact if h : x.Nonempty then ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) h.some else ∅
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
[PROOFSTEP]
rw [sInter, dif_pos h]
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ y ∈ ZFSet.sep (fun y => ∀ (z : ZFSet), z ∈ x → y ∈ z) (Set.Nonempty.some h) ↔ ∀ (z : ZFSet), z ∈ x → y ∈ z
[PROOFSTEP]
simp only [mem_toSet, mem_sep, and_iff_right_iff_imp]
[GOAL]
x y : ZFSet
h : ZFSet.Nonempty x
⊢ (∀ (z : ZFSet), z ∈ x → y ∈ z) → y ∈ Set.Nonempty.some h
[PROOFSTEP]
exact fun H => H _ h.some_mem
[GOAL]
⊢ ⋃₀ ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
z✝ : ZFSet
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
⊢ ¬ZFSet.Nonempty ∅
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
[PROOFSTEP]
rcases eq_empty_or_nonempty x with (rfl | hx)
[GOAL]
case inl
y z : ZFSet
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z
[PROOFSTEP]
exact (not_mem_empty z hz).elim
[GOAL]
case inr
x y z : ZFSet
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : ZFSet.Nonempty x
⊢ y ∈ z
[PROOFSTEP]
exact (mem_sInter hx).1 hy z hz
[GOAL]
x y : ZFSet
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x
[PROOFSTEP]
simp_rw [mem_sUnion, mem_singleton, exists_eq_left]
[GOAL]
x y : ZFSet
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x
[PROOFSTEP]
simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]
[GOAL]
x : ZFSet
⊢ toSet (⋃₀ x) = ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x x✝ : ZFSet
⊢ x✝ ∈ toSet (⋃₀ x) ↔ x✝ ∈ ⋃₀ (toSet '' toSet x)
[PROOFSTEP]
simp
[GOAL]
x : ZFSet
h : ZFSet.Nonempty x
⊢ toSet (⋂₀ x) = ⋂₀ (toSet '' toSet x)
[PROOFSTEP]
ext
[GOAL]
case h
x : ZFSet
h : ZFSet.Nonempty x
x✝ : ZFSet
⊢ x✝ ∈ toSet (⋂₀ x) ↔ x✝ ∈ ⋂₀ (toSet '' toSet x)
[PROOFSTEP]
simp [mem_sInter h]
[GOAL]
x y : ZFSet
H : {x} = {y}
⊢ x = y
[PROOFSTEP]
let this := congr_arg sUnion H
[GOAL]
x y : ZFSet
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y
[PROOFSTEP]
rwa [sUnion_singleton, sUnion_singleton] at this
[GOAL]
x y : ZFSet
⊢ toSet (x ∪ y) = toSet x ∪ toSet y
[PROOFSTEP]
change (⋃₀ { x, y }).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (⋃₀ {x, y}) = toSet x ∪ toSet y
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (x ∩ y) = toSet x ∩ toSet y
[PROOFSTEP]
change (ZFSet.sep (fun z => z ∈ y) x).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => z ∈ y) x) = toSet x ∩ toSet y
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => z ∈ y) x) ↔ x✝ ∈ toSet x ∩ toSet y
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (x \ y) = toSet x \ toSet y
[PROOFSTEP]
change (ZFSet.sep (fun z => z ∉ y) x).toSet = _
[GOAL]
x y : ZFSet
⊢ toSet (ZFSet.sep (fun z => ¬z ∈ y) x) = toSet x \ toSet y
[PROOFSTEP]
ext
[GOAL]
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (ZFSet.sep (fun z => ¬z ∈ y) x) ↔ x✝ ∈ toSet x \ toSet y
[PROOFSTEP]
simp
[GOAL]
x y z : ZFSet
⊢ z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y
[PROOFSTEP]
rw [← mem_toSet]
[GOAL]
x y z : ZFSet
⊢ z ∈ toSet (x ∪ y) ↔ z ∈ x ∨ z ∈ y
[PROOFSTEP]
simp
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x : ZFSet
⊢ toSet (image f x) = f '' toSet x
[PROOFSTEP]
ext
[GOAL]
case h
f : ZFSet → ZFSet
H : Definable 1 f
x x✝ : ZFSet
⊢ x✝ ∈ toSet (image f x) ↔ x✝ ∈ f '' toSet x
[PROOFSTEP]
simp
[GOAL]
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f ↔ Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ range f → Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case mp.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : Type (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down))
hz : PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) z)
⊢ Quotient.mk setoid y ∈ Set.range f
[PROOFSTEP]
exact ⟨z.down, Quotient.eq_mk_iff_out.2 hz.symm⟩
[GOAL]
case mpr
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
⊢ Quotient.mk setoid y ∈ Set.range f → Quotient.mk setoid y ∈ range f
[PROOFSTEP]
rintro ⟨z, hz⟩
[GOAL]
case mpr.intro
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ Quotient.mk setoid y ∈ range f
[PROOFSTEP]
use ULift.up z
[GOAL]
case h
α : Type u
f : α → ZFSet
x : ZFSet
y : PSet
z : α
hz : f z = Quotient.mk setoid y
⊢ PSet.Equiv y (Func (PSet.mk (ULift α) (Quotient.out ∘ f ∘ ULift.down)) { down := z })
[PROOFSTEP]
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)
[GOAL]
α : Type u
f : α → ZFSet
⊢ toSet (range f) = Set.range f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
f : α → ZFSet
x✝ : ZFSet
⊢ x✝ ∈ toSet (range f) ↔ x✝ ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
x y : ZFSet
⊢ toSet (pair x y) = {{x}, {x, y}}
[PROOFSTEP]
simp [pair]
[GOAL]
p : ZFSet → ZFSet → Prop
x y z : ZFSet
⊢ z ∈ pairSep p x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
[PROOFSTEP]
refine' mem_sep.trans ⟨And.right, fun e => ⟨_, e⟩⟩
[GOAL]
p : ZFSet → ZFSet → Prop
x y z : ZFSet
e : ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b ∧ p a b
⊢ z ∈ powerset (powerset (x ∪ y))
[PROOFSTEP]
rcases e with ⟨a, ax, b, bY, rfl, pab⟩
[GOAL]
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ pair a b ∈ powerset (powerset (x ∪ y))
[PROOFSTEP]
simp only [mem_powerset, subset_def, mem_union, pair, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
⊢ ∀ ⦃z : ZFSet⦄, z = {a} ∨ z = {a, b} → ∀ ⦃z_1 : ZFSet⦄, z_1 ∈ z → z_1 ∈ x ∨ z_1 ∈ y
[PROOFSTEP]
rintro u (rfl | rfl) v
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v ∈ {a} → v ∈ x ∨ v ∈ y
[PROOFSTEP]
simp only [mem_singleton, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v ∈ {a, b} → v ∈ x ∨ v ∈ y
[PROOFSTEP]
simp only [mem_singleton, mem_pair]
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.intro.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
exact Or.inl ax
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro (rfl | rfl) <;> [left; right]
[GOAL]
case intro.intro.intro.intro.intro.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
b : ZFSet
bY : b ∈ y
pab : p a b
v : ZFSet
⊢ v = a ∨ v = b → v ∈ x ∨ v ∈ y
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case intro.intro.intro.intro.intro.inr.inl
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
left
[GOAL]
case intro.intro.intro.intro.intro.inr.inr
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
v : ZFSet
bY : v ∈ y
pab : p a v
⊢ v ∈ x ∨ v ∈ y
[PROOFSTEP]
right
[GOAL]
case intro.intro.intro.intro.intro.inr.inl.h
p : ZFSet → ZFSet → Prop
x y b : ZFSet
bY : b ∈ y
v : ZFSet
ax : v ∈ x
pab : p v b
⊢ v ∈ x
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.intro.intro.intro.inr.inr.h
p : ZFSet → ZFSet → Prop
x y a : ZFSet
ax : a ∈ x
v : ZFSet
bY : v ∈ y
pab : p a v
⊢ v ∈ y
[PROOFSTEP]
assumption
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
⊢ x = x' ∧ y = y'
[PROOFSTEP]
have ae := ext_iff.1 H
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z ∈ pair x y ↔ z ∈ pair x' y'
⊢ x = x' ∧ y = y'
[PROOFSTEP]
simp only [pair, mem_pair] at ae
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'
[PROOFSTEP]
obtain rfl : x = x' := by
  cases' (ae { x }).1 (by simp) with h h
  · exact singleton_injective h
  · have m : x' ∈ ({ x } : ZFSet) := by simp [h]
    rw [mem_singleton.mp m]
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x'
[PROOFSTEP]
cases' (ae { x }).1 (by simp) with h h
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ {x} = {x} ∨ {x} = {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x'}
⊢ x = x'
[PROOFSTEP]
exact singleton_injective h
[GOAL]
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x = x'
[PROOFSTEP]
have m : x' ∈ ({ x } : ZFSet) := by simp [h]
[GOAL]
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x' ∈ {x}
[PROOFSTEP]
simp [h]
[GOAL]
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
m : x' ∈ {x}
⊢ x = x'
[PROOFSTEP]
rw [mem_singleton.mp m]
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = x ∧ y = y'
[PROOFSTEP]
have he : x = y → y = y' := by
  rintro rfl
  cases' (ae { x, y' }).2 (by simp only [eq_self_iff_true, or_true_iff]) with xy'x xy'xx
  · rw [eq_comm, ← mem_singleton, ← xy'x, mem_pair]
    exact Or.inr rfl
  · simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y → y = y'
[PROOFSTEP]
rintro rfl
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y'
[PROOFSTEP]
cases' (ae { x, y' }).2 (by simp only [eq_self_iff_true, or_true_iff]) with xy'x xy'xx
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ {x, y'} = {x} ∨ {x, y'} = {x, y'}
[PROOFSTEP]
simp only [eq_self_iff_true, or_true_iff]
[GOAL]
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ x = y'
[PROOFSTEP]
rw [eq_comm, ← mem_singleton, ← xy'x, mem_pair]
[GOAL]
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ y' = x ∨ y' = y'
[PROOFSTEP]
exact Or.inr rfl
[GOAL]
case inr
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ x = y'
[PROOFSTEP]
simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp)
[GOAL]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ y' ∈ {x, y'}
[PROOFSTEP]
simp
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain xyx | xyy' := (ae { x, y }).1 (by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ {x, y} = {x} ∨ {x, y} = {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain rfl := mem_singleton.mp ((ext_iff.1 xyx y).1 <| by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
case inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyx : {y, y} = {y}
⊢ y = y ∧ y = y'
[PROOFSTEP]
simp [he rfl]
[GOAL]
case inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ x = x ∧ y = y'
[PROOFSTEP]
obtain rfl | yy' := mem_pair.mp ((ext_iff.1 xyy' y).1 <| by simp)
[GOAL]
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ y ∈ {x, y}
[PROOFSTEP]
simp
[GOAL]
case inr.inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyy' : {y, y} = {y, y'}
⊢ y = y ∧ y = y'
[PROOFSTEP]
simp [he rfl]
[GOAL]
case inr.inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
yy' : y = y'
⊢ x = x ∧ y = y'
[PROOFSTEP]
simp [yy']
[GOAL]
x y z : ZFSet
⊢ z ∈ prod x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = pair a b
[PROOFSTEP]
simp [prod]
[GOAL]
x y a b : ZFSet
⊢ pair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y
[PROOFSTEP]
simp
[GOAL]
x y f : ZFSet
⊢ f ∈ funs x y ↔ IsFunc x y f
[PROOFSTEP]
simp [funs, IsFunc]
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
⊢ y = f z
[PROOFSTEP]
let ⟨w, _, we⟩ := mem_image.1 yx
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
⊢ y = f z
[PROOFSTEP]
let ⟨wz, fy⟩ := pair_injective we
[GOAL]
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
wz : w = z
fy : f w = y
⊢ y = f z
[PROOFSTEP]
rw [← fy, wz]
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ Hereditarily p x ↔ p x ∧ ∀ (y : ZFSet), y ∈ x → Hereditarily p y
[PROOFSTEP]
rw [← Hereditarily]
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ Hereditarily p x → p ∅
[PROOFSTEP]
apply @ZFSet.inductionOn _ x
[GOAL]
p : ZFSet → Prop
x y : ZFSet
⊢ ∀ (x : ZFSet), (∀ (y : ZFSet), y ∈ x → Hereditarily p y → p ∅) → Hereditarily p x → p ∅
[PROOFSTEP]
intro y IH h
[GOAL]
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
[PROOFSTEP]
rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)
[GOAL]
case inl
p : ZFSet → Prop
x y : ZFSet
IH : ∀ (y : ZFSet), y ∈ ∅ → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅
[PROOFSTEP]
exact h.self
[GOAL]
case inr.intro
p : ZFSet → Prop
x y✝ y : ZFSet
IH : ∀ (y_1 : ZFSet), y_1 ∈ y → Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet
ha : a ∈ toSet y
⊢ p ∅
[PROOFSTEP]
exact IH a ha (h.mem ha)
[GOAL]
⊢ ∀ (a : Class), Acc (fun x x_1 => x ∈ x_1) a
[PROOFSTEP]
have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x :=
  by
  refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
  rintro A ⟨z, rfl, hz⟩
  exact IH z hz
[GOAL]
⊢ ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
[PROOFSTEP]
refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
[GOAL]
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
⊢ ∀ (y : Class), y ∈ ↑x → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro A ⟨z, rfl, hz⟩
[GOAL]
case intro.intro
a x : ZFSet
IH : ∀ (y : ZFSet), y ∈ x → Acc (fun x x_1 => x ∈ x_1) ↑y
z : ZFSet
hz : ↑x z
⊢ Acc (fun x x_1 => x ∈ x_1) ↑z
[PROOFSTEP]
exact IH z hz
[GOAL]
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
⊢ ∀ (a : Class), Acc (fun x x_1 => x ∈ x_1) a
[PROOFSTEP]
refine' fun A => ⟨A, _⟩
[GOAL]
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
⊢ ∀ (y : Class), y ∈ A → Acc (fun x x_1 => x ∈ x_1) y
[PROOFSTEP]
rintro B ⟨x, rfl, _⟩
[GOAL]
case intro.intro
H : ∀ (x : ZFSet), Acc (fun x x_1 => x ∈ x_1) ↑x
A : Class
x : ZFSet
right✝ : A x
⊢ Acc (fun x x_1 => x ∈ x_1) ↑x
[PROOFSTEP]
exact H x
[GOAL]
⊢ congToClass ∅ = ∅
[PROOFSTEP]
ext z
[GOAL]
case a
z : ZFSet
⊢ congToClass ∅ z ↔ ∅ z
[PROOFSTEP]
simp only [congToClass, not_empty_hom, iff_false_iff]
[GOAL]
case a
z : ZFSet
⊢ ¬setOf (fun y => ↑y ∈ ∅) z
[PROOFSTEP]
exact Set.not_mem_empty z
[GOAL]
⊢ classToCong ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case h
x✝ : Class
⊢ x✝ ∈ classToCong ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
simp [classToCong]
[GOAL]
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ z ∈ x ↔ z ∈ y
[PROOFSTEP]
change (x : Class.{u}) z ↔ (y : Class.{u}) z
[GOAL]
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ ↑x z ↔ ↑y z
[PROOFSTEP]
rw [h]
[GOAL]
A : Class
x : ZFSet
x✝ : ToSet A ↑x
y : ZFSet
yx : ↑y = ↑x
py : A y
⊢ A x
[PROOFSTEP]
rwa [ofSet.inj yx] at py
[GOAL]
x : Class
y : ZFSet
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
constructor
[GOAL]
case mp
x : Class
y : ZFSet
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
[GOAL]
case mp.intro.intro.intro.intro
x : Class
y z : ZFSet
hxz : x z
hyz : y ∈ ↑z
⊢ ∃ z, x z ∧ y ∈ z
[PROOFSTEP]
exact ⟨z, hxz, hyz⟩
[GOAL]
case mpr
x : Class
y : ZFSet
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y
[PROOFSTEP]
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩
[GOAL]
x y : ZFSet
⊢ (∃ z, ↑x z ∧ y ∈ z) ↔ ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
rfl
[GOAL]
x y : Class
⊢ y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : Class
⊢ y ∈ ⋃₀ x → ∃ z, z ∈ x ∧ y ∈ z
[PROOFSTEP]
rintro ⟨w, rfl, z, hzx, hwz⟩
[GOAL]
case mp.intro.intro.intro.intro
x : Class
w : ZFSet
z : Set ZFSet
hzx : z ∈ classToCong x
hwz : w ∈ z
⊢ ∃ z, z ∈ x ∧ ↑w ∈ z
[PROOFSTEP]
exact ⟨z, hzx, coe_mem.2 hwz⟩
[GOAL]
case mpr
x y : Class
⊢ (∃ z, z ∈ x ∧ y ∈ z) → y ∈ ⋃₀ x
[PROOFSTEP]
rintro ⟨w, hwx, z, rfl, hwz⟩
[GOAL]
case mpr.intro.intro.intro.intro
x w : Class
hwx : w ∈ x
z : ZFSet
hwz : w z
⊢ ↑z ∈ ⋃₀ x
[PROOFSTEP]
exact ⟨z, rfl, w, hwx, hwz⟩
[GOAL]
x : Class
y : ZFSet
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet), x z → y ∈ z
[PROOFSTEP]
refine' ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, _⟩
[GOAL]
x : Class
y : ZFSet
⊢ (∀ (z : ZFSet), x z → y ∈ z) → (⋂₀ x) y
[PROOFSTEP]
rintro H - ⟨z, rfl, hxz⟩
[GOAL]
case intro.intro
x : Class
y : ZFSet
H : ∀ (z : ZFSet), x z → y ∈ z
z : ZFSet
hxz : x z
⊢ y ∈ ↑z
[PROOFSTEP]
exact H _ hxz
[GOAL]
x y z : Class
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z
[PROOFSTEP]
obtain ⟨w, rfl, hw⟩ := hy
[GOAL]
case intro.intro
x z : Class
hz : z ∈ x
w : ZFSet
hw : (⋂₀ x) w
⊢ ↑w ∈ z
[PROOFSTEP]
exact coe_mem.2 (hw z hz)
[GOAL]
x y : Class
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ (z : Class), z ∈ x → y ∈ z
[PROOFSTEP]
refine' ⟨fun hy z => mem_of_mem_sInter hy, fun H => _⟩
[GOAL]
x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ y ∈ ⋂₀ x
[PROOFSTEP]
simp_rw [mem_def, sInter_apply]
[GOAL]
x y : Class
h : Set.Nonempty x
H : ∀ (z : Class), z ∈ x → y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
obtain ⟨z, hz⟩ := h
[GOAL]
case intro
x y : Class
H : ∀ (z : Class), z ∈ x → y ∈ z
z : ZFSet
hz : z ∈ x
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
[GOAL]
case intro.intro.intro
x : Class
z : ZFSet
hz : z ∈ x
y : ZFSet
right✝ : ↑z y
H : ∀ (z : Class), z ∈ x → ↑y ∈ z
⊢ ∃ x_1, ↑x_1 = ↑y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
[PROOFSTEP]
refine' ⟨y, rfl, fun w hxw => _⟩
[GOAL]
case intro.intro.intro
x : Class
z : ZFSet
hz : z ∈ x
y : ZFSet
right✝ : ↑z y
H : ∀ (z : Class), z ∈ x → ↑y ∈ z
w : ZFSet
hxw : x w
⊢ y ∈ w
[PROOFSTEP]
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)
[GOAL]
⊢ ⋃₀ ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
z✝ : ZFSet
⊢ (⋃₀ ∅) z✝ ↔ ∅ z✝
[PROOFSTEP]
simp
[GOAL]
⊢ ⋂₀ ∅ = univ
[PROOFSTEP]
rw [sInter, classToCong_empty, Set.sInter_empty, univ]
[GOAL]
A : Class
hA : powerset A ⊆ A
⊢ ∀ (x : ZFSet), A x
[PROOFSTEP]
by_contra' hnA
[GOAL]
A : Class
hA : powerset A ⊆ A
hnA : ∃ x, ¬A x
⊢ False
[PROOFSTEP]
exact
  WellFounded.min_mem ZFSet.mem_wf _ hnA
    (hA fun x hx => Classical.not_not.1 fun hB => WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx)
[GOAL]
A : Class
x : ZFSet
H : ∀ (y : ZFSet), A y ↔ y = x
y : ZFSet
x✝ : iota A y
x' : ZFSet
h : setOf (fun x => ∀ (y : ZFSet), A y ↔ y = x) x'
yx' : y ∈ ↑x'
⊢ ↑x y
[PROOFSTEP]
rwa [← (H x').1 <| (h x').2 rfl]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ Class.ToSet (fun x_1 => ↑(map f x) (pair x_1 z)) ↑y ↔ z = f y
[PROOFSTEP]
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
⊢ (∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z) ↔ z = f y
[PROOFSTEP]
exact
  ⟨fun ⟨w, _, pr⟩ => by
    let ⟨wy, fw⟩ := ZFSet.pair_injective pr
    rw [← fw, wy], fun e => by
    subst e
    exact ⟨_, h, rfl⟩⟩
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
⊢ z = f y
[PROOFSTEP]
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
x✝ : ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
w : ZFSet
left✝ : w ∈ x
pr : pair w (f w) = pair y z
wy : w = y
fw : f w = z
⊢ z = f y
[PROOFSTEP]
rw [← fw, wy]
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
z : ZFSet
e : z = f y
⊢ ∃ z_1, z_1 ∈ x ∧ pair z_1 (f z_1) = pair y z
[PROOFSTEP]
subst e
[GOAL]
f : ZFSet → ZFSet
H : PSet.Definable 1 f
x y : ZFSet
h : y ∈ x
⊢ ∃ z, z ∈ x ∧ pair z (f z) = pair y (f y)
[PROOFSTEP]
exact ⟨_, h, rfl⟩
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ ∅ ∈ x
[PROOFSTEP]
rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(choice x) ′ ↑y ∈ ↑y
[PROOFSTEP]
delta choice
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y
[PROOFSTEP]
rw [@map_fval _ (Classical.allDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
[GOAL]
x : ZFSet
h : ¬∅ ∈ x
y : ZFSet
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y
[PROOFSTEP]
exact choice_mem_aux x h y yx


[GOAL]
n : ℕ
⊢ LeftMoves (powHalf n) = PUnit
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ LeftMoves (powHalf Nat.zero) = PUnit
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ LeftMoves (powHalf (Nat.succ n✝)) = PUnit
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
i : LeftMoves (powHalf n)
⊢ moveLeft (powHalf n) i = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
i : LeftMoves (powHalf Nat.zero)
⊢ moveLeft (powHalf Nat.zero) i = 0
[PROOFSTEP]
cases i
[GOAL]
case succ
n✝ : ℕ
i : LeftMoves (powHalf (Nat.succ n✝))
⊢ moveLeft (powHalf (Nat.succ n✝)) i = 0
[PROOFSTEP]
cases i
[GOAL]
case zero.unit
⊢ moveLeft (powHalf Nat.zero) PUnit.unit = 0
[PROOFSTEP]
rfl
[GOAL]
case succ.unit
n✝ : ℕ
⊢ moveLeft (powHalf (Nat.succ n✝)) PUnit.unit = 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Unique (LeftMoves (powHalf n))
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Unique (LeftMoves (powHalf Nat.zero))
[PROOFSTEP]
exact PUnit.unique
[GOAL]
case succ
n✝ : ℕ
⊢ Unique (LeftMoves (powHalf (Nat.succ n✝)))
[PROOFSTEP]
exact PUnit.unique
[GOAL]
⊢ birthday (powHalf 1) = 2
[PROOFSTEP]
rw [birthday_def]
[GOAL]
⊢ max (Ordinal.lsub fun i => birthday (moveLeft (powHalf 1) i))
      (Ordinal.lsub fun i => birthday (moveRight (powHalf 1) i)) =
    2
[PROOFSTEP]
dsimp
[GOAL]
⊢ max (Ordinal.lsub fun i => birthday (moveLeft (powHalf 1) i)) (Ordinal.lsub fun i => birthday 1) = 2
[PROOFSTEP]
simpa using Order.le_succ (1 : Ordinal)
[GOAL]
n : ℕ
⊢ Numeric (powHalf n)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ Numeric (powHalf Nat.zero)
[PROOFSTEP]
exact numeric_one
[GOAL]
case succ
n : ℕ
hn : Numeric (powHalf n)
⊢ Numeric (powHalf (Nat.succ n))
[PROOFSTEP]
constructor
[GOAL]
case succ.left
n : ℕ
hn : Numeric (powHalf n)
⊢ ∀ (i j : PUnit), OfNat.ofNat 0 i < (fun x => powHalf n) j
[PROOFSTEP]
simpa using hn.moveLeft_lt default
[GOAL]
case succ.right
n : ℕ
hn : Numeric (powHalf n)
⊢ (∀ (i : PUnit), Numeric (OfNat.ofNat 0 i)) ∧ ∀ (j : PUnit), Numeric ((fun x => powHalf n) j)
[PROOFSTEP]
exact ⟨fun _ => numeric_zero, fun _ => hn⟩
[GOAL]
n : ℕ
⊢ powHalf n ≤ 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ powHalf Nat.zero ≤ 1
[PROOFSTEP]
exact le_rfl
[GOAL]
case succ
n : ℕ
hn : powHalf n ≤ 1
⊢ powHalf (Nat.succ n) ≤ 1
[PROOFSTEP]
exact (powHalf_succ_le_powHalf n).trans hn
[GOAL]
n : ℕ
⊢ 0 < powHalf n
[PROOFSTEP]
rw [← lf_iff_lt numeric_zero (numeric_powHalf n), zero_lf_le]
[GOAL]
n : ℕ
⊢ ∃ i, 0 ≤ moveLeft (powHalf n) i
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hn
[GOAL]
case h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
[PROOFSTEP]
constructor
[GOAL]
case h.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (n + 1) + powHalf (n + 1) ≤ powHalf n
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
case h.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ≤ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
rw [le_iff_forall_lf]
[GOAL]
case h.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (∀ (i : LeftMoves (powHalf (n + 1) + powHalf (n + 1))), moveLeft (powHalf (n + 1) + powHalf (n + 1)) i ⧏ powHalf n) ∧
    ∀ (j : RightMoves (powHalf n)), powHalf (n + 1) + powHalf (n + 1) ⧏ moveRight (powHalf n) j
[PROOFSTEP]
constructor
[GOAL]
case h.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ (∀ (i : LeftMoves (powHalf n)), moveLeft (powHalf n) i ⧏ powHalf (n + 1) + powHalf (n + 1)) ∧
    ∀ (j : RightMoves (powHalf (n + 1) + powHalf (n + 1))), powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) j
[PROOFSTEP]
constructor
[GOAL]
case h.left.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : LeftMoves (powHalf (n + 1) + powHalf (n + 1))), moveLeft (powHalf (n + 1) + powHalf (n + 1)) i ⧏ powHalf n
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
[GOAL]
case h.left.left.inl.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit) ⧏ powHalf n
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.left.left.inr.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit) ⧏ powHalf n
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.left.left.inl.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit) < powHalf n
[PROOFSTEP]
calc
  0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n
[GOAL]
case h.left.left.inr.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveLeft (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit) < powHalf n
[PROOFSTEP]
calc
  powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _
  _ < powHalf n := powHalf_succ_lt_powHalf n
[GOAL]
case h.left.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf n)), powHalf (n + 1) + powHalf (n + 1) ⧏ moveRight (powHalf n) j
[PROOFSTEP]
cases' n with n
[GOAL]
case h.left.right.zero
hn : ∀ (m : ℕ), m < Nat.zero → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf Nat.zero)),
    powHalf (Nat.zero + 1) + powHalf (Nat.zero + 1) ⧏ moveRight (powHalf Nat.zero) j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.left.right.succ
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf (Nat.succ n))),
    powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1) ⧏ moveRight (powHalf (Nat.succ n)) j
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.left.right.succ.unit
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1) ⧏ moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
apply lf_of_moveRight_le
[GOAL]
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) ?h.left.right.succ.unit.j ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ RightMoves (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1))
[PROOFSTEP]
swap
[GOAL]
case h.left.right.succ.unit.j
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ RightMoves (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1))
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) ?h.left.right.succ.unit.j ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
exact Sum.inl default
[GOAL]
case h.left.right.succ.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < Nat.succ n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ moveRight (powHalf (Nat.succ n + 1) + powHalf (Nat.succ n + 1)) (Sum.inl default) ≤
    moveRight (powHalf (Nat.succ n)) PUnit.unit
[PROOFSTEP]
calc
  powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ :=
    add_le_add_left (powHalf_succ_le_powHalf _) _
  _ ≈ powHalf n := hn _ (Nat.lt_succ_self n)
[GOAL]
case h.right.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (i : LeftMoves (powHalf n)), moveLeft (powHalf n) i ⧏ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
simp only [powHalf_moveLeft, forall_const]
[GOAL]
case h.right.left
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 ⧏ powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.left.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ 0 < powHalf (n + 1) + powHalf (n + 1)
[PROOFSTEP]
calc
  0 ≈ 0 + 0 := (Equiv.symm (add_zero_equiv 0))
  _ ≤ powHalf n.succ + 0 := (add_le_add_right (zero_le_powHalf _) _)
  _ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
[GOAL]
case h.right.right
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ ∀ (j : RightMoves (powHalf (n + 1) + powHalf (n + 1))), powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) j
[PROOFSTEP]
rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
[GOAL]
case h.right.right.inl.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.right.inr.unit
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n ⧏ moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit)
[PROOFSTEP]
apply lf_of_lt
[GOAL]
case h.right.right.inl.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inl PUnit.unit)
[PROOFSTEP]
calc
  powHalf n ≈ powHalf n + 0 := (Equiv.symm (add_zero_equiv _))
  _ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _
[GOAL]
case h.right.right.inr.unit.h
n : ℕ
hn : ∀ (m : ℕ), m < n → powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m
⊢ powHalf n < moveRight (powHalf (n + 1) + powHalf (n + 1)) (Sum.inr PUnit.unit)
[PROOFSTEP]
calc
  powHalf n ≈ 0 + powHalf n := (Equiv.symm (zero_add_equiv _))
  _ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _
[GOAL]
n : ℕ
⊢ 2 • powHalf (Nat.succ n) = powHalf n
[PROOFSTEP]
rw [two_nsmul]
[GOAL]
n : ℕ
⊢ powHalf (Nat.succ n) + powHalf (Nat.succ n) = powHalf n
[PROOFSTEP]
exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)
[GOAL]
n : ℕ
⊢ 2 ^ n • powHalf n = 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
⊢ 2 ^ Nat.zero • powHalf Nat.zero = 1
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, powHalf_zero, one_smul]
[GOAL]
case succ
n : ℕ
hn : 2 ^ n • powHalf n = 1
⊢ 2 ^ Nat.succ n • powHalf (Nat.succ n) = 1
[PROOFSTEP]
rw [← hn, ← double_powHalf_succ_eq_powHalf n, smul_smul (2 ^ n) 2 (powHalf n.succ), mul_comm, pow_succ]
[GOAL]
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case zero
n : ℕ
⊢ 2 ^ n • powHalf (n + Nat.zero) = powHalf Nat.zero
[PROOFSTEP]
simp only [add_zero, Surreal.nsmul_pow_two_powHalf, Nat.zero_eq, eq_self_iff_true, Surreal.powHalf_zero]
[GOAL]
case succ
n k : ℕ
hk : 2 ^ n • powHalf (n + k) = powHalf k
⊢ 2 ^ n • powHalf (n + Nat.succ k) = powHalf (Nat.succ k)
[PROOFSTEP]
rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k, smul_algebra_smul_comm] at hk
[GOAL]
case succ
n k : ℕ
hk : 2 • 2 ^ n • powHalf (Nat.succ (n + k)) = 2 • powHalf (Nat.succ k)
⊢ 2 ^ n • powHalf (n + Nat.succ k) = powHalf (Nat.succ k)
[PROOFSTEP]
rwa [← zsmul_eq_zsmul_iff' two_ne_zero]
[GOAL]
m : ℤ
n k : ℕ
⊢ (m * 2 ^ n) • powHalf (n + k) = m • powHalf k
[PROOFSTEP]
rw [mul_zsmul]
[GOAL]
m : ℤ
n k : ℕ
⊢ m • 2 ^ n • powHalf (n + k) = m • powHalf k
[PROOFSTEP]
congr
[GOAL]
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
norm_cast
[GOAL]
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n • powHalf (n + k) = powHalf k
[PROOFSTEP]
exact nsmul_pow_two_powHalf' n k
[GOAL]
m₁ m₂ : ℤ
y₁ y₂ : ℕ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
revert m₁ m₂
[GOAL]
y₁ y₂ : ℕ
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
wlog h : y₁ ≤ y₂
[GOAL]
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
h : ¬y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
intro m₁ m₂ aux
[GOAL]
case inr
y₁ y₂ : ℕ
this : ∀ {y₁ y₂ : ℕ}, y₁ ≤ y₂ → ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
h : ¬y₁ ≤ y₂
m₁ m₂ : ℤ
aux : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
exact (this (le_of_not_le h) aux.symm).symm
[GOAL]
y₁ y₂ : ℕ
h : y₁ ≤ y₂
⊢ ∀ {m₁ m₂ : ℤ}, m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂ → m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
intro m₁ m₂ h₂
[GOAL]
y₁ y₂ : ℕ
h : y₁ ≤ y₂
m₁ m₂ : ℤ
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ y₂
⊢ m₁ • powHalf y₂ = m₂ • powHalf y₁
[PROOFSTEP]
obtain ⟨c, rfl⟩ := le_iff_exists_add.mp h
[GOAL]
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ * 2 ^ y₁ = m₂ * 2 ^ (y₁ + c)
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
rw [add_comm, pow_add, ← mul_assoc, mul_eq_mul_right_iff] at h₂
[GOAL]
case intro
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c ∨ 2 ^ y₁ = 0
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
cases' h₂ with h₂ h₂
[GOAL]
case intro.inl
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : m₁ = m₂ * 2 ^ c
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
rw [h₂, add_comm, zsmul_pow_two_powHalf m₂ c y₁]
[GOAL]
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
have := Nat.one_le_pow y₁ 2 Nat.succ_pos'
[GOAL]
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
h₂ : 2 ^ y₁ = 0
this : 1 ≤ 2 ^ y₁
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
norm_cast at h₂
[GOAL]
case intro.inr
y₁ : ℕ
m₁ m₂ : ℤ
c : ℕ
h : y₁ ≤ y₁ + c
this : 1 ≤ 2 ^ y₁
h₂ : 2 ^ y₁ = 0
⊢ m₁ • powHalf (y₁ + c) = m₂ • powHalf y₁
[PROOFSTEP]
linarith
[GOAL]
x : Localization.Away 2
⊢ ∀ {a c : ℤ} {b d : { x // x ∈ Submonoid.powers 2 }},
    ↑(Localization.r (Submonoid.powers 2)) (a, b) (c, d) → a • powHalf (Submonoid.log b) = c • powHalf (Submonoid.log d)
[PROOFSTEP]
intro m₁ m₂ n₁ n₂ h₁
[GOAL]
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨⟨n₃, y₃, hn₃⟩, h₂⟩ := Localization.r_iff_exists.mp h₁
[GOAL]
case intro.mk.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h₂ :
  ↑{ val := n₃, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = n₃) } * (↑(m₂, n₂).snd * (m₁, n₁).fst) =
    ↑{ val := n₃, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = n₃) } * (↑(m₁, n₁).snd * (m₂, n₂).fst)
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
simp only [Subtype.coe_mk, mul_eq_mul_left_iff] at h₂
[GOAL]
case intro.mk.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h₂ : ↑n₂ * m₁ = ↑n₁ * m₂ ∨ n₃ = 0
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
cases h₂
[GOAL]
case intro.mk.intro.inl
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨a₁, ha₁⟩ := n₁.prop
[GOAL]
case intro.mk.intro.inl.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : (fun x x_1 => x ^ x_1) 2 a₁ = ↑n₁
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
obtain ⟨a₂, ha₂⟩ := n₂.prop
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : (fun x x_1 => x ^ x_1) 2 a₁ = ↑n₁
a₂ : ℕ
ha₂ : (fun x x_1 => x ^ x_1) 2 a₂ = ↑n₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
simp only at ha₁ ha₂ ⊢
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have hn₁ : n₁ = Submonoid.pow 2 a₁ := Subtype.ext ha₁.symm
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have hn₂ : n₂ = Submonoid.pow 2 a₂ := Subtype.ext ha₂.symm
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
rw [hn₁, hn₂, Submonoid.log_pow_int_eq_self h₂, Submonoid.log_pow_int_eq_self h₂]
[GOAL]
case intro.mk.intro.inl.intro.intro
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ • powHalf a₁ = m₂ • powHalf a₂
[PROOFSTEP]
apply dyadic_aux
[GOAL]
case intro.mk.intro.inl.intro.intro.h₂
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : ↑n₂ * m₁ = ↑n₁ * m₂
a₁ : ℕ
ha₁ : 2 ^ a₁ = ↑n₁
a₂ : ℕ
ha₂ : 2 ^ a₂ = ↑n₂
hn₁ : n₁ = Submonoid.pow 2 a₁
hn₂ : n₂ = Submonoid.pow 2 a₂
h₂ : 1 < Int.natAbs 2
⊢ m₁ * 2 ^ a₂ = m₂ * 2 ^ a₁
[PROOFSTEP]
rwa [ha₁, ha₂, mul_comm, mul_comm m₂]
[GOAL]
case intro.mk.intro.inr
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
have : (1 : ℤ) ≤ 2 ^ y₃ := by exact_mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
[GOAL]
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
⊢ 1 ≤ 2 ^ y₃
[PROOFSTEP]
exact_mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
[GOAL]
case intro.mk.intro.inr
x : Localization.Away 2
m₁ m₂ : ℤ
n₁ n₂ : { x // x ∈ Submonoid.powers 2 }
h₁ : ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂)
n₃ : ℤ
y₃ : ℕ
hn₃ : (fun x x_1 => x ^ x_1) 2 y₃ = n₃
h✝ : n₃ = 0
this : 1 ≤ 2 ^ y₃
⊢ m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)
[PROOFSTEP]
linarith
[GOAL]
x y : Localization.Away 2
⊢ ∀ (x y : ℤ × { x // x ∈ Submonoid.powers 2 }),
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk x.fst x.snd + Localization.mk y.fst y.snd) =
      ZeroHom.toFun
          {
            toFun := fun x =>
              Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
            map_zero' :=
              (_ :
                Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                    (_ :
                      ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                        ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                          m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                  0 • powHalf (Submonoid.log 1)) }
          (Localization.mk x.fst x.snd) +
        ZeroHom.toFun
          {
            toFun := fun x =>
              Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
            map_zero' :=
              (_ :
                Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                    (_ :
                      ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                        ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                          m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                  0 • powHalf (Submonoid.log 1)) }
          (Localization.mk y.fst y.snd)
[PROOFSTEP]
rintro ⟨a, ⟨b, ⟨b', rfl⟩⟩⟩ ⟨c, ⟨d, ⟨d', rfl⟩⟩⟩
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
have hpow₂ := Submonoid.log_pow_int_eq_self h₂
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log (Submonoid.pow 2 m) = m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
simp_rw [Submonoid.pow_apply] at hpow₂
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ ZeroHom.toFun
      {
        toFun := fun x =>
          Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
            (_ :
              ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                  m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
        map_zero' :=
          (_ :
            Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                (_ :
                  ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                    ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                      m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
              0 • powHalf (Submonoid.log 1)) }
      (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd +
        Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd) =
    ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).fst
          (a,
              { val := (fun x x_1 => x ^ x_1) 2 b',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 b') }).snd) +
      ZeroHom.toFun
        {
          toFun := fun x =>
            Localization.liftOn x (fun x y => x • powHalf (Submonoid.log y))
              (_ :
                ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                  ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                    m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)),
          map_zero' :=
            (_ :
              Localization.liftOn 0 (fun x y => x • powHalf (Submonoid.log y))
                  (_ :
                    ∀ {m₁ m₂ : ℤ} {n₁ n₂ : { x // x ∈ Submonoid.powers 2 }},
                      ↑(Localization.r (Submonoid.powers 2)) (m₁, n₁) (m₂, n₂) →
                        m₁ • powHalf (Submonoid.log n₁) = m₂ • powHalf (Submonoid.log n₂)) =
                0 • powHalf (Submonoid.log 1)) }
        (Localization.mk
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).fst
          (c,
              { val := (fun x x_1 => x ^ x_1) 2 d',
                property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = (fun x x_1 => x ^ x_1) 2 d') }).snd)
[PROOFSTEP]
simp_rw [Localization.add_mk, Localization.liftOn_mk, Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂]
[GOAL]
case mk.mk.intro.mk.mk.intro
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = a • powHalf b' + c • powHalf d'
[PROOFSTEP]
calc
  (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') :=
    by simp only [add_smul, mul_comm, add_comm]
  _ = c • powHalf d' + a • powHalf b' := by simp only [zsmul_pow_two_powHalf]
  _ = a • powHalf b' + c • powHalf d' := add_comm _ _
[GOAL]
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b')
[PROOFSTEP]
simp only [add_smul, mul_comm, add_comm]
[GOAL]
x y : Localization.Away 2
a : ℤ
b' : ℕ
c : ℤ
d' : ℕ
h₂ : 1 < Int.natAbs 2
hpow₂ : ∀ (m : ℕ), Submonoid.log { val := 2 ^ m, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) 2 y = 2 ^ m) } = m
⊢ (c * 2 ^ b') • powHalf (b' + d') + (a * 2 ^ d') • powHalf (d' + b') = c • powHalf d' + a • powHalf b'
[PROOFSTEP]
simp only [zsmul_pow_two_powHalf]
[GOAL]
m : ℤ
p : { x // x ∈ Submonoid.powers 2 }
⊢ ↑dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m p) = m • powHalf (Submonoid.log p)
[PROOFSTEP]
rw [← Localization.mk_eq_mk']
[GOAL]
m : ℤ
p : { x // x ∈ Submonoid.powers 2 }
⊢ ↑dyadicMap (Localization.mk m p) = m • powHalf (Submonoid.log p)
[PROOFSTEP]
rfl
[GOAL]
m : ℤ
n : ℕ
⊢ ↑dyadicMap (IsLocalization.mk' (Localization (Submonoid.powers 2)) m (Submonoid.pow 2 n)) = m • powHalf n
[PROOFSTEP]
rw [dyadicMap_apply, @Submonoid.log_pow_int_eq_self 2 one_lt_two]
[GOAL]
m : ℤ
n : ℕ
⊢ m • powHalf (Submonoid.log (Submonoid.pow 2 n)) = m • powHalf n
[PROOFSTEP]
rw [@Submonoid.log_pow_int_eq_self 2 one_lt_two]


[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
⊢ (dite p a fun hp => dite q (b hp) (c hp)) = if hq : q then dite p a fun hp => b hp hq else dite p a fun hp => c hp hq
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ = a h✝¹
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : p
h✝ : ¬q
⊢ a h✝¹ = a h✝¹
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : q
⊢ b h✝¹ h✝ = b h✝¹ (_ : q)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ h✝ = c h✝¹ (_ : ¬q)
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
⊢ dite p (fun hp => dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun hp => a hp hq) c else dite p (fun hp => b hp hq) c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : q
⊢ a h✝¹ h✝ = a h✝¹ (_ : q)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : p
h✝ : ¬q
⊢ b h✝¹ h✝ = b h✝¹ (_ : ¬q)
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : q
⊢ c h✝¹ = c h✝¹
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a✝ b✝ c✝ : α
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h✝¹ : ¬p
h✝ : ¬q
⊢ c h✝¹ = c h✝¹
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
⊢ f True ∧ f False → ∀ (p : Prop), f p
[PROOFSTEP]
rintro ⟨h₁, h₀⟩ p
[GOAL]
case intro
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p
[PROOFSTEP]
by_cases hp : p
[GOAL]
case pos
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f p
[PROOFSTEP]
simp only [hp]
[GOAL]
case neg
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f p
[PROOFSTEP]
simp only [hp]
[GOAL]
case pos
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True
[PROOFSTEP]
assumption
[GOAL]
case neg
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False
[PROOFSTEP]
assumption
[GOAL]
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False
[PROOFSTEP]
refine' (em p).imp _ _
[GOAL]
case refine'_1
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True
[PROOFSTEP]
intro H
[GOAL]
case refine'_2
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False
[PROOFSTEP]
intro H
[GOAL]
case refine'_1
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True
[PROOFSTEP]
convert h
[GOAL]
case refine'_2
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1.a
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p
[PROOFSTEP]
simp [H]
[GOAL]
case h.e'_1.a
α : Sort u_1
p✝ q r : Prop
inst✝¹ : Decidable p✝
inst✝ : Decidable q
a b c : α
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p
[PROOFSTEP]
simp [H]
[GOAL]
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
⊢ f True ∨ f False → ∃ p, f p
[PROOFSTEP]
rintro (h | h)
[GOAL]
case inl
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h : f True
⊢ ∃ p, f p
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
case inr
α : Sort u_1
p q r : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
a b c : α
f : Prop → Prop
h : f False
⊢ ∃ p, f p
[PROOFSTEP]
exact ⟨_, h⟩


[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
h : Nonempty α
inst✝ : IsEmpty β
⊢ IsEmpty (α → β)
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p : Prop
⊢ IsEmpty p ↔ ¬p
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_Prop]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)
[PROOFSTEP]
simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Type u_5
E : α → Type u_4
⊢ IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_sigma, not_exists]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_psigma, not_exists]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
p : α → Prop
⊢ IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_subtype, not_exists]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_prod, not_and_or]
[GOAL]
α : Sort u_1
β : Sort u_2
γ : Sort u_3
⊢ IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_sum, not_or]
[GOAL]
α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_psum, not_or]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Type u_4
⊢ IsEmpty (ULift α) ↔ IsEmpty α
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_ulift]
[GOAL]
α✝ : Sort u_1
β : Sort u_2
γ : Sort u_3
α : Sort u_4
⊢ IsEmpty (PLift α) ↔ IsEmpty α
[PROOFSTEP]
simp only [← not_nonempty_iff, nonempty_plift]