harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Seminorm.lean
theorem finset_sup_smul (p : ι → Seminorm 𝕜 E) (s : Finset ι) (C : ℝ≥0) :
    s.sup (C • p) = C • s.sup p

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
⊢ s.sup (C • p) = C • s.sup p

Tactic:
ext x

Result:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ (s.sup (C • p)) x = (C • s.sup p) x

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ C • ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = ↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩)

Tactic:
exact congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.mul_finset_sup C s (fun i ↦ ⟨p i x, apply_nonneg _ _⟩))

Result:
no goals

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ (s.sup (C • p)) x = (C • s.sup p) x

Tactic:
rw [smul_apply, finset_sup_apply, finset_sup_apply]

Result:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ ↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩) = C • ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ ↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩) = C • ↑(s.sup fun i => ⟨(p i) x, ⋯⟩)

Tactic:
symm

Result:
case h
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
C : ℝ≥0
x : E
⊢ C • ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = ↑(s.sup fun i => ⟨((C • p) i) x, ⋯⟩)
-- Mathlib/Topology/Basic.lean
theorem isOpen_singleton_iff_nhds_eq_pure (x : X) : IsOpen ({x} : Set X) ↔ 𝓝 x = pure x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ 𝓝 x ≤ pure x

Tactic:
rw [le_pure_iff]

Result:
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ {x} ∈ 𝓝 x

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen {x} → 𝓝 x = pure x

Tactic:
intro h

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ 𝓝 x = pure x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ {x} ∈ 𝓝 x

Tactic:
exact h.mem_nhds (mem_singleton x)

Result:
no goals

Proof state:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
h : 𝓝 x = pure x
⊢ IsOpen {x}

Tactic:
simp [isOpen_iff_nhds, h]

Result:
no goals

Proof state:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = pure x → IsOpen {x}

Tactic:
intro h

Result:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
h : 𝓝 x = pure x
⊢ IsOpen {x}

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen {x} ↔ 𝓝 x = pure x

Tactic:
constructor

Result:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen {x} → 𝓝 x = pure x

case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 x = pure x → IsOpen {x}

Proof state:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ 𝓝 x = pure x

Tactic:
apply le_antisymm _ (pure_le_nhds x)

Result:
X : Type u
inst✝ : TopologicalSpace X
x : X
h : IsOpen {x}
⊢ 𝓝 x ≤ pure x
-- Mathlib/Algebra/Order/SuccPred.lean
theorem IsPredPrelimit.lt_sub_natCast [AddCommGroupWithOne α] [PredSubOrder α]
    (hx : IsPredPrelimit x) (hy : x < y) : ∀ n : ℕ, x < y - n
  | 0 => by simpa
  | n + 1 => by
    rw [Nat.cast_add_one, ← sub_sub]
    exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑n - 1

Tactic:
exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

Result:
no goals

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑(n + 1)

Tactic:
rw [Nat.cast_add_one, ← sub_sub]

Result:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑n - 1

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - ↑0

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R n

Proof state:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
simp_rw [x_zero, Submodule.zero_mem]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
by_cases x_zero : x = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ degreeLT R (n + 1) = degreeLE R ↑n

Tactic:
ext x

Result:
case h
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ∈ degreeLT R (n + 1) ↔ x ∈ degreeLE R ↑n

Tactic:
rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
  ← natDegree_le_iff_degree_le, Nat.lt_succ]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
x : R[X]
x_zero : ¬x = 0
⊢ x ≠ 0

Tactic:
rwa [ne_eq]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem symm [Monoid M] : ∀ {x y : M}, x ~ᵤ y → y ~ᵤ x
  | x, _, ⟨u, rfl⟩ => ⟨u⁻¹, by rw [mul_assoc, Units.mul_inv, mul_one]⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
u : Mˣ
⊢ x * ↑u * ↑u⁻¹ = x

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_eq_getLast?_reverse {xs : List α} : xs.head? = xs.reverse.getLast?

Proof state:
α : Type u_1
xs : List α
⊢ xs.head? = xs.reverse.getLast?

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
lemma zsmul_app (n : ℤ) (f : M₁ ⟶ M₂) (X : Cᵒᵖ) : (n • f).app X = n • f.app X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
⊢ (n • f).app X = n • f.app X

Tactic:
ext x

Result:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom ((n • f).app X)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Proof state:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ModuleCat.Hom.hom ((n • f).app X)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
change (toPresheaf R ⋙ (evaluation _ _).obj X).map (n • f) x = _

Result:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom ((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map (n • f))) x =
    (ModuleCat.Hom.hom (n • f.app X)) x

Proof state:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom ((toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map (n • f))) x =
    (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
rw [Functor.map_zsmul]

Result:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom (n • (toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map f)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Proof state:
case hf.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
n : ℤ
f : M₁ ⟶ M₂
X : Cᵒᵖ
x : ↑(M₁.obj X)
⊢ (ConcreteCategory.hom (n • (toPresheaf R ⋙ (evaluation Cᵒᵖ Ab).obj X).map f)) x = (ModuleCat.Hom.hom (n • f.app X)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem nearestPtInd_succ (e : ℕ → α) (N : ℕ) (x : α) :
    nearestPtInd e (N + 1) x =
      if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else nearestPtInd e N x

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (if x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x} then (const α (N + 1)) x
    else (nearestPtInd e N) x) =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x

Tactic:
congr

Result:
case e_c
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) = ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (nearestPtInd e (N + 1)) x = if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x

Tactic:
simp only [nearestPtInd, coe_piecewise, Set.piecewise]

Result:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (if x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x} then (const α (N + 1)) x
    else (nearestPtInd e N) x) =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x

Proof state:
case e_c
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (x ∈ ⋂ k, ⋂ (_ : k ≤ N), {x | edist (e (N + 1)) x < edist (e k) x}) = ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Monoidal.lean
lemma isSheaf_functorEnrichedHom (F G : Cᵒᵖ ⥤ A) (hG : Presheaf.IsSheaf J G)
    [HasFunctorEnrichedHom A F G] :
    Presheaf.IsSheaf J (functorEnrichedHom A F G) := fun M ↦ by
  rw [Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]
  rw [← isSheaf_iff_isSheaf_of_type]
  exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (functorEnrichedHom A F G ⋙ coyoneda.obj (op M))

Tactic:
rw [Presieve.isSheaf_iff_of_nat_equiv
  (functorEnrichedHomCoyonedaObjEquiv M F G)
  (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]

Result:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

Result:
no goals

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Result:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_EulerianCircuit_length {n : ℕ} :
    (cycleGraph_EulerianCircuit n).length = n + 3

Proof state:
n : ℕ
⊢ (let_fun hadj := ⋯;
      Walk.cons hadj (SimpleGraph.cycleGraph_EulerianCircuit_cons n (Fin.last (n + 2)))).length =
    n + 3

Tactic:
simp [cycleGraph_EulerianCircuit_cons_length]

Result:
no goals

Proof state:
n : ℕ
⊢ (cycleGraph_EulerianCircuit n).length = n + 3

Tactic:
unfold cycleGraph_EulerianCircuit

Result:
n : ℕ
⊢ (let_fun hadj := ⋯;
      Walk.cons hadj (SimpleGraph.cycleGraph_EulerianCircuit_cons n (Fin.last (n + 2)))).length =
    n + 3
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_sizeOf_le [SizeOf α] (l : List α) (n : Nat) : sizeOf (l.drop n) ≤ sizeOf l

Proof state:
α : Type u_1
inst✝ : SizeOf α
l : List α
n : Nat
⊢ sizeOf (drop n l) ≤ sizeOf l

Tactic:
induction l generalizing n with
| nil => rw [drop_nil]; apply Nat.le_refl
| cons _ _ lih =>
  induction n with
  | zero => apply Nat.le_refl
  | succ n =>
    exact Trans.trans (lih _) (Nat.le_add_left _ _)

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : Nat), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : Nat
a✝ : sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)
⊢ sizeOf (drop (n + 1) (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)

Tactic:
exact Trans.trans (lih _) (Nat.le_add_left _ _)

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : SizeOf α
n : Nat
⊢ sizeOf [] ≤ sizeOf []

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : SizeOf α
n : Nat
⊢ sizeOf (drop n []) ≤ sizeOf []

Tactic:
rw [drop_nil]

Result:
case nil
α : Type u_1
inst✝ : SizeOf α
n : Nat
⊢ sizeOf [] ≤ sizeOf []

Proof state:
case cons.zero
α : Type u_1
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : Nat), sizeOf (drop n tail✝) ≤ sizeOf tail✝
⊢ sizeOf (drop 0 (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : SizeOf α
head✝ : α
tail✝ : List α
lih : ∀ (n : Nat), sizeOf (drop n tail✝) ≤ sizeOf tail✝
n : Nat
⊢ sizeOf (drop n (head✝ :: tail✝)) ≤ sizeOf (head✝ :: tail✝)

Tactic:
induction n with
| zero => apply Nat.le_refl
| succ n =>
  exact Trans.trans (lih _) (Nat.le_add_left _ _)

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem right_of_add (hn : IsPeriodicPt f (n + m) x) (hm : IsPeriodicPt f n x) :
    IsPeriodicPt f m x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
exact hn.left_of_add hm

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
rw [add_comm] at hn

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_add_add (m n k : Nat) : subNatNat (m + k) (n + k) = subNatNat m n

Proof state:
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + k + (i + 1)) = -[i+1]

Tactic:
exact subNatNat_add_right

Result:
no goals

Proof state:
case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]

Tactic:
focus
  intro i j
  rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]
  exact subNatNat_add_right

Result:
no goals

Proof state:
case hp
m n k : Nat
⊢ ∀ (i n : Nat), subNatNat (n + i + k) (n + k) = ↑i

Tactic:
intro i j

Result:
case hp
m n k i j : Nat
⊢ subNatNat (j + i + k) (j + k) = ↑i

Proof state:
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + i + 1 + k) = -[i+1]

Tactic:
rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]

Result:
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + k + (i + 1)) = -[i+1]

Proof state:
case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]

Tactic:
intro i j

Result:
case hn
m n k i j : Nat
⊢ subNatNat (j + k) (j + i + 1 + k) = -[i+1]

Proof state:
case hp
m n k i j : Nat
⊢ subNatNat (j + k + i) (j + k) = ↑i

Tactic:
exact subNatNat_add_left

Result:
no goals

Proof state:
case hp
m n k i j : Nat
⊢ subNatNat (j + i + k) (j + k) = ↑i

Tactic:
rw [Nat.add_assoc, Nat.add_comm i k, ← Nat.add_assoc]

Result:
case hp
m n k i j : Nat
⊢ subNatNat (j + k + i) (j + k) = ↑i

Proof state:
m n k : Nat
⊢ subNatNat (m + k) (n + k) = subNatNat m n

Tactic:
apply subNatNat_elim m n (fun m n i => subNatNat (m + k) (n + k) = i)

Result:
case hp
m n k : Nat
⊢ ∀ (i n : Nat), subNatNat (n + i + k) (n + k) = ↑i

case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]

Proof state:
case hp
m n k : Nat
⊢ ∀ (i n : Nat), subNatNat (n + i + k) (n + k) = ↑i

case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]

Tactic:
focus
  intro i j
  rw [Nat.add_assoc, Nat.add_comm i k, ← Nat.add_assoc]
  exact subNatNat_add_left

Result:
case hn
m n k : Nat
⊢ ∀ (i m : Nat), subNatNat (m + k) (m + i + 1 + k) = -[i+1]
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_right_comm : a - b - c = a - c - b

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b - c = a - c - b

Tactic:
rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_sub (a b : Int) : -(a - b) = b - a

Proof state:
a b : Int
⊢ -(a - b) = b - a

Tactic:
simp [Int.sub_eq_add_neg, Int.add_comm]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem ENNReal.ofReal_tsum_of_nonneg {f : α → ℝ} (hf_nonneg : ∀ n, 0 ≤ f n) (hf : Summable f) :
    ENNReal.ofReal (∑' n, f n) = ∑' n, ENNReal.ofReal (f n)

Proof state:
α : Type u_1
f : α → ℝ
hf_nonneg : ∀ (n : α), 0 ≤ f n
hf : Summable f
⊢ ENNReal.ofReal (∑' (n : α), f n) = ∑' (n : α), ENNReal.ofReal (f n)

Tactic:
simp_rw [ENNReal.ofReal, ENNReal.tsum_coe_eq (NNReal.hasSum_real_toNNReal_of_nonneg hf_nonneg hf)]

Result:
no goals
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma proj_surjective (n : ℕ) : Function.Surjective (S.proj n)

Proof state:
S : LightProfinite
n : ℕ
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((lightToProfinite.obj S).asLimitCone.π.app
          ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))))

Tactic:
exact DiscreteQuotient.proj_surjective _

Result:
no goals

Proof state:
S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (lightToProfinite.map (S.proj n)))

Tactic:
rw [lightToProfinite_map_proj_eq]

Result:
S : LightProfinite
n : ℕ
⊢ Function.Surjective
    ⇑(ConcreteCategory.hom
        ((lightToProfinite.obj S).asLimitCone.π.app
          ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))))

Proof state:
S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
change Function.Surjective (lightToProfinite.map (S.proj n))

Result:
S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (lightToProfinite.map (S.proj n)))
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Sheaf J (Type v)} (t : F.val.obj X) :
    J.yonedaEquiv.symm (F.val.map f t) = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm t

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yonedaEquiv.symm (F.val.map f (J.yonedaEquiv u)) = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm (J.yonedaEquiv u)

Tactic:
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
t : F.val.obj X
⊢ J.yonedaEquiv.symm (F.val.map f t) = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := J.yonedaEquiv.surjective t

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
u : J.yoneda.obj (unop X) ⟶ F
⊢ J.yonedaEquiv.symm (F.val.map f (J.yonedaEquiv u)) = J.yoneda.map f.unop ≫ J.yonedaEquiv.symm (J.yonedaEquiv u)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.add {f g : α → E}
    (hf : IntegrableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
    IntegrableAtFilter (f + g) l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hf : IntegrableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩

Result:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hg : IntegrableAtFilter g l μ
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (f + g) l μ

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
hg : IntegrableAtFilter g l μ
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
rcases hg with ⟨t, tl, ht⟩

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
t : Set α
tl : t ∈ l
ht : IntegrableOn g t μ
⊢ IntegrableAtFilter (f + g) l μ

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
t : Set α
tl : t ∈ l
ht : IntegrableOn g t μ
⊢ IntegrableAtFilter (f + g) l μ

Tactic:
refine ⟨s ∩ t, inter_mem sl tl, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
t : Set α
tl : t ∈ l
ht : IntegrableOn g t μ
⊢ IntegrableOn (f + g) (s ∩ t) μ

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f g : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
t : Set α
tl : t ∈ l
ht : IntegrableOn g t μ
⊢ IntegrableOn (f + g) (s ∩ t) μ

Tactic:
exact (hs.mono_set inter_subset_left).add (ht.mono_set inter_subset_right)

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem enorm_toL1 {f : α → β} (hf : Integrable f μ) : ‖hf.toL1 f‖ₑ = ∫⁻ a, ‖f a‖ₑ ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ₑ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simpa [Integrable.toL1, eLpNorm, eLpNorm', enorm] using ENNReal.coe_toNNReal hf.2.ne

Result:
no goals