internlm/Lean-Github huggingface dataset:
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
H : ∃ f, ∀ (x : α), EffectiveEpiFamily (Y_n x) (f x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (f x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rcases H with ⟨π_n, H⟩
Proof state after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∃ α x Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
use Σ x, β x, inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a)
Proof state after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ (EffectiveEpiFamily
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a) ∧
    ∀ (a : (x : α) × β x),
      S.arrows
        ((fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a)
          a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ (EffectiveEpiFamily
      (fun x =>
        match x with
        | { fst := a, snd := b } => Y_n a b)
      fun x =>
      match x with
      | { fst := a, snd := b } => π_n a b ≫ π a) ∧
    ∀ (a : (x : α) × β x),
      S.arrows
        ((fun x =>
            match x with
            | { fst := a, snd := b } => π_n a b ≫ π a)
          a)
Tactic:
constructor
Proof state after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    fun x =>
    match x with
    | { fst := a, snd := b } => π_n a b ≫ π a

case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : (x : α) × β x),
    S.arrows
      ((fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)
        a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily
    (fun x =>
      match x with
      | { fst := a, snd := b } => Y_n a b)
    fun x =>
    match x with
    | { fst := a, snd := b } => π_n a b ≫ π a
Tactic:
apply EffectiveEpiFamily_transitive
Proof state after:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily (fun a => Y₁ a) π

case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.H
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.h
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ EffectiveEpiFamily (fun a => Y₁ a) π
Tactic:
exact h₁
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.left.H
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
Tactic:
exact fun a => (H a).1
Proof state after:
no goals
Theorem: coherentTopology.Sieve_iff_hasEffectiveEpiFamily
Proof state before:
case mpr.transitive.intro.intro.intro.intro.intro.intro.intro.intro.intro.right
C : Type u
inst✝¹ : Category C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : Coverage.saturate (coherentCoverage C) Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α x Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Fintype α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
w✝ : (x : α) → Fintype (β x)
Y_n : (x : α) → β x → C
π_n : (x : α) → (b : β x) → Y_n x b ⟶ Y₁ x
H : ∀ (x : α), EffectiveEpiFamily (Y_n x) (π_n x) ∧ ∀ (b : β x), (Sieve.pullback (π x) S).arrows (π_n x b)
⊢ ∀ (a : (x : α) × β x),
    S.arrows
      ((fun x =>
          match x with
          | { fst := a, snd := b } => π_n a b ≫ π a)
        a)
Tactic:
exact fun c => (H c.fst).2 c.snd
Proof state after:
no goals
Theorem: CategoryTheory.EffectiveEpiFamily.toCompHaus
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
⊢ EffectiveEpiFamily (fun a => ExtrDisc.toCompHaus.obj (X a)) fun a => ExtrDisc.toCompHaus.map (π a)
Tactic:
refine' ((CompHaus.effectiveEpiFamily_tfae _ _).out 0 2).2 (fun b => _)
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
b : ↑(ExtrDisc.toCompHaus.obj B).toTop
⊢ ∃ a x, ↑(ExtrDisc.toCompHaus.map (π a)) x = b
Theorem: CategoryTheory.EffectiveEpiFamily.toCompHaus
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
b : ↑(ExtrDisc.toCompHaus.obj B).toTop
⊢ ∃ a x, ↑(ExtrDisc.toCompHaus.map (π a)) x = b
Tactic:
exact (((effectiveEpiFamily_tfae _ _).out 0 2).1 H : ∀ _, ∃ _, _) _
Proof state after:
no goals
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f

case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → Function.Surjective ↑f
Tactic:
dsimp [Function.Surjective]
Proof state after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → ∀ (b : CoeSort.coe Y), ∃ a, ↑f a = b
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Epi f → ∀ (b : CoeSort.coe Y), ∃ a, ↑f a = b
Tactic:
contrapose!
Proof state after:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ (∃ b, ∀ (a : CoeSort.coe X), ↑f a ≠ b) → ¬Epi f
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ (∃ b, ∀ (a : CoeSort.coe X), ↑f a ≠ b) → ¬Epi f
Tactic:
rintro ⟨y,hy⟩ h
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
⊢ False
Tactic:
let C := Set.range f
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
⊢ False
Tactic:
have hC : IsClosed C := (isCompact_range f.continuous).isClosed
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
⊢ False
Tactic:
let U := Cᶜ
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ False
Tactic:
have hyU : y ∈ U := by
  refine' Set.mem_compl _
  rintro ⟨y', hy'⟩
  exact hy y' hy'
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
⊢ False
Tactic:
have hUy : U ∈ nhds y := hC.compl_mem_nhds hyU
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
⊢ False
Tactic:
haveI : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y)) :=
  show TotallyDisconnectedSpace Y from inferInstance
Proof state after:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
⊢ False
Tactic:
obtain ⟨V, hV, hyV, hVU⟩ := isTopologicalBasis_clopen.mem_nhds_iff.mp hUy
Proof state after:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mp.intro.intro.intro.intro
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
⊢ False
Tactic:
classical
let g : Y ⟶ ExtrDisc.two :=
  ⟨(LocallyConstant.ofClopen hV).map ULift.up, LocallyConstant.continuous _⟩
let h : Y ⟶ ExtrDisc.two := ⟨fun _ => ⟨1⟩, continuous_const⟩
have H : h = g := by
  rw [← cancel_epi f]
  apply ContinuousMap.ext ; intro x
  apply ULift.ext
  change 1 =  _
  dsimp [LocallyConstant.ofClopen]
  rw [comp_apply, @ContinuousMap.coe_mk _ _ (ExtrDisc.instTopologicalSpace Y),
  Function.comp_apply, if_neg]
  refine' mt (fun α => hVU α) _
  simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
  exact ⟨x, rfl⟩
apply_fun fun e => (e y).down at H
dsimp [LocallyConstant.ofClopen] at H
change 1 = ite _ _ _ at H
rw [if_pos hyV] at H
exact top_ne_bot H
Proof state after:
no goals
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ y ∈ U
Tactic:
refine' Set.mem_compl _
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
⊢ ¬y ∈ C