awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
⊢ (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
have h : ∀ (z : ℂ), Real.log ‖f z‖ = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
Tactic: funext z
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
⊢ Real.log ‖f z‖ = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have h : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
Tactic: rw [Complex.norm_def, Real.log_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
h : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
⊢ Real.log ‖f z‖ = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have h₁ : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (f z) : ℝ)
Tactic: rw [Complex.norm_def, Real.log_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₁ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₄ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₅ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₆ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
  1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) - HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₈ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₈ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₉ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₈ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₀ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₁₁ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₁₂ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z_1 : ℂ
h₁f : AnalyticAt ℂ f z_1
h₂f : f z_1 ≠ 0
z : ℂ
linarith : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₁ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → 2 / 2 = 1
linarith₃ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₅ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) → GT.gt (α := ℝ) 2 0
linarith₆ :
  Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 < 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) →
    1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) -
        HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) =
      0
linarith₇ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₈ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 2 1 = 2
linarith₁₀ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → 2 / 2 = 1
linarith₁₁ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ :
  2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 → GT.gt (α := ℝ) 2 0
⊢ Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 = 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z))
have linarith₁₃ : 2⁻¹ * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) < Real.log ((normSq : (a : ℂ) → ℝ) (f z)) / 2 →
  HMul.hMul (α := ℝ) 1 1 * (1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z))) - 1 * Real.log ((normSq : (a : ℂ) → ℝ) (f z)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (hypothesis)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
⊢ HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) z
have this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
Tactic: have : (Real.log ‖f ·‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
    funext z
    simp only [Pi.smul_apply, Function.comp_apply, smul_eq_mul]
    rw [Complex.norm_def, Real.log_sqrt]
    · linarith
    exact (f z).normSq_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
⊢ HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) z
have rw : HarmonicAt (HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)) z
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
⊢ HarmonicAt (HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)) z
have h : HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
Tactic: apply HarmonicAt.const_smul
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
have pos : ∀ (h₃f : f z ∈ slitPlane), HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
Tactic: by_cases h₃f : f z ∈ Complex.slitPlane
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
pos : ∀ (h₃f : f z ∈ slitPlane), HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
have neg : ∀ (h₃f : f z ∉ slitPlane), HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
Tactic: by_cases h₃f : f z ∈ Complex.slitPlane
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun (x : ℂ) ↦ Real.log ‖f x‖) = HSMul.hSMul (α := ℝ) 2⁻¹ (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f)
h₃f : f z ∉ slitPlane
⊢ HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ f) z
have neg : HarmonicAt (Real.log ∘ (⇑normSq : (a : ℂ) → ℝ) ∘ (-f)) z
Tactic: rw [(by aesop : Complex.normSq ∘ f = Complex.normSq ∘ (-f))]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f s
⊢ HarmonicContOnCl f s
have h₁ : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: rw [← hs.closure_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
⊢ ContinuousOn f (closedBall x r)
have inl : ∀ (h : HarmonicContOnCl f (ball x 0)), ContinuousOn f (closedBall x 0)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
inl : ∀ (h : HarmonicContOnCl f (ball x 0)), ContinuousOn f (closedBall x 0)
⊢ ContinuousOn f (closedBall x r)
have inr : ∀ (hr : r ≠ 0), ContinuousOn f (closedBall x r)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicContOnCl f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)
have inl : ContinuousOn f {x}
Tactic: rw [closedBall_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f : E → F
x : E
r : ℝ
h : HarmonicContOnCl f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)
have inr : ContinuousOn f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r))
Tactic: rw [← closure_ball x hr]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2
have rwa : ∀ (hij : ¬i = j),
  ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
    ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
Tactic: rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij
Cleared hypotheses: hij, v, h, hv1, hv2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
rwa :
  ∀ (hij : ¬i = j),
    ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
      ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2
have rwa₁ : ∀ (hij : ¬(i.1 = j.1 ∧ i.2 = j.2)),
  ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
    ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
Tactic: rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij
Cleared hypotheses: hij, v, h, hv1, hv2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
rwa :
  ∀ (hij : ¬i = j),
    ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
      ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
rwa₁ :
  ∀ (hij : ¬(i.1 = j.1 ∧ i.2 = j.2)),
    ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
      ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
⊢ i.1 ≠ j.1 ∨ i.2 ≠ j.2
have rwa₂ : ∀ (hij : ¬i.1 = j.1 ∨ ¬i.2 = j.2),
  ∀ v ∈ eigenspace A i.2 ⊓ eigenspace B i.1,
    ∀ (hv1 : v ∈ (↑(eigenspace A i.2) : Set E)) (hv2 : v ∈ (↑(eigenspace B i.1) : Set E)), i.1 ≠ j.1 ∨ i.2 ≠ j.2
Tactic: rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij
Cleared hypotheses: hij, v, h, hv1, hv2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
⊢ v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
have inl : ∀ (h₁ : i.1 ≠ j.1), v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
Tactic: obtain (h₁ | h₂) : i.1 ≠ j.1 ∨ i.2 ≠ j.2 := by rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.JointEigenspace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) A
hB : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) B
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
h : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ (↑(eigenspace A i.2) : Set E)
hv2 : v ∈ (↑(eigenspace B i.1) : Set E)
inl : ∀ (h₁ : i.1 ≠ j.1), v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
⊢ v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
have inr : ∀ (h₂ : i.2 ≠ j.2), v ∈ (eigenspace A j.2 ⊓ eigenspace B j.1)ᗮ
Tactic: obtain (h₁ | h₂) : i.1 ≠ j.1 ∨ i.2 ≠ j.2 := by rwa [Ne.eq_def, Prod.ext_iff, not_and_or] at hij