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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K ⊆ K ∪ K'

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K' ⊆ K ∪ K'

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
h : (map (⇑f) μ).Regular
⊢ μ = map (⇑f.symm ∘ ⇑f) μ

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n)⁻¹ < edist (f k x) (g x)
⊢ (↑n)⁻¹ > 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
⊢ ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0

Tactic:
simp

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 : α → β
⊢ ∫⁻ (a : α), ‖(-f) a‖ₑ ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
hg : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
calc
    (∫⁻ a, ‖f a‖ₑ ∂μ) ≤ ∫⁻ a : α, ‖g a‖ₑ ∂μ := lintegral_mono_ae h
    _ < ∞ := hg

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
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0

Tactic:
by
  simp_rw [quadratic_eq_zero_iff_discrim_eq_sq ha] at h
  generalize discrim a b c = d at h
  obtain ⟨x, rfl, hx⟩ := h
  specialize hx (-(x + b / a))
  grind

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h✝ : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ENNReal.ofReal (↑fx).toReal ≤ ↑fx

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝¹ : α
x✝ : ℕ
⊢ ENNReal.ofReal ‖F x✝ x✝¹‖ = ‖F x✝ x✝¹‖ₑ

Tactic:
simp

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

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝ : α
⊢ ENNReal.ofReal ‖f x✝‖ = ‖f x✝‖ₑ

Tactic:
simp

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

Goal state before:
pp: x : ℝ≥0
⊢ sqrt x * sqrt x = x

Tactic:
by rw [← sq, sq_sqrt]

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

Goal state before:
pp: ⊢ sqrt 0 = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ sqrt 1 = 1

Tactic:
simp

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

Goal state before:
pp: case h₁
x y : ℝ≥0
⊢ x ≤ max x y

Tactic:
simp

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

Goal state before:
pp: case h₂
x y : ℝ≥0
⊢ y ≤ max x y

Tactic:
simp

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

Goal state before:
pp: case inl
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_ge
      (hy.trans_lt hx).not_ge

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

Goal state before:
pp: case h
⊢ 1 < 2

Tactic:
simp

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

Goal state before:
pp: a : ℕ
⊢ 0 ≤ ↑a

Tactic:
simp

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

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ ↑(nndist z w) = ↑(nndist z.re w.re)

Tactic:
nndist_of_im_eq h

Goal state after:
z w : ℂ
h : z.im = w.im
⊢ ↑(nndist z.re w.re) = ↑(nndist z.re w.re)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ (f * fun x ↦ (f x)⁻¹) x ≤ 1 x

Tactic:
simp

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

Goal state before:
pp: ⊢ (I * I).re = (-1).re ∧ (I * I).im = (-1).im

Tactic:
simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : f =ᵐ[μ.restrict s] 0
⊢ μ s = 0

Tactic:
ae_eq_restrict_iff_indicator_ae_eq hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : s.indicator f =ᵐ[μ] s.indicator 0
⊢ μ s = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
⊢ (z * I).re = -z.im

Tactic:
simp

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

Goal state before:
pp: z : ℂ
⊢ (z * I).im = z.re

Tactic:
simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).re = -z.im

Tactic:
simp

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

Goal state before:
pp: z : ℂ
⊢ (I * z).im = z.re

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ (x y : ℂ), equivRealProd.toFun (x + y) = equivRealProd.toFun x + equivRealProd.toFun y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ r • z.re - 0 * z.im = r • z.re

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : SMul R ℝ
r : R
z : ℂ
⊢ r • z.im + 0 * z.re = r • z.im

Tactic:
simp

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

Tactic:
simp

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re + b✝.re + c✝.re = a✝.re + (b✝.re + c✝.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

Tactic:
simp

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ a✝.im + b✝.im + c✝.im = a✝.im + (b✝.im + c✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 + a✝).re = a✝.re

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 + a✝).im = a✝.im

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ + 0).re = a✝.re

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ + 0).im = a✝.im

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ SigmaFinite (μ.withDensity fun x ↦ ↑(f x))

Tactic:
refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ (μ.withDensity fun x ↦ ↑(f x)) (spanningSets μ n ∩ f ⁻¹' Iic ↑n) < ∞

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
⊢ ⋃ i, spanningSets μ i ∩ f ⁻¹' Iic ↑i = univ
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z ^ 2 ↔ z.im = 0

Tactic:
by
  rw [nonneg_iff, pow_two, mul_re, mul_im, mul_comm z.im z.re, ← mul_two, eq_comm,
    mul_eq_zero_iff_right two_ne_zero, ← pow_two, ← pow_two, mul_eq_zero]
  exact ⟨by aesop, fun h ↦ by simpa [h] using sq_nonneg z.re⟩

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (-a✝ + a✝).re = re 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (-a✝ + a✝).im = im 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re

Tactic:
simp

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.re + b✝.re = b✝.re + a✝.re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im

Tactic:
simp

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.im + b✝.im = b✝.im + a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
⊢ (↑0).re = re 0

Tactic:
simp

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

Goal state before:
pp: case a
⊢ (↑0).im = im 0

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).re = (↑x✝ + 1).re

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).im = (↑x✝ + 1).im

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).re = (↑x✝).re

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).im = (↑x✝).im

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).re = (-↑(x✝ + 1)).re

Tactic:
simp

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

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).im = (-↑(x✝ + 1)).im

Tactic:
simp

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

Tactic:
simp

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im

Tactic:
simp

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (1 * a✝).re = a✝.re

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (1 * a✝).im = a✝.im

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 1).re = a✝.re

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 1).im = a✝.im

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 * a✝).re = re 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 * a✝).im = im 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 0).re = re 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 0).im = im 0

Tactic:
simp

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

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).re = (b✝ * a✝).re

Tactic:
simp

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.re - a✝.im * b✝.im = b✝.re * a✝.re - b✝.im * a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).im = (b✝ * a✝).im

Tactic:
simp

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
simp

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

Goal state before:
pp: n : ℤ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ ((starRingEnd ℂ) ↑r).re = (↑r).re ∧ ((starRingEnd ℂ) ↑r).im = (↑r).im

Tactic:
simp

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

Goal state before:
pp: ⊢ ((starRingEnd ℂ) I).re = (-I).re ∧ ((starRingEnd ℂ) I).im = (-I).im

Tactic:
simp

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

Goal state before:
pp: ⊢ (starRingEnd ℂ) (-I) = I

Tactic:
simp

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

Goal state before:
pp: ⊢ re 0 * re 0 + im 0 * im 0 = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
simp

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

Goal state before:
pp: ⊢ normSq 0 = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ normSq 1 = 1

Tactic:
simp

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

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
R : Type u_2
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ c • μ = c • 1 • μ

Tactic:
simp

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

Goal state before:
pp: z : ℂ
⊢ normSq z⁻¹ = (normSq z)⁻¹

Tactic:
simp

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

Goal state before:
pp: z w : ℂ
⊢ normSq (z / w) = normSq z / normSq w

Tactic:
simp

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

Goal state before:
pp: a₁ a₂ : ℝ
x : ℂ
x₁ : (equivRealProd x).1 ∈ [[a₁, a₂]]
⊢ (fun x_1 ↦ ↑x_1 + ↑(equivRealProd x).2 * I) x.re = x

Tactic:
simp

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

Goal state before:
pp: b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ (fun y ↦ ↑x.re + ↑y * I) x.im = x

Tactic:
simp

Goal state after:
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∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), (g * fun y ↦ φ (x, y)) a ∂ν = ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (a b : M), True → True → True

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ i ∈ s, True

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s✝ : Set (α × β)
hs : MeasurableSet s✝
s : Set β
⊢ c • ν s = c • 1 * ν s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (a b : M), True → True → True

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ i ∈ s, True

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : StarAddMonoid A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : TopologicalSpace A
inst✝ : ContinuousStar A
x : A
⊢ (starL R).symm x = starAddEquiv.symm x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : StarAddMonoid A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousStar A
inst✝ : TrivialStar R
r : R
a : A
⊢ (AddEquiv.refl A).toFun (r • a) = (starRingEnd R) r • (AddEquiv.refl A).toFun a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : StarAddMonoid A
inst✝⁴ : Module R A
inst✝³ : StarModule R A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousStar A
inst✝ : TrivialStar R
x : A
⊢ (starL' R).symm x = starAddEquiv.symm x

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ ∀ (v : V₁), ‖0 v‖ ≤ 0 * ‖v‖

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ ∀ (v : V), ‖(AddMonoidHom.id V) v‖ ≤ 1 * ‖v‖

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
inst✝ : SeminormedAddCommGroup V
x : V
⊢ ‖(id V) x‖ ≤ 1 * ‖x‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
x : ℝ
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
simp

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
⊢ (incl s).toAddMonoidHom y ∈ s

Tactic:
simp

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₁
hx : x ∈ s
⊢ (incl s).toAddMonoidHom ⟨x, hx⟩ = x

Tactic:
simp

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

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
v : V₁
⊢ ‖0 v‖ ≤ ‖v‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : (i : ι) → R i
⊢ ⊥ ^ 2 = ⊥

Tactic:
simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : { φ // f.comp φ = g.comp φ }
⊢ (fun ψ ↦ ⟨(ι f g).comp ψ, ⋯⟩) ((fun φ ↦ lift ↑φ ⋯) φ) = φ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑reAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑reAddGroupHom).toFun x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑imAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑imAddGroupHom).toFun x

Tactic:
simp

Goal state after: