α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ ncard (s \ {a}) + 1 = ncard s
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) + 1 = ncard s
have h' : a ∉ s \ {a} := by rw [mem_diff_singleton]; tauto
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ ncard (insert a (s \ {a})) = ncard s
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ ncard (s \ {a}) + 1 = ncard s
rw [← ncard_insert_of_not_mem h' (hs.diff {a})]
case e_s
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ insert a (s \ {a}) = s
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ ncard (insert a (s \ {a})) = ncard s
congr
no goals
case e_s
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
h' : ¬a ∈ s \ {a}
⊢ insert a (s \ {a}) = s
simpa
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬(a ∈ s ∧ a ≠ a)
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬a ∈ s \ {a}
rw [mem_diff_singleton]
no goals
α : Type u_1
β : Type ?u.13732
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬(a ∈ s ∧ a ≠ a)
tauto