-- Mathlib/MeasureTheory/SetSemiring.lean
lemma biInter_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
    (S : Finset ι) (hS : S.Nonempty) (hs : ∀ n ∈ S, s n ∈ C) :
    ⋂ i ∈ S, s i ∈ C

Proof state:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ ⋂ i_1 ∈ cons i S hiS, s i_1 ∈ C

Tactic:
simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]

Result:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ s i ∩ ⋂ x ∈ ↑S, s x ∈ C

Proof state:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : ∀ n ∈ cons i S hiS, s n ∈ C
⊢ s i ∩ ⋂ x ∈ ↑S, s x ∈ C

Tactic:
simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs

Result:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ s i ∩ ⋂ x ∈ ↑S, s x ∈ C

Proof state:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ ⋂ x ∈ ↑S, s x ∈ C

Tactic:
exact h (fun n hnS ↦ hs.2 n hnS)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hS : S.Nonempty
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋂ i ∈ S, s i ∈ C

Tactic:
induction hS using Finset.Nonempty.cons_induction with
| singleton => simpa using hs
| cons i S hiS _ h =>
  simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
  simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
  refine hC.inter_mem hs.1 ?_
  exact h (fun n hnS ↦ hs.2 n hnS)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hS : S.Nonempty
hs : ∀ n ∈ S, s n ∈ C
⊢ ⋂ i ∈ S, s i ∈ C

Tactic:
classical
induction hS using Finset.Nonempty.cons_induction with
| singleton => simpa using hs
| cons i S hiS _ h =>
  simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
  simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
  refine hC.inter_mem hs.1 ?_
  exact h (fun n hnS ↦ hs.2 n hnS)

Result:
no goals

Proof state:
case singleton
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
a✝ : ι
hs : ∀ n ∈ {a✝}, s n ∈ C
⊢ ⋂ i ∈ {a✝}, s i ∈ C

Tactic:
simpa using hs

Result:
no goals

Proof state:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ s i ∩ ⋂ x ∈ ↑S, s x ∈ C

Tactic:
refine hC.inter_mem hs.1 ?_

Result:
case cons
α : Type u_1
C : Set (Set α)
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S✝ : Finset ι
i : ι
S : Finset ι
hiS : i ∉ S
hs✝ : S.Nonempty
h : (∀ n ∈ S, s n ∈ C) → ⋂ i ∈ S, s i ∈ C
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ ⋂ x ∈ ↑S, s x ∈ C