-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
/-- Induction principle for finset families. To prove a statement for every finset family,
it suffices to prove it for
* the empty finset family.
* the finset family which only contains the empty finset.
* `ℬ ∪ {s ∪ {a} | s ∈ 𝒞}` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the
  ground type and `𝒜` and `ℬ` are families of finsets not containing `a`.
  Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you
  `𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, so that `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.

This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.

See also `Finset.family_induction_on.` -/
@[elab_as_elim]
lemma memberFamily_induction_on {p : Finset (Finset α) → Prop}
    (𝒜 : Finset (Finset α)) (empty : p ∅) (singleton_empty : p {∅})
    (subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
      p (𝒜.nonMemberSubfamily a) → p (𝒜.memberSubfamily a) → p 𝒜) : p 𝒜

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ ∅
⊢ p 𝒜

Tactic:
simp_rw [subset_empty] at hu

Result:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s = ∅
⊢ p 𝒜

Proof state:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ p 𝒜

Tactic:
obtain rfl | rfl := hu <;> assumption

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ p 𝒜

Tactic:
refine subfamily a (ih _ ?_) (ih _ ?_)

Result:
case insert.refine_1
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u

case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜

Tactic:
clear_value u

Result:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜

Proof state:
case insert
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a✝¹ : α
s✝ : Finset α
a✝ : a✝¹ ∉ s✝
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ s✝) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a✝¹ s✝
⊢ p 𝒜

Tactic:
rename_i a u _

Result:
case insert
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ p 𝒜

Proof state:
case insert.refine_1
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ 𝒜, a ∉ s → s ⊆ u

Tactic:
exact fun s hs has ↦ (subset_insert_iff_of_not_mem has).1 <| hu _ hs

Result:
no goals

Proof state:
case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u

Tactic:
exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
⊢ p 𝒜

Tactic:
have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)

Result:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
hu : ∀ s ∈ 𝒜, s ⊆ u
⊢ p 𝒜

Proof state:
case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u

Tactic:
simp only [mem_memberSubfamily, and_imp]

Result:
case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ (s : Finset α), insert a s ∈ 𝒜 → a ∉ s → s ⊆ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p 𝒜

Tactic:
set u := 𝒜.sup id

Result:
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
u : Finset α := 𝒜.sup id
⊢ p 𝒜