awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.IdentDistrib
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 rwa rwa₁ rwa₂ rwa₃ : AEMeasurable (_m := inst_2) u (Measure.map f μ)
⊢ AEMeasurable (_m := inst_2) u (Measure.map g ν)

Tactic:
rwa [← h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
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 : Measurable u
⊢ IdentDistrib (u ∘ f) (u ∘ g) μ ν

Tactic:
h.comp_of_aemeasurable hu.aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.comp_of_aemeasurable
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
μ : Measure α
f g : α → γ
hf : AEMeasurable f μ
heq : f =ᶠ[ae μ] g
⊢ IdentDistrib f g μ μ

Tactic:
{ aemeasurable_fst := hf
    aemeasurable_snd := hf.congr heq
    map_eq := Measure.map_congr heq }

Premises used: AEMeasurable.congr, MeasureTheory.Measure.map_congr, ProbabilityTheory.IdentDistrib.mk
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → γ
hf : AEMeasurable f μ
⊢ IdentDistrib f (AEMeasurable.mk f hf) μ μ

Tactic:
IdentDistrib.of_ae_eq hf hf.ae_eq_mk

Premises used: ProbabilityTheory.IdentDistrib.of_ae_eq, AEMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
μ : Measure α
f : α → γ
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
inst_4 : BorelSpace γ
hf : AEStronglyMeasurable f μ
⊢ IdentDistrib f (AEStronglyMeasurable.mk f hf) μ μ

Tactic:
IdentDistrib.of_ae_eq hf.aemeasurable hf.ae_eq_mk

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.IdentDistrib.of_ae_eq, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.Probability.IdentDistrib
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∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) (((Measure.map g ν : 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∞)

Tactic:
rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
    Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, MeasureTheory.Measure.map_apply_of_aemeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
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)
apply : ∀ᵐ (y : γ) ∂Measure.map g ν, p y
⊢ ∀ᵐ (x : β) ∂ν, p (g x)

Tactic:
apply (ae_map_iff h.aemeasurable_snd pmeas).1

Premises used: MeasureTheory.ae_map_iff, Iff.mp, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistrib
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)
rw : ∀ᵐ (y : γ) ∂Measure.map f μ, p y
⊢ ∀ᵐ (y : γ) ∂Measure.map g ν, p y

Tactic:
rw [← h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
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 f μ, p y

Tactic:
(ae_map_iff h.aemeasurable_fst pmeas).2 hp

Premises used: Iff.mpr, MeasureTheory.ae_map_iff, ProbabilityTheory.IdentDistrib.aemeasurable_fst
-- Module: Mathlib.Probability.IdentDistrib
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 f μ, p y

Tactic:
exact (ae_map_iff h.aemeasurable_fst pmeas).2 hp

Premises used: Iff.mpr, MeasureTheory.ae_map_iff, ProbabilityTheory.IdentDistrib.aemeasurable_fst
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
t : Set γ
tmeas : MeasurableSet t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : β) ∂ν, g x ∈ t

Tactic:
h.ae_snd tmeas ht

Premises used: ProbabilityTheory.IdentDistrib.ae_snd
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
κ : Measure γ
h₀ : HasLaw f κ μ
h₁ : HasLaw g κ ν
⊢ Eq (α := Measure γ) (Measure.map f μ) (Measure.map g ν)

Tactic:
simp [h₀.map_eq, h₁.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
κ : Measure γ
h₀ : IdentDistrib f g μ ν
h₁ : HasLaw f κ μ
⊢ Measure.map g ν = κ

Tactic:
simp [h₀.map_eq, ← h₁.map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.IdentDistrib
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 : OpensMeasurableSpace γ
inst_6 : SecondCountableTopology γ
h : IdentDistrib f g μ ν
⊢ AEStronglyMeasurable f μ

Tactic:
h.aemeasurable_fst.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, ProbabilityTheory.IdentDistrib.aemeasurable_fst
-- Module: Mathlib.Probability.IdentDistrib
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 ν

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, ?_⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistrib
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 μ
refine : ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
⊢ AEStronglyMeasurable g ν

Tactic:
refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨h.aemeasurable_snd, ?_⟩

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro, ProbabilityTheory.IdentDistrib.aemeasurable_snd
-- Module: Mathlib.Probability.IdentDistrib
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 μ
rcases :
  ∀ (t : Set γ) (t_sep : IsSeparable t) (ht : ∀ᵐ (x : α) ∂μ, f x ∈ t),
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t
⊢ ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t

Tactic:
rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩

Premises used: aestronglyMeasurable_iff_aemeasurable_separable, And.right, Iff.mp
-- Module: Mathlib.Probability.IdentDistrib
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

Tactic:
⟨closure t, t_sep.closure, ?_⟩

Premises used: TopologicalSpace.IsSeparable.closure, closure, And.intro, Exists.intro
-- Module: Mathlib.Probability.IdentDistrib
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
refine : ∀ᵐ (x : β) ∂ν, g x ∈ closure[inst_3] t
⊢ ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : β) ∂ν, g x ∈ t

Tactic:
refine ⟨closure t, t_sep.closure, ?_⟩
-- Module: Mathlib.Probability.IdentDistrib
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
apply : ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst_3] t
⊢ ∀ᵐ (x : β) ∂ν, g x ∈ closure[inst_3] t

Tactic:
apply h.ae_mem_snd isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, ProbabilityTheory.IdentDistrib.ae_mem_snd, isClosed_closure
-- Module: Mathlib.Probability.IdentDistrib
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 : α
hx : f x ∈ t
⊢ f x ∈ closure[inst_3] t

Tactic:
subset_closure hx

Premises used: subset_closure
-- Module: Mathlib.Probability.IdentDistrib
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
h₂ h₃ : ∀ (x : α) (hx : f x ∈ t), f x ∈ closure[inst_3] t
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[inst_3] t

Tactic:
filter_upwards [ht] with x hx using subset_closure hx
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
⊢ AEStronglyMeasurable f μ ↔ AEStronglyMeasurable g ν

Tactic:
⟨fun hf => h.aestronglyMeasurable_snd hf, fun hg => h.symm.aestronglyMeasurable_snd hg⟩

Premises used: ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd, Iff.intro
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
⊢ ∀ (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
-- Module: Mathlib.Probability.IdentDistrib
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∞)
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∞)})
⊢ essSup f μ = essSup g ν

Tactic:
simp_rw [essSup_eq_sInf, I]

Premises used: essSup_eq_sInf
-- Module: Mathlib.Probability.IdentDistrib
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
change : ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν

Tactic:
change ∫⁻ x, id (f x) ∂μ = ∫⁻ x, id (g x) ∂ν
-- Module: Mathlib.Probability.IdentDistrib
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 ν
rw₂ rw₃ : ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν = ∫⁻ (a : ℝ≥0∞), id a ∂Measure.map g ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν

Tactic:
rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ←
    lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.IdentDistrib.aemeasurable_snd, aemeasurable_id, ProbabilityTheory.IdentDistrib.map_eq, MeasureTheory.lintegral_map'
-- Module: Mathlib.Probability.IdentDistrib
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 ∂ν)
neg : ∀ (hf : ¬AEStronglyMeasurable f μ), Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)

Tactic:
by_cases hf : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
rw :
  AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
⊢ AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)

Tactic:
rw [aestronglyMeasurable_iff_aemeasurable_separable]

Premises used: aestronglyMeasurable_iff_aemeasurable_separable
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
rcases :
  ∀ (t : Set γ) (t_sep : IsSeparable t) (ht : ∀ᵐ (x : α) ∂μ, f x ∈ t),
    AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
      ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t
⊢ AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t

Tactic:
rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩

Premises used: aestronglyMeasurable_iff_aemeasurable_separable, And.right, Iff.mp
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t

Tactic:
⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩

Premises used: TopologicalSpace.IsSeparable.closure, closure, And.intro, Exists.intro, aemeasurable_id
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
refine : ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ AEMeasurable (_m := inst_2) id (Measure.map f μ) ∧
    ∃ (t : Set γ), IsSeparable t ∧ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ t

Tactic:
refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
rw : ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
rw₁ : MeasurableSet.{u_3} (α := γ) {x : γ | id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t}
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rw [ae_map_iff h.aemeasurable_fst]

Premises used: MeasureTheory.ae_map_iff, ProbabilityTheory.IdentDistrib.aemeasurable_fst
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
x : α
hx : f x ∈ t
⊢ id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
subset_closure hx

Premises used: subset_closure
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
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 : α) ↦ id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) x} x}
      a
h₂ h₃ : ∀ (x : α) (hx : f x ∈ t), id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
filter_upwards [ht] with x hx using subset_closure hx
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ MeasurableSet.{u_3} (α := γ) {x : γ | id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t}

Tactic:
isClosed_closure.measurableSet

Premises used: Set.Mem, setOf, IsClosed.measurableSet, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ MeasurableSet.{u_3} (α := γ) {x : γ | id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t}

Tactic:
exact isClosed_closure.measurableSet

Premises used: IsClosed.measurableSet, isClosed_closure
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)

Tactic:
have A : AEStronglyMeasurable id (Measure.map f μ) := by
      rw [aestronglyMeasurable_iff_aemeasurable_separable]
      rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 hf).2 with ⟨t, t_sep, ht⟩
      refine ⟨aemeasurable_id, ⟨closure t, t_sep.closure, ?_⟩⟩
      rw [ae_map_iff h.aemeasurable_fst]
      · filter_upwards [ht] with x hx using subset_closure hx
      · exact isClosed_closure.measurableSet
-- Module: Mathlib.Probability.IdentDistrib
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 μ ν
hf : AEStronglyMeasurable f μ
A : AEStronglyMeasurable (m₀ := inst_2) id (Measure.map f μ)
pos : Eq.{u_3 + 1} (α := γ) (∫ (x : α), id (f x) ∂μ) (∫ (x : β), id (g x) ∂ν)
⊢ Eq.{u_3 + 1} (α := γ) (∫ (x : α), f x ∂μ) (∫ (x : β), g x ∂ν)

Tactic:
change ∫ x, id (f x) ∂μ = ∫ x, id (g x) ∂ν