mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x ↦ (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
⊢ ¬IntervalIntegrable f volume a b

Tactic:
by
  have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
  have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop := by
    refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)
    rw [← sub_self c]
    exact ((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero
  exact not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured
    (A.mono fun x hx => hx.differentiableAt) B
    (hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
⊢ essSup g (map QuotientGroup.mk (μ.restrict 𝓕)) = essSup (fun x ↦ g ↑x) μ

Tactic:
essSup_map_measure g_ae_measurable hπ.aemeasurable

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
⊢ essSup (g ∘ QuotientGroup.mk) (μ.restrict 𝓕) = essSup (fun x ↦ g ↑x) μ
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ ≠ ∞

Tactic:
have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg

Goal state after:
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝⁵ : Countable ↥Γ
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ.IsMulRightInvariant
f : G → K
f_ℒ_1 : Integrable f μ
g : G ⧸ Γ → K
hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕)) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))
π : G → G ⧸ Γ := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ
hg' : AEStronglyMeasurable (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ.restrict 𝓕))
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ'
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ' ≠ ∞

Tactic:
have hg' : AEStronglyMeasurable (‖g ·‖ₑ) μ_𝓕 := continuous_enorm.comp_aestronglyMeasurable hg

Goal state after:
G' : Type u_1
inst✝¹⁰ : AddGroup G'
inst✝⁹ : MeasurableSpace G'
inst✝⁸ : TopologicalSpace G'
inst✝⁷ : IsTopologicalAddGroup G'
inst✝⁶ : BorelSpace G'
μ' : Measure G'
Γ' : AddSubgroup G'
𝓕' : Set G'
h𝓕 : IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ'
inst✝⁵ : Countable ↥Γ'
inst✝⁴ : MeasurableSpace (G' ⧸ Γ')
inst✝³ : BorelSpace (G' ⧸ Γ')
K : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedSpace ℝ K
inst✝ : μ'.IsAddRightInvariant
f : G' → K
f_ℒ_1 : Integrable f μ'
g : G' ⧸ Γ' → K
hg : AEStronglyMeasurable g (Measure.map mk (μ'.restrict 𝓕'))
g_ℒ_infinity : essSup (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕')) ≠ ∞
F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ'.restrict 𝓕'))
π : G' → G' ⧸ Γ' := mk
meas_π : Measurable π
H₀ : automorphize (g ∘ π * f) = g * automorphize f
this : AEStronglyMeasurable (fun x ↦ g ↑x) μ'
hg' : AEStronglyMeasurable (fun x ↦ ‖g x‖ₑ) (Measure.map mk (μ'.restrict 𝓕'))
⊢ essSup (fun x ↦ ‖g ↑x‖ₑ) μ' ≠ ∞
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
⊢ IntervalIntegrable (fun θ ↦ (f ∘ circleMap c R) (θ + π)) volume 0 (2 * π) ↔
    IntervalIntegrable (fun θ ↦ f (circleMap c R θ)) volume 0 (2 * π)

Tactic:
IntervalIntegrable.comp_add_right_iff (c := π),

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
f : ℂ → E
⊢ IntervalIntegrable (f ∘ circleMap c R) volume (0 + π) (2 * π + π) ↔
    IntervalIntegrable (fun θ ↦ f (circleMap c R θ)) volume 0 (2 * π)
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable ((Iio a).indicator f) μ

Tactic:
aestronglyMeasurable_indicator_iff measurableSet_Iio

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable f (μ.restrict (Iio a))
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∫ (x : ℝ) in Ioc 0 (2 * π), deriv (circleMap c R) x • f (circleMap c R x) ∂volume =
    ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)

Tactic:
Measure.restrict_congr_set Ioc_ae_eq_Icc

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ ∫ (x : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) x • f (circleMap c R x) ∂volume =
    ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap c R) θ • f (circleMap c R θ)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → ℂ
a : E
c : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), f z • a = (∮ (z : ℂ) in C(c, R), f z) • a

Tactic:
by
  simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: n : ℤ
c w : ℂ
R : ℝ
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
by
  rcases eq_or_ne R 0 with (rfl | h0)
  · apply integral_radius_zero
  · apply integral_undef
    simpa [circleIntegrable_sub_zpow_iff, *, not_or] using mem_sphere_iff_norm.1 hw

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ (2 * π)⁻¹ * (|R|⁻¹ ^ n * (|R| * (|R|⁻¹ * ∫ (x : ℝ) in 0..2 * π, ‖f (circleMap c R x)‖))) ≤
    ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c R θ)‖) * |R|⁻¹ ^ n

Tactic:
rw [mul_inv_cancel_left₀, mul_assoc, mul_comm (|R|⁻¹ ^ n)]

Goal state after:
case inr.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
n : ℕ
hR : R ≠ 0
⊢ |R| ≠ 0
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
⊢ Integrable (fun y ↦ g (a✝, y)) ν →
    F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
⊢ Integrable (fun y ↦ g (a✝, y)) ν →
    F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
⊢ Integrable (fun y ↦ g (a✝, y)) ν →
    F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
h2g

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f g : α × β → E
F : E → ℝ≥0∞
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y ↦ f (a✝, y)) ν
h2g : Integrable (fun y ↦ g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s < ∞
⊢ (μ.prod ν).real s • c = ∫ (x : α), ν.real (Prod.mk x ⁻¹' s) • c ∂μ

Tactic:
integral_smul_const,

Goal state after:
case pos.h_ind
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s < ∞
⊢ (μ.prod ν).real s • c = (∫ (x : α), ν.real (Prod.mk x ⁻¹' s) ∂μ) • c
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑π * I

Tactic:
suffices H : HasSum (fun n : ℕ => ∮ z in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹)
      (2 * π * I) by
    have A : CircleIntegrable (fun _ => (1 : ℂ)) c R := continuousOn_const.circleIntegrable'
    refine (H.unique ?_).symm
    simpa only [smul_eq_mul, mul_one, add_sub_cancel] using
      hasSum_two_pi_I_cauchyPowerSeries_integral A (mem_ball_iff_norm.1 hw)

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case neg.inl
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable f μ
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
simp [integral_undef h, integral_undef H]

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

Goal state before:
pp: case neg.inr
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable g ν
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
simp [integral_undef h, integral_undef H]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: case refine_4.refine_2
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E
s : Set (Fin (n + 1) → ℝ)
hs : s.Countable
Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x
Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x
i : Fin (n + 1)
Hc : ContinuousOn f (Box.Icc I)
fI : ℝ → Box (Fin n) → E := fun y J ↦ integral J GP (fun x ↦ f (i.insertNth y x)) BoxAdditiveMap.volume
fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x ↦ ⋯.toBoxAdditive
F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯
c : ℝ≥0
x : Fin (n + 1) → ℝ
hx : x ∈ Box.Icc I \ s
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε'0 : 0 < ε'
hlt : 2 * ↑c * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : closedBall x δ ∩ Box.Icc I ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (f' x) (x_2 - x)‖ ≤ ε' * ‖x_2 - x‖) x_1}
J : Box (Fin (n + 1))
hle : J ≤ I
hJδ : Box.Icc J ⊆ closedBall x δ
hxJ : x ∈ Box.Icc J
hJc : GP.bDistortion = true → J.distortion ≤ c
⊢ 2 * ε' * ↑c * ∏ j, (J.upper j - J.lower j) ≤ ε * (volume.toBoxAdditive.restrict ↑I ⋯) J

Tactic:
rw [mul_right_comm (2 : ℝ), ← Box.volume_apply]
      gcongr
      exacts [by dsimp; positivity, by simp]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
| p.coeff k

Tactic:
← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
| (C p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod).coeff k
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
s : Set ℂ
d : ∀ y ∈ s, DifferentiableAt ℂ f y
o : IsOpen s
m : c ∈ s
z : ℂ
⊢ z ∈ s → DifferentiableWithinAt ℂ f s z

Tactic:
m

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
d✝ : ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
s : Set ℂ
d : ∀ y ∈ s, DifferentiableAt ℂ f y
o : IsOpen s
m✝ : c ∈ s
z : ℂ
m : z ∈ s
⊢ DifferentiableWithinAt ℂ f s z
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case a
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
a : Finset ℂ := ⋯
b : Finset ℂ := ⋯
c : Finset ℂ := ⋯
ha : ∀ (z : ℂ), z ∈ a ↔ (aeval z) p = 0
z : ℂ
hz1 : (aeval z) p = 0
hz2 : z.im = 0
⊢ ((IsScalarTower.toAlgHom ℚ ℝ ℂ) z.re).im = z.im

Tactic:
· rw [hz2]; rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
this✝ : Algebra K ℂ := φ.toAlgebra
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }
⊢ ∃ σ, φ.comp ↑σ.symm = ψ

Tactic:
use (AlgHom.restrictNormal' ψ' K).symm

Goal state after:
case h
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ ψ : K →+* ℂ
h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)
this✝¹ : Algebra k ℂ := ⋯
this✝ : Algebra K ℂ := ⋯
this : IsScalarTower k K ℂ
ψ' : K →ₐ[k] ℂ := ⋯
⊢ φ.comp ↑(ψ'.restrictNormal' K).symm.symm = ψ
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: case mpr
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
⊢ Nonempty v.RankOne

Tactic:
have H : StrictMono (map' (rf.comp e)) := by
      refine map'_strictMono ?_
      intro a b h
      simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h

Goal state after:
case mpr
R : Type u_1
Γ₀ : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.IsNontrivial
a✝ : MulArchimedean (ofClass v).ValueGroup₀
f : Additive (ofClass v).ValueGroup₀ˣ →+o ℝ
hf : Injective ⇑f
e : (ofClass v).ValueGroup₀ˣ →* Multiplicative ℝ := AddMonoidHom.toMultiplicativeRight ↑f
he : StrictMono ⇑e
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  { toFun := fun x ↦ Units.mk0 (NNReal.mk (2 ^ (↑x).log) ⋯) ⋯, map_one' := ⋯, map_mul' := ⋯ }
H : StrictMono ⇑(map' (rf.comp e))
⊢ Nonempty v.RankOne
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
⊢ WithTop (Lex (σ →₀ ℕ))

Tactic:
by
  classical
  exact if h : φ = 0 then ⊤ else by
    have ne : Set.Nonempty (toLex '' φ.support) := (Function.support_nonempty_iff.mpr h).image _
    apply WithTop.some
    apply WellFounded.min _ (toLex '' φ.support) ne
    · exact Finsupp.instLTLex.lt
    · exact wellFounded_lt

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ ∑ p ∈ Finset.antidiagonal (p + q), (coeff p.1) φ * (coeff p.2) ψ = (coeff p) φ * (coeff q) ψ

Tactic:
Finset.sum_eq_single_of_mem ⟨p, q⟩ (by simp)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ (coeff (p, q).1) φ * (coeff (p, q).2) ψ = (coeff p) φ * (coeff q) ψ

σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
p q : σ →₀ ℕ
hp : φ.lexOrder = ↑(toLex p)
hq : ψ.lexOrder = ↑(toLex q)
⊢ ∀ b ∈ Finset.antidiagonal (p + q), b ≠ (p, q) → (coeff b.1) φ * (coeff b.2) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ ↑(toLex u)
⊢ ¬ψ.lexOrder ≤ ↑(toLex v)

Tactic:
hv

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
hu : φ.lexOrder ≤ ↑(toLex u)
hv : ψ.lexOrder ≤ ↑(toLex v)
⊢ False
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ ∃ z,
    𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z} ∧
      𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑z}

Tactic:
use min x y

Goal state after:
case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ 𝓟 {p | v.norm (p.1 - p.2) < ↑x} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑(min x y)} ∧
    𝓟 {p | v.norm (p.1 - p.2) < ↑y} ≥ 𝓟 {p | v.norm (p.1 - p.2) < ↑(min x y)}
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x y : { ε // ε > 0 }
⊢ (∀ (a b : L), v.norm (a - b) < ↑(min x y) → v.norm (a - b) < ↑x) ∧
    ∀ (a b : L), v.norm (a - b) < ↑(min x y) → v.norm (a - b) < ↑y

Tactic:
exact ⟨fun a b hab => lt_of_lt_of_le hab (min_le_left _ _), fun a b hab =>
            lt_of_lt_of_le hab (min_le_right _ _)⟩

Goal state after: