harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integrableOn_Ioi_deriv_norm_ofReal_cpow {s : ℂ} {t : ℝ} (ht : 0 < t) (hs : s.re ≤ 0):
    IntegrableOn (deriv fun x : ℝ ↦ ‖(x : ℂ) ^ s‖) (Set.Ioi t)

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
x : ℝ
hx : x ∈ Ioi t
⊢ deriv (fun x => ‖↑x ^ s‖) x = ?m.40982 x

Tactic:
rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]

Result:
no goals

Proof state:
case inl
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
simp_rw [hs, zero_mul]

Result:
case inl
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (fun x => 0) (Ioi t) volume

Proof state:
case inl
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (fun x => 0) (Ioi t) volume

Tactic:
exact integrableOn_zero

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ s.re - 1 < -1

Tactic:
rwa [sub_lt_iff_lt_add, neg_add_cancel]

Result:
no goals

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (deriv fun x => ‖↑x ^ s‖) (Ioi t) volume

Tactic:
rw [integrableOn_congr_fun (fun x hx ↦ by
  rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]

Result:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Proof state:
case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
replace hs : s.re - 1 < - 1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]

Result:
case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re - 1 < -1
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Proof state:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
obtain hs | hs := eq_or_lt_of_le hs

Result:
case inl
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Proof state:
case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re - 1 < -1
⊢ IntegrableOn (fun x => s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
exact (integrableOn_Ioi_rpow_of_lt hs ht).const_mul s.re

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive mul_zsmul]
lemma zpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
rw [Int.mul_comm, zpow_mul]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem succ'_pred' (n) : succ' (pred' n) = n :=
  to_nat_inj.1 <| by
    rw [succ'_to_nat, pred'_to_nat, Nat.add_one, Nat.succ_pred_eq_of_pos (to_nat_pos _)]

Proof state:
n : PosNum
⊢ ↑n.pred'.succ' = ↑n

Tactic:
rw [succ'_to_nat, pred'_to_nat, Nat.add_one, Nat.succ_pred_eq_of_pos (to_nat_pos _)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_neg_nat_eq_zero (n : ℕ) : Gamma (-n) = 0

Proof state:
case succ
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
rw [this, Gamma_add_one _ A] at IH

Result:
case succ
n : ℕ
IH : -↑n.succ * Gamma (-↑n.succ) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0

Proof state:
n : ℕ
IH : Gamma (-↑n) = 0
⊢ n.succ ≠ 0

Tactic:
apply Nat.succ_ne_zero

Result:
no goals

Proof state:
case succ
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
have : -(n : ℂ) = -↑n.succ + 1 := by simp

Result:
case succ
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0

Proof state:
case succ
n : ℕ
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
IH : Gamma (-↑(n + 1)) ≠ 0
⊢ -↑n.succ * Gamma (-↑n.succ) ≠ 0

Tactic:
exact mul_ne_zero A IH

Result:
no goals

Proof state:
case succ
n : ℕ
IH : Gamma (-↑n) = 0
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
have A : -(n.succ : ℂ) ≠ 0 := by
  rw [neg_ne_zero, Nat.cast_ne_zero]
  apply Nat.succ_ne_zero

Result:
case succ
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
⊢ Gamma (-↑(n + 1)) = 0

Proof state:
case succ
n : ℕ
IH : -↑n.succ * Gamma (-↑n.succ) = 0
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
⊢ Gamma (-↑(n + 1)) = 0

Tactic:
contrapose! IH

Result:
case succ
n : ℕ
A : -↑n.succ ≠ 0
this : -↑n = -↑n.succ + 1
IH : Gamma (-↑(n + 1)) ≠ 0
⊢ -↑n.succ * Gamma (-↑n.succ) ≠ 0

Proof state:
case zero

⊢ Gamma (-↑0) = 0

Tactic:
rw [Nat.cast_zero, neg_zero, Gamma_zero]

Result:
no goals

Proof state:
n : ℕ
⊢ Gamma (-↑n) = 0

Tactic:
induction n with
| zero => rw [Nat.cast_zero, neg_zero, Gamma_zero]
| succ n IH =>
  have A : -(n.succ : ℂ) ≠ 0 := by
    rw [neg_ne_zero, Nat.cast_ne_zero]
    apply Nat.succ_ne_zero
  have : -(n : ℂ) = -↑n.succ + 1 := by simp
  rw [this, Gamma_add_one _ A] at IH
  contrapose! IH
  exact mul_ne_zero A IH

Result:
no goals

Proof state:
n : ℕ
IH : Gamma (-↑n) = 0
⊢ -↑n.succ ≠ 0

Tactic:
rw [neg_ne_zero, Nat.cast_ne_zero]

Result:
n : ℕ
IH : Gamma (-↑n) = 0
⊢ n.succ ≠ 0

Proof state:
n : ℕ
IH : Gamma (-↑n) = 0
A : -↑n.succ ≠ 0
⊢ -↑n = -↑n.succ + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
Prove a degree bound for `sinPoly n` by induction. Note this is where we find the value in an
explicit description of `sinPoly`.
-/
private lemma sinPoly_natDegree_le : ∀ n : ℕ, (sinPoly n).natDegree ≤ n
  | 0 => by simp [sinPoly]
  | 1 => by simp only [natDegree_C, mul_one, zero_le', sinPoly]
  | n + 2 => by
      rw [sinPoly]
      refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_
      · exact (sinPoly_natDegree_le (n + 1)).trans (by simp)
      refine natDegree_mul_le.trans ?_
      simpa [add_comm 2] using sinPoly_natDegree_le n

Proof state:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (sinPoly n).natDegree ≤ n + 2

Tactic:
simpa [add_comm 2] using sinPoly_natDegree_le n

Result:
no goals

Proof state:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_mul_le.trans ?_

Result:
case refine_2
n : ℕ
⊢ ((monomial 2) (-4)).natDegree + (sinPoly n).natDegree ≤ n + 2

Proof state:
⊢ (sinPoly 1).natDegree ≤ 1

Tactic:
simp only [natDegree_C, mul_one, zero_le', sinPoly]

Result:
no goals

Proof state:
case refine_1
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

Tactic:
exact (sinPoly_natDegree_le (n + 1)).trans (by simp)

Result:
no goals

Proof state:
⊢ (sinPoly 0).natDegree ≤ 0

Tactic:
simp [sinPoly]

Result:
no goals

Proof state:
n : ℕ
⊢ (sinPoly (n + 2)).natDegree ≤ n + 2

Tactic:
rw [sinPoly]

Result:
n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • sinPoly (n + 1) + (monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Proof state:
n : ℕ
⊢ ((2 * (2 * ↑n + 3)) • sinPoly (n + 1) + (monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Tactic:
refine natDegree_add_le_of_degree_le ((natDegree_smul_le _ _).trans ?_) ?_

Result:
case refine_1
n : ℕ
⊢ (sinPoly (n + 1)).natDegree ≤ n + 2

case refine_2
n : ℕ
⊢ ((monomial 2) (-4) * sinPoly n).natDegree ≤ n + 2

Proof state:
n : ℕ
⊢ n + 1 ≤ n + 2

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_mul : ∀ y1 y2 : HomogeneousLocalization 𝒜 x, (y1 * y2).val = y1.val * y2.val :=
  Quotient.ind₂' fun y1 y2 ↦ by rw [← mk_mul, val_mk, val_mk, val_mk, Localization.mk_mul]; rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk (↑y1.num * ↑y2.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (Quotient.mk'' y1 * Quotient.mk'' y2).val = val (Quotient.mk'' y1) * val (Quotient.mk'' y2)

Tactic:
rw [← mk_mul, val_mk, val_mk, val_mk, Localization.mk_mul]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 * y2).num ⟨↑(y1 * y2).den, ⋯⟩ = Localization.mk (↑y1.num * ↑y2.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_iff_omega0_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ a

Proof state:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
⊢ a ≤ ω * (a / ω)

Tactic:
refine (limit_le l).2 fun x hx => le_of_lt ?_

Result:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
⊢ x < ω * (a / ω)

Proof state:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
e : b = 0
⊢ ω * b = 0

Tactic:
simp only [e, mul_zero]

Result:
no goals

Proof state:
a : Ordinal.{u_1}
⊢ a.IsLimit ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
refine ⟨fun l => ⟨l.ne_zero, ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩⟩, fun h => ?_⟩

Result:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
⊢ a ≤ ω * (a / ω)

case refine_2
a : Ordinal.{u_1}
h : a ≠ 0 ∧ ω ∣ a
⊢ a.IsLimit

Proof state:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
⊢ ∀ b' < ω, ω * (x / ω) + b' ≤ a

Tactic:
intro b hb

Result:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
b : Ordinal.{u_1}
hb : b < ω
⊢ ω * (x / ω) + b ≤ a

Proof state:
case refine_2
a : Ordinal.{u_1}
h : a ≠ 0 ∧ ω ∣ a
⊢ a.IsLimit

Tactic:
rcases h with ⟨a0, b, rfl⟩

Result:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
⊢ (ω * b).IsLimit

Proof state:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
b : Ordinal.{u_1}
hb : b < ω
⊢ ω * (x / ω) + b ≤ a

Tactic:
rcases lt_omega0.1 hb with ⟨n, rfl⟩

Result:
case refine_1.intro
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a

Proof state:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
⊢ b = 0 → ω * b = 0

Tactic:
intro e

Result:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
e : b = 0
⊢ ω * b = 0

Proof state:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
⊢ x < ω * (a / ω)

Tactic:
rw [← div_lt omega0_ne_zero, ← succ_le_iff, le_div omega0_ne_zero, mul_succ,
  add_le_of_limit isLimit_omega0]

Result:
case refine_1
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
⊢ ∀ b' < ω, ω * (x / ω) + b' ≤ a

Proof state:
case refine_1.intro
a : Ordinal.{u_1}
l : a.IsLimit
x : Ordinal.{u_1}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a

Tactic:
exact
  (add_le_add_right (mul_div_le _ _) _).trans
    (lt_sub.1 <| nat_lt_limit (isLimit_sub l hx) _).le

Result:
no goals

Proof state:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
⊢ (ω * b).IsLimit

Tactic:
refine isLimit_mul_left isLimit_omega0 (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)

Result:
case refine_2.intro.intro
b : Ordinal.{u_1}
a0 : ω * b ≠ 0
⊢ b = 0 → ω * b = 0
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem norm_two_pi_i_inv_smul_integral_le_of_norm_le_const {f : ℂ → E} {c : ℂ} {R C : ℝ}
    (hR : 0 ≤ R) (hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
    ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), f z‖ ≤ R * C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

Tactic:
have : ‖(2 * π * I : ℂ)⁻¹‖ = (2 * π)⁻¹ := by simp [Real.pi_pos.le]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

Tactic:
rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff₀ Real.two_pi_pos, mul_comm (R * C), ← mul_assoc]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹
⊢ ‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C

Tactic:
exact norm_integral_le_of_norm_le_const hR hf

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹

Tactic:
simp [Real.pi_pos.le]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_Ioi_of_forall_Ioc {β} {mβ : MeasurableSpace β} [LinearOrder α]
    [(atTop : Filter α).IsCountablyGenerated] {x : α} {g : α → β}
    (g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))) :
    AEMeasurable g (μ.restrict (Ioi x))

Proof state:
case intro.inr
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝¹ : LinearOrder α
inst✝ : atTop.IsCountablyGenerated
x : α
g : α → β
g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))
this : Nonempty α
u : ℕ → α
hu_tendsto : Tendsto u atTop atTop
Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)
n : ℕ
h : u n ≤ x
⊢ AEMeasurable g 0

Tactic:
exact aemeasurable_zero_measure

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivWithinAt.union (hs : HasFDerivWithinAt f f' s x)
    (ht : HasFDerivWithinAt f f' t x) : HasFDerivWithinAt f f' (s ∪ t) 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
f' : E →L[𝕜] F
x : E
s t : Set E
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
⊢ HasFDerivAtFilter f f' x (𝓝[s] x ⊔ 𝓝[t] x)

Tactic:
exact .of_isLittleOTVS <| hs.isLittleOTVS.sup ht.isLittleOTVS

Result:
no goals

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
f' : E →L[𝕜] F
x : E
s t : Set E
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
⊢ HasFDerivWithinAt f f' (s ∪ t) x

Tactic:
simp only [HasFDerivWithinAt, nhdsWithin_union]

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
f' : E →L[𝕜] F
x : E
s t : Set E
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
⊢ HasFDerivAtFilter f f' x (𝓝[s] x ⊔ 𝓝[t] x)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem isUnit (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) : IsUnit ζ

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ ζ * ζ ^ (k - 1) = 1

Tactic:
rw [← pow_succ', tsub_add_cancel_of_le h0.nat_succ_le, h.pow_eq_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ IsUnit ζ

Tactic:
apply isUnit_of_mul_eq_one ζ (ζ ^ (k - 1))

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
⊢ ζ * ζ ^ (k - 1) = 1
-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem IsZGroup.coprime_commutator_index [Finite G] [IsZGroup G] :
    (Nat.card (commutator G)).Coprime (commutator G).index

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
exact Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator default

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
h : ¬(Nat.card ↥(commutator G)).Coprime (commutator G).index
⊢ ∃ p, Nat.Prime p ∧ p ∣ Nat.card ↥(commutator G) ∧ p ∣ (commutator G).index

Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mp h

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ (Nat.card ↥(commutator G)).Coprime (commutator G).index

Tactic:
suffices h : ∀ p, p.Prime → (¬ p ∣ Nat.card (commutator G) ∨ ¬ p ∣ (commutator G).index) by
  contrapose! h
  exact Nat.Prime.not_coprime_iff_dvd.mp h

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
h : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index
⊢ (Nat.card ↥(commutator G)).Coprime (commutator G).index

Tactic:
contrapose! h

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
h : ¬(Nat.card ↥(commutator G)).Coprime (commutator G).index
⊢ ∃ p, Nat.Prime p ∧ p ∣ Nat.card ↥(commutator G) ∧ p ∣ (commutator G).index

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
have := Fact.mk hp

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index

Tactic:
intro p hp

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ ¬p ∣ Nat.card ↥(commutator G) ∨ ¬p ∣ (commutator G).index
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} :
    Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f)))
      (Const.alterKey a f (toListModel m.1.buckets))

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ toListModel (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f)) ~
    Const.alterKey a f (toListModel m.val.buckets)

Tactic:
exact toListModel_updateBucket h AssocList.Const.toList_alter List.Const.alterKey_of_perm
  List.Const.alterKey_append_of_containsKey_right_eq_false

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConvexOn.exists_lipschitzOnWith_of_isBounded (hf : ConvexOn ℝ (ball x₀ r) f) (hr : r' < r)
    (hf' : IsBounded (f '' ball x₀ r)) : ∃ K, LipschitzOnWith K f (ball x₀ r')

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ (r - (r - r')))

Tactic:
exact ⟨_, hf.lipschitzOnWith_of_abs_le (sub_pos.2 hr) fun a ha ↦ (hM a ha).le⟩

Result:
no goals

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
rw [← sub_sub_cancel r r']

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ (r - (r - r')))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ r_1, f '' ball x₀ r ⊆ ball 0 r_1
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
simp only [Set.subset_def, mem_image, mem_ball, dist_zero_right, Real.norm_eq_abs,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hf'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ r_1, ∀ (a : E), dist a x₀ < r → |f a| < r_1
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ r_1, ∀ (a : E), dist a x₀ < r → |f a| < r_1
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
obtain ⟨M, hM⟩ := hf'

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')

Tactic:
rw [isBounded_iff_subset_ball 0] at hf'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ r_1, f '' ball x₀ r ⊆ ball 0 r_1
⊢ ∃ K, LipschitzOnWith K f (ball x₀ r')
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- A function from a locally finite preorder is strictly monotone if and only if it is strictly
monotone when restricted to pairs satisfying `a ⋖ b`. -/
lemma strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : StrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : a < b → f a < f b
⊢ f a < f b

Tactic:
exact this hab

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : TransGen CovBy a b → TransGen LT.lt (f a) (f b)
⊢ f a < f b

Tactic:
rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this

Result:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : a < b → f a < f b
⊢ f a < f b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
⊢ f a < f b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
⊢ f a < f b

Tactic:
have := Relation.TransGen.lift f h (a := a) (b := b)

Result:
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a < f b
a b : α
hab : a < b
this : TransGen CovBy a b → TransGen LT.lt (f a) (f b)
⊢ f a < f b