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

Goal state before:
pp: case mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nontrivial N
h : ∃ y, y ≠ Classical.arbitrary N := exists_ne (Classical.arbitrary N)
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a * Quot.mk (⇑(Homotopic.setoid N x)) b)
      (Quot.mk (⇑(Homotopic.setoid N x)) c * Quot.mk (⇑(Homotopic.setoid N x)) d) =
    Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) a) (Quot.mk (⇑(Homotopic.setoid N x)) c) *
      Mul.mul (Quot.mk (⇑(Homotopic.setoid N x)) b) (Quot.mk (⇑(Homotopic.setoid N x)) d)

Tactic:
apply congr_arg Quotient.mk'

Goal state after:
case mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nontrivial N
h : ∃ y, y ≠ Classical.arbitrary N := ⋯
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ (loopHomeo (Classical.choose h)).symm
      (((loopHomeo (Classical.choose h)).toEquiv
            ((loopHomeo (Classical.arbitrary N)).symm
              (((loopHomeo (Classical.arbitrary N)).toEquiv d).trans
                ((loopHomeo (Classical.arbitrary N)).toEquiv c)))).trans
        ((loopHomeo (Classical.choose h)).toEquiv
          ((loopHomeo (Classical.arbitrary N)).symm
            (((loopHomeo (Classical.arbitrary N)).toEquiv b).trans ((loopHomeo (Classical.arbitrary N)).toEquiv a))))) =
    (loopHomeo (Classical.arbitrary N)).symm
      (((loopHomeo (Classical.arbitrary N)).toEquiv
            ((loopHomeo (Classical.choose h)).symm
              (((loopHomeo (Classical.choose h)).toEquiv d).trans ((loopHomeo (Classical.choose h)).toEquiv b)))).trans
        ((loopHomeo (Classical.arbitrary N)).toEquiv
          ((loopHomeo (Classical.choose h)).symm
            (((loopHomeo (Classical.choose h)).toEquiv c).trans ((loopHomeo (Classical.choose h)).toEquiv a)))))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case hbc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist t y ≤ max (dist x z) (dist t y)

Tactic:
· apply le_max_right

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ ⇑ofSnowflaking ⁻¹' eball x r = eball (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' eball x r ↔ { val := y } ∈ eball (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
⊢ ⇑ofSnowflaking ⁻¹' closedEBall x r = closedEBall (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : X
r : ℝ≥0∞
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' closedEBall x r ↔ { val := y } ∈ closedEBall (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' ball x r = ball (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' ball x r ↔ { val := y } ∈ ball (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
⊢ ⇑ofSnowflaking ⁻¹' closedBall x r = closedBall (toSnowflaking x) (r ^ α)

Tactic:
ext ⟨y⟩

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' closedBall x r ↔ { val := y } ∈ closedBall (toSnowflaking x) (r ^ α)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ IsLowerSet s

Tactic:
by rw [topology_eq α]; rfl

Goal state after:
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsOpen[L] sᶜ ↔ IsOpen[S] sᶜ

Tactic:
(lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsOpen[S] sᶜ ↔ IsOpen[S] sᶜ
Module: Mathlib.Topology.Separation.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
s : Set X
hs : s.Countable
⊢ TotallyDisconnectedSpace ↑s

Tactic:
have : Countable s := hs

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
s : Set X
hs : s.Countable
this : Countable ↑s
⊢ TotallyDisconnectedSpace ↑s
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)
eΨ : ↑(range Φ) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
⊢ x = y

Tactic:
rw [← x.toGHSpace_rep, ← y.toGHSpace_rep, toGHSpace_eq_toGHSpace_iff_isometryEquiv]

Goal state after:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : (↑(range Ψ) ≃ᵢ y.Rep) = (↑(range Φ) ≃ᵢ y.Rep)
eΨ : ↑(range Φ) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
⊢ Nonempty (x.Rep ≃ᵢ y.Rep)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
⊢ (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      if h : p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop V))) then eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop U))) then c else ⊤_ C)) =
    f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯

Tactic:
have hV : p₀ ∈ (OpenNhds.inclusion p₀).obj V.unop := V.unop.2

Goal state after:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕 ⟶ skyscraperPresheaf p₀ c
U V : (OpenNhds p₀)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop V)
⊢ (f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫
      if h : p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop V))) then eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop (op ((OpenNhds.inclusion p₀).obj (unop U))) then c else ⊤_ C)) =
    f.app (op ((OpenNhds.inclusion p₀).obj (unop U))) ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hmem : ∃ (h : ↑y ∈ V), (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    { base := ↑a, germ := (ConcreteCategory.hom (F.germ U ↑a ⋯)) (surjInv ⋯ g) } ∈
      {g | ∃ (h : g.base ∈ V), g.germ = (ConcreteCategory.hom (F.germ V g.base h)) f}

Tactic:
rcases hmem with ⟨hyV, hgf⟩

Goal state after:
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    { base := ↑a, germ := (ConcreteCategory.hom (F.germ U ↑a ⋯)) (surjInv ⋯ g) } ∈
      {g | ∃ (h : g.base ∈ V), g.germ = (ConcreteCategory.hom (F.germ V g.base h)) f}
Module: Mathlib.Topology.Sheaves.EtaleSpace

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ ∃ (h : ↑z ∈ V), (ConcreteCategory.hom (F.germ U ↑z ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V (↑z) h)) f

Tactic:
use ιWV.le hz

Goal state after:
case h
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ (ConcreteCategory.hom (F.germ U ↑z ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑z ⋯)) f
Module: Mathlib.Topology.Sheaves.MayerVietoris

Goal state before:
pp: case inr
T : Type u
inst✝ : TopologicalSpace T
sq : Square (Opens T)
h₄ : sq.X₄ = sq.X₂ ⊔ sq.X₃
h₁ : sq.X₁ = sq.X₂ ⊓ sq.X₃
x : T
hx : x ∈ ↑sq.X₃
⊢ ∃ U f, (Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄).arrows f ∧ x ∈ U

Tactic:
· exact ⟨_, _, ⟨Sieve.ofArrows_mk _ _ WalkingPair.right, hx⟩⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case one.one.id
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone ((diagram U).op ⋙ F)
⊢ ((Functor.const WalkingParallelPair).obj c.pt).map (WalkingParallelPairHom.id WalkingParallelPair.one) ≫
      WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) =
    WalkingParallelPair.casesOn WalkingParallelPair.one (Pi.lift fun i ↦ c.π.app (op (single i)))
        (Pi.lift fun b ↦ c.π.app (op (Pairwise.pair b.1 b.2))) ≫
      (SheafConditionEqualizerProducts.diagram F U).map (WalkingParallelPairHom.id WalkingParallelPair.one)

Tactic:
· dsimp
          ext
          simp

Goal state after:
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 : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (i ∩ ⋂₀ a).Nonempty

Tactic:
← Set.sInter_insert

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 : IsIrreducible Z
hη : IsGenericPoint hZ_irred.genericPoint Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (⋂₀ insert i a).Nonempty
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
⊢ Continuous fun x ↦ ((γ.subpath t₀ (Icc.convexComb t₁ t₂ x.1)).trans (γ.subpath (Icc.convexComb t₁ t₂ x.1) t₂)) x.2

Tactic:
by
    let γ₁ (t : I) := γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
    let γ₂ (t : I) := γ.subpath (Icc.convexComb t₁ t₂ t) t₂
    refine Path.trans_continuous_family γ₁ ?_ γ₂ ?_ <;>
    refine γ.subpath_continuous_family.comp (.prodMk ?_ <| .prodMk ?_ ?_) <;>
    fun_prop

Goal state after:
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : Fintype ι
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₁)
inst✝¹² : (x : B) → TopologicalSpace (E₁ x)
inst✝¹¹ : FiberBundle F₁ E₁
inst✝¹⁰ : VectorBundle 𝕜 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✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
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₂'
⊢ ∃ f,
    ContinuousOn f ((continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet ∩ (continuousAlternatingMap 𝕜 ι e₁' e₂').baseSet) ∧
      ∀ b ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet ∩ (continuousAlternatingMap 𝕜 ι e₁' e₂').baseSet,
        ∀ (v : F₁ [⋀^ι]→L[𝕜] F₂),
          (f b) v =
            (↑(continuousAlternatingMap 𝕜 ι e₁' e₂')
                { proj := b, snd := (continuousAlternatingMap 𝕜 ι e₁ e₂).symm b v }).2

Tactic:
exact ⟨continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂',
      continuousOn_continuousAlternatingMapCoordChange,
      continuousAlternatingMapCoordChange_apply⟩

Goal state after: