Theorem: Profinite.EffectiveEpiFamily.ιFun_continuous (Profinite/Epi.lean)

State before:
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous (ιFun π)
Tactic:
apply Continuous.quotient_lift
State after:
case h
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(π a) x

State before:
case h
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ Continuous fun x =>
    match x with
    | { fst := a, snd := x } => ↑(π a) x
Tactic:
apply continuous_sigma
State after:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(π a) x

State before:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
⊢ ∀ (i : α),
    Continuous fun a =>
      match { fst := i, snd := a } with
      | { fst := a, snd := x } => ↑(π a) x
Tactic:
intro a
State after:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(π a) x

State before:
case h.hf
X✝ Y B✝ : Profinite
f : X✝ ⟶ B✝
g : Y ⟶ B✝
α : Type
inst✝ : Fintype α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj : ∀ (b : ↑B.toCompHaus.toTop), ∃ a x, ↑(π a) x = b
a : α
⊢ Continuous fun a_1 =>
    match { fst := a, snd := a_1 } with
    | { fst := a, snd := x } => ↑(π a) x
Tactic:
exact (π a).continuous
State after:
no goals