mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ μ
      (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
        μ.sigmaFiniteSetWRT' ν) <
    ∞

Tactic:
refine (measure_mono Set.inter_subset_left).trans_lt ?_

Goal state after:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ μ
      (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1) <
    ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ i,
      (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ

Tactic:
rw [← Set.union_iUnion]

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ i,
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ i ≤ σ j ↔ j ≤ σ i

Tactic:
← symm_le_symm,

Goal state after:
i j : ↑I
⊢ σ (σ j) ≤ σ i ↔ j ≤ σ i
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ i ≤ j ↔ σ j ≤ i

Tactic:
← symm_le_symm,

Goal state after:
i j : ↑I
⊢ σ j ≤ σ (σ i) ↔ σ j ≤ i
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y : X
z : Y
⊢ ∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε

Tactic:
simpa only [abs_sub_comm]

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

Goal state before:
pp: ι : 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 + 0 + 0 + (0 + 0 + dist ⋯.some z)

Tactic:
by
          simpa only [zero_add, add_zero] using dist_triangle _ _ _

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

Goal state before:
pp: case h
β : 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)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε

Tactic:
← ENNReal.ofReal_lt_ofReal_iff ε_pos,

Goal state after:
case h
β : 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)) ≤ ε
n : ℕ
hn : ∀ n_1 ≥ n, Metric.ediam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ENNReal.ofReal (dist y z) < ENNReal.ofReal ε
Module: Mathlib.Topology.MetricSpace.Polish

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] (⇑f ∘ Sum.inl) ∧
    Continuous[instTopologicalSpaceSubtype, inst✝¹] (⇑f ∘ Sum.inr)

Tactic:
exact ⟨continuous_subtype_val, continuous_subtype_val⟩

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

Goal state before:
pp: case a.hU
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ i < n, x i = y i
⊢ (x, y) ∈ {p | dist p.1 p.2 < ε}

Tactic:
apply lt_of_le_of_lt _ hn

Goal state after:
E✝ : ℕ → Type u_1
inst✝² : (n : ℕ) → TopologicalSpace (E✝ n)
inst✝¹ : ∀ (n : ℕ), DiscreteTopology (E✝ n)
E : ℕ → Type u_2
inst✝ : (n : ℕ) → UniformSpace (E n)
h : ∀ (n : ℕ), uniformity (E n) = 𝓟 SetRel.id
this : ∀ (n : ℕ), DiscreteTopology (E n)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (1 / 2) ^ n < ε
x y : (n : ℕ) → E n
hxy : ∀ i < n, x i = y i
⊢ dist (x, y).1 (x, y).2 ≤ (1 / 2) ^ n
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 : (n : ℕ) → E n
hx : x ∉ s
hne : s.Nonempty
A : 0 < infDist x s
n : ℕ
hn : (1 / 2) ^ n < infDist x s
y : (n : ℕ) → E n
ys : y ∈ s
hy : y ∈ cylinder x n
⊢ dist x y ≤ (1 / 2) ^ n

Tactic:
rw [mem_cylinder_comm] at hy
      exact mem_cylinder_iff_dist_le.1 hy

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 < shortestPrefixDiff x s

Tactic:
have A := exists_disjoint_cylinder hs hx
  rw [shortestPrefixDiff, dif_pos A]
  classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)

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

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsν : ∀ (i : ι), ν (s i)ᶜ = 0
⊢ ν (⋂ i, s i)ᶜ = 0

Tactic:
· rwa [compl_iInter, measure_iUnion_null_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ μ (f '' univ) = 1

Tactic:
← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ f '' univ ∈ ae μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → 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 u_2 := ⋯
t : Set γ := ⋯
t_closed : IsClosed[Pi.topologicalSpace] t
this : PolishSpace ↑t
F : ↑t → α := ⋯
F_cont : Continuous[instTopologicalSpaceSubtype, inst✝²] F
⊢ ⋂ n, s n ⊆ range F

Tactic:
intro y hy
      have A : ∀ n, ∃ x : β n, f n x = y := by
        intro n
        rw [← mem_range, f_range n]
        exact mem_iInter.1 hy n
      choose x hx using A
      have xt : x ∈ t := by
        refine mem_iInter.2 fun n => ?_
        simp [γ, hx]
      refine ⟨⟨x, xt⟩, ?_⟩
      exact hx i₀

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
change s.Infinite at hs
    simp [hs, count_apply_infinite]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
change s.Infinite at hs
    simp [hs, count_apply_infinite]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ (dirac x) A = (dirac y) A

Tactic:
· have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true]
      simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A,
                 not_false_eq_true, indicator_of_notMem]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∫⁻ (x : α) in univ, f x ∂μ < ∞

Tactic:
refine setLIntegral_lt_top_of_le_nnreal (measure_ne_top _ _) ?_

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c
⊢ ∃ y, ∀ x ∈ univ, f 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 ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ (μ.prod ν) (Metric.closedBall x (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x r)

Tactic:
← closedBall_prod_same,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ (μ.prod ν) (Metric.closedBall x.1 (2 * r) ×ˢ Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x r)
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 ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ μ (Metric.closedBall x.1 (2 * r)) * ν (Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x r)

Tactic:
← closedBall_prod_same,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : MeasurableSpace β
inst✝⁸ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁷ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝⁶ : PseudoMetricSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : PseudoMetricSpace Y
inst✝³ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst✝² : SFinite ν
inst✝¹ : IsUnifLocDoublingMeasure μ
inst✝ : IsUnifLocDoublingMeasure ν
r : ℝ
hμr : ∀ (x : X), μ (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant μ) * μ (Metric.closedBall x r)
hνr : ∀ (x : Y), ν (Metric.closedBall x (2 * r)) ≤ ↑(doublingConstant ν) * ν (Metric.closedBall x r)
x : X × Y
⊢ μ (Metric.closedBall x.1 (2 * r)) * ν (Metric.closedBall x.2 (2 * r)) ≤
    ↑(doublingConstant μ * doublingConstant ν) * (μ.prod ν) (Metric.closedBall x.1 r ×ˢ Metric.closedBall x.2 r)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
h : (μ.prod ν) s = 0
⊢ (fun x ↦ ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
  rw [measure_prod_null mt] at ht
  rw [eventuallyLE_antisymm_iff]
  exact
    ⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht,
      Eventually.of_forall fun x => zero_le⟩

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 ν'
h1 : μ ≤ μ'
h2 : ν ≤ ν'
⊢ μ.prod ν ≤ μ'.prod ν'

Tactic:
by
  apply Measure.le_iff.2 (fun s hs ↦ ?_)
  calc μ.prod ν s
  _ ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hs
  _ ≤ ∫⁻ x, ν' (Prod.mk x ⁻¹' s) ∂μ' := by gcongr
  _ = (μ'.prod ν') s := (prod_apply hs).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ IsComplement S ↑H ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q

Tactic:
isComplement_iff_existsUnique_inv_mul_mem,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
⊢ (∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ ↑H) ↔ ∀ (q : G ⧸ H), ∃! s, ↑↑s = q
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < (c • μ) U
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K

Tactic:
smul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
H : μ.InnerRegularWRT p q
c : ℝ≥0∞
U : Set α
hU : q U
r : ℝ≥0∞
hr : r < c • μ U
⊢ ∃ K ⊆ U, p K ∧ r < (c • μ) K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g : G
⊢ RightCosetEquivalence (↑H) g ↑(hHT.equiv g).2

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

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > (x • μ) A
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r

Tactic:
smul_apply,

Goal state after:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
h0 : x ≠ 0
A : Set α
x✝ : MeasurableSet A
r : ℝ≥0∞
hr : r > x • μ A
⊢ ∃ U ⊇ A, IsOpen[inst✝¹] U ∧ (x • μ) U < r
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ f (m • x)) ⁻¹' S) = μ ((fun x ↦ m • x) ⁻¹' f ⁻¹' S)

Tactic:
rw [← preimage_preimage]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
n : ℕ
hn : r < (μ.restrict (s n)) F
⊢ ∃ K ⊆ F, p K ∧ r < μ K

Tactic:
rcases h n hF _ hn with ⟨K, KF, hKp, hK⟩

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
p : Set α → Prop
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet
hs : univ ⊆ ⋃ n, s n
hmono : Monotone s
F : Set α
hF : MeasurableSet F
r : ℝ≥0∞
hr : r < ⨆ n, μ (F ∩ s n)
hBU : ⋃ n, F ∩ s n = F
this : μ F = ⨆ n, μ (F ∩ s n)
n : ℕ
hn : r < (μ.restrict (s n)) F
K : Set α
KF : K ⊆ F
hKp : p K
hK : r < (μ.restrict (s n)) K
⊢ ∃ K ⊆ F, p K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ μ K = (μ.restrict (toMeasurable μ (s ∩ A))) K

Tactic:
rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
K : Set α
K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s
pK : p K
rK : r < μ K
⊢ μ K = μ (K ∩ toMeasurable μ (s ∩ A))
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 α
⊢ α ≃ᵐ (ℕ → Bool)

Tactic:
apply Nonempty.some
  let := upgradeStandardBorel α
  obtain ⟨f, -, fcts, finj⟩ :=
    isClosed_univ.exists_nat_bool_injection_of_not_countable (α := α)
      (by rwa [← countable_coe_iff, (Equiv.Set.univ _).countable_iff])
  obtain ⟨g, gmeas, ginj⟩ :=
    MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated α
  exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x

Tactic:
filter_upwards [hfg] with x h_le using fun _ ↦ h_le

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

Goal state before:
pp: case iSup
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f_1 n)) →
      Monotone f_1 →
        (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
          ∫⁻ (a : α), (fun x ↦ ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x ↦ ⨆ n, f_1 n x) a ∂μ

Tactic:
· intro g h_mea_g h_mono_g h_ind
    have : Monotone fun n a => f a * g n a := fun m n hmn x => by dsimp; grw [h_mono_g hmn x]
    simp [lintegral_iSup, ENNReal.mul_iSup, h_mf.fun_mul (h_mea_g _), *]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ x ∧ 0 ≤ x * x - x ↔ x = 0 ∨ 1 ≤ x

Tactic:
← mul_sub_one

Goal state after:
x : ℝ
⊢ 0 ≤ x ∧ 0 ≤ x * (x - 1) ↔ x = 0 ∨ 1 ≤ x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℂ
⊢ 1 ≤ normSq x ↔ 1 ≤ ‖x‖

Tactic:
← one_le_sq_iff₀ (norm_nonneg _),

Goal state after:
x : ℂ
⊢ 1 ≤ normSq x ↔ 1 ≤ ‖x‖ ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ edist z w = edist z.re w.re

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_im_eq h]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ → HasFiniteIntegral f μ

Tactic:
intro h
    simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ _q • _a₁ ≤ _q • _a₂

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ α
inst✝² : MulAction ℚ≥0 α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulMono ℚ α
_q : ℚ≥0
hq : 0 ≤ _q
_a₁ _a₂ : α
ha : _a₁ ≤ _a₂
⊢ ↑_q • _a₁ ≤ ↑_q • _a₂
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ _q • _a₁ < _q • _a₂

Tactic:
rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ ↑_q • _a₁ < ↑_q • _a₂
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
z : ℂ
⊢ (↑(normSq z)).re = ((starRingEnd ℂ) z * z).re

Tactic:
simp [normSq, mul_comm, ofReal]

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

Goal state before:
pp: case a
z : ℂ
⊢ (↑(normSq z)).im = ((starRingEnd ℂ) z * z).im

Tactic:
simp [normSq, mul_comm, ofReal]

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

Goal state before:
pp: n : ℕ
| I ^ n

Tactic:
← Nat.div_add_mod n 4

Goal state after:
n : ℕ
| I ^ (4 * (n / 4) + n % 4)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: n : ℕ
⊢ I ^ (4 * (n / 4) + n % 4) = I ^ (n % 4)

Tactic:
simp [pow_add, pow_mul, I_pow_four]

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
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e.symm '' S = ⇑e ⁻¹' S

Tactic:
rw [e.symm.image_eq_preimage_symm, e.symm_symm]

Goal state after: