mathlib-initiative/mathlib-tactics huggingface dataset:
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 := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
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
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
x : ℂ
hx : x ∈ η₀.toFinset
⊢ 1 = 1

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 := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
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
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
x : ℂ
hx : x ∈ η₀.toFinset
⊢ canonicalFactor R x a ≠ 0 ∨
    -(divisor f (ball 0 R)) x + (divisor f (ball 0 R)) x ≠ 0 ∨
      -(divisor f (ball 0 R)) x = 0 ∧ (divisor f (ball 0 R)) x = 0

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 := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
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
a : ℂ
ha : a ∈ (-divisor f (ball 0 R)).supportᶜ
h₂a : a ∈ closedBall 0 R
x : ℂ
hx : x ∈ η₀.toFinset
⊢ canonicalFactor R x a ≠ 0 ∨
    -(divisor f (ball 0 R)) x + (divisor f (ball 0 R)) x ≠ 0 ∨
      -(divisor f (ball 0 R)) x = 0 ∧ (divisor f (ball 0 R)) x = 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e

Tactic:
]

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ∃ Γ, p ∘ ⇑Γ = ⇑γ ∧ Γ 0 = e
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).im = z.im ∨ (f z).im = -z.im
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
]

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).im = z.im ∨ (f z).im = -z.im
⊢ (f z).im = z.im ∨ (f z).im = -z.im
Module: Mathlib.Analysis.Complex.Isometry

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

Tactic:
simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]

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

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

Tactic:
]

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

Goal state before:
pp: case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ z.re = z.re

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ∀ (x : ↑I), x ∈ Set.Icc 0 1

Tactic:
]

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this : ∀ (n : ℕ), ∃ Γ, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n)) ∧ Γ 0 = e
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 1)
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 1)
Γ_0 : Γ 0 = e
⊢ ∀ (x : ↑I), x ∈ Set.Icc 0 1
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 := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
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)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • 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 := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
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)]
    (∏ i ∈ η₀.toFinset, canonicalFactor R i ^ (-(divisor f (ball 0 R)) i)) • g
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case zero
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t✝ : ℕ → ↑I
t_0 : t✝ 0 = 0
t_mono : Monotone t✝
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t✝ n) (t✝ (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t✝ m = 1
t : ↑I
ht : t = 0
⊢ (p ∘ fun x ↦ e) t = γ t

Tactic:
]

Goal state after:
case zero
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t✝ : ℕ → ↑I
t_0 : t✝ 0 = 0
t_mono : Monotone t✝
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t✝ n) (t✝ (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t✝ m = 1
t : ↑I
ht : t = 0
⊢ (p ∘ fun x ↦ e) t = γ t
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 ↑z = ⊤

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 ↑z = ⊤
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
this✝ : x ∉ sphere 0 R
this : meromorphicOrderAt g x = 0
⊢ (meromorphicOrderAt g x).untop₀ = (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
this✝ : x ∉ sphere 0 R
this : meromorphicOrderAt g x = 0
⊢ (meromorphicOrderAt g x).untop₀ = (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
⊢ ∃ᶠ (x : 𝕜) in 𝓝[≠] ↑w, ¬f x = 0

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
⊢ ∃ᶠ (x : 𝕜) in 𝓝[≠] ↑w, ¬f x = 0
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
⊢ ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 0 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 1 -
      ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 1 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 0 =
    1

Tactic:
]

Goal state after:
a : Circle
⊢ ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 0 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 1 -
      ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 0 1 * ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) 1 0 =
    1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: a : Circle
⊢ 1 = 1

Tactic:
]

Goal state after:
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
⊢ ∃ t, (∀ y ∈ t, y ∈ {↑w}ᶜ → ¬f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑w ∈ t

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
⊢ ∃ t, (∀ y ∈ t, y ∈ {↑w}ᶜ → ¬f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑w ∈ t
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖map 1‖ ≠ 0
x : ℂ
⊢ x = x

Tactic:
]

Goal state after:
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 : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • (↑ℝ ↑map) (x • 1)‖ = ‖x‖

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 : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • (↑ℝ ↑map) (x • 1)‖ = ‖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 : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • ↑map (x • 1)‖ = ‖x‖

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 : ℂ
this : x = x • 1
⊢ ‖‖map 1‖⁻¹ • ↑map (x • 1)‖ = ‖x‖
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: 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
⊢ Preperfect (closure (ball 0 R))

Tactic:
]

Goal state after:
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
⊢ Preperfect (closure (ball 0 R))
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_1.refl
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ Γ (t n) = q.invFun (p (Γ (t n)), (↑q (Γ (t n))).2)

Tactic:
]

Goal state after:
case succ.refine_1.refl
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ Γ (t n) = q.invFun (p (Γ (t n)), (↑q (Γ (t n))).2)
Module: Mathlib.Analysis.Complex.Conformal

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

Tactic:
]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_1.refl
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ γ (t n) ∈ q.baseSet

Tactic:
]

Goal state after:
case succ.refine_1.refl
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ γ (t n) ∈ q.baseSet
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) ↔ ∃ g', restrictScalars ℝ g' = fderiv ℝ f z

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case h₂
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) 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 ((starRingEnd ℂ) ((starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z ∘SL ↑conjCLE) ↔
    DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
Module: Mathlib.Analysis.Complex.Conformal

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

Tactic:
]

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