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

Goal state before:
pp: case inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist ⟨i, x⟩ ⟨i, z⟩ ≤ dist ⟨i, x⟩ ⟨j, y⟩ + dist ⟨j, y⟩ ⟨i, z⟩

Tactic:
simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]

Goal state after:
case inl.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist x z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h_nhds
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (a : (n : ℕ) → E n) (u : Set ((n : ℕ) → E n)),
    a ∈ u → IsOpen[Pi.topologicalSpace] u → ∃ v ∈ {s | ∃ x n, s = cylinder x n}, a ∈ v ∧ v ⊆ u

Tactic:
intro x u hx u_open
    obtain ⟨v, ⟨U, F, -, rfl⟩, xU, Uu⟩ :
        ∃ v ∈ { S : Set (∀ i : ℕ, E i) | ∃ (U : ∀ i : ℕ, Set (E i)) (F : Finset ℕ),
          (∀ i : ℕ, i ∈ F → U i ∈ { s : Set (E i) | IsOpen s }) ∧ S = (F : Set ℕ).pi U },
        x ∈ v ∧ v ⊆ u :=
      (isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx
        u_open
    rcases Finset.bddAbove F with ⟨n, hn⟩
    refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩
    intro y hy
    suffices ∀ i : ℕ, i ∈ F → y i ∈ U i by simpa
    intro i hi
    have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
    rw [this]
    simp only [Set.mem_pi, Finset.mem_coe] at xU
    exact xU i hi

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ map f' μa = μb

Tactic:
Measure.map_congr h.symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f f' : α → β
hf : MeasurePreserving f μa μb
hf' : Measurable f'
h : f =ᵐ[μa] f'
⊢ map f μa = μb
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
have hdiam : VanishingDiam D := by
    intro x
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hu
    · simp
    rw [eventually_atTop]
    refine ⟨1, fun m (hm : 1 ≤ m) => ?_⟩
    rw [Nat.one_le_iff_ne_zero] at hm
    rcases Nat.exists_eq_succ_of_ne_zero hm with ⟨n, rfl⟩
    dsimp
    cases x n
    · convert! (h0 _ _ _).2.2.2
      rw [PiNat.res_length]
    convert! (h1 _ _ _).2.2.2
    rw [PiNat.res_length]

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set ↑s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in s, f x ∂μ.restrict (Subtype.val '' t) = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ

Tactic:
restrict_restrict hs,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set ↑s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in s ∩ Subtype.val '' t, f x ∂μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε

Tactic:
have h₁ : (μ ⊓ ν) univ = 0 := le_bot_iff.1 (h (inf_le_left (b := ν)) inf_le_right) ▸ rfl

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : (μ ⊓ ν) univ = 0
⊢ ∃ s, μ s = 0 ∧ ν sᶜ ≤ 2 * ↑ε
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x ↦ c) μ) s = μ univ * s.indicator 1 c

Tactic:
Measure.map_apply measurable_const hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ μ ((fun x ↦ c) ⁻¹' s) = μ univ * s.indicator 1 c
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝¹] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
⊢ AnalyticSet (⋃ n, s n)

Tactic:
let F : γ → α := fun ⟨n, x⟩ ↦ f n x

Goal state after:
α : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous[hβ n, inst✝¹] (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type (max u_2 0) := (n : ι) × β n
F : γ → α :=
  fun x ↦
    match x with
    | ⟨n, x⟩ => f n x
⊢ AnalyticSet (⋃ n, s n)
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
⊢ ∀ ⦃f : ℕ → Set α⦄,
    (∀ (i : ℕ), MeasurableSet (f i)) →
      Pairwise (Function.onFun Disjoint f) →
        ∫⁻ (μ : Measure α), μ (⋃ i, f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), μ (f i) ∂m

Tactic:
intro f hf h
      simp_rw [measure_iUnion h hf]
      apply lintegral_tsum
      intro i; exact (measurable_coe (hf i)).aemeasurable

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂μ {i} • dirac i = ∑' (a : α), f a * μ {a}

Tactic:
congr 1 with a : 1

Goal state after:
case e_f
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂μ {a} • dirac a = f a * μ {a}
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst✝¹] U
⊢ μ U = 0 ↔ U = ∅

Tactic:
by
  simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using
    not_congr (hU.measure_pos_iff μ)

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hL : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ + ∫⁻ (x : α), ↑(f₂ x) ∂μ
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
simp only [hf₂, add_zero] at hL

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f₁ f₂ : α →ₛ ℝ≥0
a✝ : Disjoint (Function.support ⇑f₁) (Function.support ⇑f₂)
h₁ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₁ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₁ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
h₂ :
  ∀ {L : ℝ≥0∞},
    L < ∫⁻ (x : α), ↑(f₂ x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f₂ x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
L : ℝ≥0∞
hf₁ : ¬∫⁻ (x : α), ↑(f₁ x) ∂μ = 0
hf₂ : ∫⁻ (x : α), ↑(f₂ x) ∂μ = 0
hL : L < ∫⁻ (x : α), ↑(f₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν

Tactic:
refine Measurable.ennreal_induction (motive := fun f ↦ Measurable fun (x : α) ↦ ∫⁻ y, f (x, y) ∂ν)
    ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → Measurable fun x ↦ ∫⁻ (y : β), s.indicator (fun x ↦ c) (x, y) ∂ν

case refine_2
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (Measurable fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) →
            (Measurable fun x ↦ ∫⁻ (y : β), g (x, y) ∂ν) → Measurable fun x ↦ ∫⁻ (y : β), (f + g) (x, y) ∂ν

case refine_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
m : ∀ {α : Type ?u.42} {β : Type ?u.41} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), Measurable fun x ↦ ∫⁻ (y : β), f n (x, y) ∂ν) →
          Measurable fun x ↦ ∫⁻ (y : β), (fun x ↦ ⨆ n, f n x) (x, y) ∂ν
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ

Tactic:
refine ext_of_lintegral _ fun f hf ↦ ?_
  repeat rw [lintegral_mconv (by fun_prop)]
  refine lintegral_congr fun x ↦ ?_
  rw [lintegral_mconv (by fun_prop)]
  repeat refine lintegral_congr fun x ↦ ?_
  simp [mul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' S ×ˢ T) ∂μ = μ S * ν T

Tactic:
S,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ = μ (toMeasurable μ s) * ν T
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₁).2 * ((↑(hHT.equiv g₁).2)⁻¹ * (↑(hHT.equiv g₁).1)⁻¹)) ∈ H

Tactic:
mul_inv_cancel_left,

Goal state after:
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
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
T : Set G
inst✝ : H.FiniteIndex
h : IsComplement (↑H) T
⊢ T.encard = ↑H.index

Tactic:
← h.finite_right.cast_ncard_eq,

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
T : Set G
inst✝ : H.FiniteIndex
h : IsComplement (↑H) T
⊢ ↑T.ncard = ↑H.index
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 μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (map Prod.swap (ν.prod μ)) s = ∫⁻ (y : β), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂ν

Tactic:
map_apply measurable_swap hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (ν.prod μ) (Prod.swap ⁻¹' s) = ∫⁻ (y : β), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂ν
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K

Tactic:
have : μ F = ⨆ n, μ (F ∩ B n) := by
    rw [← Monotone.measure_iUnion, hBU]
    exact monotone_const.inter monotone_accumulate

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : MeasurableSpace X
μ : Measure X
F : Set X
hF : IsClosed[inst✝²] F
r : ℝ≥0∞
hr : r < μ F
B : ℕ → Set X := compactCovering X
hBc : ∀ (n : ℕ), IsCompact (F ∩ B n)
hBU : ⋃ n, F ∩ B n = F
this : μ F = ⨆ n, μ (F ∩ B n)
⊢ ∃ K ⊆ F, IsCompact K ∧ r < μ K
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✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
⊢ MeasurePreserving (fun z ↦ (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
convert!
    (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν) using 1
  ext1 ⟨x, y⟩
  simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]

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 g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ

Tactic:
rw [← lintegral_add_left' (hf.edist hh)]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g h : α → β
hf : AEStronglyMeasurable f μ
hh : AEStronglyMeasurable h μ
⊢ ∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) + edist (g a) (h a) ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ (x : α), Tendsto (fun n ↦ ‖F' n x‖ₑ) atTop (𝓝 ‖f' x‖ₑ) → (∀ (i : ℕ), ‖F' i x‖ₑ ≤ bound' x) → ‖f' x‖ₑ ≤ bound' x

Tactic:
intro a tendsto_norm h_bound

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
a : α
tendsto_norm : Tendsto (fun n ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ)
h_bound : ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
⊢ ‖f' a‖ₑ ≤ bound' a
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x ≠ 0 ↔ x ≠ 0

Tactic:
rw [not_iff_not, sqrt_eq_zero h]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), (f * i) a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
exact le_iSup₂_of_le (f * i) (f_meas.mul i_meas) <| le_iSup_of_le (by grw [hi]) le_rfl

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext <;> simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n = 0
⊢ n = 0

Tactic:
Nat.cast_eq_zero

Goal state after:
α : Type u_1
n : ℕ
h : n = 0
⊢ n = 0
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f g : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, g i ≤ 𝔼 i ∈ s, f i
⊢ ∃ x ∈ s, g x ≤ f x

Tactic:
obtain ⟨_, hx⟩ := hs
  contrapose! h
  exact expect_lt_expect (fun _ hx ↦ le_of_lt (h _ hx)) ⟨_, ⟨hx, h _ hx⟩⟩

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✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x ↦ x ^ 2) x ≤ (fun x ↦ x ^ 2) y

Tactic:
simpa only [sq] using mul_le_mul' h h

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : ↥(unitary R)
⊢ Commute u (star u)

Tactic:
simp [commute_iff_eq]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : ↥(unitary R)
⊢ Commute (star u) u

Tactic:
simp [commute_iff_eq]

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x✝ : α
⊢ x✝ • a • b₂ = (x✝ * a) • b₂

Tactic:
simp only [mul_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (r • z) = r * im z

Tactic:
rw [real_smul_eq_coe_mul, im_ofReal_mul]

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

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Tactic:
exact norm_sum_le s f

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(re (r • z)) - ↑(im (r • z)) * I = r • (↑(re z) - ↑(im z) * I)

Tactic:
smul_re,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(r * re z) - ↑(im (r • z)) * I = r • (↑(re z) - ↑(im z) * I)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: x : ℂ
⊢ x ∈ ℝ[I]

Tactic:
rw [← x.re_add_im, ← smul_eq_mul, ← Complex.coe_algebraMap]

Goal state after:
x : ℂ
⊢ (algebraMap ℝ ℂ) x.re + (algebraMap ℝ ℂ) x.im • I ∈ ℝ[I]
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ↑(ℜ ↑r) = ↑r

Tactic:
rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]

Goal state after:
r : ℝ
⊢ 2⁻¹ • 2 • ↑r = ↑r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖ = ↑q

Tactic:
rw [← ofReal_nnratCast]; exact norm_of_nonneg q.cast_nonneg

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / |‖z‖| ≤ 1

Tactic:
abs_norm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / |‖z‖| ≤ 1

Tactic:
abs_norm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / ‖z‖ ≤ 1
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst✝¹] (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen[inst✝] t

Tactic:
rw [← e.image_symm_image_of_subset_target hs]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst✝¹] (↑e.symm '' t)
hs' : ↑e.symm '' t ⊆ e.source
⊢ IsOpen[inst✝] (↑e.toPartialEquiv '' ↑e.symm '' t)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
simp_rw [pos_iff (K := K), ext_iff (K := K)]; aesop

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w

Tactic:
exact h.mul_im_ax

Goal state after: