case basic
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h : S ∈ insert A S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q

case univ
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q

case inter
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
H : P ∈ finiteInterClosure (insert A S)
⊢ P ∈ S ∨ ∃ Q, Q ∈ S ∧ P = A ∩ Q
induction' H with S h T1 T2 _ _ h1 h2
case basic.inl
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S = A
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q

case basic.inr
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S ∈ S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
case basic
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h : S ∈ insert A S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
cases h
no goals
case basic.inl
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S = A
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
no goals
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S = A
⊢ S = A ∩ Set.univ
simpa
no goals
case basic.inr
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S ∈ S✝
⊢ S ∈ S✝ ∨ ∃ Q, Q ∈ S✝ ∧ S = A ∩ Q
exact Or.inl (by assumption)
no goals
α : Type u_1
S✝ : Set (Set α)
A : Set α
cond : FiniteInter S✝
P S : Set α
h✝ : S ∈ S✝
⊢ S ∈ S✝
assumption
no goals
case univ
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q, Q ∈ S ∧ Set.univ = A ∩ Q
exact Or.inl cond.univ_mem
case inter.inl.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q

case inter.inl.inr.intro.intro
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q

case inter.inr.intro.intro.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1

case inter.inr.intro.intro.inr.intro.intro
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
case inter
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T2 = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
rcases h1 with (h | ⟨Q, hQ, rfl⟩) <;> rcases h2 with (i | ⟨R, hR, rfl⟩)
no goals
case inter.inl.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ T2 = A ∩ Q
exact Or.inl (cond.inter_mem h i)
no goals
case inter.inl.inr.intro.intro
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q, Q ∈ S ∧ T1 ∩ (A ∩ R) = A ∩ Q
exact
  Or.inr ⟨T1 ∩ R, cond.inter_mem h hR, by simp only [← Set.inter_assoc, Set.inter_comm _ A]⟩
no goals
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) = A ∩ (T1 ∩ R)
simp only [← Set.inter_assoc, Set.inter_comm _ A]
no goals
case inter.inr.intro.intro.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ T2 = A ∩ Q_1
exact Or.inr ⟨Q ∩ T2, cond.inter_mem hQ i, by simp only [Set.inter_assoc]⟩
no goals
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 = A ∩ (Q ∩ T2)
simp only [Set.inter_assoc]
no goals
case inter.inr.intro.intro.inr.intro.intro
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1, Q_1 ∈ S ∧ A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
exact
  Or.inr
    ⟨Q ∩ R, cond.inter_mem hQ hR, by
      ext x
      constructor <;> simp (config := { contextual := true })⟩
case h
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) = A ∩ (Q ∩ R)
ext x
no goals
case h
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
x : α
⊢ x ∈ A ∩ Q ∩ (A ∩ R) ↔ x ∈ A ∩ (Q ∩ R)
constructor <;> simp (config := { contextual := true })