α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
⊢ ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → (fun s => s ⊆ S → C s) s → (fun s => s ⊆ S → C s) (insert a s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
⊢ C S
refine' @Set.Finite.induction_on α (fun s => s ⊆ S → C s) S h (fun _ => H0) _ Subset.rfl
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : insert a s ⊆ S
⊢ C (insert a s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
⊢ ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → (fun s => s ⊆ S → C s) s → (fun s => s ⊆ S → C s) (insert a s)
intro a s has _ hCs haS
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : a ∈ S ∧ s ⊆ S
⊢ C (insert a s)
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : insert a s ⊆ S
⊢ C (insert a s)
rw [insert_subset] at haS
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
C : Set α → Prop
S : Set α
h : Set.Finite S
H0 : C ∅
H1 : ∀ {a : α} {s : Set α}, a ∈ S → s ⊆ S → ¬a ∈ s → C s → C (insert a s)
a : α
s : Set α
has : ¬a ∈ s
a✝ : Set.Finite s
hCs : s ⊆ S → C s
haS : a ∈ S ∧ s ⊆ S
⊢ C (insert a s)
exact H1 haS.1 haS.2 has (hCs haS.2)