case inl
α : Type u_1
β : Type ?u.153618
t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite ∅) _auto✝
⊢ ncard ∅ ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}

case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ ncard s ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ ncard s ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
rw [ncard_le_one_iff hs]
case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
refine' ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, _⟩
case inr.intro.inl
α : Type u_1
β : Type ?u.153618
t : Set α
a b x✝ y : α
f : α → β
x : α
hs : autoParam (Set.Finite ∅) _auto✝
hx : x ∈ ∅
⊢ ∀ {a b : α}, a ∈ ∅ → b ∈ ∅ → a = b

case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a✝ b x✝ y : α
f : α → β
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x ∈ {a}
⊢ ∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b
case inr.intro
α : Type u_1
β : Type ?u.153618
s t : Set α
a b x✝ y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
rintro (rfl | ⟨a, rfl⟩)
case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a✝ b x✝ y : α
f : α → β
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x = a
⊢ ∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b
case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a✝ b x✝ y : α
f : α → β
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x ∈ {a}
⊢ ∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b
simp_rw [mem_singleton_iff] at hx⊢
case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a b x✝ y : α
f : α → β
x : α
hs : autoParam (Set.Finite {x}) _auto✝
⊢ ∀ {a b : α}, a = x → b = x → a = b
case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a✝ b x✝ y : α
f : α → β
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x = a
⊢ ∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b
subst hx
no goals
case inr.intro.inr.intro
α : Type u_1
β : Type ?u.153618
t : Set α
a b x✝ y : α
f : α → β
x : α
hs : autoParam (Set.Finite {x}) _auto✝
⊢ ∀ {a b : α}, a = x → b = x → a = b
simp only [forall_eq_apply_imp_iff', imp_self, implies_true]
no goals
case inl
α : Type u_1
β : Type ?u.153618
t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite ∅) _auto✝
⊢ ncard ∅ ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}
exact iff_of_true (by simp) (Or.inl rfl)
no goals
α : Type u_1
β : Type ?u.153618
t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite ∅) _auto✝
⊢ ncard ∅ ≤ 1
simp
no goals
case inr.intro.inl
α : Type u_1
β : Type ?u.153618
t : Set α
a b x✝ y : α
f : α → β
x : α
hs : autoParam (Set.Finite ∅) _auto✝
hx : x ∈ ∅
⊢ ∀ {a b : α}, a ∈ ∅ → b ∈ ∅ → a = b
exact (not_mem_empty _ hx).elim