-- Mathlib/Topology/UniformSpace/Pi.lean
theorem CompleteSpace.iInf {ι X : Type*} {u : ι → UniformSpace X}
    (hu : ∀ i, @CompleteSpace X (u i))
    (ht : ∃ t, @T2Space X t ∧ ∀ i, (u i).toTopologicalSpace ≤ t) :
    @CompleteSpace X (⨅ i, u i)

Proof state:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this✝ : IsUniformInducing (const ι)
this : Pi.topologicalSpace ≤ Pi.topologicalSpace
⊢ IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})

Tactic:
refine IsClosed.isComplete <| .mono ?_ this

Result:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this✝ : IsUniformInducing (const ι)
this : Pi.topologicalSpace ≤ Pi.topologicalSpace
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x i = x i_1})

Proof state:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
⊢ IsUniformInducing (const ι)

Tactic:
simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
  Filter.comap_comap, comp_def, const, Prod.eta, comap_id']

Result:
no goals

Proof state:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})

Tactic:
have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤
       Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
  iInf_mono fun i ↦ induced_mono <| hut i

Result:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this✝ : IsUniformInducing (const ι)
this : Pi.topologicalSpace ≤ Pi.topologicalSpace
⊢ IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})

Proof state:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
⊢ CompleteSpace X

Tactic:
have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
  simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
    Filter.comap_comap, comp_def, const, Prod.eta, comap_id']

Result:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ CompleteSpace X

Proof state:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ CompleteSpace X

Tactic:
simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
  setOf_forall]

Result:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})

Proof state:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
this✝ : IsUniformInducing (const ι)
this : Pi.topologicalSpace ≤ Pi.topologicalSpace
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x i = x i_1})

Tactic:
exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
  isClosed_eq (continuous_apply _) (continuous_apply _)

Result:
no goals

Proof state:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ t, T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
a✝ : Nontrivial X
⊢ CompleteSpace X

Tactic:
rcases ht with ⟨t, ht, hut⟩

Result:
case intro.intro
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), toTopologicalSpace ≤ t
⊢ CompleteSpace X

Proof state:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ t, T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
⊢ CompleteSpace X

Tactic:
nontriviality X

Result:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
ht : ∃ t, T2Space X ∧ ∀ (i : ι), toTopologicalSpace ≤ t
a✝ : Nontrivial X
⊢ CompleteSpace X