-- 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
S : X.Opens
hS : IsCompact S.carrier
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
⊢ P S

Tactic:
obtain ⟨s, hs, hs'⟩ := (isCompactOpen_iff_eq_finset_affine_union S.1).mp ⟨hS, S.2⟩

Result:
case intro.intro
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S.carrier = ⋃ i ∈ s, ↑↑i
⊢ P S

Proof state:
case h
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S.carrier = ⋃ i ∈ s, ↑↑i
⊢ ↑S = ↑(⨆ i, ↑↑i)

Tactic:
simpa using hs'

Result:
no goals

Proof state:
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S.carrier = ⋃ i ∈ s, ↑↑i
⊢ S = ⨆ i, ↑↑i

Tactic:
ext1

Result:
case h
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S.carrier = ⋃ i ∈ s, ↑↑i
⊢ ↑S = ↑(⨆ 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
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
⊢ P (⨆ i, ↑↑i)

Tactic:
have : IsCompact (⨆ i : s, (i : X.Opens)).1 := by
  refine ((isCompactOpen_iff_eq_finset_affine_union _).mpr ?_).1; exact ⟨s, hs, by simp⟩

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)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ 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
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ↑↑i = (⨆ i, ↑↑i) ⊔ ↑x

Tactic:
rw [iSup_subtype, sup_comm]

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, ↑↑i

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)
⊢ IsCompact (⨆ i, ↑↑i).carrier

Tactic:
refine ((isCompactOpen_iff_eq_finset_affine_union _).mpr ?_).1

Result:
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

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:
rintro ⟨_, h⟩

Result:
case h.e'_1.mk
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
val✝ : ↑X.affineOpens
h : val✝ ∈ ∅
⊢ ↑↑⟨val✝, h⟩ = ⊥

Proof state:
case h.e'_1.mk
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
val✝ : ↑X.affineOpens
h : val✝ ∈ ∅
⊢ ↑↑⟨val✝, h⟩ = ⊥

Tactic:
exact h.elim

Result:
no goals

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
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ P (⨆ i, ↑↑i)

Tactic:
convert h₂ _ this x 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
x : ↑X.affineOpens
s : Set ↑X.affineOpens
a✝ : x ∉ s
hs : s.Finite
h₄ : P (⨆ i, ↑↑i)
this : IsCompact (⨆ i, ↑↑i).carrier
⊢ ⨆ i, ↑↑i = (⨆ i, ↑↑i) ⊔ ↑x

Proof state:
case intro.intro
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S = ⨆ i, ↑↑i
⊢ P S

Tactic:
subst hs'

Result:
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)

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, ⨆ (h : i ∈ s), ↑↑⟨i, h⟩

Tactic:
exact iSup_insert

Result:
no goals

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)
⊢ (⨆ i, ↑↑i).carrier = ⋃ i ∈ s, ↑↑i

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S.carrier = ⋃ i ∈ s, ↑↑i
⊢ P S

Tactic:
replace hs' : S = iSup fun i : s => (i : X.Opens) := by ext1; simpa using hs'

Result:
case intro.intro
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact S.carrier
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' : S = ⨆ i, ↑↑i
⊢ P S