mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n ↦ min 1 (c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
rw [norm_eq_zero] at hfx0
    rw [hfx0] at h_tendsto ⊢
    have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) := by
      convert! h_tendsto.norm
      rw [norm_zero]
    refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm
    calc
      ‖min 1 (c / ‖hf.approx n x‖) • hf.approx n x‖ =
          ‖min 1 (c / ‖hf.approx n x‖)‖ * ‖hf.approx n x‖ :=
        norm_smul _ _
      _ ≤ ‖(1 : ℝ)‖ * ‖hf.approx n x‖ := by
        gcongr
        rw [norm_one, Real.norm_of_nonneg]
        · exact min_le_left _ _
        · exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))
      _ = ‖hf.approx n x‖ := by rw [norm_one, one_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

Tactic:
erw [ENNReal.biSup_add] at this

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    ⨆ i ∈ fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x, (SimpleFunc.map ofNNReal i).lintegral μ + ε
⊢ ∃ φ,
    (∀ (x : α), ↑(φ x) ≤ f x) ∧
      ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε

case hs
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this :
  ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ) + ε
⊢ Set.Nonempty fun φ ↦ ∀ (x : α), ↑(φ x) ≤ f x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ f =ᵐ[μ] g

Tactic:
by
  have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + (n : ℝ≥0∞)⁻¹ := by
    intro n
    simp only [ae_iff, not_lt]
    have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
      (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
    rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
    exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))
  refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)
  suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from
    ge_of_tendsto' this fun i => (hlt i).le
  simpa only [inv_top, add_zero] using
    tendsto_const_nhds.add (tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
by
  simp_rw [← iInf_apply]
  let p : α → (ℕ → ℝ≥0∞) → Prop := fun _ f' => Antitone f'
  have hp : ∀ᵐ x ∂μ, p x fun i => f i x := h_anti
  have h_ae_seq_mono : Antitone (aeSeq h_meas p) := by
    intro n m hnm x
    by_cases hx : x ∈ aeSeqSet h_meas p
    · exact aeSeq.prop_of_mem_aeSeqSet h_meas hx hnm
    · simp only [aeSeq, hx, if_false]
      exact le_rfl
  rw [lintegral_congr_ae (aeSeq.iInf h_meas hp).symm]
  simp_rw [iInf_apply]
  rw [lintegral_iInf (aeSeq.measurable h_meas p) h_ae_seq_mono]
  · congr
    exact funext fun n ↦ lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp n)
  · rwa [lintegral_congr_ae (aeSeq.aeSeq_n_eq_fun_n_ae h_meas hp 0)]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ EqOn (fun x ↦ max (f x) (g x)) g {x | f x ≤ g x}

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ EqOn (fun x ↦ max (f x) (g x)) f {x | f x ≤ g x}ᶜ

Tactic:
exacts [fun x => max_eq_right (a := f x) (b := g x),
    fun x (hx : ¬ f x ≤ g x) => max_eq_left (not_le.1 hx).le]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case hfg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun a ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
a : α
⊢ φ a - f a ≤ g a

Tactic:
exact tsub_le_iff_left.2 <| hφ_le _

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∈ s
⊢ Function.extend Subtype.val (fun x ↦ f ↑x) (Function.extend Subtype.val (fun x ↦ f ↑x) fun x ↦ default) x = f x

Tactic:
lift x to s using hxs
    simp

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : x ∈ closure[inst✝¹] (U \ {x})
⊢ AccPt x (𝓟 U)

Tactic:
mem_closure_iff_clusterPt,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
U : Set α
hu : U.Nontrivial
x : α
hx : x ∈ U
h : ClusterPt x (𝓟 (U \ {x}))
⊢ AccPt x (𝓟 U)
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hg : ‖∑ i ∈ range n, g i - ∑ i ∈ range N, g i‖ < ε
hn : n ≥ N
⊢ ‖∑ i ∈ range n, f i - ∑ i ∈ range N, f i‖ < ε

Tactic:
← sum_Ico_eq_sub _ hn

Goal state after:
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg✝ : CauchySeq fun n ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hg : ‖∑ k ∈ Ico N n, g k‖ < ε
hn : n ≥ N
⊢ ‖∑ k ∈ Ico N n, f k‖ < ε
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
⊢ Measurable (uncurry u)

Tactic:
obtain ⟨t_sf, ht_sf⟩ :
    ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) := by
    have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
    refine ⟨h_str_meas.approx, fun j x => ?_⟩
    exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
  let U (n : ℕ) (p : ι × α) := u (t_sf n p.fst) p.snd
  have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) := by
    rw [tendsto_pi_nhds]
    exact fun p => ht_sf p.fst p.snd
  refine measurable_of_tendsto_metrizable (fun n => ?_) h_tendsto
  have h_meas : Measurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
    have :
      (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
        (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
      rfl
    rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
    exact measurable_from_prod_countable_left fun j => h j
  have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl
  simp_rw [U, this]
  refine h_meas.comp (Measurable.prodMk ?_ measurable_snd)
  exact ((t_sf n).measurable.comp measurable_fst).subtype_mk

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case inr.inl
x : { x // x ∈ I }
h₀ : 0 ≤ ↑x
h₁ : ↑x ≤ 1
⊢ ↑(σ (projIcc 0 1 ⋯ ↑x)) = ↑(projIcc 0 1 ⋯ ↑(σ x))

Tactic:
projIcc_val

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
⊢ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = inst✝¹

Tactic:
rw [DiscreteTopology.eq_bot (α := X)]
    refine eq_bot_of_singletons_open fun x ↦ ?_
    convert! @Metric.isOpen_ball _ _ x 1
    refine subset_antisymm (singleton_subset_iff.2 (Metric.mem_ball_self (by simp)))
      fun y hy ↦ ?_
    simp only [Metric.mem_ball, mem_singleton_iff] at *
    by_contra
    change (if y = x then 0 else 1) < 1 at hy
    simp_all

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (closure (eball x (ε / 2) ∩ C)) ≤ ε

Tactic:
Metric.ediam_closure

Goal state after:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (eball x (ε / 2) ∩ C) ≤ ε
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist (toInductiveLimit I n x) (toInductiveLimit I n y) = dist x y

Tactic:
by
    change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
    rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Disjoint (ae μ) (ae ν)

Tactic:
disjoint_iff_inf_le

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ae μ ⊓ ae ν ≤ ⊥
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
⊢ Disjoint μ ν

Tactic:
disjoint_iff_inf_le

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ sᶜ = 0
t : Set α
ht : ν tᶜ = 0
hst : Disjoint s t
⊢ μ ⊓ ν ≤ ⊥
Module: Mathlib.MeasureTheory.Measure.Dirac

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

Tactic:
restrict_eq_zero,

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a) s = 0
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:
restrict_eq_zero,

Goal state after:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a) s = 0
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
hne : s.Nonempty
⊢ ∃ f, (∀ (x : ↑s), f ↑x = x) ∧ Surjective f ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f

Tactic:
obtain ⟨f, fs, rfl, f_cont⟩ :
    ∃ f : (∀ n, E n) → ∀ n, E n, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f :=
    exists_retraction_of_isClosed hs hne

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
hs : IsClosed[Pi.topologicalSpace] (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
⊢ ∃ f_1,
    (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f_1
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ SFinite (μ.prod ν)

Tactic:
by
  have : μ.prod ν =
      Measure.sum (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) := by
    conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
    apply prod_sum
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
S : Set G
⊢ (∃ g, S = {g}) → IsComplement univ S

Tactic:
· rintro ⟨g, rfl⟩
    exact isComplement_univ_singleton

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
⊢ ∃ K ⊆ U, p K ∧ r < μ K

Tactic:
rcases H hqF _ hF with ⟨K, hKF, hpK, hrK⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q q' : Set α → Prop
H : μ.InnerRegularWRT p q
H' : μ.InnerRegularWRT q q'
U : Set α
hU : q' U
r : ℝ≥0∞
hr : r < μ U
F : Set α
hFU : F ⊆ U
hqF : q F
hF : r < μ F
K : Set α
hKF : K ⊆ F
hpK : p K
hrK : r < μ K
⊢ ∃ K ⊆ U, p K ∧ r < μ K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
⊢ LeftCosetEquivalence (↑K) g ↑(hSK.equiv g).1

Tactic:
by
  -- This used to be `simp [...]` before https://github.com/leanprover/lean4/pull/2644
  rw [equiv_fst_eq_mul_inv]; simp [LeftCosetEquivalence, leftCoset_eq_iff]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g : G
k : ↥K
⊢ LeftCosetEquivalence (↑K) (g * ↑k) g

Tactic:
by simp [LeftCosetEquivalence, leftCoset_eq_iff]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CocompactMap

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : ⇑f.symm '' K = ⇑f.toEquiv ⁻¹' K
⊢ IsCompact (⇑f ⁻¹' K)

Tactic:
simp only [coe_toEquiv] at this

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : ⇑f.symm '' K = ⇑f ⁻¹' K
⊢ IsCompact (⇑f ⁻¹' K)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
⊢ MeasurableSet (⋃ i, {x | ((fun n ↦ f n x) '' u i) ×ˢ ((fun n ↦ f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}})

Tactic:
refine MeasurableSet.iUnion fun N => ?_

Goal state after:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁶ : MeasurableSpace β
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : IsCompletelyPseudoMetrizableSpace γ
inst✝³ : SecondCountableTopology γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 ↦ f x_1 x) l ×ˢ map (fun x_1 ↦ f x_1 x) l).HasAntitoneBasis fun n ↦
      ((fun x_1 ↦ f x_1 x) '' u n) ×ˢ ((fun x_1 ↦ f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i ↦ True
N : ℕ
⊢ MeasurableSet {x | ((fun n ↦ f n x) '' u N) ×ˢ ((fun n ↦ f n x) '' u N) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
⊢ μ.InnerRegularWRT IsCompact IsClosed[inst✝²]

Tactic:
intro F hF r hr
  set B : ℕ → Set X := compactCovering X
  have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF
  have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
  have : μ F = ⨆ n, μ (F ∩ B n) := by
    rw [← Monotone.measure_iUnion, hBU]
    exact monotone_const.inter monotone_accumulate
  rw [this] at hr
  rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
  exact ⟨_, inter_subset_left, hBc n, hn⟩

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

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬Countable ↑univ

Tactic:
(Equiv.Set.univ _).countable_iff

Goal state after:
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ¬Countable α
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ HasFiniteIntegral X μ

Tactic:
by
  apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'
  filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)

Tactic:
rw [← ae_all_iff] at F_le_bound

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: r : ℝ
⊢ ‖↑r‖ = ‖r‖

Tactic:
by
  simp [norm_def, Real.sqrt_mul_self_eq_abs]

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

Goal state before:
pp: z : ℂ
hz : ¬z = 0
⊢ |z.im| ≤ ‖z‖

Tactic:
abs_im_le_norm

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
use g, hgm, hgf

Goal state after:
case right
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ μ.withDensity g = μ.withDensity f
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2

Tactic:
simp only [add_conj, ofReal_mul, ofReal_ofNat, mul_div_cancel_left₀ (z.re : ℂ) two_ne_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑↑(e₁.trans e₂)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0

Tactic:
ext <;> simp [smul_re, smul_im, zero_smul]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 c⁻¹)

Tactic:
convert! h.inv₀ hc using 1

Goal state after:
α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ (fun x ↦ f x / g x) = fun x ↦ (g x / f x)⁻¹
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : IsBigOWith c l k₁ k₂
h₂ : IsBigOWith c' l f' g'
⊢ IsBigOWith (c * c') l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_smul_le _ _)
  convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_smul, mul_mul_mul_comm]

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

Goal state before:
pp: x : ℂ
h : cexp x = 0
⊢ 0 = cexp 0

Tactic:
← add_neg_cancel x,

Goal state after:
x : ℂ
h : cexp x = 0
⊢ x + -x = cexp (x + -x)