mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝¹ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this✝ : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
this : range f = ⋂ n, F n
⊢ MeasurableSet (range f)

Tactic:
have E_meas : ∀ s : b, MeasurableSet (E s) := by
      intro b
      refine isClosed_closure.measurableSet.inter ?_
      refine MeasurableSet.iInter fun s => ?_
      exact MeasurableSet.iInter fun hs => (q_meas _).diff (q_meas _)
    have F_meas : ∀ n, MeasurableSet (F n) := by
      intro n
      refine MeasurableSet.iUnion fun s => ?_
      exact MeasurableSet.iUnion fun _ => E_meas _
    rw [this]
    exact MeasurableSet.iInter fun n => F_meas n

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
⊢ (map f μ).InnerRegularWRT pb qb

Tactic:
intro U hU r hr
  rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr
  rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
  refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩
  exact hK.trans_le (le_map_apply_image hf _)

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : (hSK.equiv g₁).1 = (hSK.equiv g₂).1
⊢ ↑((hSK.equiv g₁).2⁻¹ * (hSK.equiv g₂).2) ∈ K

Tactic:
exact Subtype.property _

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑((hHT.equiv g₂).1 * (hHT.equiv g₁).1⁻¹) ∈ H

Tactic:
exact Subtype.property _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > (comap f μ) A
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (comap f μ) U < r

Tactic:
f_me.comap_apply

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
⊢ ∃ U ⊇ A, IsOpen[inst✝²] U ∧ (comap f μ) U < r
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ (comap f μ) (f ⁻¹' U) < r

Tactic:
f_me.comap_apply

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ μ (f '' f ⁻¹' U) < r
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:

Tactic:
r < μ K := rK
  _ = μ.restrict (toMeasurable μ (s ∩ A)) K := by
    rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]
    congr
    apply (inter_eq_left.2 ?_).symm
    exact K_subs.trans inter_subset_left
  _ = μ.restrict (s ∩ A) K := by rwa [restrict_toMeasurable]
  _ ≤ μ.restrict A K := Measure.le_iff'.1 (restrict_mono inter_subset_right le_rfl) K

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (sum fun p ↦ (map f (sfiniteSeq μa p.1)).prod (map g (sfiniteSeq μc p.2))) =
    map (Prod.map f g) (sum fun p ↦ (sfiniteSeq μa p.1).prod (sfiniteSeq μc p.2))

Tactic:
map_sum (hf.prodMap hg).aemeasurable

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (sum fun p ↦ (map f (sfiniteSeq μa p.1)).prod (map g (sfiniteSeq μc p.2))) =
    sum fun i ↦ map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2))
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
| Measure.map (⇑f) μ

Tactic:
← map_mul_left_eq_self μ g

Goal state after:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : Mul G
μ : Measure G
inst✝⁴ : MeasurableMul G
H : Type u_3
inst✝³ : MeasurableSpace H
inst✝² : Mul H
inst✝¹ : MeasurableMul H
inst✝ : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable ⇑f
h_surj : Surjective ⇑f
g : G
| Measure.map (⇑f) (Measure.map (fun x ↦ g * x) μ)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun x ↦ x * g⁻¹) μ μ

Tactic:
measurePreserving_mul_right μ g⁻¹

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
⊢ Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 (∑' (i : ι), (μ i) s))

Tactic:
exact ENNReal.summable.hasSum

Goal state after:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
| μ

Tactic:
← map_mul_left_eq_self μ g

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map (fun x ↦ g * x⁻¹) μ
| map (fun x ↦ g * x) μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
⊢ (sum μ).InnerRegular

Tactic:
by
  constructor
  intro s hs r hr
  have : Tendsto (fun (a : Finset ι) ↦ ∑ i ∈ a, μ i s) atTop (𝓝 (Measure.sum μ s)) := by
    simp only [hs, Measure.sum_apply]
    exact ENNReal.summable.hasSum
  obtain ⟨a, ha⟩ : ∃ (a : Finset ι), r < (∑ i ∈ a, μ i) s := by
    simp only [coe_finsetSum, Finset.sum_apply]
    exact ((tendsto_order.1 this).1 r hr).exists
  rcases MeasurableSet.exists_lt_isCompact hs ha with ⟨K, Ks, hK, h'K⟩
  refine ⟨K, Ks, hK, h'K.trans_le ?_⟩
  simp only [coe_finsetSum, Finset.sum_apply]
  exact (ENNReal.sum_le_tsum _).trans (le_sum_apply _ _)

Goal state after:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

Tactic:
wlog sm : MeasurableSet s generalizing s

Goal state after:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
this : ∀ {s : Set G}, μ' s ≠ ∞ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
sm : ¬MeasurableSet s
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ μ (⇑F ⁻¹' K) < ∞

Tactic:
exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK

Goal state after:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
hμs : μ' s ≠ ∞
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

Tactic:
wlog sm : MeasurableSet s generalizing s
  · filter_upwards [this ((measure_toMeasurable _).trans_ne hμs) (measurableSet_toMeasurable ..)]
      with x hx using lt_of_le_of_lt (by gcongr; apply subset_toMeasurable) hx
  refine ae_of_forall_measure_lt_top_ae_restrict' ν'.inv _ ?_
  intro A hA _ h3A
  simp only [ν'.inv_apply] at h3A
  apply ae_lt_top (measurable_measure_mul_right ν' sm)
  have h1 := measure_mul_lintegral_eq μ' ν' sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
  rw [lintegral_indicator hA.inv] at h1
  simp_rw [Pi.one_apply, setLIntegral_one, ← image_inv_eq_inv, indicator_image inv_injective,
    image_inv_eq_inv, ← indicator_mul_right _ fun x => ν' ((· * x) ⁻¹' s), Function.comp,
    Pi.one_apply, mul_one] at h1
  rw [← lintegral_indicator hA, ← h1]
  finiteness

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ (μ.withDensity f) s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0

Tactic:
constructor
  · intro hs
    let t := toMeasurable (μ.withDensity f) s
    apply measure_mono_null (inter_subset_inter_right _ (subset_toMeasurable (μ.withDensity f) s))
    have A : μ.withDensity f t = 0 := by rw [measure_toMeasurable, hs]
    rw [withDensity_apply f (measurableSet_toMeasurable _ s),
      lintegral_eq_zero_iff' (AEMeasurable.restrict hf),
      EventuallyEq, ae_restrict_iff'₀, ae_iff] at A
    swap
    · simp only [measurableSet_toMeasurable, MeasurableSet.nullMeasurableSet]
    simp only [Pi.zero_apply] at A
    convert! A using 2
    ext x
    simp only [and_comm, exists_prop, mem_inter_iff, mem_ofPred_eq,
      not_forall]
  · intro hs
    let t := toMeasurable μ ({ x | f x ≠ 0 } ∩ s)
    have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_ofPred_eq, or_true]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩
    apply measure_mono_null A (measure_union_null _ _)
    · apply withDensity_absolutelyContinuous
      rwa [measure_toMeasurable]
    rcases hf with ⟨g, hg, hfg⟩
    have t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0} := by
      apply withDensity_absolutelyContinuous
      filter_upwards [hfg] with a ha
      rw [eq_iff_iff]
      exact ⟨fun h ↦ by rw [h] at ha; exact ha.symm,
             fun h ↦ by rw [h] at ha; exact ha⟩
    rw [measure_congr t, withDensity_congr_ae hfg]
    have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)
    rw [withDensity_apply _ M, lintegral_eq_zero_iff hg]
    filter_upwards [ae_restrict_mem M]
    simp only [imp_self, Pi.zero_apply, imp_true_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
all_goals fun_prop (disch := intro _ hs; simp [hs])

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ g z.2) * φ) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

Tactic:
all_goals fun_prop (disch := intro _ hs; simp [hs])

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

pp: case hg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

Tactic:
all_goals fun_prop (disch := intro _ hs; simp [hs])

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'

Tactic:
by
  refine ⟨|C| + 1, ?_, ?_⟩
  · linarith [abs_nonneg C]
  · apply h.mono
    linarith [le_abs_self C]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

Tactic:
rcases le_total ‖x.fst‖ ‖x.snd‖ with (h | h)

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.1‖ ≤ ‖x.2‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

case inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.2‖ ≤ ‖x.1‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ ≤ 1

Tactic:
suffices ‖e‖ * (‖e‖ - 1) = 0 by grind [sub_eq_zero]

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ * (‖e‖ - 1) = 0
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
rw [isEmbedding_iff]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (e.source.domRestrict ↑e.toPartialEquiv) ∧ Injective (e.source.domRestrict ↑e.toPartialEquiv)
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace X'
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Y'
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace Z'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding ((InjOn.toPartialEquiv f univ ⋯).source.domRestrict ↑(InjOn.toPartialEquiv f univ ⋯))

Tactic:
simpa! [domRestrict_eq] using h.comp subtypeVal

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ (fun n ↦ f (-n)) =O[cofinite] fun n ↦ g (-n)

Tactic:
← Equiv.neg_apply

Goal state after:
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ (fun n ↦ f ((Equiv.neg ℤ) n)) =O[cofinite] fun n ↦ g ((Equiv.neg ℤ) n)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
by
  refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
  · simp only [isLittleO_iff] at h
    have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left
    apply le_of_tendsto_of_tendsto tendsto_const_nhds this
    apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))
    exact eventually_principal.1 (h hc) x hx
  · apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
    exact fun x hx ↦ (h x hx).symm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : (fun _x ↦ c) =O[l] f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith C l (fun _x ↦ c) f'
⊢ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩

Goal state after:
case mp
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
h : (fun _x ↦ c) =O[l] f'
C : ℝ
hC₀ : C > 0
hC : IsBigOWith C l (fun _x ↦ c) f'
⊢ ∀ᶠ (x : α) in l, ‖c‖ / C ≤ ‖f' x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝

Tactic:
simp [exp_add, add_mul, pow_add, exp_neg, exp_nat_mul]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case pos
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp [hf] at hx

Goal state after:
case pos
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : f x = 0
hx : C ≤ 0
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
x₀ : E'
m : ℕ
h : 1 < m
⊢ (fun x ↦ ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x ↦ x - x₀

Tactic:
simpa only [isLittleO_norm_right, pow_one] using isLittleO_pow_sub_pow_sub x₀ h

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tan (-x) = -tan x

Tactic:
by simp [tan, neg_div]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ (√(1 + tan x ^ 2))⁻¹ = cos x

Tactic:
by
  rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
expNear_succ,

Goal state after:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear n x (1 + x / (↑n + 1) * a₂) - expNear n x a₁| ≤
    |x| ^ n / ↑n.factorial * b₁
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑(x / 2) * I)) * (cexp (↑(x / 2 + -(x / 2)) * I) - cexp (↑(x / 2 + x / 2) * I)) * I‖

Tactic:
rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re

Tactic:
exp_eq_exp_re_mul_sin_add_cos,

Goal state after:
z : ℂ
⊢ ‖cexp ↑z.re * (cos ↑z.im + sin ↑z.im * I)‖ = Real.exp z.re