-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem compact_open_induction_on {P : X.Opens → Prop} (S : X.Opens)
    (hS : IsCompact S.1) (h₁ : P ⊥)
    (h₂ : ∀ (S : X.Opens) (_ : IsCompact S.1) (U : X.affineOpens), P S → P (S ⊔ U)) :
    P S

Proof state:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
⊢ ∃ s_1, s_1.Finite ∧ (⨆ i, ↑↑i).carrier = ⋃ i ∈ s_1, ↑↑i

Tactic:
exact ⟨s, hs, by simp⟩

Result:
no goals

Proof state:
case intro.intro
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ P (⨆ i, ↑↑i)

Tactic:
apply @Set.Finite.induction_on _ _ _ hs

Result:
case intro.intro.empty
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ P (⨆ i, ↑↑i)

case intro.intro.insert
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ ∀ {a : ↑X.affineOpens} {s : Set ↑X.affineOpens}, a ∉ s → s.Finite → P (⨆ i, ↑↑i) → P (⨆ i, ↑↑i)

Proof state:
case intro.intro.empty
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ P (⨆ i, ↑↑i)

Tactic:
convert h₁

Result:
case h.e'_1
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ↑↑i = ⊥

Proof state:
case intro.intro.insert
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ ∀ {a : ↑X.affineOpens} {s : Set ↑X.affineOpens}, a ∉ s → s.Finite → P (⨆ i, ↑↑i) → P (⨆ i, ↑↑i)

Tactic:
intro x s _ hs h₄

Result:
case intro.intro.insert
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
⊢ P (⨆ i, ↑↑i)

Proof state:
case h.e'_1
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ↑↑i = ⊥

Tactic:
rw [iSup_eq_bot]

Result:
case h.e'_1
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
⊢ ∀ (i : ↑∅), ↑↑i = ⊥

Proof state:
case h.e'_1
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ⨆ (h : i ∈ insert x s), ↑↑⟨i, h⟩ = ↑x ⊔ ⨆ i, ↑↑i

Tactic:
conv_rhs => rw [iSup_subtype]

Result:
case h.e'_1
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s✝ : Set ↑X.affineOpens
hs✝ : s✝.Finite
hS : IsCompact (⨆ i, ↑↑i).carrier
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ⨆ (h : i ∈ insert x s), ↑↑⟨i, h⟩ = ↑x ⊔ ⨆ i, ⨆ (h : i ∈ s), ↑↑⟨i, h⟩