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

Goal state before:
pp: n : Type u_4
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
l✝ : ℕ
ih :
  ∀ {R : Type u_1} {S : Type u_2} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] (M : Matrix m m S)
    [inst_2 : DecidableEq m] [inst_3 : Fintype m] (f : S →+* Matrix n n R),
    Fintype.card m = l✝ → (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det
R : Type u_1
S : Type u_2
m : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
inst✝ : Fintype m
f : S →+* Matrix n n R
l : Fintype.card m = l✝ + 1
k : m
f' : S[X] →+* Matrix n n R[X] := f.polyToMatrix
M' : Matrix m m S[X] := cornerAddX M k
⊢ (f' M'.det).det = ((comp m m n n R[X]) (M'.map ⇑f')).det

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex) z

Tactic:
by

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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ a = c - (b - c)

Tactic:
by

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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ a < (g - dg) y

Tactic:
by

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

Goal state before:
pp: 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
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f M.det).det = ((comp m m n n R) (M.map ⇑f)).det

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContDiffAt ℂ n (f ∘ ↑ofComplex) ↑τ

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ ↑ofComplex) ↑τ

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ 0 ∉ {0}ᶜ ∨ 0 ≤ k

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun x ↦ denom g ↑x ^ k

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ (denom g ↑τ)⁻¹

Tactic:
by

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

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ g • τ

Tactic:
by

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
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
by

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

Goal state before:
pp: 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)
τ : ℍ
⊢ ‖↑(SignType.sign (↑g).det)‖₊ = 1

Tactic:
by

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
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed[inst✝²] s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f

Tactic:
by

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
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)
⊢ Continuous[inst✝², _] (Subtype.val ∘ ⇑h ∘ ⇑f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ SMulInvariantMeasure (GL (Fin 2) ℝ) ℍ volume

Tactic:
by

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
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:
by

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

Goal state before:
pp: f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ {z | 0 < z.im} ⊆ {z | 0 ≤ z.im}

Tactic:
by

Goal state after:
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
⊢ (norm R) ((norm S) a) = (norm R) a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : y ∈ (minpoly K x).aroots (AlgebraicClosure ↥F)
this : (aeval y) (Polynomial.map (algebraMap R K) (minpoly R x)) = 0
⊢ eval₂ (algebraMap R (AlgebraicClosure ↥F)) y (minpoly R x) = 0

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0

Tactic:
by

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

Goal state before:
pp: f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
hfg : f * g = 0
⊢ ∀ (x : ℍ), f x = 0 ∨ g x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
⊢ IsIntegral R ((norm K) x)

Tactic:
by

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

Goal state before:
pp: f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
⊢ f = 0 ∨ g = 0 → f * g = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∀ (x : ℍ), ∏ i ∈ s, f i x = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ ∏ i ∈ s, f i = 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ

Tactic:
by

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
H : FiniteDimensional (↥K⟮x⟯) L
⊢ FiniteDimensional K L

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * ↑(↑g 1 0) * denom g ↑τ ^ (k - 1)) ↑τ

Tactic:
by

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

Goal state before:
pp: case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯

Tactic:
refine fun H ↦ hx ?_
        rw [← isIntegral_gen]
        exact IsIntegral.isIntegral (gen K x)

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ HasStrictDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

Tactic:
by

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
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
by

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
⊢ Continuous toReal

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ HasStrictDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

Tactic:
by

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
by

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:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ deriv (fun z ↦ ↑(g • ↑ofComplex z)) ↑τ ≠ 0

Tactic:
by

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_8
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ (algebraMap K F) ((norm K) x) = ((minpoly K x).aroots F).prod ^ finrank (↥K⟮x⟯) L

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ AnalyticAt ℂ (fun z ↦ ↑(g • ↑ofComplex z)) ↑τ

Tactic:
by

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

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: ⊢ arsinh 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
⊢ (algebraMap K E) ((norm K) x) = ∏ σ, σ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ HasStrictDerivAt arsinh (√(1 + x ^ 2))⁻¹ x

Tactic:
by

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap K L) ((norm K) x) = ∏ σ, σ x

Tactic:
by

Goal state after:
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 : ℝ
⊢ inversion c R c = c

Tactic:
by

Goal state after:
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 x : P
⊢ inversion c 0 x = c

Tactic:
by

Goal state after:
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
a R : ℝ
x : P
⊢ inversion c (a * R) x = (homothety c (a ^ 2)) (inversion c R x)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 x : P
⊢ inversion c (dist x c) x = x

Tactic:
by

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

Goal state after:
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 x : P
⊢ inversion c (dist c x) x = x

Tactic:
by

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

Goal state before:
pp: z w : ℍ
⊢ cosh (dist z w / 2) = dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (smulFDeriv g z).det =
    ↑(SignType.sign ↑(Matrix.GeneralLinearGroup.det g)) * ↑(Matrix.GeneralLinearGroup.det g) ^ 2 / ‖denom g z‖ ^ 4

Tactic:
by

Goal state after:
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 x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c

Tactic:
by

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

Goal state before:
pp: z w : ℍ
⊢ tanh (dist z w / 2) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

Tactic:
by

Goal state after:
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 x : P
R : ℝ
⊢ dist c (inversion c R x) = R ^ 2 / dist c x

Tactic:
by

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

Goal state before:
pp: 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
⊢ 0 < ↑(Matrix.GeneralLinearGroup.det (J * g))

Tactic:
by

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

Goal state before:
pp: z w : ℍ
⊢ rexp (dist z w / 2) = (dist ↑z ↑w + dist (↑z) ((starRingEnd ℂ) ↑w)) / (2 * √(z.im * w.im))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

Tactic:
by

Goal state after:
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
x : P
⊢ inversion c R (inversion c R x) = x

Tactic:
by

Goal state after:
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 x : P
R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by

Goal state after:
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 x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist (inversion c R x) (inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y

Tactic:
by

Goal state after:
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 x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
⊢ inversion c R y ≠ c

Tactic:
by

Goal state after:
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 x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
⊢ dist (inversion c R x) y * dist x c = dist x (inversion c R y) * dist y c

Tactic:
by

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

Goal state before:
pp: a b c : ℍ
⊢ sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Tactic:
by

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

Goal state before:
pp: z w : ℍ
⊢ dist z w = dist w z

Tactic:
by

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist z w ≤ r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Tactic:
by

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
by

Goal state after:
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
a b c d : P
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
by

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

Goal state before:
pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2

Tactic:
by

Goal state after:
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
⊢ ContinuousAt (dist c) c

Tactic:
by

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

Goal state after:
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
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
⊢ 0 < R ^ 2

Tactic:
by

Goal state after:
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
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
⊢ Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop

Tactic:
by

Goal state after: