mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
⊢ IsGeneratedBy X ↑F

Tactic:
let W (a : Σ (i : ι), C(X i, Y)) : TopologicalSpace.Closeds (X a.1) :=
    ⟨a.2 ⁻¹' F, IsClosed.preimage a.2.continuous hF⟩
  let g (a) : W a → F := F.restrictPreimage a.2
  have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage
  suffices ∀ (V : Set F), (∀ a, IsClosed ((g a) ⁻¹' V)) → IsClosed V by
    constructor
    rw [continuous_iff_isClosed]
    exact fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)
  intro V hV
  obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ F ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩
  refine IsClosed.preimage continuous_subtype_val ?_
  rw [IsGeneratedBy.isClosed_iff X]
  intro i f
  convert! (W ⟨i, f⟩).isClosed.isClosedMap_subtype_val _ (hV ⟨i, f⟩)
  aesop

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
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∈ J

Tactic:
induction i with

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
i : ℕ
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - i

Tactic:
induction i with

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
i : ℕ
ha : 1 < a
⊢ ↑(#(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

Tactic:
induction i with

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✝
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 ≤
    a * ↑(#J)

Tactic:
Finset.sum_le_sum fun _ _ ↦ mul_le_mul_right (pow_le_pow_right₀ ha.le le_tsub_add) _

Goal state after:
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 - ?m.162 i + ?m.162 i) ≤
    a * ↑(#J)

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
⊢ ℕ → ℕ
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ x_1 ∈ s, S.domRestrict x_1 = x) →
    ∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x

Tactic:
· rintro ⟨z, hz_mem, hzx⟩
    exact ⟨Sᶜ.domRestrict z, mem_image_of_mem Sᶜ.domRestrict hz_mem, z, hz_mem,
      ⟨⟨⟨z, hz_mem, rfl⟩, rfl⟩, hzx⟩⟩

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : d x y < 0
this : d x x < 0
⊢ False

Tactic:
exact this.ne (d.refl x)

Goal state after:
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
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ pi1EquivFundamentalGroup.toFun (⟦p⟧ * ⟦q⟧) = pi1EquivFundamentalGroup.toFun ⟦p⟧ * pi1EquivFundamentalGroup.toFun ⟦q⟧

Tactic:
by
    simp only [HomotopyGroup.mul_spec (i := (0 : Fin 1))]
    apply Quotient.sound
    rw [Unique.eq_default 0, genLoopEquivOfUnique_transAt]

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 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)

Tactic:
by
        gcongr
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n

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
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ HolderWith (nnHolderNorm r f) r f

Tactic:
intro x₁

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ : X
⊢ ∀ (y : X), edist (f x₁) (f y) ≤ ↑(nnHolderNorm r f) * edist x₁ y ^ ↑r
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite
us : s ⊆ ⋃ i, ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with
    ⟨v, hsv, hvc, hcv⟩
  have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
  choose r' hlt hsub using this
  exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩

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

Goal state before:
pp: case h
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
x : X
hx : { val := x } ∈ s
y : X
hy : { val := y } ∈ s
⊢ dist x y ^ α ≤ C ^ α

Tactic:
hC hx hy

Goal state after:
case h
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
x : X
hx : { val := x } ∈ s
y : X
hy : { val := y } ∈ s
⊢ C ^ α ≤ C ^ α
Module: Mathlib.Topology.NatEmbedding

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

Tactic:
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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
K : Compacts α
inst✝ : T2Space α
⊢ ⋯.functor.Initial

Tactic:
by
  rw [Monotone.initial_functor_iff]
  intro L
  obtain ⟨U, h1, h2⟩ := exists_open_set_nhds_of_compactsNhds L
  have h3 : closure (U : Set α) ⊆ L := (IsClosed.closure_subset_iff
    (IsCompact.isClosed L.1.isCompact') ).2 h2
  exact ⟨⟨U, ⟨ IsCompact.of_isClosed_subset L.1.isCompact' isClosed_closure h3, h1⟩⟩, h3⟩

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

Goal state before:
pp: case e'_5.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) ⊤
hne : ⊤ ≠ ⊥
he : IsEmpty ↑X
⊢ s.arrows (𝟙 ⊤)

pp: case e'_5.inr
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) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)

Tactic:
· exact (hne <| SetLike.ext'_iff.2 <| Set.univ_eq_empty_iff.2 he).elim

Goal state after:
case e'_5.inr
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) ⊤
hne : ⊤ ≠ ⊥
x : ↑X
⊢ s.arrows (𝟙 ⊤)
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 : X
⊢ IsUpperSet {y | x ≤ y}

Tactic:
intro y z h1 h2

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 y z : X
h1 : y ≤ z
h2 : y ∈ {y | x ≤ y}
⊢ z ∈ {y | x ≤ y}
Module: Mathlib.Topology.Sheaves.LocallySurjective

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
ℱ 𝒢 : Presheaf C X
T : ℱ ⟶ 𝒢
h : IsLocallySurjective T
x✝ : Opens ↑X
t : ToType (𝒢.obj (op x✝))
x : ↑X
hx : x ∈ x✝
V : Opens ↑X
i : V ⟶ x✝
hi : (Presheaf.imageSieve T t).arrows i ∧ x ∈ V
⊢ ∃ V, ∃ (x_1 : V ≤ x✝), (∃ s, (ConcreteCategory.hom (T.app (op V))) s = (t |_ V) x_1) ∧ x ∈ V

Tactic:
exact ⟨V, leOfHom i, hi⟩

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

Goal state before:
pp: case neg
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scard : #↑s ≤ ↑(K n)
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)

Tactic:
rcases Cardinal.lt_aleph0.1 (scard.trans_lt Cardinal.natCast_lt_aleph0) with ⟨N, hN⟩

Goal state after:
case neg
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
p : GHSpace
hp : ¬p ∉ t
s : Set p.Rep
scard : #↑s ≤ ↑(K n)
scover : univ ⊆ ⋃ x ∈ s, ball x (u n)
N : ℕ
hN : #↑s = ↑N
⊢ ∃ s, ∃ N ≤ K n, ∃ x, p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε

Tactic:
have Aq : ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ :=
        calc
          ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ((F q).2 ((E q) (Ψ x)) ((E q) (Ψ y))).1 := by
            congr!
          _ = min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ := by simp only [F, (E q).symm_apply_apply]
          _ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ := by
            refine min_eq_right (Nat.floor_mono ?_)
            refine mul_le_mul_of_nonneg_left (le_trans ?_ (le_max_left _ _)) (inv_pos.2 εpos).le
            change dist (Ψ x : q.Rep) (Ψ y) ≤ C
            refine (dist_le_diam_of_mem isCompact_univ.isBounded (mem_univ _) (mem_univ _)).trans ?_
            exact hdiam q qt

Goal state after:
case refine_3
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
⊢ |dist x y - dist (Ψ x) (Ψ y)| ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
⊢ BddBelow (range fun x ↦ (candidatesBDist X Y) (inl x, inr y))

Tactic:
by simpa using HD_below_aux2 0

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

Goal state before:
pp: case h.refine_2
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ W ⊓ (U' ⊓ V') ⟶ ↑V

Tactic:
exact Opens.infLERight _ _ ≫ Opens.infLERight _ _ ≫ iV

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
hle : HasSmallInductiveDimensionLE X n
hlt : ¬HasSmallInductiveDimensionLT X n
⊢ smallInductiveDimension X = ↑n

Tactic:
apply (smallInductiveDimension_le_iff.2 hle).antisymm
  rwa [← not_lt, smallInductiveDimension_lt_iff]

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
⊢ False

Tactic:
let φ : segment ℝ (y1 : F) y2 ≃ₜ segment ℝ (y2 : F) y1 := .setCongr (segment_symm ℝ (y1 : F) y2)

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
⊢ False
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : UniformSpace X
inst✝ : IsUltraUniformity X
x : X
⊢ ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ i', (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)

Tactic:
intro V ⟨hV, h_symm, h_trans⟩
    exact ⟨ball x V, ⟨mem_ball_self _ hV,
      isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity _ hV⟩, le_rfl⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsSymm (⋂ i_1, id (i.snd i_1))

Tactic:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
    rintro _ _ _ _ _
    infer_instance

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
ι : Type u_3
U : ι → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ i, U i
⊢ ∀ (i : (I : Set ι) × (↑I → SetRel X X)),
    (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), i.snd i_1 ∈ uniformity X ∧ (i.snd i_1).IsSymm ∧ (i.snd i_1).IsTrans) →
      SetRel.IsTrans (⋂ i_1, id (i.snd i_1))

Tactic:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
    rintro _ _ _ _ _
    infer_instance

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case right
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
X : Set E
Y : Set F
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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
cX : Convex ℝ X
ne_Y : Y.Nonempty
η : E → F
η_mem : ∀ x ∈ X, η x ∈ Y
η_max : ∀ x ∈ X, IsMaxOn (f x) Y (η x)
hlsc : LowerSemicontinuousOn (fun x ↦ f x (η x)) X
a : E
ha : a ∈ X
ha' : IsMinOn (fun x ↦ f x (η x)) X a
ξ : F → E
ξ_mem : ∀ y ∈ Y, ξ y ∈ X
ξ_min : ∀ y ∈ Y, IsMinOn (fun x ↦ f x y) X (ξ y)
husc : UpperSemicontinuousOn (fun x ↦ f (ξ x) x) Y
b : F
hb : b ∈ Y
hb' : IsMaxOn (fun y ↦ f (ξ y) y) Y b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b

Tactic:
calc f a y ≤ f a (η a) := isMaxOn_iff.mp (η_max a ha) y hy
    _ = f (ξ b) b :=
      minimax ne_X kX hfy hfy' cY hfx hfx' cX
        _ (fun x hx ↦ (η_max x hx).isLUB (η_mem x hx))
        _ (ha'.isGLB ha)
        _ (fun y hy ↦ (ξ_min y hy).isGLB (ξ_mem y hy))
        _ (hb'.isLUB hb)
    _ ≤ f x b := isMinOn_iff.mp (ξ_min b hb) x hx

Goal state after: