awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hX₁ : AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
hY : AEStronglyMeasurable (m₀ := m𝓧) g (map X P)
⊢ cov[f ∘ X, g ∘ X; P] = cov[f, g; μ]
have hZ : AEMeasurable X P
Tactic: rw [← hX.map_eq, covariance_map]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable (m₀ := m𝓧) f (map X P)
have hX₁ : AEStronglyMeasurable f μ
Tactic: rw [hX.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEStronglyMeasurable (m₀ := m𝓧) g (map X P)
have hY : AEStronglyMeasurable g μ
Tactic: rw [hX.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
μ : Measure ℝ
X : Ω → ℝ
hX : HasLaw X μ P
⊢ Var[X; P] = Var[id; μ]
have rw : Var[X; P] = variance (mΩ := Real.measurableSpace) id (map X P)
Tactic: rw [← hX.map_eq, variance_map aemeasurable_id hX.aemeasurable, Function.id_comp]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
μ : Measure ℝ
X : Ω → ℝ
hX : HasLaw X μ P
rw : Var[X; P] = variance (mΩ := Real.measurableSpace) id (map X P)
⊢ Var[X; P] = Var[id; μ]
have rw₁ : Var[X; P] = Var[id ∘ X; P]
Tactic: rw [← hX.map_eq, variance_map aemeasurable_id hX.aemeasurable, Function.id_comp]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
μ : Measure ℝ
X : Ω → ℝ
hX : HasLaw X μ P
rw : Var[X; P] = variance (mΩ := Real.measurableSpace) id (map X P)
rw₁ : Var[X; P] = Var[id ∘ X; P]
⊢ Var[X; P] = Var[id; μ]
have rw₂ : Var[X; P] = Var[X; P]
Tactic: rw [← hX.map_eq, variance_map aemeasurable_id hX.aemeasurable, Function.id_comp]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ map (fun (ω : Ω) ↦ (X ω, Y ω)) P = μ.prod ν
have rw : Measure.prod (map X P) (map Y P) = μ.prod ν
Tactic: rw [h.map_prod_eq_prod_map_map (by fun_prop) (by fun_prop), hX.map_eq,
          hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
rw : Measure.prod (map X P) (map Y P) = μ.prod ν
⊢ map (fun (ω : Ω) ↦ (X ω, Y ω)) P = μ.prod ν
have rw₁ : μ.prod (map Y P) = μ.prod ν
Tactic: rw [h.map_prod_eq_prod_map_map (by fun_prop) (by fun_prop), hX.map_eq,
          hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
rw : Measure.prod (map X P) (map Y P) = μ.prod ν
rw₁ : μ.prod (map Y P) = μ.prod ν
⊢ map (fun (ω : Ω) ↦ (X ω, Y ω)) P = μ.prod ν
have rw₂ : μ.prod ν = μ.prod ν
Tactic: rw [h.map_prod_eq_prod_map_map (by fun_prop) (by fun_prop), hX.map_eq,
          hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ X ⟂ᵢ[P] Y
have rw : Eq (α := Measure (𝓧 × 𝓨)) (map (fun (ω : Ω) ↦ (X ω, Y ω)) P) (Measure.prod (map X P) (map Y P))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      h.map_eq, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
rw : Eq (α := Measure (𝓧 × 𝓨)) (map (fun (ω : Ω) ↦ (X ω, Y ω)) P) (Measure.prod (map X P) (map Y P))
⊢ X ⟂ᵢ[P] Y
have rw₁ : μ.prod ν = Measure.prod (map X P) (map Y P)
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      h.map_eq, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
rw : Eq (α := Measure (𝓧 × 𝓨)) (map (fun (ω : Ω) ↦ (X ω, Y ω)) P) (Measure.prod (map X P) (map Y P))
rw₁ : μ.prod ν = Measure.prod (map X P) (map Y P)
⊢ X ⟂ᵢ[P] Y
have rw₂ : μ.prod ν = μ.prod (map Y P)
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      h.map_eq, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun (ω : Ω) ↦ (X ω, Y ω)) (μ.prod ν) P
rw : Eq (α := Measure (𝓧 × 𝓨)) (map (fun (ω : Ω) ↦ (X ω, Y ω)) P) (Measure.prod (map X P) (map Y P))
rw₁ : μ.prod ν = Measure.prod (map X P) (map Y P)
rw₂ : μ.prod ν = μ.prod (map Y P)
⊢ X ⟂ᵢ[P] Y
have rw₃ : μ.prod ν = μ.prod ν
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      h.map_eq, hX.map_eq, hY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun (β := 𝓧) X P
⊢ map (fun (ω : Ω) (i : ι) ↦ X i ω) P = Measure.pi (α := 𝓧) μ
have rw : (Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P) = Measure.pi (α := 𝓧) μ
Tactic: rw [h.map_fun_eq_pi_map (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.HasLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (Measure.pi (α := 𝓧) μ) P
⊢ iIndepFun (β := 𝓧) X P
have rw : Measure.pi (α := 𝓧) μ = Measure.pi (α := 𝓧) fun (i : ι) ↦ map (X i) P
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map (by fun_prop), h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.HasLawExists (goal)
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∃ (Ω : Type (max u v)) (x : MeasurableSpace Ω) (P : Measure Ω) (X : (i : ι) → Ω → 𝓧 i),
    (∀ (i : ι), Measurable (X i)) ∧ (∀ (i : ι), HasLaw (X i) (μ i) P) ∧ iIndepFun (β := 𝓧) X P ∧ IsProbabilityMeasure P
have h : (∀ (i : ι),
    Measurable (α := (i : ι) → 𝓧 i) (β := 𝓧 i)
      ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i)) ∧
  (∀ (i : ι),
      HasLaw ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i) (μ i) (infinitePi (X := 𝓧) μ)) ∧
    iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ) ∧
      IsProbabilityMeasure (infinitePi (X := 𝓧) μ)
Tactic: use Π i, (𝓧 i), .pi, infinitePi μ, fun i ↦ Function.eval i
-- Lean 4 proof step from Mathlib.Probability.HasLawExists (goal)
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ (∀ (i : ι),
      Measurable (α := (i : ι) → 𝓧 i) (β := 𝓧 i)
        ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i)) ∧
    (∀ (i : ι),
        HasLaw ((fun (i : ι) ↦ (Function.eval (β := 𝓧) i : (f : (x : ι) → 𝓧 x) → 𝓧 i)) i) (μ i)
          (infinitePi (X := 𝓧) μ)) ∧
      iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ) ∧
        IsProbabilityMeasure (infinitePi (X := 𝓧) μ)
have h : iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
Tactic: refine ⟨by fun_prop, fun i ↦ MeasurePreserving.hasLaw (measurePreserving_eval_infinitePi _ _),
    ?_, by infer_instance⟩
-- Lean 4 proof step from Mathlib.Probability.HasLawExists (goal)
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ iIndepFun (β := 𝓧) (fun (i : ι) ↦ Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
have h : infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
Tactic: rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), map_id']
-- Lean 4 proof step from Mathlib.Probability.HasLawExists (goal)
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
have h : μ = fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.HasLawExists (goal)
Goal:
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ μ = fun (i : ι) ↦ map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
have h : ∀ (i : ι), μ i = map (Function.eval (β := 𝓧) i) (infinitePi (X := 𝓧) μ)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map f μ)
⊢ AEMeasurable (u ∘ g) ν
have hu₁ : AEMeasurable (_m := inst_2) u (Measure.map g ν)
Tactic: rw [h.map_eq] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
inst_3 : MeasurableSpace δ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
u : γ → δ
h : IdentDistrib f g μ ν
hu : AEMeasurable (_m := inst_2) u (Measure.map f μ)
⊢ Eq (α := Measure δ) (Measure.map (u ∘ f) μ) (Measure.map (u ∘ g) ν)
have rw : AEMeasurable (_m := inst_2) u (Measure.map g ν)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ←
        AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
s : Set γ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
    Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.map g ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
    Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
s : Set γ
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) (((Measure.map f μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (g ⁻¹' s) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) (((Measure.map g ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
  (((Measure.map g ν : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
    Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet.{u_3} (α := γ) {x : γ | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (x : β) ∂ν, p (g x)
have apply : ∀ᵐ (y : γ) ∂Measure.map g ν, p y
Tactic: apply (ae_map_iff h.aemeasurable_snd pmeas).1
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet.{u_3} (α := γ) {x : γ | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map g ν, p y
have rw : ∀ᵐ (y : γ) ∂Measure.map f μ, p y
Tactic: rw [← h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable g ν
have refine : ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
Tactic: refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
⊢ ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
have rcases : ∀ (t : Set γ) (t_sep : IsSeparable t) (ht : ∀ᵐ (x : α) ∂μ, f x ∈ t),
  ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
Tactic: rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
have refine : ∀ᵐ (x : β) ∂ν, g x ∈ closure[inst_3] t
Tactic: refine ⟨closure t, t_sep.closure, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : β) ∂ν, g x ∈ closure[inst_3] t
have apply : ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst_3] t
Tactic: apply h.ae_mem_snd isClosed_closure.measurableSet
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst_3] t
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ closure[inst_3] t) x} x}
    a
Tactic: filter_upwards [ht] with x hx using subset_closure hx
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : TopologicalSpace γ
inst_4 : PseudoMetrizableSpace γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ closure[inst_3] t) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst_3] t
have h₂ : ∀ (a : α), f a ∈ t → f a ∈ closure[inst_3] t
Tactic: filter_upwards [ht] with x hx using subset_closure hx
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : ConditionallyCompleteLinearOrder γ
inst_4 : TopologicalSpace γ
inst_5 : OpensMeasurableSpace γ
inst_6 : OrderClosedTopology γ
h : IdentDistrib f g μ ν
⊢ essSup f μ = essSup g ν
have I : ∀ (a : γ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) {x : β | a < g x} : ℝ≥0∞)
Tactic: have I : ∀ a, μ {x : α | a < f x} = ν {x : β | a < g x} := fun a =>
    h.measure_mem_eq measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : ConditionallyCompleteLinearOrder γ
inst_4 : TopologicalSpace γ
inst_5 : OpensMeasurableSpace γ
inst_6 : OrderClosedTopology γ
h : IdentDistrib f g μ ν
I :
  ∀ (a : γ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) {x : β | a < g x} : ℝ≥0∞)
⊢ essSup f μ = essSup g ν
have simp_rw : Eq.{u_3 + 1} (α := γ) (sInf {a : γ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
  (sInf {a : γ | Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) {x : β | a < g x} : ℝ≥0∞) (0 : ℝ≥0∞)})
Tactic: simp_rw [essSup_eq_sInf, I]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν
have change : ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
Tactic: change ∫⁻ x, id (f x) ∂μ = ∫⁻ x, id (g x) ∂ν
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
have rw : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (x : β), id (g x) ∂ν
Tactic: rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ←
    lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
rw : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (x : β), id (g x) ∂ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
have rw₁ : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν
Tactic: rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ←
    lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
rw : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (x : β), id (g x) ∂ν
rw₁ : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map f μ = ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
have rw₂ : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν = ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν
Tactic: rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ←
    lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
have pos : ∀ (hf : AEStronglyMeasurable f μ), Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.Probability.IdentDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst_3 : NormedAddCommGroup γ
inst_4 : NormedSpace ℝ γ
inst_5 : BorelSpace γ
h : IdentDistrib f g μ ν
pos : ∀ (hf : AEStronglyMeasurable f μ), Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
Tactic: by_cases hf : AEStronglyMeasurable f μ