mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ (image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ countableBasis Y}).Countable

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∀ (f : C(X, Y)) (x : X), ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V

Tactic:
· exact .image2 hScount (countable_ofPred_finite_subset (countable_countableBasis Y)) _

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS : ∀ (f : C(X, Y)) (V : Set Y), IsOpen[inst✝¹] V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
⊢ ∀ (f : C(X, Y)) (x : X), ∀ V ∈ countableBasis Y, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
Module: Mathlib.Topology.Convenient.HomSpace

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
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun x ↦
    match x with
    | (x₁, x₂) => (f₂ x₂, f₁ x₁)
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] φ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ Continuous fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2))

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
⊢ Continuous G

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
⊢ Continuous G

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 2 * ↑p.1

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 1 + ↑p.2

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ Continuous fun t ↦ γ (qRight (t, θ))

Tactic:
fun_prop

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

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (closedBall n r)

Tactic:
change IsCompact (((↑) : ℕ+ → ℕ) ⁻¹' closedBall (↑n : ℕ) r)
    rw [Nat.closedBall_eq_Icc]
    exact ((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

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
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
⊢ Continuous fun t m ↦ t (e m)

Tactic:
fun_prop

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
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
⊢ Continuous fun t n ↦ t (e.symm n)

Tactic:
fun_prop

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
⊢ Continuous[_, inst✝] (Function.uncurry fun x_1 y ↦ x_1.1 (sumArrowHomeomorphProdArrow.symm (x_1.2, y)))

Tactic:
fun_prop

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
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ Continuous Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∈ S
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ a.2 ⟨j, h⟩

Tactic:
fun_prop

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

Goal state before:
pp: case zero
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
⊢ IsClosed (preCantorSet 0)

Tactic:
exact isClosed_Icc

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace] fun x ↦ Sᶜ.domRestrict ↑x

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
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)
⊢ Continuous fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
S : Set ι
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), CompactSpace (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
⊢ IsClosed (S.domRestrict '' s)

Tactic:
have : S.domRestrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd (· ∈ S) α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

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
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 : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c (l + 1)).finset ≤ #J - #J

Tactic:
hlJ

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 : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
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
hl : l < #J - 1
⊢ t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset

Tactic:
simp only [Decidable.not_not] at h

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)
hl : l < #J - 1
h : s ∈ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ Continuous fun x i ↦ bif x i then 2 else 0

Tactic:
fun_prop

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
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ Continuous Subtype.val

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), ContinuousAt length l

Tactic:
simp only [ContinuousAt, nhds_discrete]
  refine tendsto_nhds ?_ ?_
  · exact tendsto_pure_pure _ _
  · intro l a ih
    dsimp only [List.length]
    refine Tendsto.comp (tendsto_pure_pure (fun x => x + 1) _) ?_
    exact Tendsto.comp ih tendsto_snd

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✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
⊢ Continuous[_, inst✝²] fun t ↦ p fun x ↦ t

Tactic:
fun_prop

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✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ Continuous[_, inst✝²] fun c ↦ p (c default)

Tactic:
fun_prop

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

Goal state before:
pp: case mpr.refine_1
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
⊢ Continuous fun tx ↦ (tx.1, tx.2 default)

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := fun x ↦ ⟨⋯.choose, ⋯⟩
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
⊢ D.encard ≤ C.encard

Tactic:
simp only [← Set.toENat_cardinalMk]

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
f : ↑D → ↑C := fun x ↦ ⟨⋯.choose, ⋯⟩
hf' : ∀ (x : ↑D), edist ↑x ↑(f x) ≤ ↑ε
⊢ Cardinal.toENat (Cardinal.mk ↑D) ≤ Cardinal.toENat (Cardinal.mk ↑C)
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: x✝ : ℕ
⊢ Continuous fun a ↦ cantorSpaceHomeomorphNatToCantorSpace a x✝

Tactic:
fun_prop

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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
⊢ ⨅ (_ : C ⊆ f ⁻¹' f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
have : ↑C ⊆ f ⁻¹' f '' A := hC_subset.trans (Set.subset_preimage_image f A)

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → ↑KC := Subtype.coind f ⋯
hf'_surjective : Function.Surjective f'
h : ↑KC → ↑KH := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ Continuous (⇑g.symm ∘ h ∘ f')

Tactic:
fun_prop

Goal state after:
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)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Pi

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
f g h : (i : ι) → X i
⊢ dist f h ≤ max (dist f g) (dist g h)

Tactic:
simp only [dist_pi_def, ← NNReal.coe_max, NNReal.coe_le_coe, ← Finset.sup_sup]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
f g h : (i : ι) → X i
⊢ (Finset.univ.sup fun b ↦ nndist (f b) (h b)) ≤
    Finset.univ.sup ((fun b ↦ nndist (f b) (g b)) ⊔ fun b ↦ nndist (g b) (h b))
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
simp_rw [subset_sInter_iff]

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ∀ t' ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}, hull T (kernel S) ⊆ t'
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
this : ∀ (n : ℕ), Disjoint s (U n)ᶜ
f : ℕ → C(X, ℝ)
hfs : ∀ (n : ℕ), EqOn (⇑(f n)) 0 s
hfu : ∀ (n : ℕ), EqOn (⇑(f n)) 1 (U n)ᶜ
hfr : ∀ (n : ℕ) (x : X), (f n) x ∈ Icc 0 1
hsb : ∀ (x : X) (n : ℕ), ‖(f n) x * (1 / 2 / 2 ^ n)‖ ≤ 1 / 2 / 2 ^ n
hsx : ∀ (x : X), Summable fun n ↦ (f n) x * (1 / 2 / 2 ^ n)
n : ℕ
⊢ Continuous[inst✝, _] fun x ↦ (f n) x * (1 / 2 / 2 ^ n)

Tactic:
fun_prop

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

Goal state before:
pp: case neg
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∉ unop V
⊢ 𝓕.map inc ≫ (⋯ ▸ terminalIsTerminal).from (𝓕.obj V) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)

Tactic:
exact ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext ..

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

Goal state before:
pp: X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
⊢ Continuous fun s ↦ ⟨(↑s).base, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_1.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ t₀

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_1.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ ⟨(1 - ↑x.1) * ↑t₁ + ↑x.1 * ↑t₂, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_1.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ x.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_2.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ ⟨(1 - ↑x.1) * ↑t₁ + ↑x.1 * ↑t₂, ⋯⟩

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_2.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ t₂

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case refine_2.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ t₂ : ↑I
γ₁ : (t : ↑I) → Path (γ t₀) (γ (Icc.convexComb t₁ t₂ t)) := fun t ↦ γ.subpath t₀ (Icc.convexComb t₁ t₂ t)
γ₂ : (t : ↑I) → Path (γ (Icc.convexComb t₁ t₂ t)) (γ t₂) := fun t ↦ γ.subpath (Icc.convexComb t₁ t₂ t) t₂
⊢ Continuous fun x ↦ x.2

Tactic:
fun_prop

Goal state after: