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

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑↑p ≃ᵢ ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))

Tactic:
rfl

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ }) =
    (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))

Tactic:
rfl

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ })

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : IsUltrametricDist X
x y : X
h : x ≠ y
⊢ (fun x1 x2 ↦ ∃ U, IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : EDist X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) = edist x y ^ α⁻¹

Tactic:
edist_def,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : EDist X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) = (edist (ofSnowflaking x) (ofSnowflaking y) ^ α) ^ α⁻¹
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist x y = edist y x

Tactic:
edist_def,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) ^ α = edist y x
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) ^ α = edist y x

Tactic:
edist_def,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) ^ α = edist (ofSnowflaking y) (ofSnowflaking x) ^ α
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: case mpr
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
⊢ ∃ C, ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C

Tactic:
use C ^ α⁻¹

Goal state after:
case h
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
⊢ ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C ^ α⁻¹
Module: Mathlib.Topology.Order.UpperLowerSetTopology

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen[lower α] s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ ↑(LowerSet.Iic a) = Iic a

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ IsTopologicalBasis (lowerBasis α)

Tactic:
by
  convert! isTopologicalBasis_of_subbasis (topology_eq α)
  simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]
  ext s
  constructor
  · rintro ⟨F, hF, rfl⟩
    refine ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩
    simp only [sInter_image]
  · rintro ⟨F, ⟨hF, hs⟩, rfl⟩
    have := hF.to_subtype
    rw [subset_def, Subtype.forall'] at hs
    choose f hf using hs
    exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ ↑(UpperSet.Ici a) = Ici a

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[scott α D] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
s : Set α
⊢ IsOpen[upper α] s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
⊢ scott α univ = upper α

Tactic:
let := upper α

Goal state after:
α : Type u_1
inst✝ : CompleteLinearOrder α
this : TopologicalSpace α := upper α
⊢ scott α univ = upper α
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
u v : L
⊢ {x | min (x u) (x v)} = {x | x u} ∩ {x | x v}

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
X✝ Y✝ : Locale
f : X✝ ⟶ Y✝
u : ↑(Opposite.unop Y✝)
⊢ {x | x ((ConcreteCategory.hom f.unop) u)} = (fun p ↦ FrameHom.comp p (Frm.Hom.hom f.unop)) ⁻¹' {x | x u}

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (hull T a) =
    OrderDual.ofDual (OrderDual.toDual ((⇑OrderDual.toDual ∘ kernel) ((hull T ∘ ⇑OrderDual.ofDual) a)))

Tactic:
rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
obtain hq | hq := le_or_gt q 0
    · convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := not_isPredPrelimit_iff.1 <| mt hx₂ hq.not_ge
      convert isOpen_Iio (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_left

Goal state after:
Module: Mathlib.Topology.Separation.Lemmas

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

Tactic:
← totallyDisconnectedSpace_subtype_iff

Goal state after:
X : Type u_1
inst✝ : MetricSpace X
s : Set X
hs : s.Countable
⊢ 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
⊢ x = y

Tactic:
have e := Φisom.isometryEquivOnRange.trans eΨ

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
⊢ x = y
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
by
  have ha : Isometry ((↑) : p → X) := isometry_subtype_coe
  have hb : Isometry ((↑) : q → X) := isometry_subtype_coe
  have A : dist p q = hausdorffDist (p : Set X) q := rfl
  have I : ↑p = range ((↑) : p → X) := Subtype.range_coe_subtype.symm
  have J : ↑q = range ((↑) : q → X) := Subtype.range_coe_subtype.symm
  rw [A, I, J]
  exact ghDist_le_hausdorffDist ha hb

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
U V W : Opens α
h : U ⟶ V
k : V ⟶ W
K : ↑U.compactsInside
⊢ baseChangeCompactsInside (h ≫ k) K = baseChangeCompactsInside k (baseChangeCompactsInside h K)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
U : Opens α
K : ↑U.compactsInside
⊢ baseChangeCompactsInside (𝟙 U) K = K

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L M : Compacts α
h : K ⟶ L
k : L ⟶ M
U : ↑M.openNhds
⊢ baseChangeOpenNhds (h ≫ k) U = baseChangeOpenNhds h (baseChangeOpenNhds k U)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : ↑K.openNhds
⊢ baseChangeOpenNhds (𝟙 K) U = U

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
⊢ Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows

Tactic:
by
  have : IndiscreteTopology X := ⟨hind⟩
  obtain rfl | hne := eq_or_ne U ⊥
  · intro _ _
    rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]
    · refine ⟨it.from _, fun U hU hs => IsTerminal.hom_ext ?_ _ _⟩
      rwa [le_bot_iff.1 hU.le]
    · apply it.hom_ext
  · convert! Presieve.isSheafFor_top (F ⋙ coyoneda.obj (@op C c))
    rw [Sieve.arrows_eq_top_iff, ← Sieve.id_mem_iff_eq_top]
    have := U.eq_bot_or_top.resolve_left hne
    subst this
    obtain he | ⟨⟨x⟩⟩ := isEmpty_or_nonempty X
    · exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim
    obtain ⟨U, f, hf, hm⟩ := hs x _root_.trivial
    obtain rfl | rfl := U.eq_bot_or_top
    · cases hm
    · convert! hf

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

Goal state before:
pp: case mp
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
⊢ S.Exact → ∀ (x : ↑X), (S.map (forget C X ⋙ stalkFunctor C x)).Exact

Tactic:
intro h x

Goal state after:
case mp
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
S : ShortComplex (Sheaf C X)
h : S.Exact
x : ↑X
⊢ (S.map (forget C X ⋙ stalkFunctor C x)).Exact
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
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
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∈ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ X.germ ((OpenNhds.inclusion p₀).obj (unop j✝)) p₀ ⋯ = colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
rfl

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

Goal state before:
pp: case pos
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
Y : C
U✝ : Opens ↑X
h : p₀ ∈ U✝
⊢ 𝟙 (if p₀ ∈ U✝ then Y else ⊤_ C) = (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

Tactic:
rfl

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

Goal state before:
pp: case neg
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
Y : C
U✝ : Opens ↑X
h : p₀ ∉ U✝
⊢ 𝟙 (if p₀ ∈ U✝ then Y else ⊤_ C) = (𝟙 (skyscraperPresheaf p₀ Y)).app (op U✝)

Tactic:
rfl

Goal state after:
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
⊢ Continuous fun s ↦
    (⟨(↑s).base, ⋯⟩, WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ)))

Tactic:
refine .prodMk (by fun_prop) ?_

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
⊢ Continuous fun s ↦ WithTopology.toTopology ⊥ ((ConcreteCategory.hom (F.germ U x hx)) (surjInv ⋯ (↑s).germ))
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i : ↑c
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f i)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f i)).op)) (StructuredArrow.right ↑i).snd

Tactic:
rfl

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

Goal state before:
pp: case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map (↑h₁.some.right ≫ ((f i).infLERight (f j)).op))) (↑i).right.snd

Tactic:
rfl

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

Goal state before:
pp: case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map (↑h₁.some.right ≫ ((f i).infLELeft (f j)).op))) (↑j).right.snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

Tactic:
rfl

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

Goal state before:
pp: case op.op.single.pair.left
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)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j) =
    (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.1 ≫ F.map ((U p.1).infLELeft (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j)
⊢ Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map ((U i).infLELeft (U j)).op =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op

Tactic:
rfl

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

Goal state before:
pp: case op.op.single.pair.right
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)
i j : ι
h :
  c.π.app WalkingParallelPair.one =
    Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op
h' :
  c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i) =
    (Fork.ι c ≫ Pi.lift fun p ↦ Pi.π (fun i ↦ F.obj (op (U i))) p.2 ≫ F.map ((U p.1).infLERight (U p.2)).op) ≫
      Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (j, i)
⊢ Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map ((U j).infLERight (U i)).op =
    Fork.ι c ≫ Pi.π (fun i ↦ F.obj (op (U i))) i ≫ F.map (homOfLE ⋯).op

Tactic:
rfl

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝¹ : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
⊢ (InducedCategory.Hom.hom 0).app (op W) = 0

Tactic:
rfl

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
this✝² : Presheaf.IsLocallySurjective S.g.hom
W : Opens ↑X
Wle : W ≤ U
hW : x ∈ W
t₁ : ↑(S.X₂.obj.obj (op W))
ht₁ : (ConcreteCategory.hom (S.g.hom.app (op W))) t₁ = (s |_ W) Wle
t₂ : ToType (S.X₂.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W))) :=
  ((StructuredArrow.right t).snd |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ -
    (t₁ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
this✝¹ : (ConcreteCategory.hom (S.g.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₂ = 0
t₃ : ↑(S.X₁.obj.obj (op (unop (StructuredArrow.right t).fst ⊓ W)))
ht₃ : (ConcreteCategory.hom (S.f.hom.app (op (unop (StructuredArrow.right t).fst ⊓ W)))) t₃ = t₂
t₄ : ↑(S.X₁.obj.obj (op W))
ht₄ : (t₄ |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = t₃
f : Fin 2 → Opens ↑X := ![unop (StructuredArrow.right t).fst, W]
sf : (i : Fin 2) → ↑(S.X₂.obj.obj (op (f i))) :=
  fun x ↦
    match x with
    | 0 => (StructuredArrow.right t).snd
    | 1 => t₁ + (ConcreteCategory.hom (S.f.hom.app (op W))) t₄
this✝ : (sf 0 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯ = (sf 1 |_ (unop (StructuredArrow.right t).fst ⊓ W)) ⋯
t₅ : ToType (S.X₂.obj.obj (op (iSup f)))
ht₅ : IsGluing S.X₂.obj f sf t₅
right✝ : ∀ (y : ToType (S.X₂.obj.obj (op (iSup f)))), (fun t₅ ↦ IsGluing S.X₂.obj f sf t₅) y → y = t₅
le : iSup f ≤ U
this : S.f.hom.app (op W) ≫ S.g.hom.app (op W) = 0
⊢ (s |_ W) Wle = (ConcreteCategory.hom (S.X₃.obj.map (homOfLE ⋯).op)) s

Tactic:
rfl

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

Goal state before:
pp: case op.single
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✝ : ι
⊢ F.map (coconeιApp U (single a✝)).op = F.map (leSupr U a✝).op

Tactic:
rfl

Goal state after:
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 (coconeιApp U (Pairwise.pair a✝¹ a✝)).op = F.map ((leSupr U a✝¹).op ≫ ((U a✝¹).infLELeft (U a✝)).op)

Tactic:
rfl

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

Goal state before:
pp: case op.single
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✝ : ι
⊢ F.map (leSupr U a✝).op = F.map (coconeιApp U (single a✝)).op

Tactic:
rfl

Goal state after: