-- Mathlib/Order/Filter/Finite.lean
theorem iInf_sets_induct {f : ι → Filter α} {s : Set α} (hs : s ∈ iInf f) {p : Set α → Prop}
    (uni : p univ) (ins : ∀ {i s₁ s₂}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)) : p s

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Tactic:
rw [mem_iInf_finite'] at hs

Result:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : ∃ t, s ∈ ⨅ i ∈ t, f i.down
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Proof state:
case intro.insert.intro.intro.intro.intro
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
a✝¹ : PLift ι
s✝ : Finset (PLift ι)
a✝ : a✝¹ ∉ s✝
ih : ∀ {s : Set α}, (s ∈ s✝.inf fun a => f a.down) → p s
s₁ : Set α
hs₁ : s₁ ∈ f a✝¹.down
s₂ : Set α
hs₂ : s₂ ∈ s✝.inf fun a => f a.down
⊢ p (s₁ ∩ s₂)

Tactic:
exact ins hs₁ (ih hs₂)

Result:
no goals

Proof state:
case intro.insert
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
a✝¹ : PLift ι
s✝ : Finset (PLift ι)
a✝ : a✝¹ ∉ s✝
ih : ∀ {s : Set α}, (s ∈ s✝.inf fun a => f a.down) → p s
s : Set α
his : s ∈ (insert a✝¹ s✝).inf fun a => f a.down
⊢ p s

Tactic:
rw [Finset.inf_insert, mem_inf_iff] at his

Result:
case intro.insert
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
a✝¹ : PLift ι
s✝ : Finset (PLift ι)
a✝ : a✝¹ ∉ s✝
ih : ∀ {s : Set α}, (s ∈ s✝.inf fun a => f a.down) → p s
s : Set α
his : ∃ t₁ ∈ f a✝¹.down, ∃ t₂ ∈ s✝.inf fun a => f a.down, s = t₁ ∩ t₂
⊢ p s

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Tactic:
classical
rw [mem_iInf_finite'] at hs
simp only [← Finset.inf_eq_iInf] at hs
rcases hs with ⟨is, his⟩
induction is using Finset.induction_on generalizing s with
| empty => rwa [mem_top.1 his]
| insert _ ih =>
  rw [Finset.inf_insert, mem_inf_iff] at his
  rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩
  exact ins hs₁ (ih hs₂)

Result:
no goals

Proof state:
case intro.insert
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
a✝¹ : PLift ι
s✝ : Finset (PLift ι)
a✝ : a✝¹ ∉ s✝
ih : ∀ {s : Set α}, (s ∈ s✝.inf fun a => f a.down) → p s
s : Set α
his : ∃ t₁ ∈ f a✝¹.down, ∃ t₂ ∈ s✝.inf fun a => f a.down, s = t₁ ∩ t₂
⊢ p s

Tactic:
rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩

Result:
case intro.insert.intro.intro.intro.intro
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
a✝¹ : PLift ι
s✝ : Finset (PLift ι)
a✝ : a✝¹ ∉ s✝
ih : ∀ {s : Set α}, (s ∈ s✝.inf fun a => f a.down) → p s
s₁ : Set α
hs₁ : s₁ ∈ f a✝¹.down
s₂ : Set α
hs₂ : s₂ ∈ s✝.inf fun a => f a.down
⊢ p (s₁ ∩ s₂)

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
hs : ∃ t, s ∈ ⨅ i ∈ t, f i.down
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Tactic:
simp only [← Finset.inf_eq_iInf] at hs

Result:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
hs : ∃ t, s ∈ t.inf fun a => f a.down
⊢ p s

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
hs : ∃ t, s ∈ t.inf fun a => f a.down
⊢ p s

Tactic:
rcases hs with ⟨is, his⟩

Result:
case intro
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
is : Finset (PLift ι)
his : s ∈ is.inf fun a => f a.down
⊢ p s

Proof state:
case intro
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
is : Finset (PLift ι)
his : s ∈ is.inf fun a => f a.down
⊢ p s

Tactic:
induction is using Finset.induction_on generalizing s with
| empty => rwa [mem_top.1 his]
| insert _ ih =>
  rw [Finset.inf_insert, mem_inf_iff] at his
  rcases his with ⟨s₁, hs₁, s₂, hs₂, rfl⟩
  exact ins hs₁ (ih hs₂)

Result:
no goals

Proof state:
case intro.empty
α : Type u
ι : Sort x
f : ι → Filter α
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
s : Set α
his : s ∈ ∅.inf fun a => f a.down
⊢ p s

Tactic:
rwa [mem_top.1 his]

Result:
no goals