awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
z z₁ z₂ : ℂ
hR : ¬R = 0
hz : ‖z‖ = 1
hz₁ : ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0
hz₂ : ‖z₂‖ = 1 ∧ z₂ + (↑R : ℂ)⁻¹ * (c - a) = 0
⊢ z₁ = z₂
have h : -((↑R : ℂ)⁻¹ * (c - a)) = z₂
Tactic: rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
z z₁ z₂ : ℂ
hR : ¬R = 0
hz : ‖z‖ = 1
hz₁ : ‖z₁‖ = 1 ∧ z₁ + (↑R : ℂ)⁻¹ * (c - a) = 0
hz₂ : ‖z₂‖ = 1 ∧ z₂ + (↑R : ℂ)⁻¹ * (c - a) = 0
h : -((↑R : ℂ)⁻¹ * (c - a)) = z₂
⊢ z₁ = z₂
have h₁ : -((↑R : ℂ)⁻¹ * (c - a)) = -((↑R : ℂ)⁻¹ * (c - a))
Tactic: rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖)
    fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
have this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
Tactic: have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |1|)) (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖)
    fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
have h : ∀ (z : ℂ) (hz : ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0),
  log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
Tactic: filter_upwards [this] with z hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
this : Membership.mem (γ := Filter ℂ) (codiscreteWithin (sphere 0 |1|)) {z : ℂ | ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0}
z : ℂ
hz : ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ ≠ 0
⊢ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
have h : log ‖(↑R : ℂ)‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖ = log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖
Tactic: rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
have rw : log ‖R‖ + circleAverage (fun (x : ℂ) ↦ log ‖x + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
Tactic: rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ log R + log⁺ (|R|⁻¹ * ‖c - a‖) = log R + log⁺ (R⁻¹ * ‖c - a‖)
have e_a : log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
have e_a : ∀ (h : R < 0), log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Tactic: rcases hR.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
e_a : ∀ (h : R < 0), log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
have e_a₁ : ∀ (h : 0 < R), log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Tactic: rcases hR.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
have e_a : log⁺ (R⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)
Tactic: rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)
have calc : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
  (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
Tactic: calc circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
calc :
  Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)
have calc₁ : Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
  (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)
Tactic: calc circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
calc :
  Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
calc₁ :
  Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)
have calc₂ : circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
Tactic: calc circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hR : R ≠ 0
calc :
  Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R)
    (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
calc₁ :
  Eq (α := ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖(↑R : ℂ) * (z + (↑R⁻¹ : ℂ) * (c - a))‖) 0 1)
    (circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1)
calc₂ : circleAverage (fun (z : ℂ) ↦ log ‖R‖ + log ‖z + (↑R⁻¹ : ℂ) * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)
have calc₃ : log R + log⁺ (|R|⁻¹ * ‖c - a‖) = log R + log⁺ (R⁻¹ * ‖c - a‖)
Tactic: calc circleAverage (log ‖· - a‖) c R
  _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by
    rw [circleAverage_eq_circleAverage_zero_one]
    congr
    ext z
    congr
    rw [Complex.ofReal_inv R]
    field [Complex.ofReal_ne_zero.mpr hR]
  _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by
    apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq,
        Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp
  _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by
    rw [← Pi.add_def, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1)
      (MeromorphicOn.circleIntegrable_log_norm (fun _ _ ↦ by fun_prop)), circleAverage_const]
    simp
  _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by
    congr 1
    rcases hR.lt_or_gt with h | h
    · simp [abs_of_neg h]
    · rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
have pos : ∀ (hR : R = 0), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
pos : ∀ (hR : R = 0), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
have neg : ∀ (hR : ¬R = 0), circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (goal)
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ circleAverage (fun (x : ℂ) ↦ log ‖x - a‖) c R = log R
have neg : |R|⁻¹ * ‖c - a‖ ≤ 1
Tactic: rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left,
    posLog_eq_zero_iff, abs_mul, abs_inv, abs_of_nonneg (norm_nonneg (c - a))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage (hypothesis)
Goal:
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1
have hu₁ : ‖c - a‖ ≤ |R|
Tactic: rw [mem_closedBall, dist_eq_norm'] at hu
Cleared hypotheses: hu, hR
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ≤ 1 + ‖x‖
have rw : 1 + HPow.hPow (β := ℕ) ‖x‖ 2 ≤ HPow.hPow (β := ℕ) (1 + ‖x‖) 2
Tactic: rw [sqrt_le_left (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
have rw : 1 + ‖x‖ ≤ √(2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2))
Tactic: rw [← sqrt_mul zero_le_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √(2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2))
have this : 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2
Tactic: have := sq_nonneg (‖x‖ - 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
this : 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2
⊢ 1 + ‖x‖ ≤ √(2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2))
have h : HPow.hPow (β := ℕ) (1 + ‖x‖) 2 ≤ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: apply le_sqrt_of_sq_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
x : E
this : 0 ≤ HPow.hPow (β := ℕ) (‖x‖ - 1) 2
⊢ HPow.hPow (β := ℕ) (1 + ‖x‖) 2 ≤ 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2)
have linarith : 2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) < HPow.hPow (β := ℕ) (1 + ‖x‖) 2 →
  0 - HPow.hPow (β := ℕ) (‖x‖ - 1) 2 + (2 * (1 + HPow.hPow (β := ℕ) ‖x‖ 2) - HPow.hPow (β := ℕ) (1 + ‖x‖) 2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹
have h : √2 ^ r ≠ 0
Tactic: rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
h : √2 ^ r ≠ 0
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹
have hx : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
h : √2 ^ r ≠ 0
hx : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹
have hx₁ : 0 ≤ √2
Tactic: rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
h : √2 ^ r ≠ 0
hx : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hx₁ : 0 ≤ √2
hy : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹
have hx₂ : LE.le (α := ℝ) 0 2
Tactic: rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
h : √2 ^ r ≠ 0
hx : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hx₁ : 0 ≤ √2
hy : 0 ≤ √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
hx₂ : LE.le (α := ℝ) 0 2
⊢ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2) =
    HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹
have hx₃ : 0 ≤ 1 + HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
        mul_inv_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ HPow.hPow (α := ℝ) 2 (r / 2) * ((√2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)) ^ r)⁻¹ ≤
    HPow.hPow (α := ℝ) 2 (r / 2) * ((1 + ‖x‖) ^ r)⁻¹
have hbc : 1 + ‖x‖ ≤ √2 * √(1 + HPow.hPow (β := ℕ) ‖x‖ 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ HPow.hPow (α := ℝ) 2 (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)
have hx : 0 ≤ 1 + ‖x‖
Tactic: rw [rpow_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
have rw : t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹
Tactic: rw [le_sub_iff_add_le', neg_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ Eq.{u_1 + 1} (α := Set E) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) ∅
have rw : t ^ (-r⁻¹) < 1
Tactic: rw [Metric.closedBall_eq_empty, sub_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ∞
have hr : 0 < r
Tactic: have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)
have h : 0 ≤ x ^ (-r⁻¹) - 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
h : 0 ≤ x ^ (-r⁻¹) - 1
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)
have h₁ : LE.le (α := ℝ) 0 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ 0 ≤ x ^ (-r⁻¹) - 1
have h : 1 ≤ x ^ (-r⁻¹)
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
have rw : ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)
Tactic: calc
      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
        gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp
      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
rw : ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n)
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
have rw₁ : ENNReal.ofReal ((x ^ (-r⁻¹) - 0) ^ n) = ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
Tactic: calc
      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
        gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp
      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ∞
have h_int : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
  ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
Tactic: have h_int x (hx : x ∈ Ioc (0 : ℝ) 1) := by
    calc
      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
        gcongr
        · rw [sub_nonneg]
          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
        · simp
      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ∞
have refine : ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ)))) < ∞
Tactic: refine lt_of_le_of_lt (setLIntegral_mono' measurableSet_Ioc h_int) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ)))) < ∞
have refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) (Ioc 0 1) volume
Tactic: refine IntegrableOn.setLIntegral_lt_top ?_