[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
⊢ Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F
[PROOFSTEP]
ext v
[GOAL]
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = ↑(ContinuousLinearEquiv.refl 𝕜 F) v
[PROOFSTEP]
rw [Trivialization.coordChangeL_apply']
[GOAL]
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (↑(trivialization B F) (↑(LocalHomeomorph.symm (trivialization B F).toLocalHomeomorph) (b, v))).snd =
    ↑(ContinuousLinearEquiv.refl 𝕜 F) v
case h.h.hb
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet
[PROOFSTEP]
exacts [rfl, ⟨mem_univ _, mem_univ _⟩]
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
⊢ Trivialization.IsLinear 𝕜 e
[PROOFSTEP]
rw [eq_trivialization B F e]
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
⊢ Trivialization.IsLinear 𝕜 (trivialization B F)
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
e e' : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
he' : MemTrivializationAtlas e'
⊢ ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
[PROOFSTEP]
obtain rfl := eq_trivialization B F e
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
he : MemTrivializationAtlas (trivialization B F)
⊢ ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜 (trivialization B F) e' b))
    ((trivialization B F).baseSet ∩ e'.baseSet)
[PROOFSTEP]
obtain rfl := eq_trivialization B F e'
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
he he' : MemTrivializationAtlas (trivialization B F)
⊢ ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b))
    ((trivialization B F).baseSet ∩ (trivialization B F).baseSet)
[PROOFSTEP]
simp only [trivialization.coordChangeL]
[GOAL]
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
he he' : MemTrivializationAtlas (trivialization B F)
⊢ ContinuousOn (fun b => ↑(ContinuousLinearEquiv.refl 𝕜 F))
    ((trivialization B F).baseSet ∩ (trivialization B F).baseSet)
[PROOFSTEP]
exact continuous_const.continuousOn
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
⊢ ↑(coordChangeL 𝕜 (prod e₁ e₂) (prod e₁' e₂') b) =
    ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' b) ↑(coordChangeL 𝕜 e₂ e₂' b)
[PROOFSTEP]
rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
⊢ ∀ (x : F₁ × F₂),
    ↑↑(coordChangeL 𝕜 (prod e₁ e₂) (prod e₁' e₂') b) x =
      Prod.map (↑↑(coordChangeL 𝕜 e₁ e₁' b)) (↑↑(coordChangeL 𝕜 e₂ e₂' b)) x
[PROOFSTEP]
rintro ⟨v₁, v₂⟩
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ ↑↑(coordChangeL 𝕜 (prod e₁ e₂) (prod e₁' e₂') b) (v₁, v₂) =
    Prod.map ↑↑(coordChangeL 𝕜 e₁ e₁' b) ↑↑(coordChangeL 𝕜 e₂ e₂' b) (v₁, v₂)
[PROOFSTEP]
show (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) = (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ ↑(coordChangeL 𝕜 (prod e₁ e₂) (prod e₁' e₂') b) (v₁, v₂) =
    (↑(coordChangeL 𝕜 e₁ e₁' b) v₁, ↑(coordChangeL 𝕜 e₂ e₂' b) v₂)
[PROOFSTEP]
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
[GOAL]
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ (↑(prod e₁' e₂') (↑(LocalHomeomorph.symm (prod e₁ e₂).toLocalHomeomorph) (b, v₁, v₂))).snd =
    ((↑e₁' { proj := b, snd := Trivialization.symm e₁ b v₁ }).snd,
      (↑e₂' { proj := b, snd := Trivialization.symm e₂ b v₂ }).snd)
case mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
case mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₂.baseSet ∩ e₂'.baseSet
case mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : TopologicalSpace B
F₁ : Type u_3
inst✝¹³ : NormedAddCommGroup F₁
inst✝¹² : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹¹ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁵ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁴ : (x : B) → Module 𝕜 (E₂ x)
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
b : B
hb : b ∈ (prod e₁ e₂).baseSet ∩ (prod e₁' e₂').baseSet
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₁.baseSet ∩ e₁'.baseSet
[PROOFSTEP]
exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
⊢ ∀ (e : Trivialization (F₁ × F₂) TotalSpace.proj) [inst : MemTrivializationAtlas e], Trivialization.IsLinear 𝕜 e
[PROOFSTEP]
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩
[GOAL]
case mk.intro.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
⊢ Trivialization.IsLinear 𝕜 (Trivialization.prod e₁ e₂)
[PROOFSTEP]
skip
[GOAL]
case mk.intro.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
⊢ Trivialization.IsLinear 𝕜 (Trivialization.prod e₁ e₂)
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
⊢ ∀ (e e' : Trivialization (F₁ × F₂) TotalSpace.proj) [inst : MemTrivializationAtlas e]
    [inst_1 : MemTrivializationAtlas e'], ContinuousOn (fun b => ↑(coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
[PROOFSTEP]
rintro _ _ ⟨e₁, e₂, he₁, he₂, rfl⟩ ⟨e₁', e₂', he₁', he₂', rfl⟩
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ ContinuousOn (fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b))
    ((Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet)
[PROOFSTEP]
skip
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ ContinuousOn (fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b))
    ((Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet)
[PROOFSTEP]
refine' (((continuousOn_coordChange 𝕜 e₁ e₁').mono _).prod_mapL 𝕜 ((continuousOn_coordChange 𝕜 e₂ e₂').mono _)).congr _
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ (Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet ⊆ e₁.baseSet ∩ e₁'.baseSet
[PROOFSTEP]
dsimp only [baseSet_prod, mfld_simps]
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ (Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet ⊆ e₂.baseSet ∩ e₂'.baseSet
[PROOFSTEP]
dsimp only [baseSet_prod, mfld_simps]
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ EqOn (fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b))
    (fun x => ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' x) ↑(coordChangeL 𝕜 e₂ e₂' x))
    ((Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet)
[PROOFSTEP]
dsimp only [baseSet_prod, mfld_simps]
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁.baseSet ∩ e₁'.baseSet
[PROOFSTEP]
mfld_set_tac
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
[PROOFSTEP]
mfld_set_tac
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ EqOn (fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b))
    (fun x => ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' x) ↑(coordChangeL 𝕜 e₂ e₂' x))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
[PROOFSTEP]
rintro b hb
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
⊢ (fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b)) b =
    (fun x => ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' x) ↑(coordChangeL 𝕜 e₂ e₂' x)) b
[PROOFSTEP]
rw [ContinuousLinearMap.ext_iff]
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
⊢ ∀ (x : F₁ × F₂),
    ↑((fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b)) b) x =
      ↑((fun x => ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' x) ↑(coordChangeL 𝕜 e₂ e₂' x)) b) x
[PROOFSTEP]
rintro ⟨v₁, v₂⟩
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ ↑((fun b => ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b)) b) (v₁, v₂) =
    ↑((fun x => ContinuousLinearMap.prodMap ↑(coordChangeL 𝕜 e₁ e₁' x) ↑(coordChangeL 𝕜 e₂ e₂' x)) b) (v₁, v₂)
[PROOFSTEP]
show (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) = (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ ↑(coordChangeL 𝕜 (Trivialization.prod e₁ e₂) (Trivialization.prod e₁' e₂') b) (v₁, v₂) =
    (↑(coordChangeL 𝕜 e₁ e₁' b) v₁, ↑(coordChangeL 𝕜 e₂ e₂' b) v₂)
[PROOFSTEP]
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
[GOAL]
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ (↑(Trivialization.prod e₁' e₂')
        (↑(LocalHomeomorph.symm (Trivialization.prod e₁ e₂).toLocalHomeomorph) (b, v₁, v₂))).snd =
    ((↑e₁' { proj := b, snd := Trivialization.symm e₁ b v₁ }).snd,
      (↑e₂' { proj := b, snd := Trivialization.symm e₂ b v₂ }).snd)
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ (Trivialization.prod e₁ e₂).baseSet ∩ (Trivialization.prod e₁' e₂').baseSet
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₂.baseSet ∩ e₂'.baseSet
case mk.intro.intro.intro.intro.mk.intro.intro.intro.intro.refine'_3.mk.hb
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
inst✝¹ : VectorBundle 𝕜 F₁ E₁
inst✝ : VectorBundle 𝕜 F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₁.baseSet ∩ e₁'.baseSet
[PROOFSTEP]
exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
[GOAL]
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
x : B
hx : x ∈ (prod e₁ e₂).baseSet
⊢ continuousLinearEquivAt 𝕜 (prod e₁ e₂) x hx =
    ContinuousLinearEquiv.prod (continuousLinearEquivAt 𝕜 e₁ x (_ : x ∈ e₁.baseSet))
      (continuousLinearEquivAt 𝕜 e₂ x (_ : x ∈ e₂.baseSet))
[PROOFSTEP]
ext v : 2
[GOAL]
case h.h
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
x : B
hx : x ∈ (prod e₁ e₂).baseSet
v : E₁ x × E₂ x
⊢ ↑(continuousLinearEquivAt 𝕜 (prod e₁ e₂) x hx) v =
    ↑(ContinuousLinearEquiv.prod (continuousLinearEquivAt 𝕜 e₁ x (_ : x ∈ e₁.baseSet))
          (continuousLinearEquivAt 𝕜 e₂ x (_ : x ∈ e₂.baseSet)))
      v
[PROOFSTEP]
obtain ⟨v₁, v₂⟩ := v
[GOAL]
case h.h.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
x : B
hx : x ∈ (prod e₁ e₂).baseSet
v₁ : E₁ x
v₂ : E₂ x
⊢ ↑(continuousLinearEquivAt 𝕜 (prod e₁ e₂) x hx) (v₁, v₂) =
    ↑(ContinuousLinearEquiv.prod (continuousLinearEquivAt 𝕜 e₁ x (_ : x ∈ e₁.baseSet))
          (continuousLinearEquivAt 𝕜 e₂ x (_ : x ∈ e₂.baseSet)))
      (v₁, v₂)
[PROOFSTEP]
rw [(e₁.prod e₂).continuousLinearEquivAt_apply 𝕜, Trivialization.prod]
[GOAL]
case h.h.mk
𝕜 : Type u_1
B : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝¹⁵ : NormedAddCommGroup F₁
inst✝¹⁴ : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → AddCommMonoid (E₁ x)
inst✝⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝⁷ : (x : B) → AddCommMonoid (E₂ x)
inst✝⁶ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : (x : B) → TopologicalSpace (E₂ x)
inst✝³ : FiberBundle F₁ E₁
inst✝² : FiberBundle F₂ E₂
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
x : B
hx : x ∈ (prod e₁ e₂).baseSet
v₁ : E₁ x
v₂ : E₂ x
⊢ (fun y =>
        (↑{
                toLocalHomeomorph :=
                  {
                    toLocalEquiv :=
                      { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                        source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                        target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                        map_source' :=
                          (_ :
                            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧ (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                        map_target' :=
                          (_ :
                            ∀ (x : B × F₁ × F₂),
                              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                        left_inv' :=
                          (_ :
                            ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                              x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                        right_inv' :=
                          (_ :
                            ∀ (x : B × F₁ × F₂),
                              x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                    open_source :=
                      (_ :
                        IsOpen
                          { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                              source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                              target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                              map_source' :=
                                (_ :
                                  ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                    x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                      (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                        (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                              map_target' :=
                                (_ :
                                  ∀ (x : B × F₁ × F₂),
                                    x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                              left_inv' :=
                                (_ :
                                  ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                    x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                      Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                              right_inv' :=
                                (_ :
                                  ∀ (x : B × F₁ × F₂),
                                    x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                      Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                    open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                    continuous_toFun :=
                      (_ : ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                    continuous_invFun := (_ : ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) },
                baseSet := e₁.baseSet ∩ e₂.baseSet, open_baseSet := (_ : IsOpen (e₁.baseSet ∩ e₂.baseSet)),
                source_eq :=
                  (_ :
                    {
                            toLocalEquiv :=
                              { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                map_source' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                          (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                map_target' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                left_inv' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                right_inv' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                        Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                            open_source :=
                              (_ :
                                IsOpen
                                  { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                            open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                            continuous_toFun :=
                              (_ : ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                            continuous_invFun :=
                              (_ :
                                ContinuousOn (Prod.invFun' e₁ e₂)
                                  ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }.toLocalEquiv.source =
                      {
                            toLocalEquiv :=
                              { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                map_source' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                          (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                map_target' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                left_inv' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                right_inv' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                        Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                            open_source :=
                              (_ :
                                IsOpen
                                  { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                            open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                            continuous_toFun :=
                              (_ : ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                            continuous_invFun :=
                              (_ :
                                ContinuousOn (Prod.invFun' e₁ e₂)
                                  ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }.toLocalEquiv.source),
                target_eq :=
                  (_ :
                    {
                            toLocalEquiv :=
                              { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                map_source' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                          (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                map_target' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                left_inv' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                right_inv' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                        Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                            open_source :=
                              (_ :
                                IsOpen
                                  { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                            open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                            continuous_toFun :=
                              (_ : ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                            continuous_invFun :=
                              (_ :
                                ContinuousOn (Prod.invFun' e₁ e₂)
                                  ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }.toLocalEquiv.target =
                      {
                            toLocalEquiv :=
                              { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                map_source' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                          (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                map_target' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                left_inv' :=
                                  (_ :
                                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                      x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                        Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                right_inv' :=
                                  (_ :
                                    ∀ (x : B × F₁ × F₂),
                                      x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                        Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                            open_source :=
                              (_ :
                                IsOpen
                                  { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                            open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                            continuous_toFun :=
                              (_ : ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                            continuous_invFun :=
                              (_ :
                                ContinuousOn (Prod.invFun' e₁ e₂)
                                  ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }.toLocalEquiv.target),
                proj_toFun :=
                  (_ :
                    ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                      x ∈
                          {
                                toLocalEquiv :=
                                  { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                    source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                    target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                    map_source' :=
                                      (_ :
                                        ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                          x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                            (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                              (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                    map_target' :=
                                      (_ :
                                        ∀ (x : B × F₁ × F₂),
                                          x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                    left_inv' :=
                                      (_ :
                                        ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                          x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                            Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                    right_inv' :=
                                      (_ :
                                        ∀ (x : B × F₁ × F₂),
                                          x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                            Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                                open_source :=
                                  (_ :
                                    IsOpen
                                      { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                          source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                          target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                          map_source' :=
                                            (_ :
                                              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                  (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                    (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                          map_target' :=
                                            (_ :
                                              ∀ (x : B × F₁ × F₂),
                                                x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                  x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                          left_inv' :=
                                            (_ :
                                              ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                  Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                          right_inv' :=
                                            (_ :
                                              ∀ (x : B × F₁ × F₂),
                                                x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                  Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                                open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                                continuous_toFun :=
                                  (_ :
                                    ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                                continuous_invFun :=
                                  (_ :
                                    ContinuousOn (Prod.invFun' e₁ e₂)
                                      ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }.toLocalEquiv.source →
                        (↑{
                                  toLocalEquiv :=
                                    { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                                  open_source :=
                                    (_ :
                                      IsOpen
                                        { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                            source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                            target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                            map_source' :=
                                              (_ :
                                                ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                  x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                    (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                      (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                            map_target' :=
                                              (_ :
                                                ∀ (x : B × F₁ × F₂),
                                                  x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                    x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                            left_inv' :=
                                              (_ :
                                                ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                  x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                    Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                            right_inv' :=
                                              (_ :
                                                ∀ (x : B × F₁ × F₂),
                                                  x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                    Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                                  open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                                  continuous_toFun :=
                                    (_ :
                                      ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                                  continuous_invFun :=
                                    (_ : ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }
                              x).fst =
                          (↑{
                                  toLocalEquiv :=
                                    { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                      source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                      target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                      map_source' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                      map_target' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ → x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                      left_inv' :=
                                        (_ :
                                          ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                            x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                              Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                      right_inv' :=
                                        (_ :
                                          ∀ (x : B × F₁ × F₂),
                                            x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                              Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) },
                                  open_source :=
                                    (_ :
                                      IsOpen
                                        { toFun := Prod.toFun' e₁ e₂, invFun := Prod.invFun' e₁ e₂,
                                            source := TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                                            target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ,
                                            map_source' :=
                                              (_ :
                                                ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                  x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                    (Prod.toFun' e₁ e₂ x).fst ∈ e₁.baseSet ∩ e₂.baseSet ∧
                                                      (Prod.toFun' e₁ e₂ x).snd ∈ univ),
                                            map_target' :=
                                              (_ :
                                                ∀ (x : B × F₁ × F₂),
                                                  x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                    x.fst ∈ e₁.baseSet ∩ e₂.baseSet),
                                            left_inv' :=
                                              (_ :
                                                ∀ (x : TotalSpace (F₁ × F₂) fun x => E₁ x × E₂ x),
                                                  x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
                                                    Prod.invFun' e₁ e₂ (Prod.toFun' e₁ e₂ x) = x),
                                            right_inv' :=
                                              (_ :
                                                ∀ (x : B × F₁ × F₂),
                                                  x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
                                                    Prod.toFun' e₁ e₂ (Prod.invFun' e₁ e₂ x) = x) }.source),
                                  open_target := (_ : IsOpen ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)),
                                  continuous_toFun :=
                                    (_ :
                                      ContinuousOn (Prod.toFun' e₁ e₂) (TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet))),
                                  continuous_invFun :=
                                    (_ : ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)) }
                              x).fst) }
            { proj := x, snd := y }).snd)
      (v₁, v₂) =
    ↑(ContinuousLinearEquiv.prod (continuousLinearEquivAt 𝕜 e₁ x (_ : x ∈ e₁.baseSet))
          (continuousLinearEquivAt 𝕜 e₂ x (_ : x ∈ e₂.baseSet)))
      (v₁, v₂)
[PROOFSTEP]
exact (congr_arg Prod.snd (prod_apply 𝕜 hx.1 hx.2 v₁ v₂) : _)
[GOAL]
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
⊢ ∀ (e : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e], Trivialization.IsLinear 𝕜 e
[PROOFSTEP]
rintro _ ⟨e, he, rfl⟩
[GOAL]
case mk.intro.intro
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
⊢ Trivialization.IsLinear 𝕜 (Trivialization.pullback e f)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
[PROOFSTEP]
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
[GOAL]
case mk.intro.intro.mk.intro.intro
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ ContinuousOn
    (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet)
[PROOFSTEP]
refine' ((continuousOn_coordChange 𝕜 e e').comp (map_continuous f).continuousOn fun b hb => hb).congr _
[GOAL]
case mk.intro.intro.mk.intro.intro
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ EqOn (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b))
    ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) fun b => (e.baseSet ∩ e'.baseSet) (↑f b)
[PROOFSTEP]
rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet)
[GOAL]
case mk.intro.intro.mk.intro.intro
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
⊢ (fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b)) b =
    ((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b
[PROOFSTEP]
ext v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑((fun b => ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b)) b) v =
    ↑(((fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) ∘ ↑f) b) v
[PROOFSTEP]
show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
[GOAL]
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑(Trivialization.coordChangeL 𝕜 (Trivialization.pullback e f) (Trivialization.pullback e' f) b) v =
    ↑(Trivialization.coordChangeL 𝕜 e e' (↑f b)) v
[PROOFSTEP]
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
[GOAL]
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑(Trivialization.pullback e' f)
        (↑(LocalHomeomorph.symm (Trivialization.pullback e f).toLocalHomeomorph) (b, v))).snd =
    (↑e' { proj := ↑f b, snd := Trivialization.symm e (↑f b) v }).snd
case mk.intro.intro.mk.intro.intro.h.hb
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f✝ : B' → B
inst✝¹¹ : TopologicalSpace B'
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace B
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
K : Type u_7
inst✝³ : ContinuousMapClass K B' B
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle 𝕜 F E
f : K
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : ↑f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ (Trivialization.pullback e f).baseSet ∩ (Trivialization.pullback e' f).baseSet
[PROOFSTEP]
exacts [rfl, hb]


[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
⊢ { obj := fun U => CommRingCat.of (Localization (obj G U)),
          map := fun {U V} i =>
            CommRingCat.ofHom
              (IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
      (𝟙 U) =
    𝟙
      ({ obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.obj
        U)
[PROOFSTEP]
simp_rw [F.map_id]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom
      (IsLocalization.map (Localization (obj G U)) (𝟙 (F.obj U))
        (_ : obj G U ≤ Submonoid.comap (𝟙 (F.obj U)) (obj G U))) =
    𝟙 (CommRingCat.of (Localization (obj G U)))
[PROOFSTEP]
ext x
[GOAL]
case w
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U : (Opens ↑X)ᵒᵖ
x : (forget CommRingCat).obj (CommRingCat.of (Localization (obj G U)))
⊢ ↑(CommRingCat.ofHom
          (IsLocalization.map (Localization (obj G U)) (𝟙 (F.obj U))
            (_ : obj G U ≤ Submonoid.comap (𝟙 (F.obj U)) (obj G U))))
      x =
    ↑(𝟙 (CommRingCat.of (Localization (obj G U)))) x
[PROOFSTEP]
exact IsLocalization.map_id (M := G.obj U) (S := Localization (G.obj U)) x
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ { obj := fun U => CommRingCat.of (Localization (obj G U)),
          map := fun {U V} i =>
            CommRingCat.ofHom
              (IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
      (i ≫ j) =
    { obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
        i ≫
      { obj := fun U => CommRingCat.of (Localization (obj G U)),
            map := fun {U V} i =>
              CommRingCat.ofHom
                (IsLocalization.map (Localization (obj G V)) (F.map i)
                  (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V))) }.map
        j
[PROOFSTEP]
delta CommRingCat.ofHom CommRingCat.of Bundled.of
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ { obj := fun U => Bundled.mk (Localization (obj G U)),
          map := fun {U V} i =>
            IsLocalization.map (Localization (obj G V)) (F.map i)
              (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
      (i ≫ j) =
    { obj := fun U => Bundled.mk (Localization (obj G U)),
            map := fun {U V} i =>
              IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
        i ≫
      { obj := fun U => Bundled.mk (Localization (obj G U)),
            map := fun {U V} i =>
              IsLocalization.map (Localization (obj G V)) (F.map i)
                (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)) }.map
        j
[PROOFSTEP]
simp_rw [F.map_comp, CommRingCat.comp_eq_ring_hom_comp]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
U V W : (Opens ↑X)ᵒᵖ
i : U ⟶ V
j : V ⟶ W
⊢ IsLocalization.map (Localization (obj G W)) (RingHom.comp (F.map j) (F.map i))
      (_ : obj G U ≤ Submonoid.comap (RingHom.comp (F.map j) (F.map i)) (obj G W)) =
    RingHom.comp
      (IsLocalization.map (Localization (obj G W)) (F.map j) (_ : obj G V ≤ Submonoid.comap (F.map j) (obj G W)))
      (IsLocalization.map (Localization (obj G V)) (F.map i) (_ : obj G U ≤ Submonoid.comap (F.map i) (obj G V)))
[PROOFSTEP]
rw [IsLocalization.map_comp_map]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ (fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) U ≤
    Submonoid.comap (F.map i) ((fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) V)
[PROOFSTEP]
intro s hs
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : s ∈ (fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) U
⊢ s ∈ Submonoid.comap (F.map i) ((fun U => ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ F x) (S ↑x)) V)
[PROOFSTEP]
simp only [Submonoid.mem_comap, Submonoid.mem_iInf] at hs ⊢
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
⊢ ∀ (i_1 : { x // x ∈ V.unop }), ↑(germ F i_1) (↑(F.map i) s) ∈ S ↑i_1
[PROOFSTEP]
intro x
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(germ F x) (↑(F.map i) s) ∈ S ↑x
[PROOFSTEP]
change (F.map i.unop.op ≫ F.germ x) s ∈ _
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(F.map i.unop.op ≫ germ F x) s ∈ S ↑x
[PROOFSTEP]
rw [F.germ_res]
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F : Presheaf CommRingCat X
G : SubmonoidPresheaf F
S : (x : ↑X) → Submonoid ↑(stalk F x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : (forget CommRingCat).obj (F.obj U)
hs : ∀ (i : { x // x ∈ U.unop }), ↑(germ F i) s ∈ S ↑i
x : { x // x ∈ V.unop }
⊢ ↑(germ F ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)) s ∈ S ↑x
[PROOFSTEP]
exact hs _
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
⊢ Mono (toTotalQuotientPresheaf (Sheaf.presheaf F))
[PROOFSTEP]
suffices : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (F.presheaf.toTotalQuotientPresheaf.app U)
[GOAL]
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
this : ∀ (U : (Opens ↑X)ᵒᵖ), Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
⊢ Mono (toTotalQuotientPresheaf (Sheaf.presheaf F))
[PROOFSTEP]
apply NatTrans.mono_of_mono_app
[GOAL]
case this
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
⊢ ∀ (U : (Opens ↑X)ᵒᵖ), Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
intro U
[GOAL]
case this
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Mono (NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
apply ConcreteCategory.mono_of_injective
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective ↑(NatTrans.app (toTotalQuotientPresheaf (Sheaf.presheaf F)) U)
[PROOFSTEP]
dsimp [toTotalQuotientPresheaf, CommRingCat.ofHom]
  -- Porting note : this is a hack to make the `refine` below works
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective
    ↑(algebraMap (↑((Sheaf.presheaf F).obj U))
        (Localization
          (⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰)))
[PROOFSTEP]
set m := _
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : ?m.65485 := ?m.65486
⊢ Function.Injective
    ↑(algebraMap (↑((Sheaf.presheaf F).obj U))
        (Localization
          (⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰)))
[PROOFSTEP]
change Function.Injective (algebraMap _ (Localization m))
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
⊢ Function.Injective ↑(algebraMap ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
change Function.Injective (algebraMap (F.presheaf.obj U) _)
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
⊢ Function.Injective ↑(algebraMap (↑((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
haveI : IsLocalization _ (Localization m) := Localization.isLocalization
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
⊢ Function.Injective ↑(algebraMap (↑((Sheaf.presheaf F).obj U)) (Localization m))
[PROOFSTEP]
refine IsLocalization.injective (M := m) (S := Localization m) ?_
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
⊢ m ≤ ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U))⁰
[PROOFSTEP]
intro s hs t e
[GOAL]
case this.i
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
⊢ t = 0
[PROOFSTEP]
apply section_ext F (unop U)
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
⊢ ∀ (x : { x // x ∈ U.unop }), ↑(germ (Sheaf.presheaf F) x) t = ↑(germ (Sheaf.presheaf F) x) 0
[PROOFSTEP]
intro x
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t = ↑(germ (Sheaf.presheaf F) x) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case this.i.h
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t = 0
[PROOFSTEP]
apply Submonoid.mem_iInf.mp hs x
[GOAL]
case this.i.h.a
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t * ↑(germ (Sheaf.presheaf F) x) s = 0
[PROOFSTEP]
dsimp
[GOAL]
case this.i.h.a
X : TopCat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
F✝ : Presheaf CommRingCat X
G : SubmonoidPresheaf F✝
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ((forget CommRingCat).obj ((Sheaf.presheaf F).obj U)) :=
  ⨅ (x : { x // x ∈ U.unop }), Submonoid.comap (germ (Sheaf.presheaf F) x) (↑(stalk (Sheaf.presheaf F) ↑x))⁰
this : IsLocalization m (Localization m)
s : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
hs : s ∈ m
t : (forget CommRingCat).obj ((Sheaf.presheaf F).obj U)
e : t * s = 0
x : { x // x ∈ U.unop }
⊢ ↑(germ (Sheaf.presheaf F) x) t * ↑(germ (Sheaf.presheaf F) x) s = 0
[PROOFSTEP]
rw [← map_mul, e, map_zero]