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

Goal state before:
pp: case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsEmpty X
⊢ IsEmpty X

Tactic:
;

Goal state after:
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsEmpty X
⊢ IsEmpty X
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅
⊢ 𝒮.Nonempty

Tactic:
;

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅
⊢ 𝒮.Nonempty
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ 5⁻¹ * δ + 5⁻¹ * δ / 2 + 5⁻¹ * δ = δ / 2

Tactic:
;

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ 5⁻¹ * δ + 5⁻¹ * δ / 2 + 5⁻¹ * δ = δ / 2
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
this : ∃ z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y', x ∈ sublevelLeft X f b' ↑z'
⊢ x ∈ sublevelLeft X f b' ↑y

Tactic:
obtain ⟨z', hz', hxz'⟩ := this
    /- We need to prove `x ∈ sublevelLeft X f b' y`.
       Assume that there is `z' ∈ J` such that `x ∈ sublevelLeft b' z'`.
       It suffices to prove that `sublevelLeft X f b' z' ⊆ sublevelLeft X f b' y`.` -/
    suffices sublevelLeft X f b' z' ⊆ sublevelLeft X f b' y from this hxz'
    /- Otherwise, using `sublevelLeft_subset_or`, we see that
       `sublevelLeft X f b' z' ⊆ sublevelLeft t' y'`
       hence `x ∈ sublevelLeft t' y ∩ sublevelLeft t' y' = ∅`, a contradiction. -/
    apply (sublevelLeft_subset_or hfx' hfy hfy' cY a b' y y' ha hb' z').resolve_right
    intro hz'2
    have hz'Y : (z' : F) ∈ Y := (convex_iff_segment_subset.mp cY) y.prop y'.prop z'.prop
    apply (nonempty_sublevelLeft ne_X kX hfy ⟨z', hz'Y⟩ hb).not_subset_empty
    rw [← (disjoint_sublevelLeft ha hb').inter_eq]
    apply subset_inter hz'
    grw [monotone_sublevelLeft _ hbb'.le, hz'2]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
n : ℕ
x y : GlueSpace ⋯ ⋯
⊢ edist (c n x) (c n y) = edist x y

Tactic:
;

Goal state after:
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
n : ℕ
x y : GlueSpace ⋯ ⋯
⊢ edist (c n x) (c n y) = edist x y
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : insert Y₁ B ∉ 𝒮
hY₂B : insert Y₂ B ∉ 𝒮
⊢ False

Tactic:
dsimp [𝒮] at hY₁B hY₂B

Goal state after:
case neg
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun x ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s | s ∈ B ∧ IsClosed[inst✝⁴] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst✝⁴] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
Y₁ Y₂ : Set X
hY₁_cl : IsClosed[inst✝⁴] Y₁
hY₂_cl : IsClosed[inst✝⁴] Y₂
hc₁ : IsCompact Y₁ᶜ
hc₂ : IsCompact Y₂ᶜ
hsub : Z ⊆ Y₁ ∪ Y₂
x₁ : X
hx₁ : x₁ ∈ Z ∩ Y₁ᶜ
x₂ : X
hx₂ : x₂ ∈ Z ∩ Y₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : ¬(insert Y₁ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₁ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₁ B = ∅)
hY₂B : ¬(insert Y₂ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₂ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₂ B = ∅)
⊢ False
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n : ℕ
γ : Path a b
t : Fin (n + 1) → ↑I
⊢ (concat (⇑γ ∘ t) fun k ↦ γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (last n)))

Tactic:
induction n with
  | zero =>
    simp only [concat_zero, reduceLast, subpath_self]
    exact refl _
  | succ n ih =>
    rw [concat_succ]
    exact trans ((ih (t ∘ castSucc)).hcomp (refl _)) (subpathTransSubpath γ _ _ _)

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x✝¹ : SetRel X X
x✝ : x✝¹ ∈ 𝓤 X ∧ x✝¹.IsSymm ∧ x✝¹.IsTrans
left✝ : x✝¹ ∈ 𝓤 X
hU : x✝¹.IsSymm
right✝ : x✝¹.IsTrans
⊢ SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' x✝¹)

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x✝¹ : SetRel X X
x✝ : x✝¹ ∈ 𝓤 X ∧ x✝¹.IsSymm ∧ x✝¹.IsTrans
left✝ : x✝¹ ∈ 𝓤 X
hU : x✝¹.IsSymm
right✝ : x✝¹.IsTrans
⊢ SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' x✝¹)
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
⊢ False

Tactic:
obtain
      ⟨U₁, -, V₁, V₁_in, U₂, -, V₂, V₂_in, V₁_cl, V₂_cl, U₁_op, U₂_op, VU₁, VU₂, hU₁₂⟩ :=
      disjoint_nested_nhds_of_not_inseparable ninsep_xy

Goal state after:
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
𝓝Δ : Filter (γ × γ) := 𝓝ˢ (diagonal γ)
F : Filter (γ × γ) := 𝓝Δ.lift' fun s ↦ s ○ s
V : Set (γ × γ)
V_in : V ∈ 𝓝Δ
H : ¬F ⊓ 𝓟 Vᶜ = ⊥
this : (F ⊓ 𝓟 Vᶜ).NeBot
x y : γ
hxy : ClusterPt (x, y) (F ⊓ 𝓟 Vᶜ)
clV : ClusterPt (x, y) (𝓟 Vᶜ)
ninsep_xy : ¬Inseparable x y
U₁ V₁ : Set γ
V₁_in : V₁ ∈ 𝓝 x
U₂ V₂ : Set γ
V₂_in : V₂ ∈ 𝓝 y
V₁_cl : IsClosed[inst✝²] V₁
V₂_cl : IsClosed[inst✝²] V₂
U₁_op : IsOpen[inst✝²] U₁
U₂_op : IsOpen[inst✝²] U₂
VU₁ : V₁ ⊆ U₁
VU₂ : V₂ ⊆ U₂
hU₁₂ : Disjoint U₁ U₂
⊢ False
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
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✝

Tactic:
;

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
x✝ : ι → F₁
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := c • L }).2 x✝ =
    (c • (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2) x✝

Tactic:
;

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✝