α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (?u.60636 + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
⊢ False
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (?u.60636 + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
⊢ False
let f : ι → Cardinal := Subtype.val
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
⊢ False
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (?u.60636 + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
⊢ False
haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
case intro.mk.intro
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
c : Cardinal
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
case intro.mk.intro
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
c : Cardinal
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
⊢ False
refine hc (Acc.intro _ fun j h' => byContradiction fun hj => h'.2 ?_)
case intro.mk.intro
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
c : Cardinal
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
this : (#Quotient.out (f { val := c, property := hc })) ≤ (#Quotient.out (f { val := j, property := hj }))
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
case intro.mk.intro
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
c : Cardinal
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
have : (#_) ≤ (#_) := ⟨h_1 ⟨j, hj⟩⟩
no goals
case intro.mk.intro
α β : Type u
a : Cardinal
h : ¬Acc (fun x x_1 => x < x_1) a
ι : Type (u + 1) := { c // ¬Acc (fun x x_1 => x < x_1) c }
f : ι → Cardinal := Subtype.val
hι : Nonempty ι
c : Cardinal
hc : ¬Acc (fun x x_1 => x < x_1) c
h_1 : (j : ι) → Quotient.out (f { val := c, property := hc }) ↪ Quotient.out (f j)
j : Cardinal
h' : j < c
hj : ¬Acc (fun x x_1 => x < x_1) j
this : (#Quotient.out (f { val := c, property := hc })) ≤ (#Quotient.out (f { val := j, property := hj }))
⊢ Quotient.liftOn₂ c j (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
simpa only [mk_out] using this