mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ ↑(↑N * -n) +ᵥ z ∈ verticalStrip (↑N) z.im

Tactic:
refine ⟨?_, by simp⟩

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ |(↑(↑N * -n) +ᵥ z).re| ≤ ↑N
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
⊢ ((↑n * a ^ (n - 1)) • m) ^ 2 = 0

Tactic:
simp [smul_pow, hmsq]

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

Goal state before:
pp: τ : ℍ
⊢ J • τ = ↑ofComplex (-(starRingEnd ℂ) ↑τ)

Tactic:
ext

Goal state after:
τ : ℍ
⊢ ↑(J • τ) = ↑(↑ofComplex (-(starRingEnd ℂ) ↑τ))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z✝ z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := !![w.im, z.im * w.re - w.im * z.re; 0, z.im]
⊢ GeneralLinearGroup.mkOfDetNeZero m ⋯ • z = w

Tactic:
ext

Goal state after:
g : GL (Fin 2) ℝ
z✝ z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := ⋯
⊢ ↑(GeneralLinearGroup.mkOfDetNeZero m ⋯ • z) = ↑w
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ g • z =
    {
      coe :=
        (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
          (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1))),
      coe_im_pos := ⋯ }

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ ↑(g • z) =
    ↑{
        coe :=
          (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
            (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1))),
        coe_im_pos := ⋯ }
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0 ↔ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
constructor

Goal state after:
case mp
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0 → (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

case mpr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
⊢ ((∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x) → ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
i j : Fin 2
⊢ (basisOneI.repr (z * basisOneI j)) i = !![z.re, -z.im; z.im, z.re] i j

Tactic:
Complex.coe_basisOneI_repr,

Goal state after:
z : ℂ
i j : Fin 2
⊢ ![(z * basisOneI j).re, (z * basisOneI j).im] i = !![z.re, -z.im; z.im, z.re] i j
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
this : ↑√z.im ≠ 0
⊢ z.toSL2R • I = z

Tactic:
ext

Goal state after:
z : ℍ
this : ↑√z.im ≠ 0
⊢ ↑(z.toSL2R • I) = ↑z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: ⊢ J ^ 2 = 1

Tactic:
ext

Goal state after:
i✝ j✝ : Fin 2
⊢ ↑(J ^ 2) i✝ j✝ = ↑1 i✝ j✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: ⊢ GeneralLinearGroup.det J = -1

Tactic:
ext

Goal state after:
⊢ ↑(GeneralLinearGroup.det J) = ↑(-1)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : (fun x ↦ x = k) j < (fun x ↦ x = k) i
⊢ (M * auxMat M k) i j = 0

Tactic:
simp_rw [lt_iff_not_ge, le_Prop_eq, Classical.not_imp] at lt
    simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]
    rw [Finset.sum_ite, Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton,
      Finset.sum_ite_eq', if_pos, lt.1, mul_comm, neg_add_cancel]
    exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case e_6
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) = M

Tactic:
ext

Goal state after:
case e_6
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i✝ j✝ : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i✝ j✝ = M i✝ j✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z ∧
    ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
      (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)

Tactic:
constructor

Goal state after:
case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

case right
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n (↑(extChartAt 𝓘(ℂ, ℂ) (↑ofComplex z)) ∘ ↑ofComplex ∘ ↑(extChartAt 𝓘(ℂ, ℂ) z).symm)
    (Set.range ↑𝓘(ℂ, ℂ)) (↑(extChartAt 𝓘(ℂ, ℂ) z) z)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ t'.OrdConnected

Tactic:
constructor

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := ⋯
t' : Set ℝ := ⋯
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∀ ⦃x : ℝ⦄, x ∈ t' → ∀ ⦃y : ℝ⦄, y ∈ t' → Icc x y ⊆ t'
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
this✝¹ : ‖↑(SignType.sign (↑g).det)‖₊ = 1
this✝ : (↑g).det ≠ 0
this : denom g ↑τ ≠ 0
⊢ (1 / ‖(↑τ).im‖₊) ^ 2 = ‖(smulFDeriv g ↑τ).det‖₊ * (1 / ‖(↑(g • ↑ofComplex ↑τ)).im‖₊) ^ 2

Tactic:
ext

Goal state after:
case e'_3
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
this✝¹ : ‖↑(SignType.sign (↑g).det)‖₊ = 1
this✝ : (↑g).det ≠ 0
this : denom g ↑τ ≠ 0
⊢ ↑((1 / ‖(↑τ).im‖₊) ^ 2) = ↑(‖(smulFDeriv g ↑τ).det‖₊ * (1 / ‖(↑(g • ↑ofComplex ↑τ)).im‖₊) ^ 2)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
rw [Algebra.norm_eq_matrix_det bS, ← AlgHom.coe_toRingHom, ← det_toMatrix bA, det_det,
    ← det_toMatrix (bS.smulTower' bA), restrictScalars_toMatrix, RingHom.coe_coe]

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
⊢ { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }.comp
      { toFun := toReal, continuous_toFun := continuous_coe } =
    ContinuousMap.id ℝ≥0

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
a✝ : ℝ≥0
⊢ ↑(({ toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }.comp
          { toFun := toReal, continuous_toFun := continuous_coe })
        a✝) =
    ↑((ContinuousMap.id ℝ≥0) a✝)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
⊢ (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G

Tactic:
ext

Goal state after:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
x✝ : ℂ
⊢ f (g • ↑ofComplex x✝) = (F ∘ G) x✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ smulFDeriv (J * g) z = -↑Complex.conjCLE ∘SL smulFDeriv g z

Tactic:
ext

Goal state after:
g : GL (Fin 2) ℝ
z x✝ : ℂ
⊢ (smulFDeriv (J * g) z) x✝ = (-↑Complex.conjCLE ∘SL smulFDeriv g z) x✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case e'_12
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
e_4✝ : Complex.addCommGroup = Complex.instNormedAddCommGroup.toAddCommGroup
e_5✝ : instInnerProductSpaceRealComplex.toModule ≍ instInnerProductSpaceRealComplex.toModule
⊢ smulFDeriv g ↑τ = (-↑Complex.conjCLE) ∘SL smulFDeriv (J * g) ↑τ

Tactic:
ext

Goal state after:
case e'_12
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
e_4✝ : Complex.addCommGroup = Complex.instNormedAddCommGroup.toAddCommGroup
e_5✝ : instInnerProductSpaceRealComplex.toModule ≍ instInnerProductSpaceRealComplex.toModule
x✝ : ℂ
⊢ (smulFDeriv g ↑τ) x✝ = ((-↑Complex.conjCLE) ∘SL smulFDeriv (J * g) ↑τ) x✝
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
  have H : 2 * z.im * w.im ≠ 0 := by positivity
  simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im,
    cosh_dist', mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ←
    sq]
  ring

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

Goal state before:
pp: case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (dist z w) r = cmp (dist ↑z ↑(w.center r)) (w.im * Real.sinh r)

Tactic:
simp only [← cosh_strictMonoOn.cmp_map_eq dist_nonneg hr₀,
    ← (pow_left_strictMonoOn₀ (M₀ := ℝ) two_ne_zero).cmp_map_eq dist_nonneg hr₀',
    dist_coe_center_sq]

Goal state after:
case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (Real.cosh (dist z w)) (Real.cosh r) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cosh = iteratedDeriv 0 sinh

Tactic:
ext

Goal state after:
case zero
x✝ : ℂ
⊢ iteratedDeriv (0 + 1) cosh x✝ = iteratedDeriv 0 sinh x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case zero
⊢ iteratedDeriv (0 + 1) cosh = iteratedDeriv 0 sinh

Tactic:
ext

Goal state after:
case zero
x✝ : ℝ
⊢ iteratedDeriv (0 + 1) cosh x✝ = iteratedDeriv 0 sinh x✝
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, inst✝¹] (Units.val ∘ ⇑det) ∧
    Continuous[Units.instTopologicalSpaceUnits, inst✝¹] fun x ↦ ↑(det x⁻¹)

Tactic:
constructor

Goal state after:
case left
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, inst✝¹] (Units.val ∘ ⇑det)

case right
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, inst✝¹] fun x ↦ ↑(det x⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ logDeriv cosh = tanh

Tactic:
ext

Goal state after:
x✝ : ℂ
⊢ logDeriv cosh x✝ = tanh x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ logDeriv cosh = tanh

Tactic:
ext

Goal state after:
x✝ : ℝ
⊢ logDeriv cosh x✝ = tanh x✝
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✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]) ∧
    Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]

Tactic:
constructor

Goal state after:
case left
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]

case right
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]
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, instTopologicalSpaceMatrix] (Units.val ∘ ⇑toGL) ∧
    Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun x ↦ ↑(toGL x⁻¹)

Tactic:
constructor

Goal state after:
case left
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, instTopologicalSpaceMatrix] (Units.val ∘ ⇑toGL)

case right
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, instTopologicalSpaceMatrix] fun x ↦ ↑(toGL x⁻¹)
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:
constructor

Goal state after:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom f) → Mono f
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:
ext

Goal state after:
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 := ⋯ }
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (g₁ ≫ f)) a✝ = (ConcreteCategory.hom (g₂ ≫ f)) a✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
constructor

Goal state after:
case mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r → w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
constructor

Goal state after:
case mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r → w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' ball z r
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u) ↔ ∀ s ∈ x, {v | s ∈ v} ∈ u

Tactic:
constructor

Goal state after:
case mp
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u) → ∀ s ∈ x, {v | s ∈ v} ∈ u

case mpr
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ (∀ s ∈ x, {v | s ∈ v} ∈ u) → ∀ (i : Set (Ultrafilter α)), (x ∈ i ∧ i ∈ range fun s ↦ {u | s ∈ u}) → i ∈ ↑u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
constructor

Goal state after:
case mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r → w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

case mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s // IsClopen s ∧ A ∈ s }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
⊢ s ∈ ↑B

Tactic:
have hZ : IsClopen Z := ⟨ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩

Goal state after:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s // IsClopen s ∧ A ∈ s }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
Z : Set (Ultrafilter α) := {F | s ∈ F}
hZ : IsClopen Z
⊢ s ∈ ↑B
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case rel
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a✝ b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a : ∃ x_1, ↑x ≤ 𝓝 x_1 ∧ ↑y ≤ 𝓝 x_1
⊢ Ultrafilter.extend g x = Ultrafilter.extend g y

Tactic:
exact let ⟨a, hx, hy⟩ := a; preStoneCechCompat hg hx hy

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

Goal state before:
pp: X : TopCat
Y : CompHaus
f : ↑X → ↑(compHausToTop.obj Y)
hf : Continuous f
⊢ (fun f ↦ TopCat.ofHom { toFun := ⇑(ConcreteCategory.hom f) ∘ stoneCechUnit, continuous_toFun := ⋯ })
      ((fun f ↦ ofHom (fun x ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ })
        { hom' := { toFun := f, continuous_toFun := hf } }) =
    { hom' := { toFun := f, continuous_toFun := hf } }

Tactic:
ext

Goal state after:
X : TopCat
Y : CompHaus
f : ↑X → ↑(compHausToTop.obj Y)
hf : Continuous f
x✝ : ↑(TopCat.of ↑X)
⊢ (ConcreteCategory.hom
        ((fun f ↦ TopCat.ofHom { toFun := ⇑(ConcreteCategory.hom f) ∘ stoneCechUnit, continuous_toFun := ⋯ })
          ((fun f ↦ ofHom (fun x ↦ True) { toFun := stoneCechExtend ⋯, continuous_toFun := ⋯ })
            { hom' := { toFun := f, continuous_toFun := hf } })))
      x✝ =
    (ConcreteCategory.hom { hom' := { toFun := f, continuous_toFun := hf } }) x✝
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
⊢ some ⁻¹' {∞} = ∅

Tactic:
ext

Goal state after:
X : Type u_1
x✝ : X
⊢ x✝ ∈ some ⁻¹' {∞} ↔ x✝ ∈ ∅
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

case mpr
X Y : CompHaus
f : X ⟶ Y
⊢ Function.Surjective ⇑(ConcreteCategory.hom f) → Epi f
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
⊢ univ ×ˢ t = Φ ⁻¹' snd ⁻¹' t

Tactic:
ext

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun gx ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
x✝ : G × X
⊢ x✝ ∈ univ ×ˢ t ↔ x✝ ∈ Φ ⁻¹' snd ⁻¹' t
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
⊢ ProperSMul G X

Tactic:
constructor

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f) ↔
    Continuous[inst✝¹, inst✝] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
simp_rw [continuous_iff, map_some, ← comap_coe_nhds_infty, tendsto_comap_iff, map_infty,
    isOpenEmbedding_coe.isInducing.continuous_iff (Y := Y)]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x ↦ ↑(f x)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧ Continuous[inst✝¹, instTopologicalSpace] fun x ↦ ↑(f x)) ↔
    Continuous[inst✝¹, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝¹ : UCompactlyGeneratedSpace X
inst✝ : UCompactlyGeneratedSpace Y
⊢ UCompactlyGeneratedSpace (X ⊕ Y)

Tactic:
by
  refine uCompactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sum_iff.2 ⟨?_, ?_⟩
  all_goals
    refine UCompactlyGeneratedSpace.isClosed fun S ⟨f, hf⟩ ↦ ?_
  · let g : ULift.{v} S → X ⊕ Y := Sum.inl ∘ f ∘ ULift.down
    have hg : Continuous g := continuous_inl.comp <| hf.comp continuous_uliftDown
    exact (h (CompHaus.of (ULift.{v} S)) ⟨g, hg⟩).preimage continuous_uliftUp
  · let g : ULift.{u} S → X ⊕ Y := Sum.inr ∘ f ∘ ULift.down
    have hg : Continuous g := continuous_inr.comp <| hf.comp continuous_uliftDown
    exact (h (CompHaus.of (ULift.{u} S)) ⟨g, hg⟩).preimage continuous_uliftUp

Goal state after: