harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_singleton {α : Type*} [PartialOrder α] {a : α} :
    OrdConnected ({a} : Set α)

Proof state:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
rw [← Icc_self]

Result:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Proof state:
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ (Icc a a).OrdConnected

Tactic:
exact ordConnected_Icc

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_le {a b : Ordinal} (h : a ≤ b) : a.toPGame ≤ b.toPGame

Proof state:
a b : Ordinal.{u_1}
h : a ≤ b
i : a.toPGame.LeftMoves
⊢ a.toPGame.moveLeft i ⧏ b.toPGame

Tactic:
rw [toPGame_moveLeft']

Result:
a b : Ordinal.{u_1}
h : a ≤ b
i : a.toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ b.toPGame

Proof state:
a b : Ordinal.{u_1}
h : a ≤ b
⊢ a.toPGame ≤ b.toPGame

Tactic:
refine le_iff_forall_lf.2 ⟨fun i => ?_, isEmptyElim⟩

Result:
a b : Ordinal.{u_1}
h : a ≤ b
i : a.toPGame.LeftMoves
⊢ a.toPGame.moveLeft i ⧏ b.toPGame

Proof state:
a b : Ordinal.{u_1}
h : a ≤ b
i : a.toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ b.toPGame

Tactic:
exact toPGame_lf ((toLeftMovesToPGame_symm_lt i).trans_le h)

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem val_add_eq_ite {n : ℕ} (a b : Fin n) :
    (↑(a + b) : ℕ) = if n ≤ a + b then a + b - n else a + b

Proof state:
n : ℕ
a b : Fin n
⊢ ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

Tactic:
rw [Fin.val_add, Nat.add_mod_eq_ite, Nat.mod_eq_of_lt (show ↑a < n from a.2),
  Nat.mod_eq_of_lt (show ↑b < n from b.2)]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_span (f : F) (s : Set R) : map f (span s) = span (f '' s)

Proof state:
case refine_1.intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
x : R
hx : x ∈ s
⊢ f x ∈ ↑(map f (span s))

Tactic:
exact mem_map_of_mem f (subset_span hx)

Result:
no goals

Proof state:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case refine_1.intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
x : R
hx : x ∈ s
⊢ f x ∈ ↑(map f (span s))

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ map f (span s) = span (⇑f '' s)

Tactic:
refine (Submodule.span_eq_of_le _ ?_ ?_).symm

Result:
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ ⇑f '' s ⊆ ↑(map f (span s))

case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)

Proof state:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ map f (span s) ≤ Submodule.span S (⇑f '' s)

Tactic:
rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]

Result:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ ⇑f '' s ⊆ ↑(Submodule.span S (⇑f '' s))

Proof state:
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
s : Set R
⊢ ⇑f '' s ⊆ ↑(Submodule.span S (⇑f '' s))

Tactic:
exact subset_span

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_max (hr : a ≠ ∞) (hp : b ≠ ∞) :
    ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b) :=
  (le_total a b).elim
    (fun h => by simp only [h, ENNReal.toReal_mono hp h, max_eq_right]) fun h => by
    simp only [h, ENNReal.toReal_mono hr h, max_eq_left]

Proof state:
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : b ≤ a
⊢ (a ⊔ b).toReal = a.toReal ⊔ b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hr h, max_eq_left]

Result:
no goals

Proof state:
a b : ℝ≥0∞
hr : a ≠ ⊤
hp : b ≠ ⊤
h : a ≤ b
⊢ (a ⊔ b).toReal = a.toReal ⊔ b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hp h, max_eq_right]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem length_lt_card_boundaries : c.length < c.boundaries.card

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.length + 1

Tactic:
exact Nat.lt_add_one _

Result:
no goals

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.boundaries.card

Tactic:
rw [c.card_boundaries_eq_succ_length]

Result:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.length + 1
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma shift_v (a : ℤ) (p q : ℤ) (hpq : p + n = q) (p' q' : ℤ)
    (hp' : p' = p + a) (hq' : q' = q + a) :
    (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫
      γ.v p' q' (by rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]) ≫
      (L.shiftFunctorObjXIso a q q' hq').inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ γ.v p' q' ⋯ ≫ (L.shiftFunctorObjXIso a q q' hq').inv

Tactic:
subst hp' hq'

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ (γ.shift a).v p q hpq =
    (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ p' + n = q'

Tactic:
rw [hp', hq', ← hpq, add_assoc, add_comm a, add_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ (γ.shift a).v p q hpq =
    (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma traceForm_coroot (α : Weight K H L) (x : H) :
    traceForm K H L (coroot α) x = 2 • (α <| (cartanEquivDual H).symm α)⁻¹ • α x

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
⊢ ((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
have : cartanEquivDual H ((cartanEquivDual H).symm α) x = α x := by
  rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ ((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ 2 •
      (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
        ((traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
congr 2

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
⊢ ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x

Tactic:
rw [LinearEquiv.apply_symm_apply, Weight.toLinear_apply]

Result:
no goals

Proof state:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ ((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x

Tactic:
rw [coroot, map_nsmul, map_smul, LinearMap.smul_apply, LinearMap.smul_apply]

Result:
K : Type u_2
L : Type u_3
inst✝⁵ : LieRing L
inst✝⁴ : Field K
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsKilling K L
α : Weight K (↥H) L
x : ↥H
this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x
⊢ 2 •
      (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ •
        ((traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x =
    2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem mem_cylinder_iff_le_firstDiff {x y : ∀ n, E n} (hne : x ≠ y) (i : ℕ) :
    x ∈ cylinder y i ↔ i ≤ firstDiff x y

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i ↔ i ≤ firstDiff x y

Tactic:
constructor

Result:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y

case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i

Proof state:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ i ≤ firstDiff x y → x ∈ cylinder y i

Tactic:
intro hi j hj

Result:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff x y
j : ℕ
hj : j < i
⊢ x j = y j

Proof state:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y

Tactic:
intro h

Result:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
⊢ i ≤ firstDiff x y

Proof state:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
this : firstDiff x y < i
⊢ False

Tactic:
exact apply_firstDiff_ne hne (h _ this)

Result:
no goals

Proof state:
case mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
hi : i ≤ firstDiff x y
j : ℕ
hj : j < i
⊢ x j = y j

Tactic:
exact apply_eq_of_lt_firstDiff (hj.trans_le hi)

Result:
no goals

Proof state:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
⊢ i ≤ firstDiff x y

Tactic:
by_contra!

Result:
case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
this : firstDiff x y < i
⊢ False
-- Mathlib/Combinatorics/Colex.lean
lemma lt_iff_exists_filter_lt :
    toColex s < toColex t ↔ ∃ w ∈ t \ s, {a ∈ s | w < a} = {a ∈ t | w < a}

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
⊢ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
refine ⟨w, hwt, hws, fun a has hat ↦ ?_⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
⊢ a < w

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
let u := {w ∈ t \ s | ∀ a ∈ s, a ∉ t → a < w}

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)

Tactic:
have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [u, and_assoc]

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
mem_u : ∀ {w : α}, w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
⊢ ∃ w ∈ t, w ∉ s ∧ ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the von Mangoldt function `Λ` converges at `s` when `re s > 1`. -/
lemma LSeriesSummable_vonMangoldt {s : ℂ} (hs : 1 < s.re) : LSeriesSummable ↗Λ s

Proof state:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
hΛ : ‖(fun n => ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖
⊢ ‖Complex.log ↑n‖ ≤ ‖logMul 1 n‖

Tactic:
simp

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
hΛ : ‖(fun n => ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖
⊢ ‖↑(Λ n)‖ ≤ ‖logMul 1 n‖

Tactic:
exact hΛ.trans <| by simp

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ abscissaOfAbsConv 1 < ↑s.re

Tactic:
rw [abscissaOfAbsConv_one]

Result:
s : ℂ
hs : 1 < s.re
⊢ 1 < ↑s.re

Proof state:
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun n => ↑(Λ n)) s

Tactic:
have hf := LSeriesSummable_logMul_of_lt_re
  (show abscissaOfAbsConv 1 < s.re by rw [abscissaOfAbsConv_one]; exact_mod_cast hs)

Result:
s : ℂ
hs : 1 < s.re
hf : LSeriesSummable (logMul 1) s
⊢ LSeriesSummable (fun n => ↑(Λ n)) s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ 1 < ↑s.re

Tactic:
exact_mod_cast hs

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖(fun n => ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖

Tactic:
simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg]
  using vonMangoldt_le_log

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖↑(Λ n)‖ ≤ ‖logMul 1 n‖

Tactic:
have hΛ : ‖↗Λ n‖ ≤ ‖Complex.log n‖ := by
  simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg]
    using vonMangoldt_le_log

Result:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
hΛ : ‖(fun n => ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖
⊢ ‖↑(Λ n)‖ ≤ ‖logMul 1 n‖

Proof state:
s : ℂ
hs : 1 < s.re
hf : LSeriesSummable (logMul 1) s
⊢ LSeriesSummable (fun n => ↑(Λ n)) s

Tactic:
rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢

Result:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
⊢ Summable fun x => ‖term (fun n => ↑(Λ n)) s x‖

Proof state:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
⊢ Summable fun x => ‖term (fun n => ↑(Λ n)) s x‖

Tactic:
refine hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)

Result:
s : ℂ
hs : 1 < s.re
hf : Summable fun x => ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖↑(Λ n)‖ ≤ ‖logMul 1 n‖
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelIsoOfEq_inv_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g)
    (e : Y ⟶ Z) (he) :
    (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he])

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : f ≫ e = 0
⊢ g ≫ e = 0

Tactic:
simp [← h, he]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
he : f ≫ e = 0
inst✝ : HasCokernel f
⊢ (cokernelIsoOfEq ⋯).inv ≫ cokernel.desc f e he = cokernel.desc f e ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : f ≫ e = 0
⊢ (cokernelIsoOfEq h).inv ≫ cokernel.desc f e he = cokernel.desc g e ⋯

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
e : Y ⟶ Z
he : f ≫ e = 0
inst✝ : HasCokernel f
⊢ (cokernelIsoOfEq ⋯).inv ≫ cokernel.desc f e he = cokernel.desc f e ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

Proof state:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ l.set n a' = take n l ++ a' :: drop (n + 1) l

Tactic:
simp [set_eq_take_append_cons_drop, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

Tactic:
refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩

Result:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ l.set n a' = take n l ++ a' :: drop (n + 1) l

Proof state:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ l = take n l ++ l[n] :: drop (n + 1) l

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.biUnion {f : β → Set α} {s : Set β} (hs : s.Countable)
    (h : ∀ b ∈ s, MeasurableSet (f b)) : MeasurableSet (⋃ b ∈ s, f b)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ ∀ (b : ↑s), MeasurableSet (f ↑b)

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ x, f ↑x)

Tactic:
have := hs.to_subtype

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ x, f ↑x)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ x, f ↑x)

Tactic:
exact MeasurableSet.iUnion (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ b ∈ s, f b)

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ x, f ↑x)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem le_ker_iff : I ≤ f.ker ↔ ∀ x, x ∈ I → f x = 0

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ I ≤ f.ker ↔ ∀ x ∈ I, f x = 0

Tactic:
constructor <;> intro h x hx

Result:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : I ≤ f.ker
x : L
hx : x ∈ I
⊢ f x = 0

case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ x ∈ f.ker

Proof state:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
h : f x = 0
⊢ f x = 0

Tactic:
exact h

Result:
no goals

Proof state:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : I ≤ f.ker
x : L
hx : x ∈ I
⊢ f x = 0

Tactic:
specialize h hx

Result:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
h : x ∈ f.ker
⊢ f x = 0

Proof state:
case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ x ∈ f.ker

Tactic:
rw [mem_ker]

Result:
case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ f x = 0

Proof state:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
h : x ∈ f.ker
⊢ f x = 0

Tactic:
rw [mem_ker] at h

Result:
case mp
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
h : f x = 0
⊢ f x = 0

Proof state:
case mpr
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ∀ x ∈ I, f x = 0
x : L
hx : x ∈ I
⊢ f x = 0

Tactic:
apply h x hx

Result:
no goals