mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
hnonempty : C.Nonempty
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Tactic:
by
  obtain ⟨y, yC⟩ := hnonempty
  obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
    have := hC.acc _ yC
    rw [accPt_iff_nhds] at this
    rcases this univ univ_mem with ⟨x, xC, hxy⟩
    exact ⟨x, xC.2, hxy⟩
  obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy
  use closure (U ∩ C), closure (V ∩ C)
  constructor <;> rw [← and_assoc]
  · refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
    rw [hC.closed.closure_subset_iff]
    exact inter_subset_right
  constructor
  · refine ⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩
    rw [hC.closed.closure_subset_iff]
    exact inter_subset_right
  apply Disjoint.mono _ _ hUV <;> apply closure_mono <;> exact inter_subset_left

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁴ : TopologicalSpace β
𝕜 : Type u_5
inst✝³ : TopologicalSpace 𝕜
inst✝² : Zero β
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
by
  refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩
  rw [SimpleFunc.coe_smul]
  exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

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

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
⊢ (CauchySeq fun s ↦ ∑ i ∈ s, f i) ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε

Tactic:
by
  rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
  · simp only [ball_zero_eq, Set.mem_ofPred_eq]
  · rintro s t hst ⟨s', hs'⟩
    exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ ε > 0, ∃ N, ∀ n ≥ N, Metric.ediam (A (res x n)) ≤ ε
⊢ ENNReal.ofReal (ε / 2) > 0

Tactic:
simp only [gt_iff_lt, ENNReal.ofReal_pos]; linarith

Goal state after:
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
C : ℝ
hC : ∀ (n : ℕ), 1 / infDist (↑(u n)) (↑s)ᶜ < C
Cpos : 0 < C
y : α
⊢ y ∈ s ↔ 0 < infDist y (↑s)ᶜ

Tactic:
rw [← s.isOpen.isClosed_compl.notMem_iff_infDist_pos ⟨x, xs⟩]; exact not_not.symm

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ firstDiff x y + 1 ≤ shortestPrefixDiff x s

pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s

Tactic:
· exact firstDiff_lt_shortestPrefixDiff hs hx hy

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
⊢ 1 ≤ shortestPrefixDiff x s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SFinite μa
⊢ SFinite μb

Tactic:
← hf.map_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
inst✝ : SFinite μa
⊢ SFinite (map f μa)
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
⊢ μa (f ⁻¹' s) = μb s

Tactic:
← hf.map_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = (map f μa) s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ μb s

Tactic:
← hf.map_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ (map f μa) s
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦
    hs.preimage (hf.iterate m).quasiMeasurePreserving

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol : μ univ < ↑n * μ s
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ (eapprox (f ∘ g) n) x = ((eapprox f n).comp g hg) x

Tactic:
simp only [eapprox_comp hf hg, coe_comp]

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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ μ hμν.nullSet = 0

Tactic:
hμν.measure_nullSet

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : {a | ¬p a} = ∅
x : α
⊢ p x

Tactic:
by_contra hx

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : {a | ¬p a} = ∅
x : α
hx : ¬p x
⊢ False
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous[w✝¹, inst✝²] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)

Tactic:
convert! this.analyticSet.image_of_continuous continuous_fst

Goal state after:
X : Type u_3
Y : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : PolishSpace X
inst✝ : T2Space Y
f : X → Y
hf : Continuous[inst✝³, inst✝²] f
Z : Type
w✝¹ : TopologicalSpace Z
w✝ : PolishSpace Z
g : Z → Y
hg : Continuous[w✝¹, inst✝²] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x | f x.1 = g x.2}
⊢ f ⁻¹' range g = Prod.fst '' {x | f x.1 = g x.2}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
⊢ ∫⁻ (a : α) in s, min (f a) ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ

Tactic:
have : ∫⁻ a in (toMeasurable μ s)ᶜ, min (f a) n ∂μ ≠ ∞ :=
        IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal _ ⟨n, fun _ ↦ min_le_right ..⟩ |>.ne
      have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..
      apply ENNReal.le_of_add_le_add_right this
      rw [← μ.restrict_toMeasurable_of_sFinite, lintegral_add_compl _ hsm, hgint,
        ← lintegral_add_compl _ hsm]
      gcongr with x
      exact le_min (hgf n x) (hgle n x)

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

Goal state before:
pp: M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ map (⇑L) (map (fun x ↦ x.1 * x.2) (μ.prod ν)) = map (fun x ↦ x.1 * x.2) ((map (⇑L) μ).prod (map (⇑L) ν))

Tactic:
rw [map_map (by fun_prop) (by fun_prop)]

Goal state after:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst✝⁵ : Monoid M
inst✝⁴ : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst✝³ : Monoid M'
inst✝² : MeasurableMul₂ M'
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : M →* M'
hL : Measurable ⇑L
⊢ map (⇑L ∘ fun x ↦ x.1 * x.2) (μ.prod ν) = map (fun x ↦ x.1 * x.2) ((map (⇑L) μ).prod (map (⇑L) ν))
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

Tactic:
specialize h hs ht hu

Goal state after:
case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)

Tactic:
specialize h hs ht hu

Goal state after:
case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
h : μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
⊢ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)

Tactic:
refine (prod_eq ?_).symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
⊢ ∀ (s : Set β) (t : Set α),
    MeasurableSet s →
      MeasurableSet t →
        (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) =
          (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ⇑f
⊢ Continuous f'

Tactic:
by
    rw [h]
    exact f.continuous_toFun

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

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (fun z ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
· refine AEMeasurable.comp_measurable ?_ measurable_swap
    convert! hf
    rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]

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
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
⊢ (map Inv.inv μ) s = 0

Tactic:
rw [map_apply measurable_inv hsm, inv_preimage]

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
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
⊢ μ s⁻¹ = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ μ K + ν K' ≤ μ (K ∪ K') + ν (K ∪ K')

Tactic:
gcongr <;> simp

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
⊢ (sum μ).InnerRegular

Tactic:
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.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null : a ∈ {x | f' x ≠ 0}ᶜ
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
have ha_null : f' a = 0 := Function.notMem_support.mp ha_null

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : f a = f' a
ha_null✝ : a ∈ {x | f' x ≠ 0}ᶜ
ha_null : f' a = 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ (fun n a ↦ f a * g n a) m x ≤ (fun n a ↦ f a * g n a) n x

Tactic:
dsimp; grw [h_mono_g hmn x]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ≥0
⊢ x * y ≤ max x y * max x y

Tactic:
gcongr <;> simp

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

Goal state before:
pp: z w : ℂ
⊢ √(normSq (z * w)) = √(normSq z) * √(normSq w)

Tactic:
normSq_mul,

Goal state after:
z w : ℂ
⊢ √(normSq z * normSq w) = √(normSq z) * √(normSq w)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
by
  simp only [HasFiniteIntegral]
  calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqConj f).lim.re = ((starRingEnd ℂ) f.lim).re

Tactic:
simp [cauSeqConj, (lim_re _).symm, cauSeqRe]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

Tactic:
ext <;> simp [mul_re, mul_im] <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

Tactic:
ext <;> simp [mul_re, mul_im] <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
convert! prod_subset_prod_iff
  exact reProdIm_subset_iff

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
have := dist_smul_pair r (f x) (f 0)

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : dist (r • f x) (r • f 0) ≤ dist r 0 * dist (f x) (f 0)
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
⊢ f (φ v) - g (φ v) = 0

Tactic:
sub_eq_zero,

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
⊢ f (φ v) = g (φ v)