mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
⊢ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c ≤ ↑(logSizeBallSeq J hJ a c l).radius * c

Tactic:
tsub_le_self

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
hJ : J.Nonempty
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
h : edist (logSizeBallSeq J hJ a c l).point s ≤ (↑(logSizeBallSeq J hJ a c l).radius - 1) * c
⊢ ↑(logSizeBallSeq J hJ a c l).radius * c ≤ ↑(logSizeBallSeq J hJ a c l).radius * c
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x y z : X
⊢ d x y ⊔ d y z ⊔ (d' x y ⊔ d' y z) ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z)

Tactic:
simp [sup_comm, sup_left_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ nnHolderNorm r f ≤ C

Tactic:
rw [← ENNReal.coe_le_coe, hf.memHolder.coe_nnHolderNorm_eq_eHolderNorm]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ ↑C
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ min (min (⨅ (_ : x ≠ y), edist x y) (⨅ x_1 ∈ {z}, ⨅ (_ : x ≠ x_1), edist x x_1))
      (min (⨅ y_1 ∈ {z}, ⨅ (_ : y ≠ y_1), edist y y_1) {z}.einfsep) =
    min (min (edist x y) (edist x z)) (edist y z)

Tactic:
iInf_singleton,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) {z}.einfsep) =
    min (min (edist x y) (edist x z)) (edist y z)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
cases nonempty_fintype s
  by_cases hs : s.Nontrivial
  · rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
    exact hxy'.symm ▸ edist_pos.2 hxy
  · rw [not_nontrivial_iff] at hs
    exact hs.einfsep.symm ▸ WithTop.top_pos

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
by_cases hxy : x = y

Goal state after:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ {x, y}.infsep = (edist x y).toReal

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ {x, y}.infsep = (edist x y).toReal
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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝ : IsCompact s
this : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

Tactic:
have : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ') := by
    rw [ΦΦ', ΨΨ', range_comp, range_comp]
    exact hausdorffDist_image isometry_subtype_coe

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝¹ : IsCompact s
this✝ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
Module: Mathlib.Topology.MetricSpace.Snowflaking

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

Tactic:
by
  rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedEBall,
    toSnowflaking_ofSnowflaking, ENNReal.rpow_inv_rpow hα₀.ne']

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
this : ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)
⊢ ∃ U, (∀ (n : ℕ), (U n).Infinite) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
rcases this with ⟨U, hne, ho, hd⟩
    refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩
    · refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
      suffices n.pair i = n.pair j by simpa
      apply hd.eq
      simpa [hij, onFun] using (hne _).ne_empty
    · refine fun n n' hne ↦ disjoint_iUnion_left.2 fun m ↦ disjoint_iUnion_right.2 fun m' ↦ hd ?_
      simp [hne]

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : ∃ x, (𝓝[≠] x).NeBot
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
rcases h with ⟨x, hx⟩

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x✝ ↔ IsOpen[lowerSet αᵒᵈ] x✝

Tactic:
IsUpperSet.topology_eq α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
x✝ : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x✝ ↔ IsOpen[lowerSet αᵒᵈ] x✝
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

Tactic:
specializes_iff_closure_subset,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ closure[instTopologicalSpace] {toUpperSet b} ⊆ closure[instTopologicalSpace] {toUpperSet a} ↔ b ≤ a
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toLowerSet a ⤳ toLowerSet b ↔ a ≤ b

Tactic:
specializes_iff_closure_subset,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ closure[instTopologicalSpace] {toLowerSet b} ⊆ closure[instTopologicalSpace] {toLowerSet a} ↔ a ≤ b
Module: Mathlib.Topology.Order.ScottTopology

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

Tactic:
by
  let := upper α
  ext U
  rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
    ({ topology_eq_upperTopology := rfl }) U]
  let := scott α univ
  rw [@isOpen_iff_Iic_compl_or_univ _ _ (scott α univ) ({ topology_eq_scott := rfl }) U]

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range ⇑c) x

Tactic:
by
  simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]

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

Goal state before:
pp: case right
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) := ⋯
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := ⋯
⊢ ∀ (x y : X ⊕ Y), dist (f x) (f y) ≤ ↑(GromovHausdorff.maxVar✝ X Y)

Tactic:
exact fun x y =>
          calc
            F (x, y) ≤ diam (range Φ ∪ range Ψ) := by
              have A : ∀ z : X ⊕ Y, f z ∈ range Φ ∪ range Ψ := by
                intro z
                cases z
                · apply mem_union_left; apply mem_range_self
                · apply mem_union_right; apply mem_range_self
              refine dist_le_diam_of_mem ?_ (A _) (A _)
              rw [Φrange, Ψrange]
              exact (p ⊔ q).isCompact.isBounded
            _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := I

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

Goal state before:
pp: case refine_2
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ghDist X Y ≤ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))

Tactic:
exact ghDist_le_hausdorffDist (isometry_optimalGHInjl X Y) (isometry_optimalGHInjr X Y)

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

Goal state before:
pp: x y : GHSpace
hxy : dist x y = 0
⊢ x = y

Tactic:
rcases ghDist_eq_hausdorffDist x.Rep y.Rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩

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ΦΨ : ghDist x.Rep y.Rep = hausdorffDist (range Φ) (range Ψ)
⊢ x = y
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ (range fun x ↦ U x ∩ d) ⊆ 𝒫 d

Tactic:
rw [range_subset_iff]

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
U V : ↑(𝒫 s) → Set X
hU : ∀ (t : ↑(𝒫 s)), IsOpen (U t)
hV : ∀ (t : ↑(𝒫 s)), IsOpen (V t)
hUs : ∀ (t : ↑(𝒫 s)), ↑t ⊆ U t
hVs : ∀ (t : ↑(𝒫 s)), s \ ↑t ⊆ V t
hUV : ∀ (t : ↑(𝒫 s)), Disjoint (U t) (V t)
hUd : ∀ {t₁ t₂ : ↑(𝒫 s)}, U t₁ ∩ d = U t₂ ∩ d → ↑t₁ ⊆ ↑t₂
h_inj : Injective fun x ↦ U x ∩ d
⊢ ∀ (y : ↑(𝒫 s)), U y ∩ d ∈ 𝒫 d
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
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝ : Nonempty ↑s := Nonempty.to_subtype sne
this✝ : 0 ≤ ε₂
this : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
let _ : MetricSpace (X ⊕ Y) :=
    glueMetricApprox (fun x : s => (x : X)) (fun x => Φ x) (ε₂ / 2 + δ) (by linarith) this

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
s : Set X
Φ : ↑s → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃
H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h✝ : xX ∈ univ
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
x✝¹ : Nonempty ↑s := Nonempty.to_subtype sne
this✝ : 0 ≤ ε₂
this : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x ↦ ↑x) (fun x ↦ Φ x) (ε₂ / 2 + δ) ⋯ this
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: 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
F : Sheaf C X
⊢ IsZero F ↔ ∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj F)

Tactic:
refine ⟨fun h _ => Functor.map_isZero _ h, ?_⟩

Goal state after:
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
F : Sheaf C X
⊢ (∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj F)) → IsZero F
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: case mpr
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 : ∀ (x : ↑X), IsZero (S.map (forget C X ⋙ stalkFunctor C x)).homology
⊢ IsZero S.homology

Tactic:
isZero_iff_stalkFunctor_obj_isZero S.homology

Goal state after:
case mpr
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 : ∀ (x : ↑X), IsZero (S.map (forget C X ⋙ stalkFunctor C x)).homology
⊢ ∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj S.homology)
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
𝓕 𝓖 : Presheaf C X
f : 𝓕 ⟶ 𝓖
U : Opens ↑X
h : p₀ ∉ U
⊢ f.app (op U) ≫ (⋯ ▸ terminalIsTerminal).from (𝓖.obj (op U)) =
    (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U)) ≫ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ U then 𝓕.stalk p₀ else ⊤_ C)

Tactic:
· apply ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext

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

Goal state before:
pp: X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ S.π.app (Opposite.op { obj := principalOpen x, property := ⋯ }) ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    S.π.app (Opposite.op { obj := V, property := ⋯ }) ≫
      limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
rw [← S.w ee.op, Category.assoc]

Goal state after:
X✝ : Type v
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : Preorder X✝
inst✝⁴ : Topology.IsUpperSet X✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
F✝ : X✝ ⥤ C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ S.π.app (Opposite.op VV) ≫
      ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F).map ee.op ≫
        limit.π (generator (principalOpen x) ⋙ F)
          { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    S.π.app (Opposite.op { obj := V, property := ⋯ }) ≫
      limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }
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]
⊢ x ∈ unop (StructuredArrow.right t).fst

Tactic:
let sf : (i : Fin 2) → S.X₂.obj.obj (op (f i))
    | 0 => t.right.2
    | 1 => t₁ + (S.f.hom.app (op W)) t₄

Goal state after:
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₄
⊢ x ∈ unop (StructuredArrow.right t).fst
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
⊢ ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ

Tactic:
have B : dist (inl x) (inr default) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
B : dist (inl x) (inr default) ≤ diam univ + 1 + diam univ
⊢ ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ diam univ + 1 + diam univ
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (F.stalkToFiber x))

Tactic:
apply TopCat.stalkToFiber_surjective
  intro t
  obtain ⟨U, m, s, rfl⟩ := F.exists_germ_eq t
  use ⟨U, m⟩
  fconstructor
  · exact fun y => F.germ _ _ y.2 s
  · exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩

Goal state after: