mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
inst✝ : CWComplex E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
inst✝ : CWComplex E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ⋃ n, ⋃ j, openCell n ↑j = E
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ∅ ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
empty_union

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
⊢ IsCompactSystem {s | IsCompact s}

Tactic:
convert! isCompactSystem_isCompact_isClosed α with s
  simpa using IsCompact.isClosed

Goal state after:
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
suffices f = 0 by simp [this]
    rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs

Goal state after:
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y : X
ι : Type u_3
inst✝ : StronglyLocallyContractibleSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
by
    refine contractible_basis x |>.to_hasBasis'
      (fun s ⟨hs, hs'⟩ ↦ ⟨s, ⟨hs, ?_⟩, le_rfl⟩) (fun s hs ↦ hs.1)
    rw [isPathConnected_iff_pathConnectedSpace]
    infer_instance

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ ↑(#({x ∈ V | edist t x ≤ ↑(Nat.find ⋯) * c})) ≤ a ^ Nat.find ⋯

Tactic:
exact (Nat.find_spec (exists_radius_le t V ha c)).2

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case h₂
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    ↑(#J)

Tactic:
grw [Finset.sum_le_sum fun i _ ↦ logSizeRadius_le_card_smallBall hJ i ha, ← Nat.cast_sum,
    ← Finset.card_biUnion fun _ _ _ _ ↦ disjoint_smallBall_logSizeBallSeq hJ]

Goal state after:
case h₂
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#((Finset.range #J).biUnion fun x ↦ (logSizeBallSeq J hJ a c x).smallBall c)) ≤ ↑(#J)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun x ↦ x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))

Tactic:
by
    rw [tendsto_cons_iff]
    dsimp [eraseIdx]
    exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

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

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + edist x y + hausdorffEDist ↑t ↑s = infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t)

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist x y + hausdorffEDist ↑t ↑s) = infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t)
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε (f '' A) ≤ coveringNumber ε A

Tactic:
simp only [coveringNumber, le_iInf_iff]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ ∀ i ⊆ A, IsCover ε A i → ⨅ C, ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ i.encard
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε A ≤ coveringNumber ε (f '' A)

Tactic:
simp only [coveringNumber, le_iInf_iff]

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ ∀ i ⊆ f '' A, IsCover ε (f '' A) i → ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
by_cases hf : MemHolder r f

Goal state after:
case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ {x, y}.infsep = dist x y

Tactic:
rw [infsep_pair_eq_toReal, edist_dist]
  exact ENNReal.toReal_ofReal dist_nonneg

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

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

Tactic:
rintro ⟨C, hC⟩

Goal state after:
case mp
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 : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
⊢ ∃ C, ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
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α₁) := ⋯
s : Set (Snowflaking X α hα₀ hα₁)
⊢ (∃ C, ∀ ⦃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:
rintro ⟨C, hC⟩

Goal state after:
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
Module: Mathlib.Topology.NatEmbedding

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

Tactic:
refine ⟨fun n ↦ ⋃ m, U (.pair n m), ?_, fun _ ↦ isOpen_iUnion fun _ ↦ ho _, ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∀ (n : ℕ), ((fun n ↦ ⋃ m, U (Nat.pair n m)) n).Infinite

case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ Pairwise (Disjoint on fun n ↦ ⋃ m, U (Nat.pair n m))
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a b : α
h₂ : a ≤ b
h₁ : f.toOrderHom a ≤ f.toFun b
h₀ : (g.comp f.toOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ c, a ≤ c ∧ (g.comp f.toOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
exact ⟨b, h₂, rfl⟩

Goal state after:
Module: Mathlib.Topology.Order.Hom.Esakia

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a b : α
h₂ : a ≤ b
h₁ : f.toOrderHom a ≤ f.toFun b
h₀ : (g.comp f.toContinuousOrderHom).toFun a ≤ g.toFun (f.toFun b)
⊢ ∃ c, a ≤ c ∧ (g.comp f.toContinuousOrderHom).toFun c = g.toFun (f.toFun b)

Tactic:
exact ⟨b, h₂, rfl⟩

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

Goal state before:
pp: case pos
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
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
h : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
exact A p q hp hq h

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

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ IsGδ s

Tactic:
refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩

Goal state after:
case neg.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
n : ℕ
⊢ IsOpen[inst✝] ((fun n ↦ ⇑f ⁻¹' Iio (1 / (↑n + 1))) n)

case neg.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
hse : s.Nonempty
f : C(X, ℝ)
hf : s = ⇑f ⁻¹' {0}
hfr : ∀ (x : X), f x ∈ Icc 0 1
⊢ s = ⋂ n, (fun n ↦ ⇑f ⁻¹' Iio (1 / (↑n + 1))) n
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)
h : S.Exact
x : ↑X
this :
  (forget C X ⋙ stalkFunctor C x).PreservesHomology ↔
    ∀ (S : ShortComplex (Sheaf C X)), S.Exact → (S.map (forget C X ⋙ stalkFunctor C x)).Exact
⊢ (S.map (forget C X ⋙ stalkFunctor C x)).Exact

Tactic:
exact this.mp inferInstance S h

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₂
⊢ x ∈ unop (StructuredArrow.right t).fst

Tactic:
obtain ⟨t₄, (ht₄ : t₄ |_ (t.right.1.unop ⊓ W) = t₃)⟩ := (AddCommGrpCat.epi_iff_surjective
      (S.X₁.obj.map (homOfLE inf_le_right).op)).mp inferInstance 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₃
⊢ x ∈ unop (StructuredArrow.right t).fst
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: case op.op
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)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f

Tactic:
| op y =>

Goal state after:
case op.op
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)
x y : CategoryTheory.Pairwise ι
f : op x ⟶ op y
⊢ ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj c.pt).map f ≫
      Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op y) =
    Opposite.rec
        (fun x ↦
          Pairwise.casesOn x (fun i ↦ c.π.app WalkingParallelPair.zero ≫ Pi.π (fun i ↦ F.obj (op (U i))) i) fun i j ↦
            c.π.app WalkingParallelPair.one ≫ Pi.π (fun p ↦ F.obj (op (U p.1 ⊓ U p.2))) (i, j))
        (op x) ≫
      ((diagram U).op ⋙ F).map f
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: case pos
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'
⊢ hZ_irred.genericPoint ∈ i

Tactic:
exact Set.sInter_subset_of_mem hiB' hη.mem

Goal state after:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
⊢ ds ○ (ds ○ uc ○ ds) ○ ds = ds ○ ds ○ uc ○ (ds ○ ds)

Tactic:
by simp [comp_assoc]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ds ○ (uc ○ ds) ⊆ ds ○ uc ○ ds

Tactic:
by simp [comp_assoc]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
u : Set X
x : X
uc s : SetRel X X
huc : IsOpen uc
ucu : uc ∈ 𝓤 X
hn : ball x (s ○ uc ○ s) ⊆ u
hs : s ∈ 𝓤 X
ds : SetRel X X
hdsu : ds ∈ 𝓤 X
hdso : IsOpen ds
hdsd : ds ○ ds ⊆ s
ho : IsOpen (ds ○ uc ○ ds)
hsub : ball x (ds ○ (ds ○ uc ○ ds) ○ ds) ⊆ u
this : ds.IsRefl
⊢ ds ○ (ds ○ uc ○ ds ○ ds) ⊆ ds ○ (ds ○ uc ○ ds) ○ ds

Tactic:
by simp [comp_assoc]

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: 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

Tactic:
rintro ⟨x, hx, rfl⟩

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
x : E
hx : x ∈ X
⊢ sup_y x = 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
⊢ IsInducing (↑(continuousAlternatingMap 𝕜 ι (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)

Tactic:
simp only [Function.comp_def, continuousAlternatingMap_apply, isInducing_const_prod]

Goal state after:
𝕜 : 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
⊢ IsInducing fun x' ↦
    (Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F₂ E₂ b) b).compContinuousAlternatingMap
      (x'.compContinuousLinearMap (Trivialization.symmL 𝕜 (trivializationAt F₁ E₁ b) b))