ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
⊢ ContinuousAt
    (let_fun this := fun x => { fst := x, snd := v };
    this)
    x
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
⊢ Continuous
    (let_fun this := fun x => { fst := x, snd := v };
    this)
refine continuous_iff_continuousAt.2 fun x => ?_
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (let_fun this := fun x => { fst := x, snd := v };
    this)
    x
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
⊢ ContinuousAt
    (let_fun this := fun x => { fst := x, snd := v };
    this)
    x
have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x :=
  IsOpen.mem_nhds (Z.isOpen_baseSet (Z.indexAt x)) (Z.mem_baseSet_at x)
case refine_1
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ (let_fun this := fun x => { fst := x, snd := v };
      this) ⁻¹'
      (localTrivAt Z x).toLocalHomeomorph.toLocalEquiv.source ∈
    𝓝 x

case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(localTrivAt Z x).toLocalHomeomorph ∘
      let_fun this := fun x => { fst := x, snd := v };
      this)
    x
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (let_fun this := fun x => { fst := x, snd := v };
    this)
    x
refine ((Z.localTrivAt x).toLocalHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_
no goals
case refine_1
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ (let_fun this := fun x => { fst := x, snd := v };
      this) ⁻¹'
      (localTrivAt Z x).toLocalHomeomorph.toLocalEquiv.source ∈
    𝓝 x
exact A
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (fun x_1 =>
      coordChange Z
        (indexAt Z
          ((let_fun this := fun x => { fst := x, snd := v };
              this)
              x_1).fst)
        (indexAt Z x)
        ((let_fun this := fun x => { fst := x, snd := v };
            this)
            x_1).fst
        ((let_fun this := fun x => { fst := x, snd := v };
            this)
            x_1).snd)
    x
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt
    (↑(localTrivAt Z x).toLocalHomeomorph ∘
      let_fun this := fun x => { fst := x, snd := v };
      this)
    x
apply continuousAt_id.prod
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
⊢ ContinuousAt (fun x_1 => coordChange Z (indexAt Z x_1) (indexAt Z x) x_1 v) x
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
⊢ ContinuousAt (fun x_1 => coordChange Z (indexAt Z x_1) (indexAt Z x) x_1 v) x
have : ContinuousOn (fun _ : B => v) (Z.baseSet (Z.indexAt x)) := continuousOn_const
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
y : B
hy : y ∈ baseSet Z (indexAt Z x)
⊢ coordChange Z (indexAt Z y) (indexAt Z x) y v = v
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
⊢ ContinuousAt (fun x_1 => coordChange Z (indexAt Z x_1) (indexAt Z x) x_1 v) x
refine (this.congr fun y hy ↦ ?_).continuousAt A
no goals
case refine_2
ι : Type u_2
B : Type u_1
F : Type u_3
X : Type ?u.41511
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a v : F
h : ∀ (i j : ι) (x : B), x ∈ baseSet Z i ∩ baseSet Z j → coordChange Z i j x v = v
x : B
A : baseSet Z (indexAt Z x) ∈ 𝓝 x
this : ContinuousOn (fun x => v) (baseSet Z (indexAt Z x))
y : B
hy : y ∈ baseSet Z (indexAt Z x)
⊢ coordChange Z (indexAt Z y) (indexAt Z x) y v = v
exact h _ _ _ ⟨mem_baseSet_at _ _, hy⟩