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
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.hom ≫ (coneEquivInverseObj F U c').π.app (op (Pairwise.pair i j)) =
    (coneEquivInverseObj F U c).π.app (op (Pairwise.pair i j))

Tactic:
dsimp

Goal state after:
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
c c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
i j : ι
⊢ f.hom ≫ c'.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)
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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
      ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π.app WalkingParallelPair.zero =
    ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π.app WalkingParallelPair.zero

Tactic:
dsimp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ Fork.ι c = Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))
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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).pt ≫
      ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π.app WalkingParallelPair.one =
    ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π.app WalkingParallelPair.one

Tactic:
dsimp

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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 c.pt ≫ c.π.app WalkingParallelPair.one =
    Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))
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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
      ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π.app WalkingParallelPair.zero =
    ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π.app WalkingParallelPair.zero

Tactic:
dsimp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun i ↦ ((coneEquivInverse F U).obj c).π.app (op (single i))) = Fork.ι c
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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ 𝟙 ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).pt ≫
      ((coneEquivInverse F U ⋙ coneEquivFunctor F U).obj c).π.app WalkingParallelPair.one =
    ((𝟭 (Cone (SheafConditionEqualizerProducts.diagram F U))).obj c).π.app WalkingParallelPair.one

Tactic:
dsimp

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
c : Cone (SheafConditionEqualizerProducts.diagram F U)
⊢ (𝟙 c.pt ≫ Pi.lift fun b ↦ ((coneEquivInverse F U).obj c).π.app (op (Pairwise.pair b.1 b.2))) =
    c.π.app WalkingParallelPair.one
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 := { 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

Tactic:
dsimp

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
⊢ f.hom ≫ 𝟙 d.pt = 𝟙 c.pt ≫ 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)
⊢ 𝟙 ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).pt ≫
      (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.one =
    ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.one

Tactic:
dsimp

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)
⊢ 𝟙 (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
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)
⊢ 𝟙 (SheafConditionEqualizerProducts.fork F U).pt ≫
      ((coneEquiv F U).functor.obj (Functor.mapCone F (cocone U).op)).π.app WalkingParallelPair.one =
    (SheafConditionEqualizerProducts.fork F U).π.app WalkingParallelPair.one

Tactic:
dsimp

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)
⊢ (𝟙 (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
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)

Tactic:
dsimp

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' i)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)

Tactic:
dsimp

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' i)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (id i.1 ∩ id i.2)

Tactic:
dsimp

Goal state after:
case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (i.1 ∩ i.2)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (id i.1 ∩ id i.2)

Tactic:
dsimp

Goal state after:
case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (i.1 ∩ i.2)
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
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans ((CauchyFilter.gen ∘ id) i)

Tactic:
· exact fun _ ⟨_, _, hU⟩ ↦ by simpa using CauchyFilter.isTrans_gen

Goal state after:
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
⊢ inf_sup ≤ sup_inf

Tactic:
suffices {t | ∃ x ∈ X, sup_y x = t} = {sup_inf} from (this ▸ hinf_sup).unique (by simp) |>.le

Goal state after:
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} = {sup_inf}
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)
b : B
L₁ : E₁ b ≃L[𝕜] F₁ := Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ b) b ⋯
L₂ : E₂ b ≃L[𝕜] F₂ := Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ b) b ⋯
⊢ IsInducing fun x' ↦
    (Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F₂ E₂ b) b).compContinuousAlternatingMap
      (x'.compContinuousLinearMap (Trivialization.symmL 𝕜 (trivializationAt F₁ E₁ b) b))

Tactic:
convert! (L₁.continuousAlternatingMapCongr L₂).toHomeomorph.isInducing

Goal state after:
case e'_5
𝕜 : 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)
b : B
L₁ : E₁ b ≃L[𝕜] F₁ := Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ b) b ⋯
L₂ : E₂ b ≃L[𝕜] F₂ := Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ b) b ⋯
x✝ : E₁ b [⋀^ι]→L[𝕜] E₂ b
⊢ (Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F₂ E₂ b) b).compContinuousAlternatingMap
      (x✝.compContinuousLinearMap (Trivialization.symmL 𝕜 (trivializationAt F₁ E₁ b) b)) =
    (L₁.continuousAlternatingMapCongr L₂).toHomeomorph x✝