mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y)) (x (preimage f Y)) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) (x (preimage f X)))

Tactic:
rw [← this, ← ht]

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace] fun p ↦
    p.1 + p.2

Tactic:
continuous_induced_rng

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 + p.2)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace] fun p ↦
    p.1 • p.2

Tactic:
continuous_induced_rng

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 • p.2)
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ n, v x ^ n < ↑γ

Tactic:
refine exists_pow_lt₀ (hx.trans_lt ?_) _

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ exp (-1) < 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : cell C m
hj : j ∈ J m
hxj : x ∈ openCell m j
⊢ j ∈ E.I m

Tactic:
have : x ∈ (E : Set X) := E.cellFrontier_subset_of_mem i.2 hx

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
h : x ∉ D
m : ℕ
hmn : m < n
j : cell C m
hj : j ∈ J m
hxj : x ∈ openCell m j
this : x ∈ ↑E
⊢ j ∈ E.I m
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
⊢ ContinuousGeneratedBy X g

Tactic:
rw [continuousGeneratedBy_def]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝] (g ∘ ⇑f)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ContinuousGeneratedBy X ⇑equiv.symm

Tactic:
rw [continuousGeneratedBy_def]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ (1 - if ↑y a = true then 1 else 0) = 0

Tactic:
if_pos ha,

Goal state after:
case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 - 1 = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) l) = eval (π C fun x ↦ ord I x < o₂) l

Tactic:
by
  rw [← LocallyConstant.coe_inj, ← LocallyConstant.toFun_eq_coe]
  exact evalFacProps C (fun (i : I) ↦ ord I i < o₁) (fun (i : I) ↦ ord I i < o₂) hlt
    (fun _ hh ↦ lt_of_lt_of_le hh h)

Goal state after:
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 D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ ⋃ n_1, ⋃ j, openCell n_1 ↑j = ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
apply iUnion_congr fun m ↦ ?_

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

Goal state before:
pp: case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ ↑m < ↑(a✝ + 1) ↔ ↑m ≤ ↑a✝

Tactic:
Nat.cast_lt,

Goal state after:
case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ m < a✝ + 1 ↔ ↑m ≤ ↑a✝
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ interior D ∩ closedCell n j = ∅

Tactic:
by_contra! h

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
h : (interior D ∩ closedCell n j).Nonempty
⊢ False
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ D ⊆
    ⋃ i,
      ⋃ j,
        ↑(match i, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1

Tactic:
intro x xD

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
x : X
xD : x ∈ D
⊢ x ∈
    ⋃ i,
      ⋃ j,
        ↑(match i, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {mk y}))

Tactic:
connectedComponents_preimage_singleton

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ Finite (ConnectedComponents ↑(f ⁻¹' connectedComponent y))
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
⊢ ∃ i, A ⊆ U i

Tactic:
by_contra! h

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
⊢ False
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ContinuousGeneratedBy X g

Tactic:
rw [continuousGeneratedBy_def]

Goal state after:
case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y × Z)), Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
h : x ∈ some '' Metric.eball a r
⊢ x ∈ Metric.eball (some a) r

Tactic:
obtain ⟨y, yh, yx⟩ := h

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
yh : y ∈ Metric.eball a r
yx : some y = x
⊢ x ∈ Metric.eball (some a) r
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case succ
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
| succ i ih =>

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

Goal state before:
pp: case succ
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

Tactic:
| succ i ih =>

Goal state after:
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
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset = 0

Tactic:
rw [← Nat.le_zero, ← tsub_self #J]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (if h : ↑j = i then (t₀, t).1 else (t₀, t).2 ⟨↑j, ⋯⟩) = 0 ∨ (if h : ↑j = i then (t₀, t).1 else (t₀, t).2 ⟨↑j, ⋯⟩) = 1

Tactic:
dif_neg j.prop,

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (t₀, t).2 ⟨↑j, ⋯⟩ = 0 ∨ (t₀, t).2 ⟨↑j, ⋯⟩ = 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case succ
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ preCantorSet (i + 1)

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
⊢ a = b

Tactic:
by_contra! h

Goal state after:
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : a ≠ b
⊢ False
Module: Mathlib.Topology.MetricSpace.Infsep

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

Tactic:
· rw [infsep, einfsep_pair hxy]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs
  · refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
  · rw [not_nontrivial_iff] at hs
    exact hs.infsep_zero

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s).Nontrivial ↔ s.offDiag.Nonempty

Tactic:
← Set.offDiag_nonempty,

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s).offDiag.Nonempty ↔ s.offDiag.Nonempty
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ s ∈ S✝, IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)

Tactic:
exact isLowerSet_sUnion ih

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : IsOpen[inst✝¹] s
⊢ IsLowerSet s

Tactic:
by
  replace h := isOpen_iff_generate_Ici_compl.1 h
  induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih

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

Goal state before:
pp: case inr
⊢ ∃ a, Ioi a = Ioi False

Tactic:
· use False

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : SemilatticeInf α
T : Set α
inst✝ : OrderTop α
hT : ∀ p ∈ T, InfPrime p
⊢ hull T (∅.inf id) = T ↓∩ ⋃ a ∈ ↑∅, Set.Ici a

Tactic:
simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty,
      inf_empty]
    by_contra hf
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf
    obtain ⟨x, hx⟩ := hf
    exact (hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
F : Finset α
hF : (↑F).Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure ↑F))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R

Tactic:
use Finset.inf F id

Goal state after:
case h
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
F : Finset α
hF : (↑F).Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure ↑F))ᶜ = R
⊢ (hull T (F.inf id))ᶜ = R
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set ↑T
h : IsClosed[instTopologicalSpaceSubtype] C
⊢ hull T (kernel C) = C

Tactic:
obtain ⟨a, ha⟩ := (isClosed_iff hT).mp h
  rw [ha, kernel_hull hG]

Goal state after:
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
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed t

Tactic:
rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]

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
t : Set X
ht : t ∈ 𝒫 s
⊢ IsClosed (Subtype.val '' Subtype.val ⁻¹' t)
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∃! t, x✝.IsAmalgamation t

Tactic:
rw [@existsUnique_iff_exists _ ⟨fun _ _ => _⟩]

Goal state after:
case inl
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∃ x, x✝.IsAmalgamation x

C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
this : IndiscreteTopology ↑X
s : Sieve ⊥
hs : s ∈ (Opens.grothendieckTopology ↑X) ⊥
x✝ : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op c)) s.arrows
a✝ : x✝.Compatible
⊢ ∀ (x x_1 : (F ⋙ coyoneda.obj (op c)).obj (op ⊥)), x = x_1
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ f = eqToHom ⋯ ≫ c.ι.app (op h1.choose)

Tactic:
rw [← Category.id_comp f, ← H, ← Category.assoc]

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f = (eqToHom ⋯ ≫ (skyscraperPresheafCocone p₀ A y).ι.app (op h1.choose)) ≫ f
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case hnc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
⊢ PUnit.unit ∉ ⊥

Tactic:
· #adaptation_note /-- 2024-03-24
            Previously the universe annotation was not needed here. -/
            exact Set.notMem_empty PUnit.unit.{u + 1}

Goal state after:
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 c' : Cone (SheafConditionEqualizerProducts.diagram F U)
f : c ⟶ c'
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    f.hom ≫ (coneEquivInverseObj F U c').π.app j = (coneEquivInverseObj F U c).π.app j

Tactic:
by
        intro x
        induction x with | op x => ?_
        rcases x with (⟨i⟩ | ⟨i, j⟩)
        · dsimp
          dsimp only [Fork.ι]
          rw [← f.w WalkingParallelPair.zero, Category.assoc]
        · dsimp
          rw [← f.w WalkingParallelPair.one, Category.assoc]

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

Goal state before:
pp: X : TopCat
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝¹ : S.X₁.IsFlasque
inst✝ : S.X₂.IsFlasque
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
this : Epi (S.g.hom.app U ≫ S.X₃.obj.map i)
⊢ Epi (S.X₃.obj.map i)

Tactic:
exact CategoryTheory.epi_of_epi (S.g.1.app U) (S.X₃.obj.map i)

Goal state after: