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

Goal state before:
pp: case inr.inr
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 ↦ ⋯.some) (fun x ↦ ⋯.some) 1 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.UnitInterval

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀
ht : ∀ (i : ι), ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = t i
⊢ ∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ i, t i

Tactic:
choose u hcomp hcount hut using ht
  obtain rfl : t = fun i ↦ (u i).toTopologicalSpace := (funext hut).symm
  refine ⟨⨅ i, u i, .iInf hcomp ht₀, ?_, UniformSpace.toTopologicalSpace_iInf⟩
  rw [iInf_uniformity]
  infer_instance

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

Goal state before:
pp: case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
hxy : dist x x = 0
⊢ x = x

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ι : Sort u_1
c : ι → Set ↑I
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : univ ⊆ ⋃ i, c i
⊢ ∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Tactic:
simp_rw [← Subtype.coe_inj]
  exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

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

Goal state before:
pp: case inl
E : ℕ → Type u_1
x : (n : ℕ) → E n
n i : ℕ
hi : i ≤ n
h : dist x x < (1 / 2) ^ n
⊢ x i = x i

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
n : ℕ
⊢ 1 / infDist (↑(u n)) (↑s)ᶜ < (1 / 2) ^ 0 + 1 / infDist (↑(u 0)) (↑s)ᶜ

Tactic:
rw [← sub_lt_iff_lt_add]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Opens α
inst✝ : CompleteSpace α
u : ℕ → s.CompleteCopy
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (1 / 2) ^ N
A : CauchySeq fun n ↦ ↑(u n)
x : α
xlim : Tendsto (fun n ↦ ↑(u n)) atTop (𝓝 x)
xs : x ∉ s
n : ℕ
⊢ 1 / infDist (↑(u n)) (↑s)ᶜ - 1 / infDist (↑(u 0)) (↑s)ᶜ < (1 / 2) ^ 0
Module: Mathlib.Topology.MetricSpace.Gluing

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

Tactic:
rintro ⟨i, x⟩
    simp [Sigma.dist]

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

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x : X 0
hx : ⟨0, x⟩.fst ≤ 0
y : X 0
hy : ⟨0, y⟩.fst ≤ 0
⊢ inductiveLimitDist f ⟨0, x⟩ ⟨0, y⟩ =
    dist (leRecOn hx (fun {k} ↦ f k) ⟨0, x⟩.snd) (leRecOn hy (fun {k} ↦ f k) ⟨0, y⟩.snd)

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ max x.fst y.fst
hy : y.fst ≤ max x.fst y.fst
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} ↦ f k) x.snd) (leRecOn hy (fun {k} ↦ f k) y.snd)

Tactic:
rfl

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)
this : CauchySeq u
⊢ x ∈ (inducedMap A).fst

Tactic:
obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this

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)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ x ∈ (inducedMap A).fst
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case h1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n, x⟩.fst ≤ n

Tactic:
rfl

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

Goal state before:
pp: case hx
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ ⟨n.succ, f n x⟩.fst ≤ n.succ

Tactic:
rfl

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
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∈ s
A : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ (if x ∈ s then x else ⋯.some) = A.some

Tactic:
if_neg xs

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
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
⊢ (if x ∈ s then x else ⋯.some) = Ax.some

Tactic:
if_neg xs

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x✝ : Set α
⊢ 1 / 2 = ↑1 / ↑2

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
ξ : Measure α
⊢ ξ = ⊥ ↔ ξ = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (dirac a).restrict s = if a ∈ s then dirac a else 0

Tactic:
by
  split_ifs with has
  · apply restrict_eq_self_of_ae_mem
    rwa [ae_dirac_eq]
  · rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]

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)
f : ((n : ℕ) → E n) → (n : ℕ) → E n
f_cont : Continuous[Pi.topologicalSpace, Pi.topologicalSpace] f
hs : IsClosed[Pi.topologicalSpace] (range f)
hne : (range f).Nonempty
fs : ∀ x ∈ range f, f x = x
A : ∀ (x : ↑(range f)), rangeFactorization f ↑x = x
⊢ ∃ f_1,
    (∀ (x : ↑(range f)), f_1 ↑x = x) ∧ Surjective f_1 ∧ Continuous[Pi.topologicalSpace, instTopologicalSpaceSubtype] f_1

Tactic:
exact ⟨rangeFactorization f, A, fun x => ⟨x, A x⟩, f_cont.subtype_mk _⟩

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

Goal state before:
pp: case zero
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := { p // ¬MeasurablySeparable (f '' cylinder p.2.1 p.1) (g '' cylinder p.2.2 p.1) }
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⟨(0, fun x ↦ 0, fun x ↦ 0), ⋯⟩
p : ℕ → A := fun n ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
⊢ (↑(p 0)).1 = 0

Tactic:
rfl

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

Goal state before:
pp: case base
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := ⋯
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⋯
p : ℕ → A := ⋯
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
m : ℕ
⊢ (↑(p (m + 1))).2.1 m = (↑(p (m + 1))).2.1 m

Tactic:
rfl

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

Goal state before:
pp: case base
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst✝³] f
hg : Continuous[_, inst✝³] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : ℕ → ℕ),
    ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y',
        x' ∈ cylinder x n ∧
          y' ∈ cylinder y n ∧ ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1))
A : Type := ⋯
F : A → A
hFn : ∀ (p : A), (↑(F p)).1 = (↑p).1 + 1
hFx : ∀ (p : A), (↑(F p)).2.1 ∈ cylinder (↑p).2.1 (↑p).1
hFy : ∀ (p : A), (↑(F p)).2.2 ∈ cylinder (↑p).2.2 (↑p).1
p0 : A := ⋯
p : ℕ → A := ⋯
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n)).2.1 m = (↑(p (m + 1))).2.1 m
m : ℕ
⊢ (↑(p (m + 1))).2.2 m = (↑(p (m + 1))).2.2 m

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ map f (m i)).join = sum fun i ↦ (map f (m i)).join

Tactic:
join_sum

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (map (fun x ↦ dirac (f x)) m).join = (map (dirac ∘ f) m).join

pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable dirac

pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable f

Tactic:
Function.comp_def

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (map (fun x ↦ dirac (f x)) m).join = (map (fun x ↦ dirac (f x)) m).join

case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable dirac

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ Measurable f
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Dense {x | p x}

Tactic:
dense_iff_closure_eq,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ closure[inst✝¹] {x | p x} = univ
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x r) ≤ ↑(scalingConstantOf μ K⁻¹) * μ (closedBall x (K * r))

Tactic:
convert! eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: case add
α : 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₁ + f₂) x) ∂μ
⊢ ∃ g, (∀ (x : α), g x ≤ (f₁ + f₂) x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ∞ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ

Tactic:
| @add f₁ f₂ _ h₁ h₂ =>

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case mpr.py₂
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑(hSK.equiv g₂).1)⁻¹ * g₁ ∈ K

Tactic:
← mul_mem_cancel_right h

Goal state after:
case mpr.py₂
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (↑(hSK.equiv g₂).1)⁻¹ * g₁ * (g₁⁻¹ * g₂) ∈ K
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 γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
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 β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
s : ℕ → ↑b
hs : ∀ (n : ℕ), Bornology.IsBounded ↑(s n) ∧ diam ↑(s n) ≤ u n
hxs : ∀ (n : ℕ), x ∈ E (s n)
n : ℕ
⊢ ↑(s n) ≠ ∅

Tactic:
grind

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 (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), μ (Prod.mk x ⁻¹' Prod.swap ⁻¹' s) ∂ν = ∫⁻ (y : β), μ ((fun x ↦ (x, y)) ⁻¹' s) ∂ν

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f (sum (sfiniteSeq μa))).prod (map g μc) = map (Prod.map f g) ((sum (sfiniteSeq μa)).prod μc)

Tactic:
← sum_sfiniteSeq μc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst✝¹ : SFinite μa
inst✝ : SFinite μc
hf : Measurable f
hg : Measurable g
⊢ (map f (sum (sfiniteSeq μa))).prod (map g (sum (sfiniteSeq μc))) =
    map (Prod.map f g) ((sum (sfiniteSeq μa)).prod (sum (sfiniteSeq μc)))
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ {x | p x} ∈ Filter.map (fun h ↦ t * h) (ae μ)

Tactic:
rfl

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ {x | p x} ∈ Filter.map (fun h ↦ h * t) (ae μ)

Tactic:
rfl

Goal state after:
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 β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (ν.prod μ)
⊢ AEMeasurable (fun z ↦ f z.swap) (μ.prod ν)

Tactic:
rw [← Measure.prod_swap] at hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (map Prod.swap (μ.prod ν))
⊢ AEMeasurable (fun z ↦ f z.swap) (μ.prod ν)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ {x | p x} ∈ Filter.map (fun t_1 ↦ t_1 / t) (ae μ)

Tactic:
rfl

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 β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' Prod.snd ⁻¹' s) = (map Y μ) s

Tactic:
Measure.map_apply_of_aemeasurable hY hs,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' Prod.snd ⁻¹' s) = μ (Y ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)
    · fun_prop
    · exact .of_forall fun x ↦ hm.choose_spec.apply_nhds x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.fst ∘ Prod.swap) ρ = ρ.snd

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.snd ∘ Prod.swap) ρ = ρ.fst

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SFinite μb
inst✝ : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
B : MeasurableSet (⇑MeasurableEquiv.prodAssoc ⁻¹' s)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), μc (Prod.mk (x, y) ⁻¹' ⇑MeasurableEquiv.prodAssoc ⁻¹' s) ∂μb ∂μa =
    ∫⁻ (x : α), ∫⁻ (x_1 : β), μc (Prod.mk x_1 ⁻¹' Prod.mk x ⁻¹' s) ∂μb ∂μa

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

Tactic:
by
  ext1 s hs
  simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]

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

Goal state before:
pp: case e'_2.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
x y x✝ : G
⊢ 1 = ((fun x ↦ 1) ∘ fun y ↦ y * x) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ 2 * a * x = -b + s ∨ 2 * a * x = -b - s

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
x : K
hx : (fun x_1 ↦ (2 * a * x + b) ^ 2 = (2 * a * x_1 + b) ^ 2) (-(x + b / a)) → -(x + b / a) = x
⊢ (2 * a * x + b) ^ 2 = 0

Tactic:
grind

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

Goal state before:
pp: x y : ℝ
⊢ √7 ≠ 0

Tactic:
grind

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

Goal state before:
pp: ⊢ √2 ^ 2 < (3 / 2) ^ 2

Tactic:
grind

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

Goal state before:
pp: ⊢ (√2 - 1)⁻¹ = √2 + 1

Tactic:
grind

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

Goal state before:
pp: x : ℝ
⊢ (↑(NNReal.sqrt x.toNNReal))⁻¹ = (√x)⁻¹

Tactic:
Real.sqrt

Goal state after:
x : ℝ
⊢ (↑(NNReal.sqrt x.toNNReal))⁻¹ = (↑(NNReal.sqrt x.toNNReal))⁻¹