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

Goal state before:
pp: case refine_3
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x y : (i : ι) × E i), Sigma.dist x y = 0 → x = y

Tactic:
· rintro ⟨i, x⟩ ⟨j, y⟩
    rcases eq_or_ne i j with (rfl | hij)
    · simp [Sigma.dist]
    · intro h
      apply (lt_irrefl (1 : ℝ) _).elim
      calc
        1 ≤ Sigma.dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
        _ < 1 := by rw [h]; exact zero_lt_one

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ IsClopenable s

Tactic:
have : PolishSpace s := hs.polishSpace
  let t : Set α := sᶜ
  have : PolishSpace t := hs.isOpen_compl.polishSpace
  let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
  have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
    simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
      ← continuous_iff_coinduced_le]
    exact ⟨continuous_subtype_val, continuous_subtype_val⟩
  refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
  · rw [← f.induced_symm]
    exact f.symm.polishSpace_induced
  · rw [isOpen_coinduced, isOpen_sum_iff]
    simp [preimage_preimage, f, t]

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

Goal state before:
pp: case a
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)
⊢ ∀ i > 0, {p | dist p.1 p.2 < i} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}

Tactic:
intro ε

Goal state after:
case a
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)
ε : ℝ
⊢ ε > 0 → {p | dist p.1 p.2 < ε} ∈ ⨅ i, 𝓟 {a | a.1 i = a.2 i}
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ

Tactic:
by
  let i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
  let _ := i.toUniformSpace.toTopologicalSpace
  funext
  simp only [comp, toGlueL, toGlueR]
  refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)
  exact glueDist_glued_points Φ Ψ 0 _

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Tactic:
intro ε

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
⊢ ε > 0 → ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u 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 y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0

Tactic:
dif_pos A

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < Nat.find A
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B :
  (if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0) - 1 <
    if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0
⊢ (s ∩ cylinder x ((if h : ∃ n, Disjoint s (cylinder x n) then Nat.find h else 0) - 1)).Nonempty

Tactic:
dif_pos A

Goal state after:
case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
⊢ (s ∩ cylinder x (Nat.find A - 1)).Nonempty
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : x ∈ cylinder y (Nat.find A - 1)
⊢ y ∈ cylinder x (Nat.find A - 1)

Tactic:
rw [mem_cylinder_iff_eq] at hy ⊢

Goal state after:
case neg
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
x : (n : ℕ) → E n
hx : x ∉ s
A : ∃ n, Disjoint s (cylinder x n)
B : Nat.find A - 1 < Nat.find A
y : (n : ℕ) → E n
ys : y ∈ s
hy : cylinder x (Nat.find A - 1) = cylinder y (Nat.find A - 1)
⊢ cylinder y (Nat.find A - 1) = cylinder x (Nat.find A - 1)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case refine_1.h₁
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 : ((n : ℕ) → E n) → (n : ℕ) → E n := ⋯
fs : ∀ x ∈ s, f x = x
⊢ range f ⊆ s

Tactic:
rintro x ⟨y, rfl⟩
      by_cases hy : y ∈ s
      · rwa [fs y hy]
      simpa [f, if_neg hy] using! (inter_cylinder_longestPrefix_nonempty hs hne y).choose_spec.1

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
⊢ (dirac a) s = 1

Tactic:
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
  refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)
  rw [← dirac_apply' a MeasurableSet.univ]
  exact measure_mono (subset_univ s)

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ count s = ↑s.encard

Tactic:
simp [count, hs, ← tsum_subtype]

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

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

Tactic:
have hsm : MeasurableSet (toMeasurable μ s) := measurableSet_toMeasurable ..

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
μ : Measure α
inst✝ : SFinite μ
h : IsFiniteMeasure μ
g : ℕ → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hgle : ∀ (n : ℕ), g n ≤ ↑n
hgint : ∀ (n : ℕ), ∫⁻ (a : α), min (f a) ↑n ∂μ = ∫⁻ (a : α), g n a ∂μ
φ : α → ℝ≥0∞ := fun x ↦ ⨆ n, g n x
hφm : Measurable φ
hφle : φ ≤ f
s : Set α
ψ : SimpleFunc α ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
n : ℕ
hn : ∀ (x : α), ψ x ≤ ↑n
this : ∫⁻ (a : α) in (toMeasurable μ s)ᶜ, min (f a) ↑n ∂μ ≠ ∞
hsm : MeasurableSet (toMeasurable μ s)
⊢ ∫⁻ (a : α) in s, min (f a) ↑n ∂μ ≤ ∫⁻ (a : α) in s, g n a ∂μ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
⊢ ∀ (i : ℝ≥0∞), 0 < i → {p | edist p.1 p.2 < i} ∈ ⨅ i, ⨅ i_2, ⨅ (_ : 0 < i_2), 𝓟 {a | edist (a.1 i) (a.2 i) < i_2}

Tactic:
intro ε

Goal state after:
case left
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
⊢ 0 < ε → {p | edist p.1 p.2 < ε} ∈ ⨅ i, ⨅ i_1, ⨅ (_ : 0 < i_1), 𝓟 {a | edist (a.1 i) (a.2 i) < i_1}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
C : ℝ≥0∞
f : Set α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → f s ≤ C
h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)
⊢ f univ ≤ C

Tactic:
by
  let S := @spanningSets _ m (μ.trim hm) _
  have hS_mono : Monotone S := @monotone_spanningSets _ m (μ.trim hm) _
  have hS_meas : ∀ n, MeasurableSet[m] (S n) := @measurableSet_spanningSets _ m (μ.trim hm) _
  rw [← @iUnion_spanningSets _ m (μ.trim hm)]
  refine (h_F_lim S hS_meas hS_mono).trans ?_
  refine iSup_le fun n => hf (S n) (hS_meas n) ?_
  exact ((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne

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

Goal state before:
pp: case ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
⊢ ↑c ≠ ∞ ∨ L ≠ ∞

Tactic:
simp only [Ne, coe_ne_top, not_false_iff, true_or]

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

Goal state before:
pp: case const.refine_3.ht
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
s : Set α
hs : MeasurableSet s
L : ℝ≥0∞
hL : L < ↑c * μ s
c_ne_zero : c ≠ 0
this : L / ↑c < μ s
t : Set α
ht : MeasurableSet t
ts : t ⊆ s
mlt : L / ↑c < μ t
t_top : μ t < ∞
⊢ ↑c ≠ ∞ ∨ L ≠ ∞

Tactic:
simp only [Ne, coe_ne_top, not_false_iff, true_or]

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

Goal state before:
pp: case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
⊢ Pairwise (Disjoint on f) →
    (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
h_disj

Goal state after:
case refine_3
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
s : Set (α × β)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
⊢ (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst✝ : IsFiniteMeasure μ
h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
⊢ μ = ν

Tactic:
ext s hs
  have h_univ : μ univ = ν univ := by
    rw [← univ_prod_univ]
    exact h .univ .univ
  have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
  refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
    ?_ ?_ ?_ s hs
  · rintro - ⟨s, hs, t, ht, rfl⟩
    exact h hs ht
  · intro t ht h
    simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
  · intro f h_disj hf h_eq
    simp_rw [measure_iUnion h_disj hf, h_eq]

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

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ r < (comap f μ) (f ⁻¹' K)

Tactic:
hf.comap_apply,

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure β
pa qa : Set α → Prop
pb qb : Set β → Prop
H : μ.InnerRegularWRT pb qb
f : α → β
hf : MeasurableEmbedding f
hAB : ∀ (U : Set α), qa U → qb (f '' U)
hAB' : ∀ K ⊆ range f, pb K → pa (f ⁻¹' K)
U : Set α
hU : qa U
r : ℝ≥0∞
hr : r < μ (f '' U)
K : Set β
hKU : K ⊆ f '' U
hK : pb K
hμU : r < μ K
hKrange : K ⊆ range f
⊢ r < μ (f '' f ⁻¹' K)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_5
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
⊢ Pairwise (Disjoint on f) →
    (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)

Tactic:
h_disj

Goal state after:
case refine_5
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
h_disj : Pairwise (Disjoint on f)
⊢ (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), μ (f i) = ν (f i)) → μ (⋃ i, f i) = ν (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:

Tactic:
μ s ≤ μ U := μ.mono hsU
    _ < μ K + ε := hKr
    _ ≤ μ (K \ U') + μ U' + ε := by grw [tsub_le_iff_right.1 le_measure_sdiff]
    _ ≤ μ (K \ U') + ε + ε := by gcongr
    _ = μ (K \ U') + (ε + ε) := add_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 β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ (sfiniteSeq μ i.1) (s' ∩ s) * (sfiniteSeq ν i.2) (t' ∩ t) =
    (sfiniteSeq μ i.1) (s' ∩ s) * ((sfiniteSeq ν i.2).restrict t) t'

Tactic:
restrict_apply ht'

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ (sfiniteSeq μ i.1) (s' ∩ s) * (sfiniteSeq ν i.2) (t' ∩ t) = (sfiniteSeq μ i.1) (s' ∩ s) * (sfiniteSeq ν i.2) (t' ∩ t)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : DivisionMonoid G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun t ↦ g / t) μ μ

Tactic:
simp_rw [div_eq_mul_inv]
  exact (measurePreserving_mul_left μ g).comp (measurePreserving_inv μ)

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✝ : IsProbabilityMeasure μ
⊢ (μ.prod ν).snd = ν

Tactic:
by
  ext1 s hs
  rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 → μ' s_1 < ∞ → ν'.inv s_1 < ∞ → ∀ᵐ (x : G) ∂μ'.restrict s_1, ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞

Tactic:
intro A hA _ h3A

Goal state after:
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
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν'.inv A < ∞
⊢ ∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ μ (V ∩ A) ≠ ∞

Tactic:
exact ((measure_mono inter_subset_right).trans_lt h'A.lt_top).ne

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
μ.inv_inv

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ y ↔ x ≤ y ^ 2

Tactic:
rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re * z.re - z.im * z.im ∧ 0 = z.re * z.im + z.im * z.re ↔ z.im = 0

Tactic:
mul_comm z.im z.re,

Goal state after:
z : ℂ
⊢ 0 ≤ z.re * z.re - z.im * z.im ∧ 0 = z.re * z.im + z.re * z.im ↔ z.im = 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ z.re * z.re - z.im * z.im ≤ 0 ∧ z.re * z.im + z.im * z.re = 0 ↔ z.re = 0

Tactic:
mul_comm z.im z.re,

Goal state after:
z : ℂ
⊢ z.re * z.re - z.im * z.im ≤ 0 ∧ z.re * z.im + z.re * z.im = 0 ↔ z.re = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: r : ℝ
⊢ normSq ↑r = r * r

Tactic:
by
  simp [normSq, ofReal]

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
ι : Type u_5
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
v : V₁
⊢ (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

Tactic:
by simp only [coe_sum, Finset.sum_apply]

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

Goal state before:
pp: case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k‖₊ ^ 2 = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
hk,

Goal state after:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ (‖x‖₊ ^ 2 ^ k) ^ 2 = ‖x‖₊ ^ (2 * 2 ^ k)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z✝ z w : K
⊢ re (z * w) * re (z * w) + im (z * w) * im (z * w) = (re z * re z + im z * im z) * (re w * re w + im w * im w)

Tactic:
by
    simp only [mul_im, mul_re]
    ring

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ √(normSq z) = ‖z‖

Tactic:
rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝² : RCLike K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = n • ‖x‖

Tactic:
by
  simpa [Nat.cast_smul_eq_nsmul] using norm_smul (n : K) x

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ List.range 0 = []

Tactic:
List.range_zero

Goal state after:
n : ℕ
pn : NormNum.IsNat n 0
⊢ [] = []
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ / sInf (Norm.norm '' f '' s) * ‖f x‖

Tactic:
mul_comm_div

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hs : IsCompact s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x : α
hx : x ∈ s
⊢ ‖c‖ ≤ ‖c‖ * (‖f x‖ / sInf (Norm.norm '' f '' s))
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
⊢ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
intro ε

Goal state after:
a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
ε : ℝ
⊢ ε > 0 → ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.zero
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
hk,

Goal state after:
case inr.zero
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ abv (f (0 + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (0 + n.succ)