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

Goal state before:
pp: case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
⊢ v.Countable

pp: case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
⊢ ∀ a ∈ v, (a ∩ C).Countable

Tactic:
· exact bct.mono (sep_subset _ _)

Goal state after:
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
⊢ ∀ a ∈ v, (a ∩ C).Countable
Module: Mathlib.Analysis.Normed.Group.FunctionSeries

Goal state before:
pp: β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
ε : ℝ
εpos : ε > 0
t : Finset ι
ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x // x ∉ b }), u ↑a < ε
N : Set ι
hN : N ∈ cofinite
HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y
n : Finset ι
hn : Finite.toFinset hN ∪ t ⊆ n
x : β
hx : x ∈ s
A : Summable fun n ↦ ‖f n x‖
i : ι
hi : i ∉ n
this : i ∉ Finite.toFinset hN
⊢ i ∈ N

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
⊢ ∃ m, ∀ n ≥ m, ↑(addNSMul h δ n) = b

Tactic:
refine ⟨m, fun n hn ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
a b : α
h : a ≤ b
δ : α
inst✝ : Archimedean α
hδ : 0 < δ
m : ℕ
hm : b - a ≤ m • δ
n : ℕ
hn : n ≥ m
⊢ ↑(addNSMul h δ n) = b
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (firstDiff x y) ≠ y (firstDiff x y)

Tactic:
firstDiff_def,

Goal state after:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (if h : x ≠ y then Nat.find ⋯ else 0) ≠ y (if h : x ≠ y then Nat.find ⋯ else 0)
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
ht : ¬↑t = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

Tactic:
· have : (1 - s * t : ℝ) ≠ 0 := by
        intro h
        have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
        grind
      field_simp
      ring_nf

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : ¬x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : x = y
h✝¹ : ¬x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : ¬x = z
h✝ : y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y z : X
h✝² : ¬x = y
h✝¹ : ¬x = z
h✝ : ¬y = z
⊢ (if x = z then 0 else 1) ≤ (if x = y then 0 else 1) + if y = z then 0 else 1

Tactic:
simp_all

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

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
refine ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ Filter.map (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)
hsY : s ∈ Filter.map (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)
εX : ℝ
εX0 : εX > 0
hX : ∀ ⦃a b : X⦄, dist a b < εX → (a, b) ∈ (fun p ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < εY → (a, b) ∈ (fun p ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s
⊢ ∀ (a b : X ⊕ Y), Sum.dist a b < min (min εX εY) 1 → (a, b) ∈ s
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ 0 ≤ (↑y - ↑x) / (↑z - ↑x)

Tactic:
simp_all

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
x y : X
this : ¬y = x
hy : (if y = x then 0 else 1) < 1
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case pos
a b : ℝ
x y z : ↑(Icc a b)
hxy : x ≤ y
hyz : y ≤ z
h : ↑z - ↑x = 0
⊢ (↑y - ↑x) / (↑z - ↑x) ≤ 1

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
m : MetricSpace X :=
  { dist := fun x y ↦ if x = y then 0 else 1, dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯, edist_dist := ⋯,
    uniformity_dist := ⋯, cobounded_sets := ⋯, eq_of_dist_eq_zero := ⋯ }
u : ℕ → X
hu : ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
N n : ℕ
hn : n ≥ N
this : ¬u n = u N
hN : (if u n = u N then 0 else 1) < 1
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: case refine_2
α : 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
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[instTopologicalSpaceSum] (⇑f ⁻¹' s)

Tactic:
isOpen_sum_iff

Goal state after:
case refine_2
α : 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
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen[instTopologicalSpaceSubtype] (Sum.inl ⁻¹' ⇑f ⁻¹' s) ∧
    IsOpen[instTopologicalSpaceSubtype] (Sum.inr ⁻¹' ⇑f ⁻¹' s)
Module: Mathlib.Topology.Separation.CountableSeparatingOn

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : T0Space ↑s
inst✝ : SecondCountableTopology ↑s
x : ↑s
x✝¹ : x ∈ univ
y : ↑s
x✝ : y ∈ univ
h : ∀ s_1 ∈ countableBasis ↑s, x ∈ s_1 ↔ y ∈ s_1
⊢ x = y

Tactic:
exact ((isBasis_countableBasis _).inseparable_iff.2 h).eq

Goal state after:
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:
mem_cylinder_iff_eq

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.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (a : α), μ {a} = ν {a}
⊢ ∀ s ∈ range singleton, μ.restrict s = ν.restrict s

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
⊢ count ≠ 0

Tactic:
simp [count]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
⊢ map f count ≤ count

Tactic:
refine le_intro fun s hs _ ↦ ?_
  rw [map_apply h2f hs, count_apply (hs.preimage h2f), count_apply hs, ← hf.encard_image]
  have := image_preimage_subset f s
  gcongr

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

Goal state before:
pp: case refine_3
ι : Type u_2
inst✝¹ : Countable ι
α : Type u_3
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
m : ι
⊢ MeasurableSet (⋂ n, u m n)

Tactic:
exact MeasurableSet.iInter fun n => hu m n

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ count {i | ε ≤ a i} ≤ c / ε

Tactic:
apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ∞
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
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, ∀ (x : α), ψ x ≤ ↑n

Tactic:
rcases ψ.range.bddAbove with ⟨C, hC⟩

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
C : ℝ≥0
hC : C ∈ upperBounds ↑ψ.range
⊢ ∃ n, ∀ (x : α), ψ x ≤ ↑n
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)
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_mono : Monotone S
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
n : ℕ
⊢ μ (S n) ≠ ∞

Tactic:
exact ((le_trim hm).trans_lt (@measure_spanningSets_lt_top _ m (μ.trim hm) _ n)).ne

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

Goal state before:
pp: case inl
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ = ∅
⊢ ∃ n, C ∈ comap (distDenseSeq X n) (𝓝 (distDenseSeq X n x))

Tactic:
simp_all

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

Goal state before:
pp: X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : dist y (denseSeq X n) < ε / 2
⊢ ε / 2 + ε / 2 ≤ infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)

Tactic:
simp [ε]

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

Goal state before:
pp: 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 (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ∫⁻ (y : β), (Prod.mk x ⁻¹' s).indicator ((fun x ↦ c) ∘ Prod.mk x) y ∂ν

Tactic:
suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator (m hs)]

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 (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ c * ν (Prod.mk x ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : μ U ≠ ∞
hε : ε ≠ 0
⊢ ∃ K ⊆ U, p K ∧ μ U < μ K + ε

Tactic:
by
  rcases eq_or_ne (μ U) 0 with h₀ | h₀
  · refine ⟨∅, empty_subset _, h0, ?_⟩
    rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
  · rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩
    exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ IsComplement (range f) ↑H

Tactic:
rw [isComplement_subgroup_right_iff_bijective]
  refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩
  rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
  exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

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

Goal state before:
pp: γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := ⋯
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := ⋯
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := ⋯
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := ⋯
y : γ
n : ℕ
⊢ ball y (u n / 2) ∈ 𝓝 y

Tactic:
exact ball_mem_nhds _ (half_pos (u_pos n))

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : μ.OuterRegular
x : ℝ≥0∞
hx : x ≠ ∞
⊢ (x • μ).OuterRegular

Tactic:
by
  rcases eq_or_ne x 0 with (rfl | h0)
  · rw [zero_smul]
    exact OuterRegular.zero
  · refine ⟨fun A _ r hr => ?_⟩
    rw [smul_apply, A.measure_eq_iInf_isOpen, smul_eq_mul] at hr
    simpa only [ENNReal.mul_iInf_of_ne h0 hx, gt_iff_lt, iInf_lt_iff, exists_prop] using! hr

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) K ∧ r < μ K

Tactic:
have : μ s = ⨆ n, μ (s ∩ B n) := by
    rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ n, s ∩ B n = s
this : μ s = ⨆ n, μ (s ∩ B n)
⊢ ∃ K ⊆ s, (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞) 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 μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s (Filter.map Inv.inv (ae μ)) ↔ EventuallyConst s (ae μ)

Tactic:
Filter.map_inv,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s (ae μ)⁻¹ ↔ EventuallyConst s (ae μ)
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
⊢ f ⋆ₘₗ[μ] g = g ⋆ₘₗ[μ] f

Tactic:
ext x
  simp only [mlconvolution_def]
  rw [← lintegral_mul_left_eq_self _ x, ← lintegral_inv_eq_self]
  simp [mul_comm]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : CommSemigroup G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun x ↦ x * g) μ = μ

Tactic:
by simp_rw [mul_comm, map_mul_left_eq_self]

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hν : ν' = 0
⊢ 0 s = 0

Tactic:
Pi.zero_apply

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hν : ν' = 0
⊢ 0 = 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ √(y * y) = y

Tactic:
sqrt_mul_self hy

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
⊢ y = y
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
by
  rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y

Tactic:
simp_rw [Real.sqrt, ← NNReal.coe_mul, NNReal.coe_inj, Real.toNNReal_mul hx, NNReal.sqrt_mul]

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)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)

Tactic:
rw [← ENNReal.ofReal_zero]

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)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 (ENNReal.ofReal 0))
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
h : z.im = 0
⊢ 0 ≤ z.re ^ 2 - z.im ^ 2 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
simpa [h] using sq_nonneg z.re

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

Goal state before:
pp: 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'✝ }

Tactic:
simp_all

Goal state after: