awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
neg :
  ∀ (s : Set E) (hs1 : s ⊆ U) (hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    ∀ x ∈ g '' s, g '' s ∈ 𝓝 x
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds, Or.inr
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
s : Set E
hs1 : s ⊆ U
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
w : E
hw1 : w ∈ s
⊢ g '' s ∈ 𝓝 (g w)

Tactic:
(hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
        (image_mem_map (hs2.mem_nhds hw1))

Premises used: Filter.image_mem_map, AnalyticAt.eventually_constant_or_nhds_le_map_nhds, Or.resolve_left, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∀ x ∈ U, ¬∀ᶠ (z : E) in 𝓝 x, g z = g x
s : Set E
hs1 : s ⊆ U
hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
w : E
hw1 : w ∈ s
⊢ g '' s ∈ 𝓝 (g w)

Tactic:
exact (hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1))
        (image_mem_map (hs2.mem_nhds hw1))

Premises used: Filter.image_mem_map, AnalyticAt.eventually_constant_or_nhds_le_map_nhds, Or.resolve_left, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
g : E → ℂ
hg : AnalyticOnNhd ℂ g univ
⊢ (∃ (w : ℂ), ∀ (z : E), g z = w) ∨ IsOpenMap g

Tactic:
(hg.is_constant_or_isOpen PreconnectedSpace.isPreconnected_univ).imp
    (fun ⟨w, eq⟩ ↦ ⟨w, fun z ↦ eq z ⟨⟩⟩) (· · <| subset_univ _)

Premises used: AnalyticOnNhd.is_constant_or_isOpen, PreconnectedSpace.isPreconnected_univ, Or.imp
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
obtain : ∀ z₀ ∈ U, ∃ (c : ℂ), ∀ x ∈ U, f x = c
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c

Tactic:
obtain ⟨z₀, _⟩ := h₂U.nonempty

Premises used: IsConnected.nonempty
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
by_contra : ∀ (h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c), False
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c

Tactic:
by_contra h₅
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c
⊢ re '' f '' U = {c₀}

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c
tauto tauto₁ tauto₂ : ∀ ⦃a : ℂ⦄, a ∈ U → a ∈ U
⊢ U ⊆ U

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
obtain : ∀ (cc : ℂ) (hcc : ∀ x ∈ U, f x = cc), ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑c : ℂ) * I
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑c : ℂ) * I

Tactic:
obtain ⟨cc, hcc⟩ := eq_const_of_re_eq_const h₁f h₂f h₁U h₂U

Premises used: AnalyticOnNhd.eq_const_of_re_eq_const
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
h : ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑cc.im : ℂ) * I
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑c : ℂ) * I

Tactic:
use cc.im

Premises used: Complex.im
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
h : ∀ x ∈ U, (f x).re = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).re ∧ (f x).im = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).im
⊢ ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑cc.im : ℂ) * I

Tactic:
simp_rw [Complex.ext_iff]

Premises used: Complex.ext_iff
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).re = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, (f x).re = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).re ∧ (f x).im = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).im

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
obtain : ∀ z₀ ∈ U, ∃ (c : ℂ), ∀ x ∈ U, f x = c
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c

Tactic:
obtain ⟨z₀, _⟩ := h₂U.nonempty

Premises used: IsConnected.nonempty
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
by_contra : ∀ (h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c), False
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c

Tactic:
by_contra h₅
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c
⊢ im '' f '' U = {c₀}

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h : z₀ ∈ U
h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c
tauto tauto₁ tauto₂ : ∀ ⦃a : ℂ⦄, a ∈ U → a ∈ U
⊢ U ⊆ U

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
obtain : ∀ (cc : ℂ) (hcc : ∀ x ∈ U, f x = cc), ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c : ℂ) + (↑c₀ : ℂ) * I
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c : ℂ) + (↑c₀ : ℂ) * I

Tactic:
obtain ⟨cc, hcc⟩ := AnalyticOnNhd.eq_const_of_im_eq_const h₁f h₂f h₁U h₂U

Premises used: AnalyticOnNhd.eq_const_of_im_eq_const
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
h : ∀ x ∈ U, f x = (↑cc.re : ℂ) + (↑c₀ : ℂ) * I
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c : ℂ) + (↑c₀ : ℂ) * I

Tactic:
use cc.re

Premises used: Complex.re
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
h : ∀ x ∈ U, (f x).re = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).re ∧ (f x).im = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).im
⊢ ∀ x ∈ U, f x = (↑cc.re : ℂ) + (↑c₀ : ℂ) * I

Tactic:
simp_rw [Complex.ext_iff]

Premises used: Complex.ext_iff
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∀ x ∈ U, (f x).re = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).re ∧ (f x).im = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).im

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
⊢ (∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p) ∨ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
or_iff_not_imp_left.mpr fun h ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
refine : ∀ (h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p), IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
⊢ (∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p) ∨ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
refine or_iff_not_imp_left.mpr fun h ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
inl : ∀ (x : ℂ) (eq : ∀ (z : ℂ), eval z p = x), IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
inr : ∀ (hp : IsOpenMap (Y := ℂ) fun (x : ℂ) ↦ eval x p), IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
obtain ⟨x, eq⟩ | hp := (AnalyticOnNhd.eval_polynomial p).is_constant_or_isOpenMap

Premises used: AnalyticOnNhd.is_constant_or_isOpenMap, AnalyticOnNhd.eval_polynomial
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ ∀ (r : ℂ), eval r ((C : (a : ℂ) → ℂ[X]) x) = eval r p

Tactic:
simpa [eq_comm (a := x)]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
exact (h ⟨x, funext <| by simpa [eq_comm (a := x)]⟩).elim

Premises used: False.elim, Polynomial.funext, Exists.intro
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
hp : IsOpenMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
⟨IsAlgClosed.eval_surjective <| natDegree_eq_zero.not.mpr h, p.continuous_aeval, hp⟩

Premises used: Iff.mpr, Polynomial.continuous_aeval, IsOpenQuotientMap.mk, Iff.not, IsAlgClosed.eval_surjective, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
hp : IsOpenMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
exact ⟨IsAlgClosed.eval_surjective <| natDegree_eq_zero.not.mpr h, p.continuous_aeval, hp⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
p : ℂ[X]
hp : p.natDegree ≠ 0
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p

Tactic:
p.C_eq_or_isOpenQuotientMap_eval.resolve_left <| natDegree_eq_zero.not.mp hp

Premises used: Iff.not, Or.resolve_left, Polynomial.C_eq_or_isOpenQuotientMap_eval, Iff.mp, Polynomial.natDegree_eq_zero
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ Polynomial.eval x (HPow.hPow (α := Polynomial ℂ) Polynomial.X n)

Tactic:
Polynomial.isOpenQuotientMap_eval (.X ^ n) _

Premises used: HPow.hPow, Polynomial.isOpenQuotientMap_eval
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
h : ∀ (x : ℂ), x ^ n = Polynomial.eval x (HPow.hPow (α := Polynomial ℂ) Polynomial.X n)
convert! : (HPow.hPow (α := Polynomial ℂ) Polynomial.X n).natDegree ≠ 0
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ x ^ n

Tactic:
convert! Polynomial.isOpenQuotientMap_eval (.X ^ n) _

Premises used: HPow.hPow, Polynomial.isOpenQuotientMap_eval
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
x : ℂ
⊢ x ^ n = Polynomial.eval x (HPow.hPow (α := Polynomial ℂ) Polynomial.X n)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
⊢ (HPow.hPow (α := Polynomial ℂ) Polynomial.X n).natDegree ≠ 0

Tactic:
simpa using NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
z : { z : ℂ // z ≠ 0 }
h : (fun (x : ℂ) ↦ x ^ n) 0 = (↑z : ℂ)
⊢ (↑z : ℂ) = 0

Tactic:
simpa [zero_pow (NeZero.ne n)] using h.symm

Premises used: Eq.symm, zero_pow, NeZero.ne
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
z : { z : ℂ // z ≠ 0 }
h : (fun (x : ℂ) ↦ x ^ n) 0 = (↑z : ℂ)
⊢ False

Tactic:
exact z.2 (by simpa [zero_pow (NeZero.ne n)] using h.symm)

Premises used: Subtype.property
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero n
⊢ Continuous (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℤ
inst : NeZero n
inl :
  ∀ (n : ℕ) [NeZero (R := ℤ) (↑n : ℤ)],
    IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
      Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (↑n : ℤ)) ⋯
inr :
  ∀ (n : ℕ) [NeZero (R := ℤ) (-(↑n : ℤ))],
    IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
      Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (-(↑n : ℤ))) ⋯
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (↑n : ℤ)
⊢ NeZero n

Tactic:
have : NeZero n := ⟨Nat.cast_ne_zero.mp (NeZero.ne (n : ℤ))⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (↑n : ℤ)
this : NeZero n
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (↑n : ℤ)) ⋯

Tactic:
isOpenQuotientMap_pow_compl_zero n

Premises used: zpowRec, Complex.isOpenQuotientMap_pow_compl_zero
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (↑n : ℤ)
this : NeZero n
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (↑n : ℤ)) ⋯

Tactic:
exact isOpenQuotientMap_pow_compl_zero n

Premises used: Complex.isOpenQuotientMap_pow_compl_zero
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (-(↑n : ℤ))
⊢ NeZero n

Tactic:
have : NeZero n := ⟨Nat.cast_ne_zero.mp <| neg_ne_zero.mp (NeZero.ne (-n : ℤ))⟩
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (-(↑n : ℤ))
this : NeZero n
⊢ IsOpenQuotientMap (X := { g : ℂ // g ≠ 0 }) (Y := { z : ℂ // z ≠ 0 })
    ((fun (z : { z : ℂ // z ≠ 0 }) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯) ∘
      (⇑(Homeomorph.inv₀ ℂ) : (a : { g : ℂ // g ≠ 0 }) → { g : ℂ // g ≠ 0 }))

Tactic:
(isOpenQuotientMap_pow_compl_zero n).comp (Homeomorph.inv₀ ℂ).isOpenQuotientMap

Premises used: Homeomorph.inv₀, Complex.isOpenQuotientMap_pow_compl_zero, Complex, IsOpenQuotientMap.comp, Homeomorph.isOpenQuotientMap
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (-(↑n : ℤ))
this : NeZero n
h :
  ∀ (x : { z : ℂ // z ≠ 0 }),
    HPow.hPow (β := ℤ) (↑x : ℂ) (-(↑n : ℤ)) =
      (↑(((fun (z : { z : ℂ // z ≠ 0 }) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯) ∘
              (⇑(Homeomorph.inv₀ ℂ) : (a : { g : ℂ // g ≠ 0 }) → { g : ℂ // g ≠ 0 }))
            x) :
        ℂ)
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (-(↑n : ℤ))) ⋯

Tactic:
convert! (isOpenQuotientMap_pow_compl_zero n).comp (Homeomorph.inv₀ ℂ).isOpenQuotientMap

Premises used: Homeomorph.inv₀, Complex.isOpenQuotientMap_pow_compl_zero, Complex, IsOpenQuotientMap.comp, Homeomorph.isOpenQuotientMap
-- Module: Mathlib.Analysis.Complex.OpenMapping
Goal:
n : ℕ
inst : NeZero (R := ℤ) (-(↑n : ℤ))
this : NeZero n
x : { z : ℂ // z ≠ 0 }
⊢ HPow.hPow (β := ℤ) (↑x : ℂ) (-(↑n : ℤ)) =
    (↑(((fun (z : { z : ℂ // z ≠ 0 }) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯) ∘
            (⇑(Homeomorph.inv₀ ℂ) : (a : { g : ℂ // g ≠ 0 }) → { g : ℂ // g ≠ 0 }))
          x) :
      ℂ)

Tactic:
simp [Homeomorph.inv₀]

Premises used: Homeomorph.inv₀
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ Eq (α := ℝ) ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ) (↑conjLIE.toLinearEquiv : ℂ →ₗ[ℝ] ℂ) : ℝ) (-1 : ℝ)

Tactic:
det_conjAe

Premises used: Complex.det_conjAe
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ Eq (α := ℝˣ) ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ) conjLIE.toLinearEquiv : ℝˣ) (-1 : ℝˣ)

Tactic:
linearEquiv_det_conjAe

Premises used: Complex.linearEquiv_det_conjAe, AlgEquiv.toLinearEquiv
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ 1 = norm (E := ℝ) ((reCLM : (a : ℂ) → ℝ) 1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ norm (E := ℂ) 1 ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖reCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖reCLM‖₊ = 1

Tactic:
Subtype.ext reCLM_norm

Premises used: NNReal, Complex.reCLM_norm, Subtype.ext
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ 1 = norm (E := ℝ) ((imCLM : (a : ℂ) → ℝ) I : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖I‖ ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖imCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖imCLM‖₊ = 1

Tactic:
Subtype.ext imCLM_norm

Premises used: Complex.imCLM_norm, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖(↑conjCLE : ℂ →L[ℝ] ℂ)‖ = 1

Tactic:
conjLIE.toLinearIsometry.norm_toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.norm_toContinuousLinearMap, Complex.conjLIE, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖(↑conjCLE : ℂ →L[ℝ] ℂ)‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖(↑conjCLE : ℂ →L[ℝ] ℂ)‖₊ = 1

Tactic:
Subtype.ext conjCLE_norm

Premises used: NNReal, Complex.conjCLE_norm, Subtype.ext
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖ofRealCLM‖ = 1

Tactic:
ofRealLI.norm_toContinuousLinearMap

Premises used: LinearIsometry.norm_toContinuousLinearMap, Complex.ofRealCLM, Complex.ofRealLI
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖ofRealCLM‖ₑ = 1

Tactic:
simp [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.Analysis.Complex.OperatorNorm
Goal:
⊢ ‖ofRealCLM‖₊ = 1

Tactic:
Subtype.ext <| ofRealCLM_norm

Premises used: Complex.ofRealCLM_norm, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
rw : (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)

Tactic:
rw [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
mp : (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im → (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
mpr : (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im) → (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im
mp₁ mp₂ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
mp₃ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → z.re ≤ w.re
mp₄ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → z.im = w.im
mp₅ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → ¬(w.re ≤ z.re ∧ w.im = z.im)
mpr₁ mpr₂ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im
mpr₃ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → z.re ≤ w.re
mpr₄ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → ¬w.re ≤ z.re
mpr₅ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → z.im = w.im
mp₆ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → w.re ≤ z.re → w.im = z.im → False
mpr₆ : z.re ≤ w.re → z.im = w.im → w.re ≤ z.re → ¬w.re ≤ z.re → False
mpr₇ mpr₈ mpr₉ mpr₁₀ mpr₁₁ mpr₁₂ mpr₁₃ mpr₁₄ : z.re ≤ w.re → z.im = w.im → w.re ≤ z.re → ¬w.im = z.im → False
⊢ (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
⊢ z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
⊢ z < w ↔ z.re < w.re ∧ z.im = w.im

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 ≤ z ↔ 0 ≤ z.re ∧ 0 = z.im

Tactic:
le_def

Premises used: Complex.le_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 < z ↔ 0 < z.re ∧ 0 = z.im

Tactic:
lt_def

Premises used: Complex.lt_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ z ≤ 0 ↔ z.re ≤ 0 ∧ z.im = 0

Tactic:
le_def

Premises used: Complex.le_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ z < 0 ↔ z.re < 0 ∧ z.im = 0

Tactic:
lt_def

Premises used: Complex.lt_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
rw : 0 ≤ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.im = 0
⊢ 0 ≤ HPow.hPow (β := ℕ) z 2 ↔ z.im = 0

Tactic:
rw [nonneg_iff, pow_two, mul_re, mul_im, mul_comm z.im z.re, ← mul_two, eq_comm,
    mul_eq_zero_iff_right two_ne_zero, ← pow_two, ← pow_two, mul_eq_zero]

Premises used: Complex.mul_im, Complex.mul_re, pow_two, Complex.im, eq_comm, mul_eq_zero, Complex.re, two_ne_zero, mul_comm, mul_eq_zero_iff_right, Complex.nonneg_iff, mul_two
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 ≤ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ∧ (z.re = 0 ∨ z.im = 0) → z.im = 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
h : z.im = 0
⊢ 0 ≤ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
simpa [h] using sq_nonneg z.re

Premises used: Complex.re, sq_nonneg
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 ≤ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.im = 0

Tactic:
exact ⟨by aesop, fun h ↦ by simpa [h] using sq_nonneg z.re⟩
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
rw : HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.re = 0
⊢ HPow.hPow (β := ℕ) z 2 ≤ 0 ↔ z.re = 0

Tactic:
rw [nonpos_iff, pow_two, mul_re, mul_im, mul_comm z.im z.re, ← mul_two, mul_eq_zero_iff_right
    two_ne_zero, ← pow_two, ← pow_two, mul_eq_zero]

Premises used: Complex.mul_im, Complex.mul_re, pow_two, Complex.im, Complex.nonpos_iff, mul_eq_zero, Complex.re, two_ne_zero, mul_comm, mul_eq_zero_iff_right, mul_two
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0) → z.re = 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
h : z.re = 0
⊢ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
simpa [h] using sq_nonneg z.im

Premises used: Complex.im, sq_nonneg
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0) ↔ z.re = 0

Tactic:
exact ⟨by aesop, fun h ↦ by simpa [h] using sq_nonneg z.im⟩
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x y : ℝ
⊢ (↑x : ℂ) ≤ (↑y : ℂ) ↔ x ≤ y

Tactic:
simp [le_def, ofReal]

Premises used: Complex.ofReal, Complex.le_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x y : ℝ
⊢ (↑x : ℂ) < (↑y : ℂ) ↔ x < y

Tactic:
simp [lt_def, ofReal]

Premises used: Complex.ofReal, Complex.lt_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x : ℝ
⊢ 0 ≤ (↑x : ℂ) ↔ 0 ≤ x

Tactic:
real_le_real

Premises used: Complex.real_le_real
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x : ℝ
⊢ 0 < (↑x : ℂ) ↔ 0 < x

Tactic:
real_lt_real

Premises used: Complex.real_lt_real
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
rw : ¬(z.re ≤ w.re ∧ z.im = w.im) ↔ w.re < z.re ∨ z.im ≠ w.im
rw₁ : ¬z.re ≤ w.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im
rw₂ rw₃ : w.re < z.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
rw [le_def, not_and_or, not_le]

Premises used: not_le, not_and_or, Complex.le_def