awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ (∃ (w : ℂ), ∀ z ∈ U, g z = w) ∨
    ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
have neg : ∀ (s : Set E) (hs1 : s ⊆ U) (hs2 : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  ∀ x ∈ g '' s, g '' s ∈ 𝓝 x
Tactic: refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c
have obtain : ∀ z₀ ∈ U, ∃ (c : ℂ), ∀ x ∈ U, f x = c
Tactic: obtain ⟨z₀, _⟩ := h₂U.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c
have by_contra : ∀ (h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c), False
Tactic: by_contra h₅
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ U ⊆ U
have tauto : ∀ ⦃a : ℂ⦄, a ∈ U → a ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑c : ℂ) * I
have obtain : ∀ (cc : ℂ) (hcc : ∀ x ∈ U, f x = cc), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑c : ℂ) * I
have h : ∀ x ∈ U, f x = (↑c₀ : ℂ) + (↑cc.im : ℂ) * I
Tactic: use cc.im
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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 = (↑c₀ : ℂ) + (↑cc.im : ℂ) * I
have h : ∀ x ∈ U, (f x).re = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).re ∧ (f x).im = ((↑c₀ : ℂ) + (↑cc.im : ℂ) * I).im
Tactic: simp_rw [Complex.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c
have obtain : ∀ z₀ ∈ U, ∃ (c : ℂ), ∀ x ∈ U, f x = c
Tactic: obtain ⟨z₀, _⟩ := h₂U.nonempty
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℂ), ∀ x ∈ U, f x = c
have by_contra : ∀ (h₅ : ¬∃ (c : ℂ), ∀ x ∈ U, f x = c), False
Tactic: by_contra h₅
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ U ⊆ U
have tauto : ∀ ⦃a : ℂ⦄, a ∈ U → a ∈ U
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c : ℂ) + (↑c₀ : ℂ) * I
have obtain : ∀ (cc : ℂ) (hcc : ∀ x ∈ U, f x = cc), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ ∃ (c : ℝ), ∀ x ∈ U, f x = (↑c : ℂ) + (↑c₀ : ℂ) * I
have h : ∀ x ∈ U, f x = (↑cc.re : ℂ) + (↑c₀ : ℂ) * I
Tactic: use cc.re
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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 = (↑cc.re : ℂ) + (↑c₀ : ℂ) * I
have h : ∀ x ∈ U, (f x).re = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).re ∧ (f x).im = ((↑cc.re : ℂ) + (↑c₀ : ℂ) * I).im
Tactic: simp_rw [Complex.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
p : ℂ[X]
⊢ (∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p) ∨ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
have refine : ∀ (h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p), IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
Tactic: refine or_iff_not_imp_left.mpr fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
p : ℂ[X]
h : ¬∃ (x : ℂ), (C : (a : ℂ) → ℂ[X]) x = p
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
have inl : ∀ (x : ℂ) (eq : ∀ (z : ℂ), eval z p = x), IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
Tactic: obtain ⟨x, eq⟩ | hp := (AnalyticOnNhd.eval_polynomial p).is_constant_or_isOpenMap
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ eval x p
have inr : ∀ (hp : IsOpenMap (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ x ^ n
have h : ∀ (x : ℂ), x ^ n = Polynomial.eval x (HPow.hPow (α := Polynomial ℂ) Polynomial.X n)
Tactic: convert! Polynomial.isOpenQuotientMap_eval (.X ^ n) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
n : ℕ
inst : NeZero n
h : ∀ (x : ℂ), x ^ n = Polynomial.eval x (HPow.hPow (α := Polynomial ℂ) Polynomial.X n)
⊢ IsOpenQuotientMap (Y := ℂ) fun (x : ℂ) ↦ x ^ n
have convert! : (HPow.hPow (α := Polynomial ℂ) Polynomial.X n).natDegree ≠ 0
Tactic: convert! Polynomial.isOpenQuotientMap_eval (.X ^ n) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
Goal:
n : ℤ
inst : NeZero n
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯
have 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 : ℤ)) sorry
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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 : ℤ)) ⋯
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) ⋯
have 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 : ℤ))) sorry
Tactic: obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
Goal:
n : ℕ
inst : NeZero (R := ℤ) (↑n : ℤ)
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (↑n : ℤ)) ⋯
have this : NeZero n
Tactic: have : NeZero n := ⟨Nat.cast_ne_zero.mp (NeZero.ne (n : ℤ))⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (hypothesis)
Goal:
n : ℕ
inst : NeZero (R := ℤ) (-(↑n : ℤ))
⊢ IsOpenQuotientMap (Y := { z : ℂ // z ≠ 0 }) fun (z : { z : ℂ // z ≠ 0 }) ↦
    Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) (HPow.hPow (β := ℤ) (↑z : ℂ) (-(↑n : ℤ))) ⋯
have this : NeZero n
Tactic: have : NeZero n := ⟨Nat.cast_ne_zero.mp <| neg_ne_zero.mp (NeZero.ne (-n : ℤ))⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.OpenMapping (goal)
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 : ℤ))) ⋯
have h : ∀ (x : { z : ℂ // z ≠ 0 }),
  HPow.hPow (β := ℤ) (↑x : ℂ) (-(↑n : ℤ)) =
    (↑(((fun (z : { z : ℂ // z ≠ 0 }) ↦ Subtype.mk (p := fun (z : ℂ) ↦ z ≠ 0) ((↑z : ℂ) ^ n) sorry) ∘
            (⇑(Homeomorph.inv₀ ℂ) : (a : { g : ℂ // g ≠ 0 }) → { g : ℂ // g ≠ 0 }))
          x) :
      ℂ)
Tactic: convert! (isOpenQuotientMap_pow_compl_zero n).comp (Homeomorph.inv₀ ℂ).isOpenQuotientMap
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
⊢ z.re < w.re ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)
have 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)
Tactic: rw [lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
⊢ (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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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)
⊢ (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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have 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)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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)
⊢ (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)
have mp₃ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → z.re ≤ w.re
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mp₄ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → z.im = w.im
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mp₅ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → ¬(w.re ≤ z.re ∧ w.im = z.im)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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)
⊢ (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)
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mpr₃ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → z.re ≤ w.re
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mpr₄ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → ¬w.re ≤ z.re
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mpr₅ : ¬(w.re ≤ z.re ∧ w.im = z.im) → z.re ≤ w.re → z.im = w.im → z.im = w.im
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mp₆ : z.im = w.im → z.re ≤ w.re → ¬w.re ≤ z.re → w.re ≤ z.re → w.im = z.im → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mpr₆ : z.re ≤ w.re → z.im = w.im → w.re ≤ z.re → ¬w.re ≤ z.re → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ (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)
have mpr₇ : z.re ≤ w.re → z.im = w.im → w.re ≤ z.re → ¬w.im = z.im → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
⊢ 0 ≤ HPow.hPow (β := ℕ) z 2 ↔ z.im = 0
have rw : 0 ≤ HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ∧ (z.re = 0 ∨ z.im = 0) ↔ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) z 2 ≤ 0 ↔ z.re = 0
have rw : HPow.hPow (β := ℕ) z.re 2 - HPow.hPow (β := ℕ) z.im 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
have rw : ¬(z.re ≤ w.re ∧ z.im = w.im) ↔ w.re < z.re ∨ z.im ≠ w.im
Tactic: rw [le_def, not_and_or, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
rw : ¬(z.re ≤ w.re ∧ z.im = w.im) ↔ w.re < z.re ∨ z.im ≠ w.im
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
have rw₁ : ¬z.re ≤ w.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im
Tactic: rw [le_def, not_and_or, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im
have rw₂ : w.re < z.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im
Tactic: rw [le_def, not_and_or, not_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
have rw : ¬(z.re < w.re ∧ z.im = w.im) ↔ w.re ≤ z.re ∨ z.im ≠ w.im
Tactic: rw [lt_def, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z w : ℂ
rw : ¬(z.re < w.re ∧ z.im = w.im) ↔ w.re ≤ z.re ∨ z.im ≠ w.im
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
have rw₁ : ¬z.re < w.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im
Tactic: rw [lt_def, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
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
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im
have rw₂ : w.re ≤ z.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im
Tactic: rw [lt_def, not_and_or, not_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
⊢ z = (↑z.re : ℂ)
have rw : (↑z.re : ℂ) = z
Tactic: rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
rw : (↑z.re : ℂ) = z
⊢ z = (↑z.re : ℂ)
have rw₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
Tactic: rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
rw : (↑z.re : ℂ) = z
rw₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
⊢ z = (↑z.re : ℂ)
have rw₂ : z.im = 0
Tactic: rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
rw : (↑z.re : ℂ) = z
rw₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
rw₂ : z.im = 0
⊢ z = (↑z.re : ℂ)
have rw₃ : (↑r : ℂ).im = 0
Tactic: rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]