harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Deriv.lean
/-- The derivative of the terms of an L-series. -/
lemma LSeries.hasDerivAt_term (f : ℕ → ℂ) (n : ℕ) (s : ℂ) :
    HasDerivAt (fun z ↦ term f z n) (-(term (logMul f) s n)) s

Proof state:
case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z => f n * ↑n ^ (-z)) (f n * (-log ↑n * ↑n ^ (-s))) s

Tactic:
exact HasDerivAt.const_mul (f n) (by simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
  using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn))

Result:
no goals

Proof state:
case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z => term f z n) (-term (logMul f) s n) s

Tactic:
simp_rw [term_of_ne_zero hn, ← neg_div, ← neg_mul, mul_comm, mul_div_assoc, div_eq_mul_inv,
  ← cpow_neg]

Result:
case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z => f n * ↑n ^ (-z)) (f n * (-log ↑n * ↑n ^ (-s))) s

Proof state:
case inl
f : ℕ → ℂ
s : ℂ
⊢ HasDerivAt (fun z => term f z 0) (-term (logMul f) s 0) s

Tactic:
simp [hasDerivAt_const]

Result:
no goals

Proof state:
f : ℕ → ℂ
n : ℕ
s : ℂ
⊢ HasDerivAt (fun z => term f z n) (-term (logMul f) s n) s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
f : ℕ → ℂ
s : ℂ
⊢ HasDerivAt (fun z => term f z 0) (-term (logMul f) s 0) s

case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z => term f z n) (-term (logMul f) s n) s

Proof state:
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z => ↑n ^ (-z)) (-log ↑n * ↑n ^ (-s)) s

Tactic:
simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn)

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem IsBoundedBilinearMap.continuous (h : IsBoundedBilinearMap 𝕜 f) : Continuous f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
⊢ Continuous f

Tactic:
refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 => f x_1 - f x) (𝓝 x) (𝓝 0)

Proof state:
case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Tendsto (fun x_1 => f (x.1, x_1.2 - x.2)) (𝓝 x) (𝓝 0)

Tactic:
refine Continuous.tendsto' ?_ _ _ (by rw [h.map_sub_right, sub_self])

Result:
case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Continuous fun x_1 => f (x.1, x_1.2 - x.2)
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem forall_generateFrom_mem_iff_mem_iff {S : Set (Set α)} {x y : α} :
    (∀ s, MeasurableSet[generateFrom S] s → (x ∈ s ↔ y ∈ s)) ↔ (∀ s ∈ S, x ∈ s ↔ y ∈ s)

Proof state:
case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n : ℕ), x ∈ s n ↔ y ∈ s n) → (x ∈ ⋃ i, s i ↔ y ∈ ⋃ i, s i)

Tactic:
intro f _ hf

Result:
case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), x ∈ f n ↔ y ∈ f n
⊢ x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i

Proof state:
α : Type u_1
S : Set (Set α)
x y : α
⊢ (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) ↔ ∀ s ∈ S, x ∈ s ↔ y ∈ s

Tactic:
refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩

Result:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)

Proof state:
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)

Tactic:
apply generateFrom_induction

Result:
case hC
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ t ∈ S, MeasurableSet t → (x ∈ t ↔ y ∈ t)

case empty
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅

case compl
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (t : Set α), MeasurableSet t → (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (s : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (s n)) → (∀ (n : ℕ), x ∈ s n ↔ y ∈ s n) → (x ∈ ⋃ i, s i ↔ y ∈ ⋃ i, s i)

Proof state:
case hC
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ t ∈ S, MeasurableSet t → (x ∈ t ↔ y ∈ t)

Tactic:
exact fun s hs _ ↦ H s hs

Result:
no goals

Proof state:
case empty
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅

Tactic:
rfl

Result:
no goals

Proof state:
case iUnion
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), x ∈ f n ↔ y ∈ f n
⊢ x ∈ ⋃ i, f i ↔ y ∈ ⋃ i, f i

Tactic:
simp only [mem_iUnion, hf]

Result:
no goals

Proof state:
case compl
α : Type u_1
S : Set (Set α)
x y : α
H : ∀ s ∈ S, x ∈ s ↔ y ∈ s
s : Set α
⊢ ∀ (t : Set α), MeasurableSet t → (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

Tactic:
exact fun _ _ ↦ Iff.not

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem prod_univ_units_id_eq_neg_one [CommRing K] [IsDomain K] [Fintype Kˣ] :
    ∏ x : Kˣ, x = (-1 : Kˣ)

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ univ.erase (-1)), (fun x x_1 => x⁻¹) ((fun x x_1 => x⁻¹) a ha) ⋯ = a

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1

Tactic:
have : (∏ x ∈ (@univ Kˣ _).erase (-1), x) = 1 :=
  prod_involution (fun x _ => x⁻¹) (by simp)
    (fun a => by simp +contextual [Units.inv_eq_self_iff])
    (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)

Result:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x ∈ univ.erase (-1), x = 1
⊢ ∏ x : Kˣ, x = -1

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
this : ∏ x ∈ univ.erase (-1), x = 1
⊢ ∏ x : Kˣ, x = -1

Tactic:
rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∏ x : Kˣ, x = -1

Tactic:
classical
  have : (∏ x ∈ (@univ Kˣ _).erase (-1), x) = 1 :=
    prod_involution (fun x _ => x⁻¹) (by simp)
      (fun a => by simp +contextual [Units.inv_eq_self_iff])
      (fun a => by simp [@inv_eq_iff_eq_inv _ _ a]) (by simp)
  rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _), this, mul_one]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
⊢ ∀ (a : Kˣ) (ha : a ∈ univ.erase (-1)), a * (fun x x_1 => x⁻¹) a ha = 1

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ univ.erase (-1)), a ≠ 1 → (fun x x_1 => x⁻¹) a ha ≠ a

Tactic:
simp +contextual [Units.inv_eq_self_iff]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : CommRing K
inst✝¹ : IsDomain K
inst✝ : Fintype Kˣ
a : Kˣ
⊢ ∀ (ha : a ∈ univ.erase (-1)), (fun x x_1 => x⁻¹) a ha ∈ univ.erase (-1)

Tactic:
simp [@inv_eq_iff_eq_inv _ _ a]

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem fst_eq_iff : ∀ {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
  | ⟨a, b⟩, x => by simp

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
x : α
⊢ (a, b).fst = x ↔ (a, b) = (x, (a, b).snd)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_closedBall_zero {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ} (hk : 0 < ‖k‖) :
    k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r

Tactic:
intro x

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r

Proof state:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x

Tactic:
rw [← smul_assoc, smul_eq_mul, ← div_eq_mul_inv, div_self (norm_pos_iff.mp hk), one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)

Tactic:
refine subset_antisymm smul_closedBall_subset ?_

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
⊢ p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r

Tactic:
rw [Set.mem_smul_set, Seminorm.mem_closedBall_zero]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Proof state:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r

Tactic:
rwa [Seminorm.mem_closedBall_zero, map_smul_eq_mul, norm_inv, ← mul_le_mul_left hk, ← mul_assoc,
  ← div_eq_mul_inv ‖k‖ ‖k‖, div_self (ne_of_gt hk), one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Tactic:
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r

case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.comp_affineMap {f : F → β} (g : E →ᵃ[𝕜] F) {s : Set F} (hf : ConvexOn 𝕜 s f) :
    ConvexOn 𝕜 (g ⁻¹' s) (f ∘ g) :=
  ⟨hf.1.affine_preimage _, fun x hx y hy a b ha hb hab =>
    calc
      (f ∘ g) (a • x + b • y) = f (g (a • x + b • y)) := rfl
      _ = f (a • g x + b • g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (g (a • x + b • y)) = f (a • g x + b • g y)

Tactic:
rw [Convex.combo_affine_apply hab]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_map (as : List α) (f : α → β) : (as.map f).length = as.length

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
as : List α
ih : (map f as).length = as.length
⊢ (map f (head✝ :: as)).length = (head✝ :: as).length

Tactic:
simp [List.map, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).length = [].length

Tactic:
simp [List.map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : List α
f : α → β
⊢ (map f as).length = as.length

Tactic:
induction as with
| nil => simp [List.map]
| cons _ as ih => simp [List.map, ih]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- The radius of the Cartesian product of two formal series is the minimum of their radii. -/
lemma FormalMultilinearSeries.radius_prod_eq_min
    (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) :
    (p.prod q).radius = min p.radius q.radius

Proof state:
case a.right.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
⊢ (fun n => ‖q n‖ * ↑r ^ n) =O[atTop] fun x => 1

Tactic:
refine (isBigO_of_le _ fun n ↦ ?_).trans this.isBigO

Result:
case a.right.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
n : ℕ
⊢ ‖‖q n‖ * ↑r ^ n‖ ≤ ‖‖p.prod q n‖ * ↑r ^ n‖
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_radius_eq_zero_of_tendsto [NormOneClass E]
    (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop) : (ofScalars E c).radius = 0

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * (‖c n‖ * ↑r ^ n) ≤ ‖c (n + 1)‖ * ↑r ^ (n + 1)

Tactic:
rw [mul_comm ‖c n‖, ← mul_assoc, ← div_le_div_iff₀, mul_div_assoc]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 2 * (↑r ^ n / ↑r ^ (n + 1)) ≤ ‖c (n + 1)‖ / ‖c n‖

case h.hb
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ↑r ^ (n + 1)

case h.hd
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n => ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ 0 < ‖c n‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
    (as.modify x f)[i] = if x = i then f (as[i]'(by simpa using h)) else as[i]'(by simpa using h)

Proof state:
α : Type u_1
f : α → α
as : Array α
x : Nat
h✝ : ¬x < as.size
h : x < (as.modify x f).size
⊢ ?m.511823 h

Tactic:
exact h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : x < as.size
⊢ (do
        let v ← f as[x]
        as.set x v ⋯)[i] =
    if x = i then f as[i] else as[i]

Tactic:
simp only [Id.bind_eq, get_set _ _ _ _ (by simpa using h)]

Result:
case isTrue
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : x < as.size
⊢ (if x = i then f as[x] else as[i]) = if x = i then f as[i] else as[i]

Proof state:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : ¬x < as.size
⊢ ¬x < (as.modify x f).size

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : x < as.size
⊢ ?m.510396 < size ?m.510393

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.508606
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
⊢ i < as.size

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : x < as.size
⊢ (if x = i then f as[x] else as[i]) = if x = i then f as[i] else as[i]

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : ¬x < as.size
⊢ as[i] = if x = i then f as[i] else as[i]

Tactic:
rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
⊢ (as.modify x f)[i] = if x = i then f as[i] else as[i]

Tactic:
simp only [modify, modifyM, get_eq_getElem, Id.run, Id.pure_eq]

Result:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
⊢ (if h : x < as.size then do
        let v ← f as[x]
        as.set x v ⋯
      else as)[i] =
    if x = i then f as[i] else as[i]

Proof state:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
⊢ (if h : x < as.size then do
        let v ← f as[x]
        as.set x v ⋯
      else as)[i] =
    if x = i then f as[i] else as[i]

Tactic:
split

Result:
case isTrue
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : x < as.size
⊢ (do
        let v ← f as[x]
        as.set x v ⋯)[i] =
    if x = i then f as[i] else as[i]

case isFalse
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : ¬x < as.size
⊢ as[i] = if x = i then f as[i] else as[i]

Proof state:
α : Type u_1
f : α → α
as : Array α
x i : Nat
h : i < (as.modify x f).size
h✝ : ¬x < as.size
⊢ x = i → ?m.511664

Tactic:
rintro rfl

Result:
α : Type u_1
f : α → α
as : Array α
x : Nat
h✝ : ¬x < as.size
h : x < (as.modify x f).size
⊢ ?m.511823 h
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem Balanced.neg_mem_iff [NormOneClass 𝕜] (h : Balanced 𝕜 s) {x : E} : -x ∈ s ↔ x ∈ s :=
  ⟨fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx,
    fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx⟩

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ ‖-1‖ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ ‖-1‖ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : x ∈ s
⊢ -x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : NormOneClass 𝕜
h : Balanced 𝕜 s
x : E
hx : -x ∈ s
⊢ x ∈ s

Tactic:
simpa using h.smul_mem (a := -1) (by simp) hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem remainingBytes : ∀ {it}, ValidFor l r it → it.remainingBytes = utf8Len r
  | _, ⟨⟩ => by simp [Iterator.remainingBytes, Nat.add_sub_cancel_left]

Proof state:
l r : List Char
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.remainingBytes = utf8Len r

Tactic:
simp [Iterator.remainingBytes, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem continuous_proj : @Continuous _ _ a.totalSpaceTopology _ (π F E)

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous TotalSpace.proj

Tactic:
letI := a.toFiberBundle

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
⊢ Continuous TotalSpace.proj

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
⊢ Continuous TotalSpace.proj

Tactic:
exact FiberBundle.continuous_proj F E

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
⊢ Continuous TotalSpace.proj

Tactic:
letI := a.totalSpaceTopology

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ Continuous TotalSpace.proj
-- Mathlib/Data/Vector/Basic.lean
theorem id_traverse : ∀ x : Vector α n, x.traverse (pure : _ → Id _) = x

Proof state:
case mk
α : Type u
x : List α
⊢ Vector.traverse pure ⟨x, ⋯⟩ = ⟨x, ⋯⟩

Tactic:
dsimp [Vector.traverse, cast]

Result:
case mk
α : Type u
x : List α
⊢ List.Vector.traverseAux pure x = ⟨x, ⋯⟩

Proof state:
case mk.cons
α : Type u
x : α
xs : List α
IH : List.Vector.traverseAux pure xs = ⟨xs, ⋯⟩
⊢ List.Vector.traverseAux pure (x :: xs) = ⟨x :: xs, ⋯⟩

Tactic:
simp! [IH]

Result:
case mk.cons
α : Type u
x : α
xs : List α
IH : List.Vector.traverseAux pure xs = ⟨xs, ⋯⟩
⊢ cons x <*> ⟨xs, ⋯⟩ = ⟨x :: xs, ⋯⟩

Proof state:
case mk
α : Type u
x : List α
⊢ List.Vector.traverseAux pure x = ⟨x, ⋯⟩

Tactic:
induction' x with x xs IH

Result:
case mk.nil
α : Type u
⊢ List.Vector.traverseAux pure [] = ⟨[], ⋯⟩

case mk.cons
α : Type u
x : α
xs : List α
IH : List.Vector.traverseAux pure xs = ⟨xs, ⋯⟩
⊢ List.Vector.traverseAux pure (x :: xs) = ⟨x :: xs, ⋯⟩

Proof state:
case mk.cons
α : Type u
x : α
xs : List α
IH : List.Vector.traverseAux pure xs = ⟨xs, ⋯⟩
⊢ cons x <*> ⟨xs, ⋯⟩ = ⟨x :: xs, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
α : Type u
⊢ ∀ (x : Vector α n), Vector.traverse pure x = x

Tactic:
rintro ⟨x, rfl⟩

Result:
case mk
α : Type u
x : List α
⊢ Vector.traverse pure ⟨x, ⋯⟩ = ⟨x, ⋯⟩

Proof state:
case mk.nil
α : Type u
⊢ List.Vector.traverseAux pure [] = ⟨[], ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Icc_mul_Ico_subset' [LocallyFiniteOrder α] (a b c d : α) :
    Icc a b * Ico c d ⊆ Ico (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Icc_mul_Ico_subset' _ _ _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Icc a b * Ico c d) ⊆ ↑(Ico (a * c) (b * d))

Tactic:
simpa using Set.Icc_mul_Ico_subset' _ _ _ _

Result:
no goals