mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
γ : 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)
C2 : ∀ (n : ℕ), (↑(s n)).Nonempty
⊢ x ∈ range f

Tactic:
choose y hy using C2

Goal state after:
case h₂
γ : 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)
y : ℕ → γ
hy : ∀ (n : ℕ), y n ∈ ↑(s n)
⊢ x ∈ range f
Module: Mathlib.MeasureTheory.Measure.Prod

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

Tactic:
exact h hs ht hu

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 μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (sum (sfiniteSeq ν) + sum (sfiniteSeq ν')) = μ.prod (sum (sfiniteSeq ν)) + μ.prod (sum (sfiniteSeq ν'))

Tactic:
sum_add_sum,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
ν' : Measure β
inst✝ : SFinite ν'
⊢ μ.prod (sum fun n ↦ sfiniteSeq ν n + sfiniteSeq ν' n) = μ.prod (sum (sfiniteSeq ν)) + μ.prod (sum (sfiniteSeq ν'))
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
U : Set α
⊢ IsOpen[inst✝²] U →
    ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε

Tactic:
hU

Goal state after:
case isOpen
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
U : Set α
hU : IsOpen[inst✝²] U
⊢ ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ U, ∃ U_1 ⊇ U, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U_1 ∧ μ U ≤ μ F + ε ∧ μ U_1 ≤ μ U + ε
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 μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (sum (sfiniteSeq μ) + sum (sfiniteSeq μ')).prod ν = (sum (sfiniteSeq μ)).prod ν + (sum (sfiniteSeq μ')).prod ν

Tactic:
sum_add_sum,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
μ' : Measure α
inst✝ : SFinite μ'
⊢ (sum fun n ↦ sfiniteSeq μ n + sfiniteSeq μ' n).prod ν = (sum (sfiniteSeq μ)).prod ν + (sum (sfiniteSeq μ')).prod ν
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ ≤ borel γ

Tactic:
intro s hs

Goal state after:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet s
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 : G) ∂μ, p x

Tactic:
by
  conv_rhs => rw [Filter.Eventually, ← map_mul_left_ae μ t]
  rfl

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

Goal state before:
pp: X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
⊢ IsOpen[inst✝²] U → ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
hU

Goal state after:
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : PseudoMetrizableSpace X
inst✝ : MeasurableSpace X
μ : Measure X
A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
U : Set X
hU : IsOpen[inst✝²] U
⊢ ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
⊢ IsOpen[inst✝²] U → ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K

Tactic:
hU

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : OpensMeasurableSpace α
h : μ.InnerRegular
U : Set α
hU : IsOpen[inst✝²] U
⊢ ∀ r < μ U, ∃ K ⊆ U, IsClosed[inst✝²] K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst✝ : IsFiniteMeasure μ
⊢ μ.InnerRegular

Tactic:
by
  constructor
  convert! h.innerRegular with s
  simp [measure_ne_top μ s]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0 ∨ False
⊢ μ s = 0

Tactic:
or_false

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ (x * y, x⁻¹) = (x * y, y / y / x)

Tactic:
div_self',

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ (x * y, x⁻¹) = (x * y, 1 / x)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * ↑(f' a) * g a

Tactic:
ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = 1 * g a
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
discrim

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0

Tactic:
discrim

Goal state after:
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * (x * x) + b * x + c = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
⊢ ∀ (s : Set α), MeasurableSet s → Measurable fun b ↦ (μ.withDensity (f b)) s

Tactic:
intro s hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (μ.withDensity (f b)) s
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
by
  simp only [HasFiniteIntegral]

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

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

Tactic:
← sq,

Goal state after:
x : ℝ≥0
⊢ sqrt x ^ 2 = x
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
← sq,

Goal state after:
x : ℝ≥0
⊢ sqrt (x ^ 2) = x
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
by rw [← h, mul_self_sqrt hx]

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

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

Tactic:
sqrt_mul hx,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √x * √y⁻¹ = √x / √y
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.re * z.re + z.im * z.im - z.re ^ 2 = z.im ^ 2

Tactic:
← sq,

Goal state after:
z : ℂ
⊢ z.re ^ 2 + z.im * z.im - z.re ^ 2 = z.im ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.re ^ 2 + z.im * z.im - z.re ^ 2 = z.im ^ 2

Tactic:
← sq,

Goal state after:
z : ℂ
⊢ z.re ^ 2 + z.im ^ 2 - z.re ^ 2 = z.im ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ ‖z‖ = √(z.re ^ 2 + z.im ^ 2)

Tactic:
rw [norm_def, normSq_apply, sq, sq]

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

Goal state before:
pp: z : ℂ
⊢ z.im ^ 2 ≤ z.re * z.re + z.im * z.im

Tactic:
← sq,

Goal state after:
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im * z.im
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.im ^ 2 ≤ normSq z

Tactic:
rw [normSq_apply, ← sq, ← sq]

Goal state after:
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.re ^ 2 < z.re * z.re + z.im * z.im ↔ z.im ≠ 0

Tactic:
← sq,

Goal state after:
z : ℂ
⊢ z.re ^ 2 < z.re ^ 2 + z.im * z.im ↔ z.im ≠ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im } = { re := b.re, im := -b.im } * { re := a.re, im := -a.im }

Tactic:
by ext <;> simp [add_comm] <;> ring

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

Goal state before:
pp: α : Type u_1
n : ℚ≥0
z : ℂ
⊢ (n • z).re = (↑n * z).re ∧ (n • z).im = (↑n * z).im

Tactic:
by simp [NNRat.smul_def, smul_re, smul_im]

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 : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν ∂μ

Tactic:
refine lintegral_congr (fun x ↦ ?_)
    rw [lintegral_withDensity_eq_lintegral_mul₀ hg (by fun_prop)]
    simp

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

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
| (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a

Tactic:
rw [(lintegral_mul_const'' _ (by fun_prop)).symm]

Goal state after:
G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
| ∫⁻ (a_1 : G), f a_1 * g (a_1⁻¹ * a) * φ a ∂μ
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₂
g : NormedAddGroupHom V₂ V₃
⊢ ∀ (a b : NormedAddGroupHom V₁ V₂), g.comp (a + b) = g.comp a + g.comp b

Tactic:
by
          intros
          ext
          exact map_add g _ _

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ (starRingEnd K) (r • z) = r • (starRingEnd K) z

Tactic:
conj_eq_re_sub_im,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(re (r • z)) - ↑(im (r • z)) * I = r • (starRingEnd K) z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(re (r • z)) - ↑(im (r • z)) * I = r • (starRingEnd K) z

Tactic:
conj_eq_re_sub_im,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ ↑(re (r • z)) - ↑(im (r • z)) * I = r • (↑(re z) - ↑(im z) * I)
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
B : Type u_2
F : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module ℂ B
inst✝⁴ : StarAddMonoid B
inst✝³ : StarModule ℂ B
inst✝² : FunLike F A B
inst✝¹ : StarHomClass F A B
inst✝ : LinearMapClass F ℂ A B
f : F
x : A
⊢ f ↑(ℑ x) = ↑(ℑ (f x))

Tactic:
simp [imaginaryPart_apply_coe, ← Complex.coe_smul, map_star]

Goal state after:
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
⊢ ℑ.ker = selfAdjoint.submodule ℝ A

Tactic:
by
  ext x
  simp [selfAdjoint.submodule, selfAdjoint.mem_iff, imaginaryPart, Subtype.ext_iff]
  grind

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

Goal state before:
pp: case hre
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re (z * (starRingEnd K) z) = re (↑‖z‖ ^ 2)

Tactic:
simp [← ofReal_pow, norm_sq_eq_def, mul_comm]

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

Goal state before:
pp: case him
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im (z * (starRingEnd K) z) = im (↑‖z‖ ^ 2)

Tactic:
simp [← ofReal_pow, norm_sq_eq_def, mul_comm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ re (OfNat.ofNat n * z) = OfNat.ofNat n * re z

Tactic:
by
  rw [← ofReal_ofNat, re_ofReal_mul]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ a
⊢ 0 ≤ ℜ a

Tactic:
simpa +singlePass [← h.isSelfAdjoint.coe_realPart] using! h

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

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

Tactic:
rw [← realPart_add_I_smul_imaginaryPart a, h.2]
    simpa using! h.1

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x

Tactic:
simpa only [div_eq_mul_inv] using h₁.mul h₂.inv

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ -f' x) =o[l] g ↔ f' =o[l] g

Tactic:
by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_neg_left

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
⊢ IsBigOWith c l (fun x ↦ (f' x, g' x)) k'

Tactic:
rw [isBigOWith_iff] at *; filter_upwards [hf, hg] with x using max_le

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = rexp x

Tactic:
by rw [exp, Complex.exp, ← cauSeqRe, lim_re]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j with n ≤ m, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_filter, mem_range] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (↑x).cot = (↑x).cot

Tactic:
rw [← cot_conj, conj_ofReal]

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

Goal state before:
pp: x : ℂ
⊢ cos x * cos x - sin x * sin x = cos x ^ 2 - sin x ^ 2

Tactic:
← sq,

Goal state after:
x : ℂ
⊢ cos x ^ 2 - sin x * sin x = cos x ^ 2 - sin x ^ 2
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =O[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =O[l] g'

Tactic:
simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]
  exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
rw [← eventually_forall_ge_atTop] at h

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := ⋯
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
← prod_atTop_atTop_eq

Goal state after:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
h3 : dist (cexp (x - y)) (cexp 0) < ε / (2 * Real.exp a)
⊢ dist (cexp x) (cexp y) < ε

Tactic:
rw [dist_eq_norm, exp_zero] at *

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ ‖cexp x - cexp y‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x : ℝ
⊢ rexp (x / 2) = √(rexp x)

Tactic:
rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves]

Goal state after:
case hx
x : ℝ
⊢ 0 ≤ rexp x

case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ s = infEDist x s⁻¹

Tactic:
← infEDist_inv_inv,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹⁻¹ s⁻¹ = infEDist x s⁻¹