-- Mathlib/Topology/FiberBundle/Basic.lean
theorem continuous_const_section (v : F)
    (h : ∀ i j, ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v) :
    Continuous (show B → Z.TotalSpace from fun x => ⟨x, v⟩)

Proof state:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(Z.localTrivAt x).toPartialHomeomorph ∘
      let_fun this := fun x => { proj := x, snd := v };
      this)
    x

Tactic:
apply continuousAt_id.prod

Result:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (fun x_1 =>
      Z.coordChange
        (Z.indexAt
          ((let_fun this := fun x => { proj := x, snd := v };
              this)
              x_1).proj)
        (Z.indexAt x)
        ((let_fun this := fun x => { proj := x, snd := v };
            this)
            x_1).proj
        ((let_fun this := fun x => { proj := x, snd := v };
            this)
            x_1).snd)
    x

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x

Tactic:
have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x :=
  IsOpen.mem_nhds (Z.isOpen_baseSet (Z.indexAt x)) (Z.mem_baseSet_at x)

Result:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x

Proof state:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (Z.baseSet (Z.indexAt x))
y : B
hy : y ∈ Z.baseSet (Z.indexAt x)
⊢ Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v

Tactic:
exact h _ _ _ ⟨mem_baseSet_at _ _, hy⟩

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (Z.baseSet (Z.indexAt x))
⊢ ContinuousAt (fun x_1 => Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x

Tactic:
refine (this.congr fun y hy ↦ ?_).continuousAt A

Result:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (Z.baseSet (Z.indexAt x))
y : B
hy : y ∈ Z.baseSet (Z.indexAt x)
⊢ Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
⊢ Continuous
    (let_fun this := fun x => { proj := x, snd := v };
    this)

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Result:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (let_fun this := fun x => { proj := x, snd := v };
    this)
    x

Tactic:
refine ((Z.localTrivAt x).toPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_

Result:
case refine_1
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ (let_fun this := fun x => { proj := x, snd := v };
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(Z.localTrivAt x).toPartialHomeomorph ∘
      let_fun this := fun x => { proj := x, snd := v };
      this)
    x

Proof state:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt (fun x_1 => Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x

Tactic:
have : ContinuousOn (fun _ : B => v) (Z.baseSet (Z.indexAt x)) := continuousOn_const

Result:
case refine_2
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (Z.baseSet (Z.indexAt x))
⊢ ContinuousAt (fun x_1 => Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x

Proof state:
case refine_1
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ (let_fun this := fun x => { proj := x, snd := v };
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

Tactic:
exact A

Result:
no goals