mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²¹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²⁰ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁸ : FiberBundle F₁ E₁
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₂ E₂
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
x : B
x✝ : x ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet
L L' : E₁ x [⋀^ι]→L[𝕜] E₂ x
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L + L' }).2 =
    (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2 +
      (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L' }).2

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝²¹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²⁰ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁸ : FiberBundle F₁ E₁
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₂ E₂
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
x : B
x✝¹ : x ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet
L L' : E₁ x [⋀^ι]→L[𝕜] E₂ x
x✝ : ι → F₁
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L + L' }).2 x✝ =
    ((↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2 +
        (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L' }).2)
      x✝
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²¹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²⁰ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁸ : FiberBundle F₁ E₁
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₂ E₂
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
x : B
x✝ : x ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet
c : 𝕜
L : E₁ x [⋀^ι]→L[𝕜] E₂ x
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := c • L }).2 =
    c • (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝²¹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²⁰ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁸ : FiberBundle F₁ E₁
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₂ E₂
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
x : B
x✝¹ : x ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet
c : 𝕜
L : E₁ x [⋀^ι]→L[𝕜] E₂ x
x✝ : ι → F₁
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := c • L }).2 x✝ =
    (c • (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2) x✝