mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
pt : p ∈ closedBall x t ×ˢ closedBall x t
hp : IsMaxOn (fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) (closedBall x t ×ˢ closedBall x t) p
⊢ ∃ b < s * r, ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b

Tactic:
simp only [mem_prod, mem_closedBall] at pt

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
B : Continuous[instTopologicalSpaceProd, _] fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖
C : (closedBall x t ×ˢ closedBall x t).Nonempty
p : E × E
hp : IsMaxOn (fun p ↦ ‖f a p.2 - f a p.1 - (L p.2 - L p.1)‖) (closedBall x t ×ˢ closedBall x t) p
pt : dist p.1 x ≤ t ∧ dist p.2 x ≤ t
⊢ ∃ b < s * r, ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|

Tactic:
abs_intervalIntegral_eq

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
ι : Type u_8
s : Finset ι
f : ι → ℝ → E
h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b
⊢ ∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_finsetSum s fun i hi => (h i hi).def',
    Finset.smul_sum]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (c * x - d) = c⁻¹ • ∫ (x : ℝ) in c * a - d..c * b - d, f x

Tactic:
by
  simpa only [sub_eq_add_neg] using integral_comp_mul_add f hc (-d)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case h
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := ⋯
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
⊢ (fun x ↦ y) ≤ᵐ[volume.restrict (Icc t u)] fun x ↦ (G' x).toReal

Tactic:
have C1 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), G' x < ∞ :=
              ae_mono (Measure.restrict_mono I le_rfl) G'lt_top
            have C2 : ∀ᵐ x : ℝ ∂volume.restrict (Icc t u), x ∈ Icc t u :=
              ae_restrict_mem measurableSet_Icc
            filter_upwards [C1, C2] with x G'x hx
            apply EReal.coe_le_coe_iff.1
            have : x ∈ Ioo m M := by
              simp only [hm.trans_le hx.left,
                (hx.right.trans_lt hu.right).trans_le (min_le_left M b), mem_Ioo, and_self_iff]
            refine (H this).out.le.trans_eq ?_
            exact (EReal.coe_toReal G'x.ne (f_lt_G' x).ne_bot).symm

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₂
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ‖f a z - f a y - (L z - L y)‖ ≤ b

Tactic:
· simp [hb, dyx, dzx]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a 0..a n, f x ∂μ

Tactic:
exact sum_integral_adjacent_intervals_Ico zero_le fun k hk => hint k hk.2

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ =
    ∫ (x : ℝ) in a..c, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ

Tactic:
add_assoc,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in c..d, f x ∂μ =
    ∫ (x : ℝ) in a..c, f x ∂μ + (∫ (x : ℝ) in c..d, f x ∂μ + ∫ (x : ℝ) in c..b, f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ 0 ≤ᵐ[μ.restrict (Ioc a b)] fun x ↦ g x - f x

pp: case hfi
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hfi : IntervalIntegrable f μ a b
hgi : IntervalIntegrable g μ a b
hle : f ≤ᵐ[μ.restrict (Ioc a b)] g
hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0
⊢ Integrable (fun x ↦ g x - f x) (μ.restrict (Ioc a b))

Tactic:
exacts [hle.mono fun x => sub_nonneg.2, hgi.1.sub hfi.1]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: a : ℝ
⊢ ¬IntegrableOn (fun x ↦ x⁻¹) (Ici a) volume

Tactic:
have A : ∀ᶠ x in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x := by
    filter_upwards [Ioi_mem_atTop 0] with x hx using Real.hasDerivAt_log (ne_of_gt hx)

Goal state after:
a : ℝ
A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x ↦ Real.log x) x⁻¹ x
⊢ ¬IntegrableOn (fun x ↦ x⁻¹) (Ici a) volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b

Tactic:
← (AddCircle.measurePreserving_mk T t).map_eq

Goal state after:
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ) in Ioc t (t + T), f ↑a =
    ∫⁻ (b : AddCircle T), f b ∂Measure.map QuotientAddGroup.mk (volume.restrict (Ioc t (t + T)))
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case ctop
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := ⋯
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) ≠ ∞

Tactic:
change ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤

Goal state after:
case ctop
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := PositiveCompacts.map QuotientGroup.mk ⋯ ⋯ K
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ ν (QuotientGroup.mk ⁻¹' QuotientGroup.mk '' ↑K ∩ s) ≠ ∞
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h₁
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ (q, x) ∈ {q} ×ˢ Icc a b

Tactic:
simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]

Goal state after:
case h₁
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ x ∈ Icc a b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : ℝ → E
⊢ ∫ (a : AddCircle T), liftIoc T t f a = ∫ (a : ℝ) in t..t + T, f a

Tactic:
rw [← AddCircle.intervalIntegral_preimage T t]
  apply intervalIntegral.integral_congr_ae
  refine .of_forall fun x hx ↦ ?_
  rw [uIoc_of_le (by linarith [hT.out])] at hx
  rw [liftIoc_coe_apply hx]

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : NormedSpace ℂ E
hf : IntegrableOn (fun θ ↦ f (circleMap c R θ)) (Ι 0 (2 * π)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ι 0 (2 * π)), ‖(circleMap 0 R a * I) • f (circleMap c R a)‖ ≤ |R| * ‖f (circleMap c R a)‖

Tactic:
simp [norm_smul]

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

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

Tactic:
by_cases h₀ : R = 0
  · simp +unfoldPartialApp [h₀, const]
  refine ⟨fun h => h.out, fun h => ?_⟩
  simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢
  refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_
  · have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
    simpa only [inv_smul_smul₀ H]
      using ((continuous_circleMap 0 R).aestronglyMeasurable.mul_const
        I).aemeasurable.fun_inv.aestronglyMeasurable.fun_smul h.aestronglyMeasurable
  · simp [norm_smul, h₀]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst✝ : IsFiniteMeasure ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ AEStronglyMeasurable f (Measure.map Prod.fst (μ.prod ν))

Tactic:
· simpa using hf'.1

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ AEStronglyMeasurable f (Measure.map Prod.snd (μ.prod ν))

Tactic:
· simpa using hf'.1

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h₀ : 0 < ∫ (x : ℝ) in 0..T, g x
hT : 0 < T
h_int : IntervalIntegrable g volume 0 T
⊢ Tendsto (fun x ↦ ⌊x / T⌋) atTop atTop

Tactic:
exact tendsto_floor_atTop.comp (tendsto_id.atTop_mul_const (inv_pos.mpr hT))

Goal state after:
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 ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)

Tactic:
rw [← and_congr_right_iff, and_iff_right_of_imp h1]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C
θ : ℝ
x✝ : θ ∈ Ι 0 (2 * π)
⊢ ‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖

Tactic:
simp [norm_smul]

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

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

Tactic:
have hR : 0 < R := dist_nonneg.trans_lt hw
  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)
  have H : ∀ n : ℕ, n ≠ 0 → (∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ)) = 0 := by
    refine fun n hn => integral_sub_zpow_of_ne ?_ _ _ _; simpa
  have : (∮ z in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹) = 2 * π * I := by simp [hR.ne']
  refine this ▸ hasSum_single _ fun n hn => ?_
  simp only [div_eq_mul_inv, mul_pow, integral_const_mul, mul_assoc]
  rw [(integral_congr hR.le fun z hz => _).trans (H n hn), mul_zero]
  intro z _
  rw [← pow_succ, ← zpow_natCast, inv_zpow, ← zpow_neg, Int.natCast_succ, neg_add,
    sub_eq_add_neg _ (1 : ℤ)]

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

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
n : ℕ
⊢ IsClosedMap fun x ↦ x ^ n

Tactic:
by
  simpa [eval_X_pow] using (X ^ n).isClosedMap_eval

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

Goal state before:
pp: case mpr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ (∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z) → AnalyticAt ℂ f c

Tactic:
· intro d
    rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩
    have h : AnalyticOnNhd ℂ f s := by
      refine DifferentiableOn.analyticOnNhd ?_ o
      intro z m
      exact (d z m).differentiableWithinAt
    exact h _ m

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ dist y z ≤ dist x z

Tactic:
apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left

Goal state after:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h✝ : dist x y ≠ dist y z
h : dist x y < dist y z
⊢ ¬dist y z ≤ dist y x
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : valuation.restrict x ≠ 0
⊢ False

Tactic:
← isUnit_iff_ne_zero

Goal state after:
case neg
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : Subsingleton (ofClass valuation).ValueGroup₀ˣ
x : K
hx : valuation.restrict x < 1
hx0 : IsUnit (valuation.restrict x)
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ (coeff e) x * constantCoeff φ = ∑ p ∈ antidiagonal e, (coeff p.1) x * (coeff p.2) φ

Tactic:
Finset.sum_eq_single (e, 0),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ (coeff e) x * constantCoeff φ = (coeff (e, 0).1) x * (coeff (e, 0).2) φ

case h₀
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ ∀ b ∈ antidiagonal e, b ≠ (e, 0) → (coeff b.1) x * (coeff b.2) φ = 0

case h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
hφ : constantCoeff φ ∈ nonZeroDivisorsRight R
x : MvPowerSeries σ R
hx : x * φ = 0
d e : σ →₀ ℕ
he : ∀ y < e, (coeff y) x = (coeff y) 0
⊢ (e, 0) ∉ antidiagonal e → (coeff (e, 0).1) x * (coeff (e, 0).2) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ ≠ 0
⊢ φ * φ⁻¹ = 1

Tactic:
← invOfUnit_eq φ h,

Goal state after:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ ≠ 0
⊢ φ * φ.invOfUnit (Units.mk0 (constantCoeff φ) h) = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
rw [isElliptic_iff, ofJNe0Or1728_Δ]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (j ^ 2 * (j - 1728) ^ 9)
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
⊢ f = g

Tactic:
ext x
  apply induction_on I M x (fun a ↦ LinearMap.ext_iff.mp h a)

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
⊢ (P.reindex e f).jacobian = P.jacobian

Tactic:
cases nonempty_fintype σ
  cases nonempty_fintype σ'
  simp_rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
  simp only [reindex_toPresentation, Presentation.reindex_toGenerators, jacobiMatrix_reindex,
    Matrix.reindex_apply, Equiv.symm_symm, Generators.algebraMap_apply, Generators.reindex_val]
  simp_rw [← MvPolynomial.aeval_rename,
    ← AlgHom.mapMatrix_apply, ← Matrix.det_submatrix_equiv_self f, AlgHom.map_det,
    AlgHom.mapMatrix_apply, Matrix.map_map]
  simp [← AlgHom.coe_comp, rename_comp_rename, rename_id]

Goal state after: