internlm/Lean-Github huggingface dataset:
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), ∃ Y₀ π₀ f₀, S.arrows π₀ ∧ π a = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
Proof state after:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∃ f, ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∃ f, ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨Y₀, H₂⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∀ (x : α), ∃ π₀ f₀, S.arrows π₀ ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map π₀
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∃ f, ∀ (x : α), ∃ f₀, S.arrows (f x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (f x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
H₂ : ∃ f, ∀ (x : α), ∃ f₀, S.arrows (f x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (f x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨π₀, H₂⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∀ (x : α), ∃ f₀, S.arrows (π₀ x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∀ (x : α), ∃ f₀, S.arrows (π₀ x) ∧ π x = f₀ ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [Classical.skolem] at H₂
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∃ f, ∀ (x : α), S.arrows (π₀ x) ∧ π x = f x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
H₂ : ∃ f, ∀ (x : α), S.arrows (π₀ x) ∧ π x = f x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H₂ with ⟨f₀, H₂⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
use Y₀ , π₀
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀ ∧ ∀ (a : α), S.arrows (π₀ a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀ ∧ ∀ (a : α), S.arrows (π₀ a)
Tactic:
constructor
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀

case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (a : α), S.arrows (π₀ a)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ EffectiveEpiFamily Y₀ π₀
Tactic:
simp only [(ExtrDisc.effectiveEpiFamily_tfae _ _).out 0 2]
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Tactic:
simp only [(CompHaus.effectiveEpiFamily_tfae _ _).out 0 2] at H₁
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (b : CoeSort.coe X), ∃ a x, ↑(π₀ a) x = b
Tactic:
intro b
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
b : CoeSort.coe X
⊢ ∃ a x, ↑(π₀ a) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
H₁ : ∀ (b : ↑(ExtrDisc.toCompHaus.obj X).toTop), ∃ a x, ↑(π a) x = b
b : CoeSort.coe X
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
replace H₁ := H₁ b
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
H₁ : ∃ a x, ↑(π a) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
H₁ : ∃ a x, ↑(π a) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
rcases H₁ with ⟨i, x, H₁⟩
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ∃ a x, ↑(π₀ a) x = b
Tactic:
use i, f₀ i x
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ↑(π₀ i) (↑(f₀ i) x) = b
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.left.intro.intro
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
b : CoeSort.coe X
i : α
x : ↑(Y i).toTop
H₁ : ↑(π i) x = b
⊢ ↑(π₀ i) (↑(f₀ i) x) = b
Tactic:
aesop_cat
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
⊢ ∀ (a : α), S.arrows (π₀ a)
Tactic:
intro i
Proof state after:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
i : α
⊢ S.arrows (π₀ i)
Theorem: Condensed.ExtrDiscCompHaus.coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily
Proof state before:
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.right
X : ExtrDisc
S : Sieve X
α : Type
w✝ : Fintype α
Y : α → CompHaus
π : (a : α) → Y a ⟶ ExtrDisc.toCompHaus.obj X
H₁ : EffectiveEpiFamily Y π
Y₀ : α → ExtrDisc
π₀ : (x : α) → Y₀ x ⟶ X
f₀ : (x : α) → Y x ⟶ (Y₀ x).compHaus
H₂ : ∀ (x : α), S.arrows (π₀ x) ∧ π x = f₀ x ≫ ExtrDisc.toCompHaus.map (π₀ x)
i : α
⊢ S.arrows (π₀ i)
Tactic:
exact (H₂ i).1
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coherentTopology_is_induced
Proof state before:
⊢ coherentTopology ExtrDisc = CoverDense.inducedTopology coverDense
Tactic:
ext X S
Proof state after:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Theorem: Condensed.ExtrDiscCompHaus.coherentTopology_is_induced
Proof state before:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
rw [← coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily X]
Proof state after:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Theorem: Condensed.ExtrDiscCompHaus.coherentTopology_is_induced
Proof state before:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [← coherentTopology.Sieve_iff_hasEffectiveEpiFamily S]
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverPreserving
Proof state before:
⊢ CoverPreserving (coherentTopology ExtrDisc) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
rw [coherentTopology_is_induced]
Proof state after:
⊢ CoverPreserving (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Theorem: Condensed.ExtrDiscCompHaus.coverPreserving
Proof state before:
⊢ CoverPreserving (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
exact LocallyCoverDense.inducedTopology_coverPreserving (CoverDense.locallyCoverDense coverDense)
Proof state after:
no goals
Theorem: Condensed.ExtrDiscCompHaus.coverLifting
Proof state before:
⊢ CoverLifting (coherentTopology ExtrDisc) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
rw [coherentTopology_is_induced]
Proof state after:
⊢ CoverLifting (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Theorem: Condensed.ExtrDiscCompHaus.coverLifting
Proof state before:
⊢ CoverLifting (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
exact LocallyCoverDense.inducedTopology_coverLifting (CoverDense.locallyCoverDense coverDense)
Proof state after:
no goals
Theorem: CompHaus.lift_lifts
Proof state before:
X Y : CompHaus
Z : ExtrDisc
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e
Tactic:
simp [lift]
Proof state after:
no goals
Theorem: sigma_mk_preimage_image'
Proof state before:
α✝ : Type u_1
i j : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' (Sigma.mk i '' U) = ∅
Tactic:
change Sigma.mk j ⁻¹' {⟨i, u⟩ | u ∈ U} = ∅
Proof state after:
α✝ : Type u_1
i j : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = ∅
Theorem: sigma_mk_preimage_image'
Proof state before:
α✝ : Type u_1
i j : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = ∅
Tactic:
simp [h]
Proof state after:
no goals
Theorem: sigma_mk_preimage_image_eq_self
Proof state before:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' (Sigma.mk i '' U) = U
Tactic:
change Sigma.mk i ⁻¹' {⟨i, u⟩ | u ∈ U} = U
Proof state after:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = U
Theorem: sigma_mk_preimage_image_eq_self
Proof state before:
α✝ : Type u_1
i : α✝
β✝ : α✝ → Type u_2
U : Set (β✝ i)
⊢ Sigma.mk i ⁻¹' {x | ∃ u, u ∈ U ∧ { fst := i, snd := u } = x} = U
Tactic:
simp
Proof state after:
no goals
Theorem: ExtrDisc.finiteCoproduct.hom_ext
Proof state before:
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
Tactic:
ext ⟨a,x⟩
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: ExtrDisc.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
specialize h a
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: ExtrDisc.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
apply_fun (fun q => q x) at h
Proof state after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Theorem: ExtrDisc.finiteCoproduct.hom_ext
Proof state before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
exact h
Proof state after:
no goals
Theorem: CompHaus.Gleason
Proof state before:
X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected ↑X.toTop
Tactic:
constructor
Proof state after:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop

case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X
Theorem: CompHaus.Gleason
Proof state before:
case mp
X : CompHaus
⊢ Projective X → ExtremallyDisconnected ↑X.toTop
Tactic:
intro h
Proof state after:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop
Theorem: CompHaus.Gleason
Proof state before:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected ↑X.toTop
Tactic:
show ExtremallyDisconnected X.toExtrDisc
Proof state after:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected (CoeSort.coe (toExtrDisc X))
Theorem: CompHaus.Gleason
Proof state before:
case mp
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected (CoeSort.coe (toExtrDisc X))
Tactic:
infer_instance
Proof state after:
no goals
Theorem: CompHaus.Gleason
Proof state before:
case mpr
X : CompHaus
⊢ ExtremallyDisconnected ↑X.toTop → Projective X
Tactic:
intro h
Proof state after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X
Theorem: CompHaus.Gleason
Proof state before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
⊢ Projective X
Tactic:
let X' : ExtrDisc := ⟨X⟩
Proof state after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X
Theorem: CompHaus.Gleason
Proof state before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X
Tactic:
show Projective X'.compHaus
Proof state after:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X'.compHaus
Theorem: CompHaus.Gleason
Proof state before:
case mpr
X : CompHaus
h : ExtremallyDisconnected ↑X.toTop
X' : ExtrDisc := ExtrDisc.mk X
⊢ Projective X'.compHaus
Tactic:
apply ExtrDisc.instProjectiveCompHausCategoryCompHaus
Proof state after:
no goals
Theorem: CategoryTheory.clopen_extremallyDisconnected
Proof state before:
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ExtremallyDisconnected ↑U
Tactic:
constructor
Proof state after:
case open_closure
X : ExtrDisc
U : Set (CoeSort.coe X)
hU : IsClopen U
⊢ ∀ (U_1 : Set ↑U), IsOpen U_1 → IsOpen (closure U_1)