-- 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)
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
refine h_int.congr' ?_ hsymm.restrict

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 ∘ 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)
⊢ AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici 0)))

Tactic:
exact h_map_neg ▸ hf.aestronglyMeasurable.restrict

Result:
no goals

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) μ
⊢ Integrable f μ

Tactic:
rw [← integrableOn_univ, ← Iic_union_Ici_of_le le_rfl, integrableOn_union]

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) μ
⊢ IntegrableOn f (Iic ?m.44211) μ ∧ IntegrableOn f (Ici ?m.44211) μ

α : 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) μ
⊢ α

α : 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) μ
⊢ α

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 ?m.44211) μ ∧ IntegrableOn f (Ici ?m.44211) μ

α : 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) μ
⊢ α

α : 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) μ
⊢ α

Tactic:
refine ⟨?_, h_int⟩

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) μ
⊢ IntegrableOn f (Iic 0) μ