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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ P (⋃ m, ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n

Tactic:
simp only [h'', compl_iUnion, ge_iff_le]

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
seq : ℕ → α := denseSeq α
hseq_dense : DenseRange seq
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
htu : ∀ (i : ℕ), t i ∈ 𝓤 α
hto : ∀ (i : ℕ), IsOpen (t i)
a✝ : ∀ (i : ℕ), (t i).IsSymm
f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n ↦ s' n (δ n)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ P (⋂ i, ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
· have key := h _ (f.add_norm_nonneg)
    simp_rw [f.integral_add_const ‖f‖] at key
    simp only [probReal_univ, smul_eq_mul, one_mul] at key
    have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
    rwa [this, add_le_add_iff_right] at key

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ

pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (ball 0 (1 * 1) \ closedBall 0 (0 * 1)) = ↑(dim E) * μ (ball 0 1 \ {0})

pp: case ha
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 ≤ 0

pp: case hr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 < 1

Tactic:
<;>

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ ↑(dim E) * μ (ball 0 (1 * 1) \ closedBall 0 (0 * 1)) = ↑(dim E) * μ (ball 0 1 \ {0})

case ha
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 ≤ 0

case hr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case zero
h : 0 ≠ 0
⊢ nthRoot 0 0 = 0

pp: case succ.zero
h : 0 + 1 ≠ 0
⊢ (0 + 1).nthRoot 0 = 0

pp: case succ.succ
n✝ : ℕ
h : n✝ + 1 + 1 ≠ 0
⊢ (n✝ + 1 + 1).nthRoot 0 = 0

Tactic:
<;>

Goal state after:
case zero
h : 0 ≠ 0
⊢ nthRoot 0 0 = 0

case succ.zero
h : 0 + 1 ≠ 0
⊢ (0 + 1).nthRoot 0 = 0

case succ.succ
n✝ : ℕ
h : n✝ + 1 + 1 ≠ 0
⊢ (n✝ + 1 + 1).nthRoot 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case zero
⊢ nthRoot 0 1 = 1

pp: case succ.zero
⊢ (0 + 1).nthRoot 1 = 1

pp: case succ.succ
n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot 1 = 1

Tactic:
<;>

Goal state after:
case zero
⊢ nthRoot 0 1 = 1

case succ.zero
⊢ (0 + 1).nthRoot 1 = 1

case succ.succ
n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case zero
a : ℕ
⊢ nthRoot 0 a ^ 0 ≤ a ↔ 0 ≠ 0 ∨ a ≠ 0

pp: case succ.zero
a : ℕ
⊢ (0 + 1).nthRoot a ^ (0 + 1) ≤ a ↔ 0 + 1 ≠ 0 ∨ a ≠ 0

pp: case succ.succ
a n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot a ^ (n✝ + 1 + 1) ≤ a ↔ n✝ + 1 + 1 ≠ 0 ∨ a ≠ 0

Tactic:
<;>

Goal state after:
case zero
a : ℕ
⊢ nthRoot 0 a ^ 0 ≤ a ↔ 0 ≠ 0 ∨ a ≠ 0

case succ.zero
a : ℕ
⊢ (0 + 1).nthRoot a ^ (0 + 1) ≤ a ↔ 0 + 1 ≠ 0 ∨ a ≠ 0

case succ.succ
a n✝ : ℕ
⊢ (n✝ + 1 + 1).nthRoot a ^ (n✝ + 1 + 1) ≤ a ↔ n✝ + 1 + 1 ≠ 0 ∨ a ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case inl
a : ℕ
⊢ (∃ x, x ^ 0 = a) ↔ 0 = 0 ∧ a = 1 ∨ 0 ≠ 0 ∧ nthRoot 0 a ^ 0 = a

pp: case inr
n a : ℕ
h✝ : n ≠ 0
⊢ (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a

Tactic:
<;>

Goal state after:
case inl
a : ℕ
⊢ (∃ x, x ^ 0 = a) ↔ 0 = 0 ∧ a = 1 ∨ 0 ≠ 0 ∧ nthRoot 0 a ^ 0 = a

case inr
n a : ℕ
h✝ : n ≠ 0
⊢ (∃ x, x ^ n = a) ↔ n = 0 ∧ a = 1 ∨ n ≠ 0 ∧ n.nthRoot a ^ n = a
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

pp: case hx
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖↑x‖ = 1

pp: case hε
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

pp: case hε2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2

Tactic:
<;>

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

case hx
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖↑x‖ = 1

case hε
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

case hε2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

pp: case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2 + 0 = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

Tactic:
<;>

Goal state after:
case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + (1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2) = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2 + 0 = 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: case pos
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
hxr : x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

pp: case neg
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
hxr : ¬x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

Tactic:
<;>

Goal state after:
case pos
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
hxr : x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x

case neg
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r x : ℝ
hx : 0 < x
hxr : ¬x < r
⊢ (fun y ↦ y ^ (dim E - 1) • (Iio r).indicator f y) x = (Ioo 0 r).indicator (fun y ↦ y ^ (dim E - 1) • f y) x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_a.e_z
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) + ↑l = ↑l / 2

pp: case e_a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ 1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2 =
    1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)

Tactic:
<;>

Goal state after:
case e_a.e_z
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ -(↑l / 2) + ↑l = ↑l / 2

case e_a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ 1 / ↑⟨l₀, hl₀⟩ ^ 2 - 1 / (-(↑l / 2) + ↑l - ↑⟨l₀, hl₀⟩) ^ 2 =
    1 / ↑⟨-(l₀ - ↑l), ⋯⟩ ^ 2 - 1 / (↑l / 2 - ↑⟨-(l₀ - ↑l), ⋯⟩) ^ 2 + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
have hl0 : l ≠ 0 := by rintro rfl; simp at hl

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
⊢ ℘[L] (z + ↑l) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ eval (cos θ) (T ℂ (↑n + 2)) = cos (↑(↑n + 2) * θ)

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]

Goal state after:
case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ 2 * cos θ * cos (↑(↑n + 1) * θ) = 2 * cos ((↑(↑n + 2) * θ + ↑↑n * θ) / 2) * cos ((↑(↑n + 2) * θ - ↑↑n * θ) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case inl
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
i : ℂ
⊢ ℘[L] (i + L.ω₁) = ℘[L] i

Tactic:
exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ ℘'[L - ↑l₀] z - 2 / (z - ↑l₀) ^ 3 = ℘'[L - ↑l₀] z + ∑' (i : ↥L.lattice), if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0

Tactic:
simp [sub_eq_add_neg, neg_div]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + -2 / (z - ↑l₀) ^ 3 = -(2 / (z - ↑w) ^ 3)

pp: case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ -2 / (z - ↑w) ^ 3 + 0 = -(2 / (z - ↑w) ^ 3)

Tactic:
<;>

Goal state after:
case pos
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ↑w = ↑l₀
⊢ 0 + -2 / (z - ↑l₀) ^ 3 = -(2 / (z - ↑w) ^ 3)

case neg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
h✝ : ¬↑w = ↑l₀
⊢ -2 / (z - ↑w) ^ 3 + 0 = -(2 / (z - ↑w) ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / 0) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
div_zero

Goal state after:
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / 0) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
div_zero

Goal state after:
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ω arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case e'_9
h : 1 ≠ -1
⊢ 1 / √(1 - 1 ^ 2) = 0

pp: case inl.convert_3
h : 1 ≠ -1
⊢ ∀ x ∈ Ici 1, arcsin x = π / 2

pp: case inl.convert_4
h : 1 ≠ -1
⊢ arcsin 1 = π / 2

Tactic:
<;>

Goal state after:
case e'_9
h : 1 ≠ -1
⊢ 1 / √(1 - 1 ^ 2) = 0

case inl.convert_3
h : 1 ≠ -1
⊢ ∀ x ∈ Ici 1, arcsin x = π / 2

case inl.convert_4
h : 1 ≠ -1
⊢ arcsin 1 = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case e'_9
h : -1 ≠ 1
⊢ 1 / √(1 - (-1) ^ 2) = 0

pp: case inl.convert_3
h : -1 ≠ 1
⊢ ∀ x ∈ Iic (-1), arcsin x = -(π / 2)

pp: case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)

Tactic:
<;>

Goal state after:
case e'_9
h : -1 ≠ 1
⊢ 1 / √(1 - (-1) ^ 2) = 0

case inl.convert_3
h : -1 ≠ 1
⊢ ∀ x ∈ Iic (-1), arcsin x = -(π / 2)

case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ ↑0! / 0 = 0

Tactic:
div_zero

Goal state after:
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg.inl
⊢ 0 = 1 / √(1 - (-1) ^ 2)

pp: case neg.inr
⊢ 0 = 1 / √(1 - 1 ^ 2)

Tactic:
<;>

Goal state after:
case neg.inl
⊢ 0 = 1 / √(1 - (-1) ^ 2)

case neg.inr
⊢ 0 = 1 / √(1 - 1 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case refine_1
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x

pp: case refine_2
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x

Tactic:
<;>

Goal state after:
case refine_1
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x

case refine_2
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

pp: case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

pp: case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

Tactic:
<;>

Goal state after:
case succ.hx
n✝ : ℕ
⊢ 0 < 2 * ↑(n✝ + 1)

case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case zero
⊢ 1 / (12 * ↑0 * (↑0 + 1)) ≤ 1 / (4 * ↑0 ^ 2)

pp: case succ
n✝ : ℕ
⊢ 1 / (12 * ↑(n✝ + 1) * (↑(n✝ + 1) + 1)) ≤ 1 / (4 * ↑(n✝ + 1) ^ 2)

Tactic:
<;>

Goal state after:
case zero
⊢ 1 / (12 * ↑0 * (↑0 + 1)) ≤ 1 / (4 * ↑0 ^ 2)

case succ
n✝ : ℕ
⊢ 1 / (12 * ↑(n✝ + 1) * (↑(n✝ + 1) + 1)) ≤ 1 / (4 * ↑(n✝ + 1) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

pp: n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 0 ≤ 2

pp: n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0

Tactic:
<;>

Goal state after:
n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 0 ≤ 2

n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case hx
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
<;>

Goal state after:
case hx
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)

Tactic:
suffices (∑ i ∈ range n, exp ((k * ((2 * i + 1) / (2 * n) * π)) * I)) *
    exp (-(k / (2 * n) * π * I)) * (exp (k / n * π * I) - 1) = (-1) ^ k - 1 by
    rw [Complex.exp_neg] at this
    have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
    apply hf this (Complex.exp_ne_zero _) (by grind [exp_sub_one_ne_zero])
  convert! geom_sum_mul (exp (k / n * π * I)) n using 1
  · simp_rw [sum_mul]
    congr! 1 with i hi
    rw [← Complex.exp_nat_mul, ← Complex.exp_add]
    grind
  · rw [← Complex.exp_nat_mul,
      show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
      Complex.exp_int_mul, Complex.exp_pi_mul_I]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ -2 ≤ ↑k

pp: case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ ↑k ≤ 2

Tactic:
<;>

Goal state after:
case left
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ -2 ≤ ↑k

case right
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ ↑k ≤ 2