mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
⊢ False

Tactic:
have hle : (⨅ i, 𝓟 (A \ U i)) ≤ 𝓟 A :=
    iInf_le_of_le ‹Nonempty ι›.some <| principal_mono.mpr sdiff_subset

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
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
hle : ⨅ i, 𝓟 (A \ U i) ≤ 𝓟 A
⊢ False
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A✝ B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
⊢ ∃ k, ∀ n > k, a ∉ closure[inst✝³] {x n}

Tactic:
by_contra!
    obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this
    refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)
    simpa using mem_closure_iff.1 (hφ2 n) U hUo ha

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ MapsTo (⇑f) (⋃₀ (L '' ↑s)) (⋃₀ t)

Tactic:
mapsTo_sUnion,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ s_1 ∈ L '' ↑s, MapsTo (⇑f) s_1 (⋃₀ t)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x ↦ x ∈ i) ⁻¹' t_1 = u

Tactic:
exact ⟨⟨u, h⟩, {True}, isOpen_singleton_true, by simp [Set.preimage]⟩

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set α
⊢ IsOpen {l | s ∈ l}

Tactic:
by
  simpa only [Iic_principal] using isOpen_Iic_principal

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

Goal state before:
pp: case pos
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
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

pp: case neg
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
h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
· refine Finset.mem_of_subset ?_ (point_mem_finset_logSizeBallSeq hJ (i + 1) h)
      apply finset_logSizeBallSeq_subset_logSizeBallSeq_init

Goal state after:
case neg
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
h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

Tactic:
simp only [Hj, p.coe_toContinuousMap, p.source, p.target]

Goal state after:
case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑const fun j_1 ↦ y ↑j_1) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

Tactic:
simp only [Hj, p.coe_toContinuousMap, p.source, p.target]

Goal state after:
case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑const fun j_1 ↦ y ↑j_1) = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
⊢ 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n

Tactic:
induction n with
  | zero =>
    simp only [preCantorSet_zero]
    refine ⟨⟨ ?_, ?_⟩, ?_, ?_⟩ <;> norm_num
  | succ n ih =>
    apply And.intro
    · -- goal: 1 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 3 / 4 ∈ preCantorSet n
      exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩
    · -- goal: 3 / 4 ∈ preCantorSet (n + 1)
      -- follows by the inductive hypothesis, since 1 / 4 ∈ preCantorSet n
      exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

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

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
⊢ (homotopyTo i H) t ∈ Ω^ { j // j ≠ i } X x

Tactic:
rintro y ⟨i, iH⟩

Goal state after:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ ((homotopyTo i✝ H) t) y = x
Module: Mathlib.Topology.EMetricSpace.PairReduction

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

Tactic:
have hl : l < #J - 1 := by
        by_contra hl
        simp only [not_lt, tsub_le_iff_right] at hl
        have hlJ : l + 1 = #J := by
          refine Nat.le_antisymm_iff.mpr ⟨?_, hl⟩
          dsimp [l]
          grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ),
            Nat.findGreatest_le]
          rfl
        apply h
        suffices h_emp : (logSizeBallSeq J hJ a c (l + 1)).finset = ∅ from by simp [h_emp]
        rw [← Finset.card_eq_zero, ← Nat.le_zero, ← Nat.sub_self #J, hlJ]
        apply card_finset_logSizeBallSeq_le

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

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b

Tactic:
rw [dist_eq_norm]

Goal state after:
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ ‖embeddingOfSubset x a - embeddingOfSubset x b‖ ≤ dist a b
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x ↦ ↑(f x) i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s

Tactic:
choose g hgl hgeq using this

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:

Tactic:
edist (x : X) y ≤ edist (x : X) (f x) + edist (f x : X) y := edist_triangle ..
    _ ≤ 2 * ε := by
      rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
⊢ s.einfsep = ⋯.toFinset.inf (uncurry edist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_
  simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag,
    Prod.forall, uncurry_apply_pair, and_imp]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

pp: case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
· have hb : BddBelow (uncurry dist '' s.offDiag) := by
      refine ⟨0, fun d h => ?_⟩
      simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
      rcases h with ⟨_, _, _, rfl⟩
      exact dist_nonneg
    refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]

Goal state after:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : ¬s.Nontrivial
⊢ s.infsep = 0
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α₁) := ⋯
s : Set (Snowflaking X α hα₀ hα₁)
C : ℝ
hC : ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C
⊢ ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C ^ α

Tactic:
rintro ⟨x⟩ hx ⟨y⟩ 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
⊢ dist { val := x } { val := y } ≤ C ^ α
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
← mem_Iic,

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ∈ Iic b
⊢ f a ∈ Iic (f b)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ lower (α × β) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) (IsLower.lowerBasis α) (IsLower.lowerBasis β))

Tactic:
le_generateFrom_iff_subset_isOpen,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ image2 (fun x1 x2 ↦ x1 ×ˢ x2) (IsLower.lowerBasis α) (IsLower.lowerBasis β) ⊆ {s | IsOpen[lower (α × β)] s}
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Ioi c)

Tactic:
have : IsOpen (⋃ a ∈ c.right, Ioi a) := isOpen_biUnion fun _ _ ↦ isOpen_Ioi

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
this : IsOpen (⋃ a ∈ c.right, Ioi a)
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Ioi c)
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.{w, v} C
inst✝ : HasTerminal C
A : C
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
h : p₀ ∈ unop V
⊢ (if p₀ ∈ unop U then A else ⊤_ C) = if p₀ ∈ unop V then A else ⊤_ C

Tactic:
by rw [if_pos h, if_pos (by simpa using i.unop.le h)]

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

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

Tactic:
simp only [hf, ← preimage_iInter,
            ← preimage_range_inter (s := ⋂ (n : ℕ), Iio (1 / (n + 1) : ℝ)), inter_iInter]

Goal state after:
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
⊢ ⇑f ⁻¹' {0} = ⇑f ⁻¹' ⋂ i, range ⇑f ∩ Iio (1 / (↑i + 1))
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}
I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}
I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}
I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}
I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(maxVar X Y)}
this :
  candidatesB X Y =
    (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)}
⊢ IsClosed
    ((((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩
            ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩
          ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩
        ⋂ x, {f | f (x, x) = 0}) ∩
      ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(maxVar X Y)})

Tactic:
repeat'
    first
      | apply IsClosed.inter _ _
      | apply isClosed_iInter _
      | apply I1 _ _ | apply I2 _ _ | apply I3 _ _ | apply I4 _ _ _ | apply I5 _ | apply I6 _ _
      | intro x

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ U_1 f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Tactic:
use ⟨U, m⟩

Goal state after:
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis {s | IsClopen s}

Tactic:
intro (.succ _ s hs h)

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) 0
⊢ IsTopologicalBasis {s | IsClopen s}
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
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
⊢ sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y

Tactic:
apply (sublevelLeft_subset_or hfx' hfy hfy' cY a b' y y' ha hb' z').resolve_right

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
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := ⋯
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
z' : ↑(segment ℝ ↑y ↑y')
hz' : z' ∈ setOfPred_sublevelLeft_subset X Y f b b' y y'
hxz' : x ∈ sublevelLeft X f b' ↑z'
⊢ ¬sublevelLeft X f b' ↑z' ⊆ sublevelLeft X f b' ↑y'
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity (SeparationQuotient X)

Tactic:
apply mk_of_hasBasis this

Goal state after:
case h_symm
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)

case h_trans
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
⊢ IsUltraUniformity (UniformSpace.Completion X) ↔ IsUltraUniformity X

Tactic:
by
  rw [iff_comm, ← cauchyFilter_iff, ← separationQuotient_iff]
  exact Iff.rfl

Goal state after: