mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.pair
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
P : IsLimit (SheafConditionEqualizerProducts.fork F U)
a✝¹ a✝ : ι
⊢ F.map ((leSupr U a✝¹).op ≫ ((U a✝¹).infLELeft (U a✝)).op) = F.map (coconeιApp U (Pairwise.pair a✝¹ a✝)).op

Tactic:
rfl

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ SheafConditionEqualizerProducts.res F U = Pi.lift fun i ↦ F.map (coconeιApp U (single i)).op

Tactic:
rfl

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
j✝ : Discrete (ι × ι)
⊢ F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op) =
    F.map (coconeιApp U (Pairwise.pair j✝.as.1 j✝.as.2)).op

Tactic:
rfl

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
⊢ (Pi.lift fun i ↦ F.map (coconeιApp U (single i)).op) = SheafConditionEqualizerProducts.res F U

Tactic:
rfl

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
Q : IsLimit (Functor.mapCone F (cocone U).op)
j✝ : Discrete (ι × ι)
⊢ F.map (coconeιApp U (Pairwise.pair j✝.as.1 j✝.as.2)).op =
    F.map ((leSupr U j✝.as.1).op ≫ ((U j✝.as.1).infLELeft (U j✝.as.2)).op)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝¹ : S.X₁.IsFlasque
inst✝ : S.X₂.IsFlasque
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ Epi (S.g.hom.app U ≫ S.X₃.obj.map i)

Tactic:
← S.g.hom.naturality i

Goal state after:
X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝¹ : S.X₁.IsFlasque
inst✝ : S.X₂.IsFlasque
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
⊢ Epi (S.X₂.obj.map i ≫ S.g.hom.app V)
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Epi (terminalIsTerminal.from A)
U V : (Opens ↑X)ᵒᵖ
r : U ⟶ V
h1 : p₀ ∈ unop U
h2 : p₀ ∉ unop V
⊢ Epi (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C))

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case refine_1.f
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ t ∈ {s | IsOpen[inst✝²] s ∧ IsCompact s} → IsOpen[inst✝²] t

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case refine_1.g
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ t ∈ {s | IsClosed[inst✝²] s ∧ IsCompact sᶜ} → IsClosed[inst✝²] t

Tactic:
grind

Goal state after:
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 = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ⋃₀ c ⊆ 𝔅

Tactic:
grind

Goal state after:
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 = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
x✝ hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h✝ : hne = ⋯
⊢ ⋂₀ ⋃₀ c = ∅

Tactic:
grind

Goal state after:
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 = ∅}
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 ⊆ B

Tactic:
grind

Goal state after:
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 = ∅}
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₂ ∈ 𝔅
⊢ Y₁ ∩ ⋂₀ B = ∅

Tactic:
grind

Goal state after:
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 = ∅}
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 = ∅
⊢ Y₂ ∩ ⋂₀ B = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
p : Fin (n + 2) → X
F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
⊢ trans (dfoldl n ((fun i ↦ Path (p 0) (p i)) ∘ castSucc) (fun x1 x2 ↦ trans x2 (F x1.castSucc)) (refl (p 0)))
      (F (last n)) =
    (concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))

Tactic:
rfl

Goal state after:
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 = ∅}
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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
⊢ Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅

Tactic:
grind

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 ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : ℕ → Set (UniformSpace.Completion Z0) := fun n ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
n : ℕ
⊢ X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))

Tactic:
rfl

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

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsSymm (⋂ i_1, id (i.snd i_1))

Tactic:
· simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
    rintro _ _ _ _ _
    infer_instance

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

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsTrans (⋂ i_1, id (i.snd i_1))

Tactic:
· simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
    rintro _ _ _ _ _
    infer_instance

Goal state after:
Module: Mathlib.Util.SleepHeartbeats

Goal state before:
pp: ⊢ 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
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
cX : Convex ℝ X
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
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
have hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X := fun x hx ↦ by
    apply lowerSemicontinuousWithinAt_iSup
    intro i
    exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : CompleteLinearOrder β
inst✝¹⁰ : DenselyOrdered β
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
cX : Convex ℝ X
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
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
hlsc : LowerSemicontinuousOn (fun x ↦ ⨆ y ∈ Y, f x y) X
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
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₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : Trivialization.IsLinear 𝕜 e₁
inst✝ : Trivialization.IsLinear 𝕜 e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ [⋀^ι]→L[𝕜] F₂
⊢ cast ⋯ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂).symm (b, L)).snd =
    (Trivialization.symmL 𝕜 e₂ b).compContinuousAlternatingMap
      (L.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ b))

Tactic:
rfl

Goal state after: