mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (inversion c R) (𝓝[≠] c) (Bornology.cobounded P)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist a c ≤ dist a b + dist b c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist z w ≤ dist ↑z ↑w / √(z.im * w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r : ℝ
z : ℍ
⊢ dist z z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w✝ : ℍ
r : ℝ
z w : ℍ
h : dist z w = 0
⊢ z = w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r✝ : ℝ
z : ℍ
r : ℝ
⊢ 0 < { re := z.re, im := z.im * Real.cosh r }.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
⊢ z.center 0 = z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ 2 * z.im * w.im ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
⊢ 0 ≤ w.im * Real.sinh r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
⊢ 0 < 2 * z.im * w.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ sinh ~[𝓝 0] id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℂ
⊢ HasStrictDerivAt cosh (sinh x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ ∀ (x : ℝ), 0 < deriv sinh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ 0 < sinh x ↔ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x < 0 ↔ x < 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ 0 ≤ sinh x ↔ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ |sinh x| = sinh |x|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ |0| ≤ |x|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ |0| < |x| ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
⊢ 0 < z.im / w.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ StrictMono fun x ↦ sinh x - x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sinh = sinh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cosh = cosh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) sinh = cosh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n + 1) cosh = sinh

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → GL n R
hf : Continuous[inst✝, Units.instTopologicalSpaceUnits] f
i : n
⊢ Continuous[instTopologicalSpaceMatrix, Pi.topologicalSpace] fun A ↦ A i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → GL n R
hf : Continuous[inst✝, Units.instTopologicalSpaceUnits] f
i : n
⊢ Continuous[inst✝, instTopologicalSpaceMatrix] fun x ↦ ↑(f x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) sinh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n✝ n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) cosh)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ logDeriv cosh = tanh

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] ⇑det

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < Real.sinh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ Real.sinh x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ Real.sinh x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist { coe := { re := 0, im := z.im }, coe_im_pos := ⋯ } { coe := { re := 0, im := w.im }, coe_im_pos := ⋯ } ≤
    dist z w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ z.im ≤ w.im * rexp (dist z w)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑(w.center (dist z w)) + dist ↑w ↑(w.center (dist z w)) = w.im * (rexp (dist z w) - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) = dist ↑z ↑(w.center (dist z w)) - dist ↑w ↑(w.center (dist z w))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
x : ℍ × ℍ
⊢ 2 * √(x.1.im * x.2.im) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, Units.instTopologicalSpaceUnits] ⇑upperRightHom

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst✝, instTopologicalSpace] f
i : n
⊢ Continuous[instTopologicalSpaceMatrix, Pi.topologicalSpace] fun A ↦ A i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst✝, instTopologicalSpace] f
i : n
⊢ Continuous[inst✝, instTopologicalSpaceMatrix] fun x ↦ ↑(f x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : Continuous[inst✝², inst✝] ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : IsInducing ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : IsEmbedding ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, Units.instTopologicalSpaceUnits] ⇑toGL

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
x : GL n A
x✝ : ∃ y, ↑y = ↑x
y : SL n A
hy : ↑y = ↑x
⊢ (↑x).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ instTopologicalSpace = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
⊢ Set.range ⇑toGL = ⇑GeneralLinearGroup.det ⁻¹' {1}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] ⇑GeneralLinearGroup.det

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ IsClosed[Units.instTopologicalSpaceUnits] (Set.range ⇑toGL)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
w : ℂ
h : dist w ↑(z.center r) ≤ z.im * Real.sinh r
⊢ dist (↑(z.center r)) w ≤ z.im * Real.sinh r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Epi f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x ↦ x₁, continuous_toFun := ⋯ }
⊢ x₁ = x₂

Tactic:
let g₂ : X ⟶ X := ofHom _ ⟨fun _ => x₂, continuous_const⟩

Goal state after:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x ↦ x₂, continuous_toFun := ⋯ }
⊢ x₁ = x₂
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x ↦ x₂, continuous_toFun := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ Continuous ⇑E.symm

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
⊢ ∀ {A B : CompHausLike P} (f : A ⟶ B) [IsIso ((forget (CompHausLike P)).map f)], IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ ∀ t₁ ∈ ultrafilterBasis α, ∀ t₂ ∈ ultrafilterBasis α, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ultrafilterBasis α, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
s : Set α
⊢ IsClosed {u | s ∈ u}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' ball z r = ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ x = joinM u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ ProperSpace ℍ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : ℝ
⊢ Isometry fun y ↦ { coe := { re := a, im := rexp y }, coe_im_pos := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : ℝ
y₁ y₂ : ℍ
⊢ dist (a +ᵥ y₁) (a +ᵥ y₂) = dist y₁ y₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ TotallyDisconnectedSpace (Ultrafilter α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ Tendsto pure (↑b) (𝓝 b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ comap pure (𝓝 b) ≤ ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : { x // 0 < x }
⊢ Isometry fun x ↦ a • x

Tactic:
refine Isometry.of_dist_eq fun y₁ y₂ => ?_
  simp only [dist_eq, coe_pos_real_smul, pos_real_im]; congr 2
  rw [dist_smul₀, mul_mul_mul_comm, Real.sqrt_mul (mul_self_nonneg _), Real.sqrt_mul_self_eq_abs,
    Real.norm_eq_abs, mul_left_comm]
  exact mul_div_mul_left _ _ (mt _root_.abs_eq_zero.1 a.2.ne')

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
⊢ Ultrafilter.extend f ∘ pure = f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : { x // 0 < x }
⊢ Isometry fun x ↦ a • x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ 0 ≤ y₁.im * y₂.im

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ ↑(Ultrafilter.map f b) ≤ 𝓟 univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
⊢ ‖↑y₁ * ↑y₂‖ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
⊢ Continuous[_, inst✝²] (Ultrafilter.extend f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ ↑(Ultrafilter.map pure g) ≤ 𝓝 g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ Tendsto preStoneCechUnit (↑g) (𝓝 (preStoneCechUnit x))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous[_, inst✝¹] g₁
h₂ : Continuous[_, inst✝¹] g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : ↑F ≤ 𝓝 x
hG : ↑G ≤ 𝓝 x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
⊢ dist (ModularGroup.S • y₁) (ModularGroup.S • y₂) = dist y₁ y₂

Tactic:
by

Goal state after: