awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg : ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₁ : ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₂ : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
    (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₃ : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₄ : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
    (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₅ : (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
    (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
neg₅ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₆ : (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
    ‖c‖ ≤
  c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
neg₅ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
    c
neg₆ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      ‖c‖ ≤
    c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₇ : 1 * ‖c‖ ≤ c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
neg₅ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
    c
neg₆ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      ‖c‖ ≤
    c
neg₇ : 1 * ‖c‖ ≤ c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₈ : ‖c‖ ≤ c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
neg₅ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
    c
neg₆ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      ‖c‖ ≤
    c
neg₇ : 1 * ‖c‖ ≤ c
neg₈ : ‖c‖ ≤ c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg₉ : c ≤ c
Tactic: rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
have inl : ∀ (hα : IsEmpty α), StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
inl : ∀ (hα : IsEmpty α), StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
have inr : ∀ (hα : Nonempty α), StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
have inr : ∀ (hf : StronglyMeasurable f), ∃ (c : β), f = fun (x : α) ↦ c
Tactic: refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
inr : ∀ (hf : StronglyMeasurable f), ∃ (c : β), f = fun (x : α) ↦ c
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
have inr₁ : ∀ (hf_eq : ∃ (c : β), f = fun (x : α) ↦ c), StronglyMeasurable f
Tactic: refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ (c : β), f = fun (x : α) ↦ c
have inr : f = fun (x : α) ↦ f hα.some
Tactic: refine ⟨f hα.some, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
⊢ f = fun (x : α) ↦ f hα.some
have h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ f = fun (x : α) ↦ f hα.some
have this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
Tactic: have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
⊢ f = fun (x : α) ↦ f hα.some
have h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
Tactic: have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
| ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have h : ∀ (x : α) (n : ℕ), ((fs n : (a : α) → β) x : β)
Tactic: enter [x, 1, n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
x : α
n : ℕ
| ((fs n : (a : α) → β) x : β)
have h : (fun (x : α) ↦ cs n) x
Tactic: rw [h_cs_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
| ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have h : ∀ (x : α) (n : ℕ), (fun (x : α) ↦ cs n) x
Tactic: enter [x, 1, n]; rw [h_cs_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
⊢ f = fun (x : α) ↦ f hα.some
have h_fs_tendsto₁ : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
Tactic: conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
Cleared hypotheses: h_fs_tendsto, h_cs_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
⊢ f = fun (x : α) ↦ f hα.some
have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
Tactic: have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
⊢ f = fun (x : α) ↦ f hα.some
have inr : ∀ (x : α), f x = f hα.some
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf_eq : ∃ (c : β), f = fun (x : α) ↦ c
⊢ StronglyMeasurable f
have inr : ∀ (c : β), StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c
Tactic: obtain ⟨c, rfl⟩ := hf_eq
Cleared hypotheses: f, hf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
⊢ FinStronglyMeasurable f μ
have hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
Tactic: have hS_meas : ∀ n, MeasurableSet (S n) := measurableSet_spanningSets (μ.restrict t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
n : ℕ
x : α
hxt : x ∉ t
⊢ Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
have rw : Eq.{u_2 + 1} (α := β) ((S n ∩ t).indicator (⇑(f_approx n) : (a : α) → β) x) 0
Tactic: rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]