harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem exp_polynomial_approx_aux (f : ℤ[X]) (s : ℂ) :
    ∃ c ≥ 0,
      ∀ p ≠ 0, ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Proof state:
f : ℤ[X]
s : ℂ
h :
  (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1 ⊆
    (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Icc 0 1
⊢ Continuous fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖

Tactic:
fun_prop

Result:
no goals

Proof state:
case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : ¬x * ‖s‖ ≤ 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Tactic:
push_neg at hx1

Result:
case neg
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
h : |(x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖| ≤ c
hx1 : 1 < x * ‖s‖
⊢ (x * ‖s‖) ^ (p - 1) ≤ (x * ‖s‖) ^ p

Proof state:
f : ℤ[X]
s : ℂ
h :
  (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1 ⊆
    (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Icc 0 1
⊢ Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)

Tactic:
refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h

Result:
f : ℤ[X]
s : ℂ
h :
  (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1 ⊆
    (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Icc 0 1
⊢ Continuous fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖

Proof state:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, ‖x‖ ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
simp_rw [Real.norm_eq_abs] at h

Result:
case intro
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Proof state:
f : ℤ[X]
s : ℂ
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
have : Bornology.IsBounded
    ((fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1) := by
  have h :
    (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1 ⊆
      (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Icc 0 1 :=
    Set.image_subset _ Set.Ioc_subset_Icc_self
  refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h
  fun_prop

Result:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x => (x * ‖s‖ ⊔ 1) * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖LindemannWeierstrass.P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_succ_const (n : ℕ) (c : F) :
    iteratedFDerivWithin 𝕜 (n + 1) (fun _ : E ↦ c) s = 0

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
n : ℕ
IH : iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 0 s = 0

Tactic:
simp only [Pi.zero_def, comp_def, fderivWithin_const, map_zero]

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
⊢ iteratedFDerivWithin 𝕜 (0 + 1) (fun x => c) s = 0

Tactic:
ext1

Result:
case zero.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
x✝ : E
⊢ iteratedFDerivWithin 𝕜 (0 + 1) (fun x => c) s x✝ = 0 x✝

Proof state:
case zero.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
x✝ : E
⊢ iteratedFDerivWithin 𝕜 (0 + 1) (fun x => c) s x✝ = 0 x✝

Tactic:
simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
n : ℕ
c : F
⊢ iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0

Tactic:
induction n  with
| zero =>
  ext1
  simp [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp, comp_def]
| succ n IH =>
  rw [iteratedFDerivWithin_succ_eq_comp_left, IH]
  simp only [Pi.zero_def, comp_def, fderivWithin_const, map_zero]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
n : ℕ
IH : iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0
⊢ iteratedFDerivWithin 𝕜 (n + 1 + 1) (fun x => c) s = 0

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left, IH]

Result:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
c : F
n : ℕ
IH : iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s = 0
⊢ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 0 s = 0
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem comp_assoc {δ : Type*} {mδ : MeasurableSpace δ} (ξ : Kernel γ δ)
    (η : Kernel β γ) (κ : Kernel α β) : ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
⊢ ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)

Tactic:
refine ext_fun fun a f hf => ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a

Tactic:
simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel]

Result:
no goals
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
private lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
    (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
    {n : ℕ} (v : Fin n → E) (h's : s ⊆ EMetric.ball x r) :
    iteratedFDerivWithin 𝕜 n f s x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ EMetric.ball x r
I : insert x s ∩ EMetric.ball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z => (p n) fun x_1 => z - x
⊢ ContDiff 𝕜 ω g

Tactic:
apply (p n).contDiff.comp

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ EMetric.ball x r
I : insert x s ∩ EMetric.ball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z => (p n) fun x_1 => z - x
⊢ ContDiff 𝕜 ω fun z x_1 => z - x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ EMetric.ball x r
I : insert x s ∩ EMetric.ball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z => (p n) fun x_1 => z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k => if h : n = k then h ▸ p n else 0
m : ℕ
hm : n + 1 ≤ m
⊢ n ≠ m

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma isOfFinOrder_iff_zpow_eq_one {G} [Group G] {x : G} :
    IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1

Proof state:
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
⊢ x ^ n.natAbs = 1

Tactic:
rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h

Result:
case inl
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

case inr
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Proof state:
G : Type u_6
inst✝ : Group G
x : G
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Tactic:
refine ⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.natCast_ne_zero_iff_pos.mpr hn, zpow_natCast x n ▸ hn'⟩,
  fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩

Result:
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
⊢ x ^ n.natAbs = 1

Proof state:
case inl
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_natCast] at hn'

Result:
no goals

Proof state:
G : Type u_6
inst✝ : Group G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Tactic:
rw [isOfFinOrder_iff_pow_eq_one]

Result:
G : Type u_6
inst✝ : Group G
x : G
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Proof state:
case inr
G : Type u_6
inst✝ : Group G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp] lemma toNNReal_rpow (x : ℝ≥0∞) (z : ℝ) : (x ^ z).toNNReal = x.toNNReal ^ z

Proof state:
case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
simp [← coe_rpow_of_ne_zero hx]

Result:
no goals

Proof state:
case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
cases x

Result:
case inr.inr.top
z : ℝ
H : 0 < z
⊢ (⊤ ^ z).toNNReal = ⊤.toNNReal ^ z

case inr.inr.coe
z : ℝ
H : 0 < z
x✝ : ℝ≥0
⊢ (↑x✝ ^ z).toNNReal = (↑x✝).toNNReal ^ z

Proof state:
case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
simp [H]

Result:
no goals

Proof state:
case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
simp [hx, H, ne_of_lt]

Result:
no goals

Proof state:
case inr.inr.top
z : ℝ
H : 0 < z
⊢ (⊤ ^ z).toNNReal = ⊤.toNNReal ^ z

Tactic:
simp [H, ne_of_gt]

Result:
no goals

Proof state:
case inl.top
z : ℝ
H : z < 0
⊢ (⊤ ^ z).toNNReal = ⊤.toNNReal ^ z

Tactic:
simp [H, ne_of_lt]

Result:
no goals

Proof state:
case inr.inr.coe
z : ℝ
H : 0 < z
x✝ : ℝ≥0
⊢ (↑x✝ ^ z).toNNReal = (↑x✝).toNNReal ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt H)]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
rcases lt_trichotomy z 0 with (H | H | H)

Result:
case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Proof state:
case inl.coe
z : ℝ
H : z < 0
x : ℝ≥0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

Tactic:
by_cases hx : x = 0

Result:
case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z

case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ (↑x ^ z).toNNReal = (↑x).toNNReal ^ z
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_spec (n : ℕ) :
    (∑ k ∈ range n.succ, (n.choose (n - k) : ℚ) / (n - k + 1) * bernoulli' k) = 1

Proof state:
n x : ℕ
hx : x ∈ range n
⊢ ↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x = 0

Tactic:
rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ k ∈ range n.succ, ↑(n.choose (n - k)) / (↑n - ↑k + 1) * bernoulli' k = 1

Tactic:
rw [sum_range_succ_comm, bernoulli'_def n, tsub_self, choose_zero_right, sub_self, zero_add,
  div_one, cast_one, one_mul, sub_add, ← sum_sub_distrib, ← sub_eq_zero, sub_sub_cancel_left,
  neg_eq_zero]

Result:
n : ℕ
⊢ ∑ x ∈ range n, (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) = 0

Proof state:
n : ℕ
⊢ ∑ x ∈ range n, (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) = 0

Tactic:
exact Finset.sum_eq_zero (fun x hx => by rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self])

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma mem_liminf_iff_eventually_mem : (a ∈ liminf s 𝓕) ↔ (∀ᶠ i in 𝓕, a ∈ s i)

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simpa only [liminf_eq_iSup_iInf, iSup_eq_iUnion, iInf_eq_iInter, mem_iUnion, mem_iInter]
  using ⟨fun ⟨S, hS, hS'⟩ ↦ mem_of_superset hS (by tauto), fun h ↦ ⟨{i | a ∈ s i}, h, by tauto⟩⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
h : ∀ᶠ (i : ι) in 𝓕, a ∈ s i
⊢ ∀ i ∈ {i | a ∈ s i}, a ∈ s i

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
x✝ : ∃ i, ∃ (_ : i ∈ 𝓕), ∀ i_1 ∈ i, a ∈ s i_1
S : Set ι
hS : S ∈ 𝓕
hS' : ∀ i ∈ S, a ∈ s i
⊢ S ⊆ {x | (fun i => a ∈ s i) x}

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fract_fract (m : E) : fract b (fract b m) = fract b m :=
  Basis.ext_elem b fun _ => by classical simp only [repr_fract_apply, Int.fract_fract]

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ (b.repr (fract b (fract b m))) x✝ = (b.repr (fract b m)) x✝

Tactic:
classical simp only [repr_fract_apply, Int.fract_fract]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ (b.repr (fract b (fract b m))) x✝ = (b.repr (fract b m)) x✝

Tactic:
simp only [repr_fract_apply, Int.fract_fract]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Ioi_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
    f.measure (Ioi x) = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
⊢ f.measure (Ioi x) = ⊤

Tactic:
refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
r : ℝ≥0
⊢ ↑r ≤ f.measure (Ioi x)

Proof state:
case intro
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
r : ℝ≥0
N : ℝ
hN : ∀ b ≥ N, ↑r + ↑f x ≤ ↑f b
⊢ ↑r ≤ f.measure (Ioi x)

Tactic:
exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
  le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self)

Result:
no goals

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
r : ℝ≥0
⊢ ↑r ≤ f.measure (Ioi x)

Tactic:
obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))

Result:
case intro
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
x : ℝ
r : ℝ≥0
N : ℝ
hN : ∀ b ≥ N, ↑r + ↑f x ≤ ↑f b
⊢ ↑r ≤ f.measure (Ioi x)
-- Mathlib/Algebra/Group/End.lean
@[simp] lemma pow_addLeft (n : ℕ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a)

Proof state:
case H
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.addLeft a ^ n) x✝ = (Equiv.addLeft (n • a)) x✝

Tactic:
simp [Perm.coe_pow]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
⊢ Equiv.addLeft a ^ n = Equiv.addLeft (n • a)

Tactic:
ext

Result:
case H
α : Type u_4
inst✝ : AddGroup α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.addLeft a ^ n) x✝ = (Equiv.addLeft (n • a)) x✝
-- Mathlib/Algebra/Category/MonCat/Colimits.lean
theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
    F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Proof state:
case hf.h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Result:
case hf.h.a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Proof state:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
ext

Result:
case hf.h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Proof state:
case hf.h.a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Tactic:
apply Relation.map

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_mem {f : R →+* S} {p : MvPolynomial σ R} {s : subS}
    (hs : ∀ i ∈ p.support, f (p.coeff i) ∈ s) {v : σ → S} (hv : ∀ i, v i ∈ s) :
    MvPolynomial.eval₂ f v p ∈ s

Proof state:
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ ∀ (i : σ →₀ ℕ), f (coeff i p) ∈ s

Tactic:
intro i

Result:
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
⊢ f (coeff i p) ∈ s

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ f (coeff i p) ∈ s

Tactic:
rw [MvPolynomial.not_mem_support_iff.1 hi, f.map_zero]

Result:
case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, f (coeff i p) ∈ s
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ 0 ∈ s

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
i : σ →₀ ℕ
h : ¬a = i
this : f✝ (0 + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
rwa [zero_add] at this

Result:
no goals

Proof state:
case h_add_weak.refine_1
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : (σ →₀ ℕ) →₀ R
ha : a ∉ f.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    f✝
        (coeff i
          ((let_fun this := (monomial a) b;
            this) +
            f)) ∈
      s
this :
  f✝
      (coeff a
        ((let_fun this := (monomial a) b;
          this) +
          f)) ∈
    s
⊢ f✝ b ∈ s

Tactic:
rwa [coeff_add, MvPolynomial.not_mem_support_iff.1 ha, add_zero, coeff_monomial,
  if_pos rfl] at this

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_ge_inv_of_tendsto {r : ℝ≥0} (hr : r ≠ 0)
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
      (ofScalars E c).radius ≥ ofNNReal r⁻¹

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
⊢ (ofScalars E c).radius ≥ ↑r⁻¹

Tactic:
refine le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : ↑r' < ↑r⁻¹
⊢ ↑r' ≤ (ofScalars E c).radius

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : r' = 0
⊢ ↑r' ≤ (ofScalars E c).radius

Tactic:
simp [hrz]

Result:
no goals

Proof state:
case neg.hs.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * ↑r' ^ n‖ ≠ 0

Tactic:
refine (hc.eventually_ne (NNReal.coe_ne_zero.mpr hr)).mp (Eventually.of_forall ?_)

Result:
case neg.hs.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ (x : ℕ), ‖c x.succ‖ / ‖c x‖ ≠ 0 → ‖‖c x‖ * ↑r' ^ x‖ ≠ 0

Proof state:
case neg.hs.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n => ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ((fun a => ↑a) (r' * r)))

Tactic:
simp_rw [norm_norm]

Result:
case neg.hs.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n => ‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖ / ‖‖c n‖ * ↑r' ^ n‖) atTop (𝓝 ↑(r' * r))