mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z = 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

pp: case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
·

Goal state after:
case left.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z = 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case refine_1
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ r * ↑g⁻¹ i i = 1

pp: case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1

Tactic:
·

Goal state after:
case refine_1
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ r * ↑g⁻¹ i i = 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Goal state before:
pp: case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1

Tactic:
·

Goal state after:
case refine_2
n : Type u_1
R : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
g : SpecialLinearGroup n R
i : n
x✝ : ∃ r, r ^ Fintype.card n = 1 ∧ (diagonal fun x ↦ r) = ↑g
r : R
hr1 : r ^ Fintype.card n = 1
hr : (diagonal fun x ↦ r) = ↑g
⊢ ↑g⁻¹ i i * r = 1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0

pp: case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im

Tactic:
·

Goal state after:
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im

Tactic:
·

Goal state after:
case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ

Tactic:
·

Goal state after:
case refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t

Tactic:
·

Goal state after:
case left.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
⊢ ∃ t ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ, IsOpen[instTopologicalSpaceSubtype] t ∧ z ∈ t
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f = conjLIE

Tactic:
·

Goal state after:
case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f = conjLIE
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⋯
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
have : (f.trans (rotation a).symm) 1 = 1 := by simpa [a] using rotation_apply a⁻¹ (f 1)

Goal state after:
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case h.refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = rotation a

pp: case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)

Tactic:
·

Goal state after:
case h.refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = rotation a
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g

Tactic:
·

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := ⋯
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := ⋯
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
⊢ (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • φ =ᶠ[codiscreteWithin (closedBall 0 R)]
    (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)

Tactic:
·

Goal state after:
case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ

pp: case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
·

Goal state after:
case h.left
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ Subtype.val ⁻¹' t' ⊆ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬meromorphicOrderAt f ↑w = ⊤

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬meromorphicOrderAt f ↑w = ⊤

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : w = z
⊢ ¬meromorphicOrderAt f ↑w = ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ < R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬meromorphicOrderAt f ↑w = ⊤

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ¬meromorphicOrderAt f ↑w = ⊤
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
·

Goal state after:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
a : ℂ
ha : a ∈ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
a : ℂ
ha : a ∉ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
a : ℂ
ha : a ∈ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖

pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ restrictScalars ℝ map = ‖map 1‖ • { toLinearMap := ‖map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := ?refine_1 }.toContinuousLinearMap

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖(‖map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ restrictScalars ℝ map = ‖map 1‖ • { toLinearMap := ‖map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := ⋯ }.toContinuousLinearMap

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
⊢ restrictScalars ℝ map = ‖map 1‖ • { toLinearMap := ‖map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := ⋯ }.toContinuousLinearMap
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
a : ℂ
ha : a ∉ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
a : ℂ
ha : a ∉ ball 0 R
⊢ AnalyticAt ℂ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'

Tactic:
·

Goal state after:
case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
hz : z ∈ {u | meromorphicOrderAt f ↑u = ⊤}ᶜ
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] ↑z, f z ≠ 0
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y ≠ 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' t') ∧ z ∈ Subtype.val ⁻¹' t'
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case inl
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE

pp: case inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE

Tactic:
·

Goal state after:
case inl
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE

Tactic:
·

Goal state after:
case inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∈ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∉ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∈ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mp
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0

pp: case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g

Tactic:
·

Goal state after:
case mp
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g

Tactic:
·

Goal state after:
case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g ∘SL ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ IsOpen[instTopologicalSpaceSubtype] {u | meromorphicOrderAt f ↑u = ⊤}

Tactic:
·

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ IsOpen[instTopologicalSpaceSubtype] {u | meromorphicOrderAt f ↑u = ⊤}
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mpr.inl
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

pp: case mpr.inr
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL ↑conjCLE
⊢ IsConformalMap g

Tactic:
·

Goal state after:
case mpr.inl
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case mpr.inr
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL ↑conjCLE
⊢ IsConformalMap g

Tactic:
·

Goal state after:
case mpr.inr
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL ↑conjCLE
⊢ IsConformalMap g
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∉ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : ‖x‖ = R
η₁ : AnalyticAt ℂ (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) x
η₀ : f =ᶠ[𝓝[≠] x] (∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g
a : ℂ
ha : a ∉ ball 0 R
⊢ (canonicalFactor R a ^ (-(divisor f (ball 0 R)) a)) x ≠ 0
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case h₁
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z

pp: case h₂
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ↔
    DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)

Tactic:
·

Goal state after:
case h₁
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x

Tactic:
·

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f g : ℂ → E
x : ℂ
D : CanonicalDecomp f g R
hR : 0 < R
h : R < ‖x‖
⊢ (divisor g (closedBall 0 R)) x = (divisor f (sphere 0 R)) x