mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case 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
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

pp: case inr
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✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
;

Goal state after:
case 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
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

case inr
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✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)
hgf : ⇑g ∘ e = ⇑f
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
refine ⟨g, fun y => ?_, hgf⟩

Goal state after:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)
hgf : ⇑g ∘ e = ⇑f
y : Y
⊢ g y ∈ t
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)

pp: case inl.inr
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✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
;

Goal state after:
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)

case inl.inr
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✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
A : Type u_6
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
a : A
⊢ LinearMap.det (↑R ((lmul S A) a)) = LinearMap.det ((lmul R A) a)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case e'_9.e'_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0) =
    ↑(↑g 0 0) * (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) - (↑(↑g 0 0) * ↑τ + ↑(↑g 0 1)) * ↑(↑g 1 0)

Tactic:
;

Goal state after:
case e'_9.e'_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g 0 0) * ↑(↑g 1 1) - ↑(↑g 0 1) * ↑(↑g 1 0) =
    ↑(↑g 0 0) * (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) - (↑(↑g 0 0) * ↑τ + ↑(↑g 0 1)) * ↑(↑g 1 0)
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
a✝ : ℝ≥0
⊢ ↑(({ toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal }.comp
          { toFun := toReal, continuous_toFun := continuous_coe })
        a✝) =
    ↑((ContinuousMap.id ℝ≥0) a✝)

Tactic:
;

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)
x✝ : ℂ
⊢ f (g • ↑ofComplex x✝) = (F ∘ G) x✝

Tactic:
;

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.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x

Tactic:
;

Goal state after:
x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c

Tactic:
;

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c 0 x) y * dist x c = dist x (inversion c 0 y) * dist y c

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist b a * dist c d + dist b c * dist d a = dist b c * dist d a + dist b a * dist c d

Tactic:
;

Goal state after:
case e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist b a * dist c d + dist b c * dist d a = dist b c * dist d a + dist b a * dist c d
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 (dist c) (𝓝[≠] c) (𝓝[>] 0)

Tactic:
tendsto_nhdsWithin_iff

Goal state after:
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 (dist c) (𝓝[≠] c) (𝓝 0) ∧ ∀ᶠ (n : P) in 𝓝[≠] c, dist c n ∈ Ioi 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
by
  rw [dist_le_iff_le_sinh, sinh_half_dist_add_dist, div_mul_eq_div_div _ _ (dist _ _), le_div_iff₀,
    div_mul_eq_mul_div]
  · gcongr
    exact EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist (a : ℂ) b c (conj (b : ℂ))
  · rw [dist_comm, dist_pos, Ne, Complex.conj_eq_iff_im]
    exact b.im_ne_zero

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

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

Tactic:
;

Goal state after:
⊢ ∀ (x : ℝ), 0 < cosh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x

Tactic:
;

Goal state after:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ -sinh x + x = x - sinh x

Tactic:
;

Goal state after:
x : ℝ
⊢ -sinh x + x = x - sinh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ (fun x ↦ 1) x < cosh x

pp: case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

pp: case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x

Tactic:
one_lt_cosh

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

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

Tactic:
;

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
x✝ : ℝ
⊢ iteratedDeriv (0 + 1) cosh x✝ = iteratedDeriv 0 sinh x✝

Tactic:
;

Goal state after:
case zero
x✝ : ℝ
⊢ iteratedDeriv (0 + 1) cosh x✝ = iteratedDeriv 0 sinh x✝
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)

Tactic:
;

Goal state after:
z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)
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
  refine IsInducing.subtypeVal.continuous_iff.mpr ?_
  exact (continuous_id.matrix_map hf).comp continuous_subtype_val

Goal state after:
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:
;

Goal state after:
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)
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 := ⋯ }
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (g₁ ≫ f)) a✝ = (ConcreteCategory.hom (g₂ ≫ f)) a✝

Tactic:
;

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.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
hf : IsIso ((forget (CompHausLike P)).map f)
⊢ IsIso f

Tactic:
;

Goal state after:
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
hf : IsIso ((forget (CompHausLike P)).map f)
⊢ IsIso f
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
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget (CompHausLike P)).map f))
⊢ IsIso f

Tactic:
;

Goal state after:
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
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget (CompHausLike P)).map f))
⊢ IsIso f
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:
;

Goal state after:
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' ball z r ↔ w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)
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:
;

Goal state after:
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B

Tactic:
connectedComponent_eq_iInter_isClopen,

Goal state after:
α : Type u
A B : Ultrafilter α
hB : B ∈ ⋂ s, ↑s
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ 2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
;

Goal state after:
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ 2 * arsinh (dist (↑a • ↑y₁) (↑a • ↑y₂) / (2 * √(↑a * y₁.im * (↑a * y₂.im)))) =
    2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))
Module: Mathlib.Topology.Compactification.StoneCech

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

Tactic:
;

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f ↑x)) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
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 Φ
x✝ : G × X
⊢ x✝ ∈ univ ×ˢ t ↔ x✝ ∈ Φ ⁻¹' snd ⁻¹' t

Tactic:
;

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.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
⊢ Function.Even (proximity f a)

Tactic:
intro r

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
⊢ proximity f a (-r) = proximity f a r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
intro r

Goal state after:
case pos
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
r : ℝ
⊢ 0 r ≤ proximity f a r
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
⊢ 0 ≤ proximity f a

Tactic:
intro r

Goal state after:
case neg
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
r : ℝ
⊢ 0 r ≤ proximity f a r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous ↿fun g z ↦ ↑(↑g 0 0) * z + ↑(↑g 0 1)

Tactic:
;

Goal state after:
⊢ Continuous ↿fun g z ↦ ↑(↑g 0 0) * z + ↑(↑g 0 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: ⊢ Continuous ↿fun g z ↦ ↑(↑g 1 0) * z + ↑(↑g 1 1)

Tactic:
;

Goal state after:
⊢ Continuous ↿fun g z ↦ ↑(↑g 1 0) * z + ↑(↑g 1 1)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ circleAverage (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 ≤
    ∑ x ∈ s, circleAverage (fun x_1 ↦ log⁺ ‖f x x_1‖) 0 + fun x ↦ log ↑s.card

Tactic:
intro r

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
⊢ circleAverage (fun x ↦ log⁺ ‖∑ c ∈ s, f c x‖) 0 r ≤
    (∑ x ∈ s, circleAverage (fun x_1 ↦ log⁺ ‖f x x_1‖) 0 + fun x ↦ log ↑s.card) r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case inl
hK : IsCompact ∅
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ ∅ → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

pp: case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

Tactic:
;

Goal state after:
case inl
hK : IsCompact ∅
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ ∅ → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A

case inr
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
⊢ ∃ A, ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0

Tactic:
intro r

Goal state after:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ circleAverage (fun x ↦ log⁺ (‖f₁ x‖ * ‖f₂ x‖)) 0 r ≤ circleAverage (fun x ↦ log⁺ ‖f₁ x‖ + log⁺ ‖f₂ x‖) 0 r
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: case e'_3
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
x✝ : Matrix (Fin 2) (Fin 2) ℝ
⊢ x✝ ∈
      {m |
        ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
          (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')} ↔
    x✝ ∈
      {y |
        (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
          (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}

Tactic:
;

Goal state after:
case e'_3
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝ : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
x✝ : Matrix (Fin 2) (Fin 2) ℝ
⊢ x✝ ∈
      {m |
        ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
          (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')} ↔
    x✝ ∈
      {y |
        (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
          (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
⊢ locallyFinsupp E ℤ →+ locallyFinsuppWithin (closedBall 0 |r|) ℤ

Tactic:
by
  apply restrictMonoidHom
  tauto

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

Goal state before:
pp: case «0»
K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A // A.det = 1 }
hg : g ∈ (fun g ↦ g • I) ⁻¹' K
j : Fin 2
⊢ |↑g ((fun i ↦ i) ⟨0, ⋯⟩) j| ≤ √A

Tactic:
exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA g hg)

Goal state after: