mathlib-initiative/mathlib-tactics huggingface dataset:
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)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x✝ : TopologicalSpace ((n : ℕ) × X n) := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x : X n
⊢ dist ⟨n.succ, f n x⟩.snd (leRecOn ?hy (fun {k} ↦ f k) ⟨n, x⟩.snd) = 0

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

pp: case hy
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.succ

Tactic:
leRecOn_succ,

Goal state after:
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
⊢ dist ⟨n.succ, f n x⟩.snd (f n (leRecOn ?h1 (fun {k} ↦ f k) ⟨n, x⟩.snd)) = 0

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

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

case hy
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.succ
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
⊢ Injective fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩

Tactic:
intro x y hxy

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
hdom : ∀ {x : ℕ → Bool}, x ∈ (inducedMap D).fst
x y : ℕ → Bool
hxy : (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) x = (fun x ↦ (inducedMap D).snd ⟨x, ⋯⟩) y
⊢ x = y
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : ↑measurableAtoms
y : α
left✝ : y ∈ univ
hy : measurableAtom y = ↑s
⊢ (↑s).Nonempty

Tactic:
← hy

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
s : ↑measurableAtoms
y : α
left✝ : y ∈ univ
hy : measurableAtom y = ↑s
⊢ (measurableAtom y).Nonempty
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ False

Tactic:
apply apply_firstDiff_ne hne'

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := ⋯
g : ↑s → α := ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := ⋯
h : firstDiff ↑x ↑y ≤ 0
⊢ ↑x (firstDiff ↑x ↑y) = ↑y (firstDiff ↑x ↑y)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ ↑x 0 = ↑y 0

Tactic:
apply apply_eq_of_dist_lt _ le_rfl

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := ⋯
g : ↑s → α := ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := ⋯
h : firstDiff ↑x ↑y ≤ 0
⊢ dist ↑x ↑y < (1 / 2) ^ 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : 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), ⋯⟩
⊢ False

Tactic:
let p : ℕ → A := fun n => F^[n] p0

Goal state after:
α : 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
⊢ False
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Countable

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
by
  rw [restrict_dirac]
  split_ifs
  · exact lintegral_dirac _ _
  · exact lintegral_zero_measure _

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ μ ∗ₘ ν = ν ∗ₘ μ

Tactic:
by
  unfold mconv
  rw [← prod_swap, map_map (by fun_prop)]
  · simp [Function.comp_def, mul_comm]
  fun_prop

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf : (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ
⊢ IsComplement ↑K ↑H

Tactic:
isComplement_iff_bijective,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
ϕ : ↥H × ↥K ≃ ↥K × ↥H :=
  { toFun := fun x ↦ (x.2⁻¹, x.1⁻¹), invFun := fun x ↦ (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }
ψ : G ≃ G := { toFun := fun g ↦ g⁻¹, invFun := fun g ↦ g⁻¹, left_inv := ⋯, right_inv := ⋯ }
hf : (⇑ψ ∘ fun x ↦ ↑x.1 * ↑x.2) = (fun x ↦ ↑x.1 * ↑x.2) ∘ ⇑ϕ
⊢ Bijective fun x ↦ ↑x.1 * ↑x.2
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (↑(hST.equiv g).1)⁻¹ * g = ↑⟨1, h1⟩

Tactic:
equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (↑⟨g, hg⟩)⁻¹ * g = ↑⟨1, h1⟩
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
α : Type u_2
inst✝ : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ h, h • g • a = a
⊢ H.IsComplement' (MulAction.stabilizer G a)

Tactic:
by
  refine isComplement_iff_existsUnique.mpr fun g => ?_
  obtain ⟨h, hh⟩ := h2 g
  have hh' : (↑h * g) • a = a := by rwa [mul_smul]
  refine ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, ?_⟩
  rintro ⟨h', g, hg : g • a = a⟩ rfl
  specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
  refine Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)
  rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1

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 β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : ν t ≠ 0
⊢ NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)

Tactic:
exact h.preimage measurePreserving_swap.quasiMeasurePreserving

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SFinite μ
inst✝ : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x ↦ f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
by
  rw [← prod_swap]
  convert!
    (QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
      ((measurable_swap.measurePreserving (ν.prod μ)).symm
          MeasurableEquiv.prodComm).quasiMeasurePreserving

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

Goal state before:
pp: case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')

Tactic:
exact hu.mono (by simp [t']) |>.measurableSet

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✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
| μ.inv

Tactic:
rw [← map_mul_left_eq_self μ g⁻¹]

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
| (map (fun x ↦ g⁻¹ * x) μ).inv
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (f x)) S = 0

Tactic:
rw [withDensity_apply _ hS, lintegral_eq_zero_iff hf.ennreal_ofReal, EventuallyEq]

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∀ᵐ (x : α) ∂μ.restrict S, ENNReal.ofReal (f x) = 0 x
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
⊢ a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]

Goal state after:
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) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case e'_2
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = ↑(NNReal.sqrtHom (∏ x_1 ∈ s, (toNNReal ∘ x) x_1))

Tactic:
simp +contextual [-map_prod, NNReal.sqrtHom, hx]

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

Goal state before:
pp: case e'_3
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ ∏ i ∈ s, √(x i) = ↑(∏ x_1 ∈ s, NNReal.sqrtHom ((toNNReal ∘ x) x_1))

Tactic:
simp +contextual [-map_prod, NNReal.sqrtHom, hx]

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
x : α
⊢ x ∈ f ⁻¹' Iic ↑(max (spanningSetsIndex μ x) ⌈f x⌉₊)

Tactic:
· simp [Nat.le_ceil]

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

Goal state before:
pp: ⊢ Monotone ofReal

Tactic:
intro x y hxy

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2

Tactic:
rw [prod_withDensity_left₀ hf, prod_withDensity_right₀ hg, ← withDensity_mul₀, mul_comm]
  · rfl
  all_goals fun_prop (disch := intro _ hs; simp [hs])

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

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ x ∈ s

Tactic:
← hy

Goal state after:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ (incl s).toAddMonoidHom y ∈ s
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ g * star g = 1 ∧ star g * g = 1

Tactic:
exact hg.symm

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

Goal state before:
pp: z w : ℂ
⊢ dist ((starRingEnd ℂ) ((starRingEnd ℂ) z)) ((starRingEnd ℂ) w) = dist z ((starRingEnd ℂ) w)

Tactic:
conj_conj

Goal state after:
z w : ℂ
⊢ dist z ((starRingEnd ℂ) w) = dist z ((starRingEnd ℂ) w)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) = 2 * ↑(re z) / 2

Tactic:
mul_div_cancel_left₀ (re z : K) two_ne_zero

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) = ↑(re z)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
← Complex.ofReal_intCast,

Goal state after:
⊢ ∀ (x y : ℤ), dist ↑↑x ↑↑y = dist x y
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ span ℂ ↑(selfAdjoint A)

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
| star x * x

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
| star (↑(ℜ x) + I • ↑(ℑ x)) * (↑(ℜ x) + I • ↑(ℑ x))
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ re (ofScientific m s e) = ofScientific m s e

Tactic:
by rw [← ofReal_ofScientific, ofReal_re]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
⊢ 0 ≤ a ↔ 0 ≤ ℜ a ∧ ℑ a = 0

Tactic:
by
  refine ⟨fun h ↦ ⟨?_, h.isSelfAdjoint.imaginaryPart⟩, fun h ↦ ?_⟩
  · simpa +singlePass [← h.isSelfAdjoint.coe_realPart] using! h
  · rw [← realPart_add_I_smul_imaginaryPart a, h.2]
    simpa using! h.1

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star x) = star (φ x)

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Goal state after:
A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star (↑(ℜ x) + I • ↑(ℑ x))) = star (φ (↑(ℜ x) + I • ↑(ℑ x)))
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
p : Y → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p (↑e x)

Tactic:
by
  refine Iff.trans ?_ eventually_map
  rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.nhdsWithin_target_inter (e.mapsTo hx)]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =O[l] f' → ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
intro h
    rcases h.exists_pos with ⟨C, hC₀, hC⟩
    refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
    exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2

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

Goal state before:
pp: x : ℝ
⊢ (cosh ↑x).im = 0

Tactic:
by rw [← ofReal_cosh_ofReal_re, ofReal_im]

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

Goal state before:
pp: x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
  · congr <;> field
  · rw [cos_add, cos_sub]
  ring

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

Goal state before:
pp: x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)

Tactic:
simp [cosh_add]

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

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x)‖₊ = 1

Tactic:
by
  rw [← nnnorm_norm, norm_exp_I_mul_ofReal, ← NNReal.coe_eq_one]; simp

Goal state after: