harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_list_prod_le (l : List S[X]) : degree l.prod ≤ (l.map degree).sum

Proof state:
case nil
S : Type u_1
inst✝ : Semiring S
⊢ [].prod.degree ≤ (List.map degree []).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : tl.prod.degree ≤ (List.map degree tl).sum
⊢ (hd :: tl).prod.degree ≤ (List.map degree (hd :: tl)).sum

Tactic:
simpa using (degree_mul_le _ _).trans (add_le_add_left IH _)

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.prod.degree ≤ (List.map degree l).sum

Tactic:
induction' l with hd tl IH

Result:
case nil
S : Type u_1
inst✝ : Semiring S
⊢ [].prod.degree ≤ (List.map degree []).sum

case cons
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : tl.prod.degree ≤ (List.map degree tl).sum
⊢ (hd :: tl).prod.degree ≤ (List.map degree (hd :: tl)).sum
-- Mathlib/Logic/Equiv/Option.lean
theorem removeNone_aux_none {x : α} (h : e (some x) = none) :
    some (removeNone_aux e x) = e none

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone_aux x) = e none

Tactic:
simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
@[simp] lemma le_sub_one_iff {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0

Proof state:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k ≤ ↑(k - 1) ↔ k = 0

Tactic:
rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp,
  eq_comm, sub_eq_iff_eq_add]

Result:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k = k + 1 → k = 0

Proof state:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
simp only [le_def]

Result:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ ↑k ≤ ↑(k - 1) ↔ k = 0

Proof state:
case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k = k + 1 → k = 0

Tactic:
simp

Result:
no goals

Proof state:
case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
simp [fin_one_eq_zero k]

Result:
no goals

Proof state:
n : ℕ
k : Fin (n + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
cases n

Result:
case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0

case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k ≤ k - 1 ↔ k = 0
-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.coeff_support_bddBelow {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) :
    BddBelow (coeff hℱ).support

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
hNd : ¬⋯.choose ≤ d
⊢ False

Tactic:
exact hd ((exists_lb_support hℱ).choose_spec d (not_le.mp hNd))

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ BddBelow (Function.support (coeff hℱ))

Tactic:
refine ⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
⊢ ⋯.choose ≤ d

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
⊢ ⋯.choose ≤ d

Tactic:
by_contra hNd

Result:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
hNd : ¬⋯.choose ≤ d
⊢ False
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_eq_sSup_image [CompleteLattice β] (s : Finset α) (f : α → β) :
    s.sup f = sSup (f '' s)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' ↑s)

Tactic:
classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' ↑s)

Tactic:
rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem {s : AffineSubspace k P} {p₁ p₂ p₃ : P}
    (hp₁p₃ : p₁ ≠ p₃) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∉ s) (hp₃ : p₃ ∈ s) :
    AffineIndependent k ![p₁, p₂, p₃]

Proof state:
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₃, p₂] x

Tactic:
fin_cases x <;> rfl

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k ![p₁, p₂, p₃]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap (1 : Fin 3) 2)]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2))

Proof state:
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2) = ![p₁, p₃, p₂]

Tactic:
ext x

Result:
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2)) x = ![p₁, p₃, p₂] x

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2))

Tactic:
convert affineIndependent_of_ne_of_mem_of_mem_of_not_mem hp₁p₃ hp₁ hp₃ hp₂ using 1

Result:
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₁p₃ : p₁ ≠ p₃
hp₁ : p₁ ∈ s
hp₂ : p₂ ∉ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 1 2) = ![p₁, p₃, p₂]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m

Proof state:
n m : Nat
⊢ (n - 1) * m = n * m - m

Tactic:
cases n with
| zero   => simp
| succ n =>
  rw [Nat.add_sub_cancel, add_one_mul, Nat.add_sub_cancel]

Result:
no goals

Proof state:
case zero
m : Nat
⊢ (0 - 1) * m = 0 * m - m

Tactic:
simp

Result:
no goals

Proof state:
case succ
m n : Nat
⊢ (n + 1 - 1) * m = (n + 1) * m - m

Tactic:
rw [Nat.add_sub_cancel, add_one_mul, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff
    [HasWeakSheafify J (Type v)]
    (F : Sheaf J (Type v)) (sq : Square C) :
    (sq.op.map ((yoneda ⋙ presheafToSheaf J _).op ⋙ yoneda.obj F)).IsPullback ↔
      (sq.op.map F.val).IsPullback

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₂ =
    (sq.op.map F.val).f₁₂ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₁₃ =
    (sq.op.map F.val).f₁₃ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₁)) F).trans yonedaEquiv)

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₂₄ =
    (sq.op.map F.val).f₂₄ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₂)) F).trans yonedaEquiv)

case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₄)) F).trans yonedaEquiv) ∘
      (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).f₃₄ =
    (sq.op.map F.val).f₃₄ ∘
      ⇑(((sheafificationAdjunction J (Type v)).homEquiv (yoneda.obj (unop sq.op.X₃)) F).trans yonedaEquiv)

Tactic:
all_goals
  ext x
  dsimp
  rw [yonedaEquiv_naturality]
  erw [Adjunction.homEquiv_naturality_left]
  rfl

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
theorem exists_finset_support (x : FreeCommRing α) : ∃ s : Finset α, IsSupported x ↑s :=
  let ⟨s, hfs, hxs⟩ := exists_finite_support x
  ⟨hfs.toFinset, by rwa [Set.Finite.coe_toFinset]⟩

Proof state:
α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs : x.IsSupported s
⊢ x.IsSupported ↑hfs.toFinset

Tactic:
rwa [Set.Finite.coe_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem of_decide_eq_true {p : Prop} {_ : Decidable p} : decide p = true → p = True

Proof state:
p : Prop
x✝ : Decidable p
⊢ decide p = true → p = True

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_liminf_le {ι} [Countable ι] [LinearOrder ι] (f : ι → α → ℝ≥0∞) :
    essSup (fun x => atTop.liminf fun n => f n x) μ ≤
      atTop.liminf fun n => essSup (fun x => f n x) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → ℝ≥0∞
⊢ essSup (fun x => liminf (fun n => f n x) atTop) μ ≤ liminf (fun n => essSup (fun x => f n x) μ) atTop

Tactic:
simp_rw [essSup]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → ℝ≥0∞
⊢ limsup (fun x => liminf (fun n => f n x) atTop) (ae μ) ≤ liminf (fun n => limsup (fun x => f n x) (ae μ)) atTop

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
inst✝¹ : Countable ι
inst✝ : LinearOrder ι
f : ι → α → ℝ≥0∞
⊢ limsup (fun x => liminf (fun n => f n x) atTop) (ae μ) ≤ liminf (fun n => limsup (fun x => f n x) (ae μ)) atTop

Tactic:
exact ENNReal.limsup_liminf_le_liminf_limsup fun a b => f b a

Result:
no goals
-- Mathlib/Data/Prod/TProd.lean
theorem ext :
    ∀ {l : List ι} (_ : l.Nodup) {v w : TProd α l}
      (_ : ∀ (i) (hi : i ∈ l), v.elim hi = w.elim hi), v = w
  | [], _, v, w, _ => PUnit.ext v w
  | i :: is, hl, v, w, hvw => by
    apply Prod.ext
    · rw [← elim_self v, hvw, elim_self]
    refine ext (nodup_cons.mp hl).2 fun j hj => ?_
    rw [← elim_of_mem hl, hvw, elim_of_mem hl]

Proof state:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.2 = w.2

Tactic:
refine ext (nodup_cons.mp hl).2 fun j hj => ?_

Result:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.2 hj = TProd.elim w.2 hj

Proof state:
case fst
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.1 = w.1

Tactic:
rw [← elim_self v, hvw, elim_self]

Result:
no goals

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v = w

Tactic:
apply Prod.ext

Result:
case fst
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.1 = w.1

case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.2 = w.2

Proof state:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
j : ι
hj : j ∈ is
⊢ TProd.elim v.2 hj = TProd.elim w.2 hj

Tactic:
rw [← elim_of_mem hl, hvw, elim_of_mem hl]

Result:
no goals
-- Mathlib/Analysis/SumOverResidueClass.lean
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` is not summable. -/
lemma not_summable_of_antitone_of_neg {f : ℕ → ℝ} (hf : Antitone f) {n : ℕ} (hn : f n < 0) :
    ¬ Summable f

Proof state:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
⊢ ¬Summable f

Tactic:
intro hs

Result:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
⊢ False

Proof state:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : |f (n ⊔ N)| < |f n|
⊢ False

Tactic:
contrapose! hN

Result:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ¬False
⊢ |f n| ≤ |f (n ⊔ N)|

Proof state:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (n ⊔ N) ≤ f n
⊢ |f n| ≤ |f (n ⊔ N)|

Tactic:
rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]

Result:
no goals

Proof state:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : Filter.Tendsto f Filter.atTop (nhds 0)
⊢ False

Tactic:
simp only [Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs] at this

Result:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
⊢ False

Proof state:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
⊢ False

Tactic:
obtain ⟨N, hN⟩ := this (|f n|) (abs_pos_of_neg hn)

Result:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ∀ n_1 ≥ N, |f n_1| < |f n|
⊢ False

Proof state:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ¬False
⊢ |f n| ≤ |f (n ⊔ N)|

Tactic:
clear hN

Result:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
⊢ |f n| ≤ |f (n ⊔ N)|

Proof state:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
⊢ False

Tactic:
have := hs.tendsto_atTop_zero

Result:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : Filter.Tendsto f Filter.atTop (nhds 0)
⊢ False

Proof state:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
⊢ |f n| ≤ |f (n ⊔ N)|

Tactic:
have H : f (max n N) ≤ f n := hf (n.le_max_left N)

Result:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (n ⊔ N) ≤ f n
⊢ |f n| ≤ |f (n ⊔ N)|

Proof state:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ∀ n_1 ≥ N, |f n_1| < |f n|
⊢ False

Tactic:
specialize hN (max n N) (n.le_max_right N)

Result:
case intro
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
hN : |f (n ⊔ N)| < |f n|
⊢ False
-- Mathlib/RingTheory/FiniteLength.lean
theorem IsSemisimpleModule.finite_tfae [IsSemisimpleModule R M] :
    List.TFAE [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M,
      ∃ s : Set (Submodule R M), s.Finite ∧ sSupIndep s ∧
        sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m]

Proof state:
case intro
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_5_to_4 :
  (∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m) → IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : IsNoetherian R M ∧ IsArtinian R M → IsNoetherian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Tactic:
tfae_have 4 → 3 := And.right

Result:
case intro
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_5_to_4 :
  (∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m) → IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : IsNoetherian R M ∧ IsArtinian R M → IsNoetherian R M
tfae_4_to_3 : IsNoetherian R M ∧ IsArtinian R M → IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

Proof state:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s✝ : Set (Submodule R M)
hs : sSupIndep s✝ ∧ sSup s✝ = ⊤ ∧ ∀ m ∈ s✝, IsSimpleModule R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 : IsNoetherian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
tfae_3_to_5 : IsArtinian R M → ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
x✝ : ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m
s : Set (Submodule R M)
fin : s.Finite
left✝ : sSupIndep s
sSup_eq_top : sSup s = ⊤
simple : ∀ (x : ↑s), IsSimpleModule R ↥↑x
this : Finite ↑s
⊢ IsNoetherian R ↥(⨆ i, ↑i) ∧ IsArtinian R ↥(⨆ i, ↑i)

Tactic:
exact ⟨isNoetherian_iSup, isArtinian_iSup⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/Properties.lean
theorem isReduced_of_isReduced_stalk [∀ x : X, _root_.IsReduced (X.presheaf.stalk x)] :
    IsReduced X

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0

Tactic:
change X.presheaf.germ U x hx s = 0

Result:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hx)) s = 0

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Tactic:
rw [RingHom.map_zero]

Result:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
⊢ IsReduced X

Tactic:
refine ⟨fun U => ⟨fun s hs => ?_⟩⟩

Result:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ s = 0

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
    (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Tactic:
intro x hx

Result:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hx)) s = 0

Tactic:
exact (hs.map _).eq_zero

Result:
no goals

Proof state:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ s = 0

Tactic:
apply Presheaf.section_ext X.sheaf U s 0

Result:
X : Scheme
inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
    (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_top : ￢(⊤ : α) = ⊥

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
⊢ ￢⊤ = ⊥

Tactic:
rw [← top_sdiff', sdiff_self]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.strictConvex' {s : Set E} (hs : Convex 𝕜 s)
    (h : (s \ interior s).Pairwise fun x y => ∃ c : 𝕜, lineMap x y c ∈ interior s) :
    StrictConvex 𝕜 s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s
⊢ StrictConvex 𝕜 s

Tactic:
refine strictConvex_iff_openSegment_subset.2 ?_

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s
⊢ s.Pairwise fun x y => openSegment 𝕜 x y ⊆ interior s

Proof state:
case pos
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ∃ c, (lineMap x y) c ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
exact hs.openSegment_self_interior_subset_interior hx hy'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_eq_none [DecidablePred p] : Option.guard p a = none ↔ ¬ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝ : DecidablePred p
h : ¬p a
⊢ guard p a = none ↔ ¬p a

Tactic:
simp [Option.guard, h]

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝ : DecidablePred p
h : p a
⊢ guard p a = none ↔ ¬p a

Tactic:
simp [Option.guard, h]

Result:
no goals