-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant
    [IsMeasurablyGenerated (atTop (α := α))] [MeasurableNeg α] [μ.IsNegInvariant]
    (hf : LocallyIntegrable f μ) (hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg) (ho : f =O[atTop] g)
    (hg : IntegrableAtFilter g atTop μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici 0)))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ IntegrableOn f (Iic 0) μ

Tactic:
rw [IntegrableOn, ← h_map_neg, measurableEmbedding_neg.integrable_map_iff]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ IntegrableOn f (Iic 0) μ

Tactic:
have h_map_neg : (μ.restrict (Ici 0)).map Neg.neg = μ.restrict (Iic 0) := by
  conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
  simp

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ IntegrableOn f (Iic 0) μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)

Tactic:
conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁸ : TopologicalSpace α
inst✝⁷ : SecondCountableTopology α
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
⊢ Measure.map Neg.neg (μ.restrict (Ici 0)) = Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))

Tactic:
simp

Result:
no goals