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

Goal state before:
pp: case refine_3
α : 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
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
x y : ℕ → Bool
⊢ (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) x = (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) y → x = y

Tactic:
hxy

Goal state after:
case refine_3
α : 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
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
x y : ℕ → Bool
hxy : (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) x = (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) y
⊢ x = y
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ count.real {a} = 1

Tactic:
rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
⊢ (c • m).bind f = c • m.bind f

Tactic:
by
  simp_rw [bind, Measure.map_smul, join_smul]

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

Goal state before:
pp: case left.hU
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ (x, y) ∈ {p | edist p.1 p.2 < ε}

Tactic:
calc
          edist x y = ∑' i : ι, min (2⁻¹ ^ encode i) (edist (x i) (y i)) := rfl
          _ = ∑ i ∈ K, min (2⁻¹ ^ encode i) (edist (x i) (y i)) +
                ∑' i : ↑(K : Set ι)ᶜ, min (2⁻¹ ^ encode (i : ι)) (edist (x i) (y i)) :=
            (ENNReal.sum_add_tsum_compl ..).symm
          _ ≤ ∑ i ∈ K, edist (x i) (y i) + ∑' i : ↑(K : Set ι)ᶜ, 2⁻¹ ^ encode (i : ι) := by
            gcongr
            · apply min_le_right
            · apply min_le_left
          _ < ∑ _i ∈ K, δ + ε / 2 := by
            refine ENNReal.add_lt_add_of_le_of_lt (by simpa using fun i hi ↦ (hxy i hi).ne_top) ?_
              hK
            gcongr with i hi
            exact (hxy i hi).le
          _ ≤ ε / 2 + ε / 2 := by gcongr; simpa [mul_comm] using hδ.le
          _ = ε := ENNReal.add_halves _

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

Goal state before:
pp: case neg
α : 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
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
rcases h₂ hL₂ with ⟨g₂, g₂_le, g₂_top, hg₂⟩

Goal state after:
case neg
α : 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
L₁ : ℝ≥0∞
hL₁ : L₁ < ∫⁻ (x : α), ↑(f₁ x) ∂μ
L₂ : ℝ≥0∞
hL₂ : L₂ < ∫⁻ (x : α), ↑(f₂ x) ∂μ
hL : L < L₁ + L₂
g₁ : α →ₛ ℝ≥0
g₁_le : ∀ (x : α), g₁ x ≤ f₁ x
g₁_top : ∫⁻ (x : α), ↑(g₁ x) ∂μ < ∞
hg₁ : L₁ < ∫⁻ (x : α), ↑(g₁ x) ∂μ
g₂ : α →ₛ ℝ≥0
g₂_le : ∀ (x : α), g₂ x ≤ f₂ x
g₂_top : ∫⁻ (x : α), ↑(g₂ x) ∂μ < ∞
hg₂ : L₂ < ∫⁻ (x : α), ↑(g₂ x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↑↑H''

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') = Nat.card ↥H''

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↑(⇑H.subtype '' S) = Nat.card ↑S

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ ↑(hST.equiv g).1 = g ↔ g ∈ S

Tactic:
constructor
  · intro h
    rw [← h]
    exact Subtype.prop _
  · intro h
    rw [hST.equiv_fst_eq_self_of_mem_of_one_mem h1 h]

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

Goal state before:
pp: case e_6
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν✝ : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
x : (α × β) × γ
⊢ x ∈ ⇑MeasurableEquiv.prodAssoc ⁻¹' s ×ˢ t ×ˢ u ↔ x ∈ (s ×ˢ t) ×ˢ u

Tactic:
simp [MeasurableEquiv.prodAssoc]

Goal state after:
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 : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) (s ×ˢ t) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
map_apply measurable_swap (hs.prod ht),

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 α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) (Prod.swap ⁻¹' s ×ˢ t) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
⊢ g x = g y → x = y

Tactic:
hxy

Goal state after:
case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : g x = g y
⊢ x = y
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 ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.fst

Tactic:
by
  rcases eq_zero_or_isProbabilityMeasure ρ with h | h
  · simp only [h, fst_zero]
    infer_instance
  · infer_instance

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

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U

Tactic:
simp only [le_iInf_iff]

Goal state after:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (i : Set α), K ⊆ i → IsOpen[inst✝⁴] i → μ K ≤ μ i
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
⊢ μ (s * closure[inst✝³] {1}) ≤ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t

Tactic:
simp only [le_iInf_iff]

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
μ : Measure G
⊢ ∀ (i : Set G), s ⊆ i → MeasurableSet i → μ (s * closure[inst✝³] {1}) ≤ μ i
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:
by
  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.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ✝ : Measure α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SigmaCompactSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
⊢ μ.Regular

Tactic:
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  exact ⟨(InnerRegularWRT.isCompact_isClosed μ).trans (InnerRegularWRT.of_pseudoMetrizableSpace μ)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ HasFiniteIntegral f μ

Tactic:
refine HasFiniteIntegral.mono hg ?_

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : AddLeftMono β
f g : α → β
hg : HasFiniteIntegral g μ
hnonneg : ∀ᵐ (a : α) ∂μ, 0 ≤ f a
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := ⋯
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := ⋯
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x

Tactic:
have Z := hg.ae_eq_mk

Goal state after:
case ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᵐ[μ.withDensity f'] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}, (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
simp [sqrt, Real.toNNReal_eq_zero.2 h]

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

Goal state before:
pp: case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩

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 : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) = b a

Tactic:
← two_mul

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 2 * ENNReal.ofReal (bound a) = b a
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal (bound a) + ENNReal.ofReal (bound a) = b a

Tactic:
rw [← two_mul]

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

Goal state before:
pp: z : ℂ
⊢ dist z ((starRingEnd ℂ) z) = 2 * |z.im|

Tactic:
rw [dist_comm, dist_conj_self]

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

Goal state before:
pp: x y : ℝ
⊢ x ≤ y → ↑x ≤ ↑y

Tactic:
hxy

Goal state after:
x y : ℝ
hxy : x ≤ y
⊢ ↑x ≤ ↑y
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case hf
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (Function.uncurry fun a x ↦ ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (a, a⁻¹ * x)) (μ.prod μ)

Tactic:
dsimp; fun_prop

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

Goal state before:
pp: case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
g : A →⋆* B
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
toMonoidHom✝¹ : A →* B
map_star'✝¹ : ∀ (a : A), (↑toMonoidHom✝¹).toFun (star a) = star ((↑toMonoidHom✝¹).toFun a)
toMonoidHom✝ : A →* B
map_star'✝ : ∀ (a : A), (↑toMonoidHom✝).toFun (star a) = star ((↑toMonoidHom✝).toFun a)
h :
  (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } =
    (fun f ↦ (↑f.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_star' := map_star'✝¹ } = { toMonoidHom := toMonoidHom✝, map_star' := map_star'✝ }
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
g : A ≃⋆* B
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h : { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun = g.toFun
⊢ { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun = g.invFun →
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
toMulEquiv✝¹ : A ≃* B
map_star'✝¹ : ∀ (a : A), toMulEquiv✝¹.toFun (star a) = star (toMulEquiv✝¹.toFun a)
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h :
  { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.toFun =
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun
⊢ { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.invFun =
      { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun →
    { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ } = { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk
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✝ g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h : { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ }.toFun =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }