-- Mathlib/Order/Filter/Prod.lean
theorem map_prod_map_const_id_principal_coprod_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
    map (Prod.map (fun _ : α => b) id) ((𝓟 {a}).coprod (𝓟 {i})) =
      𝓟 (({b} : Set β) ×ˢ (univ : Set ι))

Proof state:
case e_s.h.mk.mp.intro.mk.intro.refl
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ

Tactic:
simp

Result:
no goals

Proof state:
case e_s.h.mk
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ

Tactic:
constructor

Result:
case e_s.h.mk.mp
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

case e_s.h.mk.mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Proof state:
case e_s
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ

Tactic:
ext ⟨b', i'⟩

Result:
case e_s.h.mk
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ

Proof state:
case e_s.h.mk.mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Tactic:
rintro ⟨h₁, _⟩

Result:
case e_s.h.mk.mpr.intro
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Proof state:
case h
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')

Tactic:
simpa using h₁.symm

Result:
no goals

Proof state:
case e_s.h.mk.mp
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

Tactic:
rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩

Result:
case e_s.h.mk.mp.intro.mk.intro.refl
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)

Tactic:
congr

Result:
case e_s
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x => b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)

Tactic:
rw [principal_coprod_principal, map_principal]

Result:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)

Proof state:
case e_s.h.mk.mpr.intro
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Tactic:
use (a, i')

Result:
case h
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')