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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ (coneEquivInverse F U ⋙ coneEquivFunctor F U).map f ≫
      { hom := { hom := 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj d).pt, w := ⋯ },
          inv := { hom := 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj d).pt, w := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
    { hom := { hom := 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt, w := ⋯ },
          inv := { hom := 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt, w := ⋯ },
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).map f

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c d : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ d
⊢ ((coneEquivInverse F U ⋙ coneEquivFunctor F U).map f ≫
        { hom := { hom := 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj d).pt, w := ⋯ },
            inv := { hom := 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj d).pt, w := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom).hom =
    ({ hom := { hom := 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt, w := ⋯ },
            inv := { hom := 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt, w := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).map f).hom
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)
⊢ 𝟙 (F.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U =
    Pi.lift fun b ↦ F.map (coconeιApp U (Pairwise.pair b.1 b.2)).op

Tactic:
ext

Goal state after:
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.obj (op (iSup U))) ≫ SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (Pi.lift fun b ↦ F.map (coconeιApp U (Pairwise.pair b.1 b.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
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)
⊢ (𝟙 (F.obj (op (iSup U))) ≫ Pi.lift fun b ↦ F.map (coconeιApp U (Pairwise.pair b.1 b.2)).op) =
    SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U

Tactic:
ext

Goal state after:
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.obj (op (iSup U))) ≫ Pi.lift fun b ↦ F.map (coconeιApp U (Pairwise.pair b.1 b.2)).op) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝ =
    (SheafConditionEqualizerProducts.res F U ≫ SheafConditionEqualizerProducts.leftRes F U) ≫
      limit.π (Discrete.functor fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) j✝
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩
wV : (fun x_1 ↦ fV (iV x_1)) ⟨↑w, ⋯⟩ = (ConcreteCategory.hom (F.germ V' ↑⟨↑w, ⋯⟩ ⋯)) gV
wU : (fun x_1 ↦ fU (iU x_1)) ⟨↑w, ⋯⟩ = (ConcreteCategory.hom (F.germ U' ↑⟨↑w, ⋯⟩ ⋯)) gU
⊢ (ConcreteCategory.hom (F.map iU'.op ≫ F.germ W ↑w ⋯)) gU = (ConcreteCategory.hom (F.germ V' ↑⟨↑w, ⋯⟩ ⋯)) gV

Tactic:
← F.germ_res iV' w w.2.1,

Goal state after:
case h.refine_3
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩
wV : (fun x_1 ↦ fV (iV x_1)) ⟨↑w, ⋯⟩ = (ConcreteCategory.hom (F.germ V' ↑⟨↑w, ⋯⟩ ⋯)) gV
wU : (fun x_1 ↦ fU (iU x_1)) ⟨↑w, ⋯⟩ = (ConcreteCategory.hom (F.germ U' ↑⟨↑w, ⋯⟩ ⋯)) gU
⊢ (ConcreteCategory.hom (F.map iU'.op ≫ F.germ W ↑w ⋯)) gU = (ConcreteCategory.hom (F.map iV'.op ≫ F.germ W ↑w ⋯)) gV
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ HasSmallInductiveDimensionLT X 1 ↔ IsTopologicalBasis {s | IsClopen s}

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis {s | IsClopen s}

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsTopologicalBasis {s | IsClopen s} → HasSmallInductiveDimensionLT X 1
Module: Mathlib.Topology.Subpath

Goal state before:
pp: t₀ t₁ : ↑I
⊢ (∀ (a : ↑I), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁) ∧ ∀ b ∈ uIcc t₀ t₁, ∃ a, Icc.convexComb t₀ t₁ a = b

Tactic:
constructor

Goal state after:
case left
t₀ t₁ : ↑I
⊢ ∀ (a : ↑I), Icc.convexComb t₀ t₁ a ∈ uIcc t₀ t₁

case right
t₀ t₁ : ↑I
⊢ ∀ b ∈ uIcc t₀ t₁, ∃ a, Icc.convexComb t₀ t₁ a = b
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case h
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ Icc.convexComb t₀ t₁ ⟨s, hs⟩ = t

Tactic:
ext

Goal state after:
case h
t₀ t₁ : ↑I
t : ↑(Icc 0 1)
s : ℝ
hs : s ∈ Icc 0 1
hst : (fun θ ↦ (1 - θ) • ↑t₀ + θ • ↑t₁) s = ↑t
⊢ ↑(Icc.convexComb t₀ t₁ ⟨s, hs⟩) = ↑t
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 = ∅
hY₁B : insert Y₁ B ∈ 𝒮
⊢ False

Tactic:
grind [show insert Y₁ B ⊆ B from hB.le_of_ge hY₁B (Set.subset_insert Y₁ B)]

Goal state after:
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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : { x // x ∈ segment ℝ ↑y1 ↑y2 }
h1 : sublevelLeft X f t' ↑z ⊆ sublevelLeft X f t' ↑y1
⊢ z ∈ J1

Tactic:
mem_J1_iff,

Goal state after:
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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : { x // x ∈ segment ℝ ↑y1 ↑y2 }
h1 : sublevelLeft X f t' ↑z ⊆ sublevelLeft X f t' ↑y1
⊢ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) → ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s

case mpr
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: case h_trans
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
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
⊢ SetRel.IsTrans (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U)

Tactic:
constructor

Goal state after:
case h_trans
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
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
⊢ ∀ (a b c : SeparationQuotient X),
    (a, b) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
      (b, c) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
        (a, c) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: case h_trans
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
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
⊢ ∀ (a b c : SeparationQuotient X),
    (a, b) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
      (b, c) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
        (a, c) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U

Tactic:
rintro x y z

Goal state after:
case h_trans
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
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
x y z : SeparationQuotient X
⊢ (x, y) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
    (y, z) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U →
      (x, z) ∈ Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U
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))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := fun n ↦ { carrier := X2 n, isCompact' := ⋯, nonempty' := ⋯ }
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
n : ℕ
⊢ Nonempty (↥(X3 n) ≃ᵢ (u n).Rep)

Tactic:
constructor

Goal state after:
X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := ⋯
this✝ : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := ⋯
Y : (n : ℕ) → AuxGluingStruct (X n) := ⋯
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := ⋯
Z : Type := ⋯
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := ⋯
coeZ : Z0 → UniformSpace.Completion Z0 := ⋯
X2 : ℕ → Set (UniformSpace.Completion Z0) := ⋯
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))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
D2 : ∀ (n : ℕ), hausdorffDist (X2 n) (X2 n.succ) < d n
X3 : ℕ → NonemptyCompacts Z := ⋯
this : CauchySeq X3
L : NonemptyCompacts Z
hL : Tendsto X3 atTop (𝓝 L)
n : ℕ
⊢ ↥(X3 n) ≃ᵢ (u n).Rep
Module: Mathlib.Topology.Sion

Goal state before:
pp: case a.inl
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
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
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ (∃ x ∈ X, sup_y x = t) ↔ t = sup_inf

Tactic:
constructor

Goal state after:
case a.inl.mp
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
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
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ (∃ x ∈ X, sup_y x = t) → t = sup_inf

case a.inl.mpr
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
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
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
sup_y : E → β
inf_sup : β
hinf_sup : IsGLB {x | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup
inf_x : F → β
sup_inf : β
cY : Convex ℝ ∅
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) ∅
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ ∅ fun y ↦ f x y
hfy hfy' hinf_x : True
hsup_inf : IsBot sup_inf
hsup_y : ∀ x ∈ X, sup_y x = sup_inf
t : β
⊢ t = sup_inf → ∃ x ∈ X, sup_y x = t
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝¹⁸ : NontriviallyNormedField 𝕜
B₁ : Type u_3
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 B₁
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹¹ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹⁰ : FiberBundle F₁ E₁
inst✝⁹ : VectorBundle 𝕜 F₁ E₁
B₂ : Type u_6
F₂ : Type u_7
inst✝⁸ : NormedAddCommGroup F₂
inst✝⁷ : NormedSpace 𝕜 F₂
E₂ : B₂ → Type u_8
inst✝⁶ : (x : B₂) → AddCommGroup (E₂ x)
inst✝⁵ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝⁴ : TopologicalSpace B₂
inst✝³ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝² : (x : B₂) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
x₀ x : B₁
y₀ y : B₂
ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y
hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet
⊢ inCoordinates F₁ F₂ x₀ x y₀ y ϕ =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
          ϕ).compContinuousLinearMap
      ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm

Tactic:
ext

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁸ : NontriviallyNormedField 𝕜
B₁ : Type u_3
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 B₁
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹¹ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹⁰ : FiberBundle F₁ E₁
inst✝⁹ : VectorBundle 𝕜 F₁ E₁
B₂ : Type u_6
F₂ : Type u_7
inst✝⁸ : NormedAddCommGroup F₂
inst✝⁷ : NormedSpace 𝕜 F₂
E₂ : B₂ → Type u_8
inst✝⁶ : (x : B₂) → AddCommGroup (E₂ x)
inst✝⁵ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝⁴ : TopologicalSpace B₂
inst✝³ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝² : (x : B₂) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
x₀ x : B₁
y₀ y : B₂
ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y
hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet
x✝ : ι → F₁
⊢ (inCoordinates F₁ F₂ x₀ x y₀ y ϕ) x✝ =
    (((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
            ϕ).compContinuousLinearMap
        ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm)
      x✝