mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : IsSquare n
hd : IsSquare d
ha : IsNNRat a n d
⊢ IsSquare a

Tactic:
rcases hn with ⟨n, rfl⟩
  rcases hd with ⟨d, rfl⟩
  use n / d
  simp [ha.to_eq, div_mul_div_comm]

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
⊢ Irrational (x ^ y)

Tactic:
rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x ^ y)
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
⊢ Irrational (x ^ y)

Tactic:
rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
⊢ Irrational (x ^ y)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val

Tactic:
← Set.image_eq_range

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
n : ℕ
x✝¹ : True
x : X
hx : x ∈ U n
x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}
f : X →* Y
hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}
⊢ (↑⟨f, hf⟩ 1, ↑⟨f, hf⟩ x) ∈ {x | x.2 / x.1 ∈ V n}

Tactic:
rw [Set.mem_ofPred_eq, map_one, div_one]

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
n : ℕ
x✝¹ : True
x : X
hx : x ∈ U n
x✝ : ↑{f | Set.MapsTo (⇑f) (U 0) (V 0)}
f : X →* Y
hf : f ∈ {f | Set.MapsTo (⇑f) (U 0) (V 0)}
⊢ (1, ↑⟨f, hf⟩ x).2 ∈ V n
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: case hab
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
⊢ ∀ b ∈ {I | I.IsMaximal}, ∏ p, p.asIdeal ≤ b

Tactic:
exact fun I hI ↦ Ideal.prod_le_inf.trans
      (Finset.inf_le (b := PrimeSpectrum.mk I hI.isPrime) (by simp))

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x ↦ x ∈ s)
a : I
hx : ↑x a = true
⊢ e (π C fun x ↦ x ∈ s) a ∈ factors C s x

Tactic:
by
  rcases x with ⟨_, z, hz, rfl⟩
  simp only [factors, List.mem_map, Finset.mem_sort]
  refine ⟨a, ?_, if_pos hx⟩
  aesop (add simp Proj)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
⊢ ∃ a, ↑y a ≠ ↑x a

Tactic:
contrapose! h; ext; apply h

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
⊢ cl A = closure A

Tactic:
by
  ext
  rw [mem_closure_iff_ultrafilter]
  constructor
  · rintro ⟨F, h1, h2⟩
    exact ⟨F, h1, le_nhds_of_str_eq _ _ h2⟩
  · rintro ⟨F, h1, h2⟩
    exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ (y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ), (Linear_CC' C hsC ho) ((πs C o) y) = 0

Tactic:
intro y
  ext x
  dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁, LocallyConstant.sub_apply]
  simp only [sub_eq_zero]
  congr 1
  ext i
  dsimp [CC'₀, CC'₁, ProjRestrict, Proj]
  apply if_ctx_congr Iff.rfl _ (fun _ ↦ rfl)
  simp only [SwapTrue, ite_eq_right_iff]
  intro h₁ h₂
  exact (h₁.ne h₂).elim

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

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

Tactic:
eval

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
x : ↑(π C fun x ↦ ord I x < o₂)
⊢ ((πs' C h) (Products.eval (π C fun x ↦ ord I x < o₁) l)) x =
    ((πs' C h) (Products.eval (π C fun x ↦ ord I x < o₁) ↑⟨l, gl⟩)) x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i ≠ false → ord I i < o) → (π C fun x ↦ ord I x < o) = C
⊢ C = π C fun x ↦ ord I x < o

Tactic:
simp only [ne_eq, Bool.not_eq_false, π] at this

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
h : contained C o
this : (∀ (i : I), ∀ x ∈ C, x i = true → ord I i < o) → (Proj fun x ↦ ord I x < o) '' C = C
⊢ C = π C fun x ↦ ord I x < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h
S : Profinite
⊢ Continuous (ι S)

Tactic:
dsimp +unfoldPartialApp [ι]
    refine continuous_pi ?_
    intro C
    rw [← IsLocallyConstant.iff_continuous]
    refine ((IsLocallyConstant.tfae _).out 0 3).mpr ?_
    rintro ⟨⟩
    · refine IsClopen.isOpen (isClopen_compl_iff.mp ?_)
      convert! C.2
      ext x
      simp
    · refine IsClopen.isOpen ?_
      convert! C.2
      ext x
      simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]

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

Goal state before:
pp: x✝ : UniformSpaceCat
⊢ ⇑(ConcreteCategory.hom (ConcreteCategory.ofHom ⟨Completion.map ⇑(𝟙 x✝).hom', ⋯⟩).hom) =
    ⇑(ConcreteCategory.hom (𝟙 (CpltSepUniformSpace.of (Completion x✝.carrier))).hom)

Tactic:
by apply Completion.map_id

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
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ Disjoint (interior D) (closedCell n j)

Tactic:
by
  rw [disjoint_iff_inter_eq_empty]
  by_contra! h
  rw [← closure_openCell_eq_closedCell, inter_comm,
    closure_inter_open_nonempty_iff isOpen_interior] at h
  rcases h with ⟨x, xmemcell, xmemD⟩
  suffices x ∈ (skeletonLT C 0 : Set X) ∩ openCell n j by
    rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this
  exact ⟨(skeletonLT C 0).base_subset (interior_subset xmemD), xmemcell⟩

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

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
· exact norm_lt_iff_of_compactlySupported h hM

Goal state after:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
x✝¹ : f.NeBot
x✝ : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
by
    obtain ⟨x, hx⟩ := f.exists_seq_tendsto
    obtain ⟨a, ha, hxa⟩ := hA x (by simpa using hx.mono_right hle)
    exact ⟨a, ha, hxa.clusterPt.mono hx⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ
      (⇑(ConcreteCategory.hom (ModuleCat.ofHom (Linear_CC' C hsC ho))) ∘ SumEval C ho ∘ Sum.inr)

Tactic:
by
  dsimp [SumEval, ModuleCat.ofHom]
  rw [max_eq_eval_unapply C hsC ho]
  intro h
  let f := MaxToGood C hC hsC ho h₁
  have hf : f.Injective := maxToGood_injective C hC hsC ho h₁
  have hh : (fun l ↦ Products.eval (C' C ho) l.val.Tail) = eval (C' C ho) ∘ f := rfl
  rw [hh]
  exact h.comp f hf

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
isOpen_iff_mem_nhds

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top.top
⊢ ¬edist ∞ ∞ = ∞

pp: case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞

pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞

Tactic:
· exact zero_ne_top

Goal state after:
case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞

case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ ¬edist ↑x✝¹ ↑x✝ = ∞
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ x - 3⁻¹ ^ n) Filter.atTop (nhds x)

Tactic:
rw [← tendsto_sub_nhds_zero_iff]
    simp only [sub_sub_cancel_left]
    rw [show 0 = -(0 : ℝ) by simp]
    exact (tendsto_pow_atTop_nhds_zero_of_abs_lt_one (by norm_num)).neg

Goal state after:
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
x y : X
⊢ d x y ⊔ d' x y = d y x ⊔ d' y x

Tactic:
simp [d.symm, d'.symm]

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

Goal state before:
pp: case inl.inl
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : IsEmpty ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

pp: case inl.inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
· simp only [Finset.isEmpty_coe_sort] at hJ
      simp [hJ]

Goal state after:
case inl.inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : Nonempty ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
⊢ auxGroup i = auxGroup j

Tactic:
by
  by_cases h : i = j; · rw [h]
  refine Group.ext (EckmannHilton.mul (isUnital_auxGroup i) (isUnital_auxGroup j) ?_)
  rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩
  change Quotient.mk' _ = _
  apply congr_arg Quotient.mk'
  simp only [fromLoop_trans_toLoop, transAt_distrib h, coe_toEquiv, loopHomeo_apply,
    coe_symm_toEquiv, loopHomeo_symm_apply]

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)|

Tactic:
by grw [← le_abs_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Tactic:
← _root_.bot_eq_zero,

Goal state after:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ ⨅ x ∈ s, ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y = ⊥ ↔ ∀ C > ⊥, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : s.Nontrivial
⊢ 0 < s.einfsep

pp: case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep

Tactic:
· rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
    exact hxy'.symm ▸ edist_pos.2 hxy

Goal state after:
case neg
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ 0 < s.einfsep
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
γ : 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 Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
⊢ hausdorffDist (F '' range Φ') (F '' range Ψ') ∈
    (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y}

Tactic:
apply (mem_image _ _ _).2

Goal state after:
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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := ⋯
Φ' : X → ↑s := ⋯
Ψ' : Y → ↑s := ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := ⋯
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := ⋯
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := ⋯
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
⊢ ∃ x ∈ {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y},
    hausdorffDist ↑x.1 ↑x.2 = hausdorffDist (F '' range Φ') (F '' range Ψ')
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 Ψ
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

Tactic:
rcases exists_mem_of_nonempty X with ⟨xX, _⟩
  let s : Set γ := range Φ ∪ range Ψ
  let Φ' : X → s := fun y => ⟨Φ y, mem_union_left _ (mem_range_self _)⟩
  let Ψ' : Y → s := fun y => ⟨Ψ y, mem_union_right _ (mem_range_self _)⟩
  have IΦ' : Isometry Φ' := fun x y => ha x y
  have IΨ' : Isometry Ψ' := fun x y => hb x y
  have : IsCompact s := (isCompact_range ha.continuous).union (isCompact_range hb.continuous)
  have : CompactSpace s := ⟨isCompact_iff_isCompact_univ.1 ‹IsCompact s›⟩
  have ΦΦ' : Φ = Subtype.val ∘ Φ' := rfl
  have ΨΨ' : Ψ = Subtype.val ∘ Ψ' := rfl
  have : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ') := by
    rw [ΦΦ', ΨΨ', range_comp, range_comp]
    exact hausdorffDist_image isometry_subtype_coe
  rw [this]
  -- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
  let F := kuratowskiEmbedding s
  have : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ') :=
    hausdorffDist_image (kuratowskiEmbedding.isometry _)
  rw [← this]
  -- Let `A` and `B` be the images of `X` and `Y` under this embedding. They are in `ℓ^∞(ℝ)`, and
  -- their Hausdorff distance is the same as in the original space.
  let A : NonemptyCompacts ℓ_infty_ℝ :=
    ⟨⟨F '' range Φ',
        (isCompact_range IΦ'.continuous).image (kuratowskiEmbedding.isometry _).continuous⟩,
      (range_nonempty _).image _⟩
  let B : NonemptyCompacts ℓ_infty_ℝ :=
    ⟨⟨F '' range Ψ',
        (isCompact_range IΨ'.continuous).image (kuratowskiEmbedding.isometry _).continuous⟩,
      (range_nonempty _).image _⟩
  have AX : ⟦A⟧ = toGHSpace X := by
    rw [eq_toGHSpace_iff]
    exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩
  have BY : ⟦B⟧ = toGHSpace Y := by
    rw [eq_toGHSpace_iff]
    exact ⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩
  refine csInf_le ⟨0, ?_⟩ ?_
  · simp only [lowerBounds, mem_image, mem_prod, mem_ofPred_eq, Prod.exists, and_imp,
      forall_exists_index]
    intro t _ _ _ _ ht
    rw [← ht]
    exact hausdorffDist_nonneg
  apply (mem_image _ _ _).2
  exists (⟨A, B⟩ : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ)

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ ∃ a, (Ici a)ᶜ = U

Tactic:
have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)

Goal state after:
case mpr
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
⊢ ∃ a, (Ici a)ᶜ = U
Module: Mathlib.Topology.Order.HullKernel

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

Tactic:
obtain ⟨a, ha'⟩ := ha

Goal state after:
case mp
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
a : α
ha' : (hull T a)ᶜ = R
⊢ ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R
Module: Mathlib.Topology.Sets.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LE α
s t : ClopenUpperSet α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
by
    obtain ⟨⟨_, _⟩, _⟩ := s
    obtain ⟨⟨_, _⟩, _⟩ := t
    congr

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

Goal state before:
pp: 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
⊢ ∃! s_1, IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1

Tactic:
refine Sheaf.existsUnique_gluing F _ _ (fun i j ↦ ?_)
    obtain (rfl | h₁ | h₁) : i = j ∨ Nonempty (i.val ⟶ j.val) ∨ Nonempty (j.val ⟶ i.val) := by
      grind [Subtype.ext_iff, h i.property j.property]
    · rfl
    all_goals
      rw [← CategoryOfElements.map_snd h₁.some.2]
      dsimp
      rw [← Functor.map_comp_apply]
      rfl

Goal state after: