harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem cauchy_tendsto_of_tendsto {f : ℕ → α → E} (hf : ∀ n, AEStronglyMeasurable (f n) μ)
    (f_lim : α → E) {B : ℕ → ℝ≥0∞} (hB : ∑' i, B i ≠ ∞)
    (h_cau : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N)
    (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))

Tactic:
refine h_lim.mono fun x hx => ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
B : ℕ → ℝ≥0∞
hB : ∑' (i : ℕ), B i ≠ ⊤
h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
ε : ℝ≥0∞
hε : ε > 0
N : ℕ
h_B : B N ≤ ε
n : ℕ
hn : n ≥ N
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun n_1 => (f n - f n_1) x) atTop (𝓝 ((f n - f_lim) x))
-- Mathlib/Data/Finset/Erase.lean
theorem erase_idem {a : α} {s : Finset α} : erase (erase s a) a = erase s a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (s.erase a).erase a = s.erase a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_nonneg_iff_neg_imp_nonpos [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftMono α] [AddLeftReflectLE α] :
    0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
rw [← neg_mul_neg, mul_nonneg_iff_pos_imp_nonneg (α := α)]

Result:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem natDegree_derivative_le (p : R[X]) : p.derivative.natDegree ≤ p.natDegree - 1

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
simp [p0, derivative_of_natDegree_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (derivative p).natDegree ≤ p.natDegree - 1

Tactic:
by_cases p0 : p.natDegree = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ (derivative p).natDegree ≤ p.natDegree - 1
-- Mathlib/RingTheory/Binomial.lean
theorem descPochhammer_succ_succ_smeval {R} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R]
    (r : R) (k : ℕ) : smeval (descPochhammer ℤ (k + 1)) (r + 1) =
    (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + ((X - ↑k) * descPochhammer ℤ k).smeval r

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
nth_rw 1 [descPochhammer_succ_left]

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ (k + 1)).smeval r

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (X * (descPochhammer ℤ k).comp (X - 1)).smeval (r + 1) =
    (k + 1) • (descPochhammer ℤ k).smeval r + ((X - ↑k) * descPochhammer ℤ k).smeval r

Tactic:
simp only [smeval_comp, smeval_sub, smeval_add, smeval_mul, smeval_X, smeval_one, npow_one,
  npow_zero, one_smul, add_sub_cancel_right, sub_mul, add_mul, add_smul, one_mul]

Result:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    k • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r +
      (r * (descPochhammer ℤ k).smeval r - (↑k).smeval r * (descPochhammer ℤ k).smeval r)

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ r * (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r =
    k • (descPochhammer ℤ k).smeval r + (descPochhammer ℤ k).smeval r +
      (r * (descPochhammer ℤ k).smeval r - (↑k).smeval r * (descPochhammer ℤ k).smeval r)

Tactic:
rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
  add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc,  ← add_sub_assoc,
  nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem ξ_ne_0 : ξ K x ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
⊢ False

Tactic:
apply hxl

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
⊢ x = 0

Proof state:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)

Tactic:
have hblin := Basis.linearIndependent (newBasis K)

Result:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : LinearIndependent ℤ ⇑(NumberField.house.newBasis K)
⊢ x (l, r) = 0 (l, r)

Proof state:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : LinearIndependent ℤ ⇑(NumberField.house.newBasis K)
⊢ x (l, r) = 0 (l, r)

Tactic:
simp only [zsmul_eq_mul, Fintype.linearIndependent_iff] at hblin

Result:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : ∀ (g : (K →+* ℂ) → ℤ), ∑ x : K →+* ℂ, ↑(g x) * (NumberField.house.newBasis K) x = 0 → ∀ (i : K →+* ℂ), g i = 0
⊢ x (l, r) = 0 (l, r)

Proof state:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)

Tactic:
rw [funext_iff] at H

Result:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)

Proof state:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), NumberField.house.ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : ∀ (g : (K →+* ℂ) → ℤ), ∑ x : K →+* ℂ, ↑(g x) * (NumberField.house.newBasis K) x = 0 → ∀ (i : K →+* ℂ), g i = 0
⊢ x (l, r) = 0 (l, r)

Tactic:
exact hblin (fun r ↦ x (l,r)) (H _) r

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
⊢ x = 0

Tactic:
ext ⟨l, r⟩

Result:
case h.mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
⊢ NumberField.house.ξ K x ≠ 0

Tactic:
intro H

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : NumberField.house.ξ K x = 0
⊢ False
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
lemma norm_sub_nonneg (f : α →ᵇ ℝ) :
    0 ≤ const _ ‖f‖ - f

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (const α ‖f‖ - f) x

Tactic:
simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_sub,
  const_apply, Pi.sub_apply, sub_nonneg]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x ≤ ‖f‖

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ 0 ≤ const α ‖f‖ - f

Tactic:
intro x

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (const α ‖f‖ - f) x

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ f x ≤ ‖f‖

Tactic:
linarith [(abs_le.mp (norm_coe_le_norm f x)).2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem_insertIdx_of_ge {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k)
    (hk : k < (insertIdx n x l).length) :
    (insertIdx n x l)[k] = l[k - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega)

Proof state:
α : Type u
l : List α
x : α
n k : Nat
hn : n + 1 ≤ k
hk : k < (insertIdx n x l).length
⊢ (insertIdx n x l)[k] = l[k - 1]

Tactic:
induction l generalizing n k with
| nil =>
  cases n with
  | zero =>
    simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk
    omega
  | succ n => simp at hk
| cons _ _ ih =>
  cases n with
  | zero =>
    simp only [insertIdx_zero] at hk
    cases k with
    | zero => omega
    | succ k => simp
  | succ n =>
    cases k with
    | zero => simp
    | succ k =>
      simp only [insertIdx_succ_cons, getElem_cons_succ]
      rw [ih (by omega)]
      cases k with
      | zero => omega
      | succ k => simp

Result:
no goals

Proof state:
case cons.succ.succ
α : Type u
x head✝ : α
tail✝ : List α
ih : ∀ {n k : Nat} (hn : n + 1 ≤ k) (hk : k < (insertIdx n x tail✝).length), (insertIdx n x tail✝)[k] = tail✝[k - 1]
n k : Nat
hn : n + 1 + 1 ≤ k + 1
hk : k + 1 < (insertIdx (n + 1) x (head✝ :: tail✝)).length
⊢ tail✝[k - 1] = (head✝ :: tail✝)[k + 1 - 1]

Tactic:
cases k with
| zero => omega
| succ k => simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
x : α
n k : Nat
hn : n + 1 ≤ k
hk : k < if n ≤ l.length then l.length + 1 else l.length
⊢ k - 1 < l.length

Tactic:
split at hk <;> omega

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supported_le_supported_iff [Nontrivial R] : supported R s ≤ supported R t ↔ s ⊆ t

Proof state:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t

Tactic:
intro h i

Result:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t

Proof state:
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t

Tactic:
constructor

Result:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t → s ⊆ t

case mpr
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t

Proof state:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t

Tactic:
simpa using @h (X i)

Result:
no goals

Proof state:
case mpr
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ s ⊆ t → supported R s ≤ supported R t

Tactic:
exact supported_mono

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem iUnion_compactCovering : ⋃ n, compactCovering X n = univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ n, compactCovering X n = univ

Tactic:
rw [compactCovering, iUnion_accumulate]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ x, ⋯.choose x = univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ x, ⋯.choose x = univ

Tactic:
exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_succ_eq_sum_choose :
    ∀ n : ℕ, fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, choose p.1 p.2 :=
  twoStepInduction rfl rfl fun n h1 h2 => by
    rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
    simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]

Proof state:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 +
      ∑
        p ∈
          Finset.cons (n + 1, 0)
            (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯,
        p.1.choose p.2 =
    ∑
      p ∈
        Finset.cons (0, n + 2)
          (Finset.cons (n + 2, 0)
            (Finset.map ({ toFun := succ, inj' := succ_injective }.prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯)
          ⋯,
      p.1.choose p.2

Tactic:
simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]

Result:
no goals

Proof state:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ fib (n + 2 + 1) = ∑ p ∈ Finset.antidiagonal (n + 2), p.1.choose p.2

Tactic:
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']

Result:
n : ℕ
h1 : fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2
h2 : fib (n + 1 + 1) = ∑ p ∈ Finset.antidiagonal (n + 1), p.1.choose p.2
⊢ ∑ p ∈ Finset.antidiagonal n, p.1.choose p.2 +
      ∑
        p ∈
          Finset.cons (n + 1, 0)
            (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯,
        p.1.choose p.2 =
    ∑
      p ∈
        Finset.cons (0, n + 2)
          (Finset.cons (n + 2, 0)
            (Finset.map ({ toFun := succ, inj' := succ_injective }.prodMap { toFun := succ, inj' := succ_injective })
              (Finset.antidiagonal n))
            ⋯)
          ⋯,
      p.1.choose p.2
-- Mathlib/FieldTheory/Finiteness.lean
theorem iff_fg : IsNoetherian K V ↔ Module.Finite K V

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ span K ↑(finsetBasisIndex K V) = ⊤

Tactic:
convert (finsetBasis K V).span_eq

Result:
case h.e'_2.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ ↑(finsetBasisIndex K V) = Set.range ⇑(finsetBasis K V)

Proof state:
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V → Module.Finite K V

Tactic:
intro h

Result:
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ Module.Finite K V

Proof state:
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ Module.rank K ↥(span K ↑s) < ℵ₀

Tactic:
exact lt_of_le_of_lt (rank_span_le _) s.finite_toSet.lt_aleph0

Result:
no goals

Proof state:
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ Module.Finite K V

Tactic:
exact
  ⟨⟨finsetBasisIndex K V, by
      convert (finsetBasis K V).span_eq
      simp⟩⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.Finite K V

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V → Module.Finite K V

case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.Finite K V → IsNoetherian K V

Proof state:
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.Finite K V → IsNoetherian K V

Tactic:
rintro ⟨s, hs⟩

Result:
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ IsNoetherian K V

Proof state:
case h.e'_2.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ ↑(finsetBasisIndex K V) = Set.range ⇑(finsetBasis K V)

Tactic:
simp

Result:
no goals

Proof state:
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ IsNoetherian K V

Tactic:
rw [IsNoetherian.iff_rank_lt_aleph0, ← rank_top, ← hs]

Result:
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ Module.rank K ↥(span K ↑s) < ℵ₀
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_sup_left : map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f₁ f₂ : Filter α
g : Filter β
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g

Tactic:
simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma mapClusterPt_iff (hf : IsInducing f) {x : X} {l : Filter X} :
    MapClusterPt (f x) l f ↔ ClusterPt x l

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ MapClusterPt (f x) l f ↔ ClusterPt x l

Tactic:
delta MapClusterPt ClusterPt

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot

Tactic:
rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem coeff_eq_zero_of_totalDegree_lt {f : MvPolynomial σ R} {d : σ →₀ ℕ}
    (h : f.totalDegree < ∑ i ∈ d.support, d i) : coeff d f = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
refine not_not.mp (mt h ?_)

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ ¬(d.sum fun x e => e) < ∑ i ∈ d.support, d i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
rw [totalDegree, Finset.sup_lt_iff] at h

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, (b.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s => s.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s => s.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i

Tactic:
exact lt_of_le_of_lt (Nat.zero_le _) h

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ f.support → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
rw [mem_support_iff] at h

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ b ∈ f.support, (b.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
specialize h d

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ f.support → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e => e) < ∑ i ∈ d.support, d i
⊢ ¬(d.sum fun x e => e) < ∑ i ∈ d.support, d i

Tactic:
exact lt_irrefl _

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated genEigenspace_inf_le_add (since := "2024-10-23")]
lemma iSup_genEigenspace_inf_le_add
    (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) :
    (⨆ k : ℕ, f₁.genEigenspace μ₁ k) ⊓ (⨆ k : ℕ, f₂.genEigenspace μ₂ k) ≤
    ⨆ k : ℕ, (f₁ + f₂).genEigenspace (μ₁ + μ₂) k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
h : Commute f₁ f₂
⊢ f₁.maxGenEigenspace μ₁ ⊓ f₂.maxGenEigenspace μ₂ ≤ (f₁ + f₂).maxGenEigenspace (μ₁ + μ₂)

Tactic:
apply genEigenspace_inf_le_add

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
h : Commute f₁ f₂
⊢ Commute f₁ f₂

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
h : Commute f₁ f₂
⊢ Commute f₁ f₂

Tactic:
assumption

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
h : Commute f₁ f₂
⊢ (⨆ k, (f₁.genEigenspace μ₁) ↑k) ⊓ ⨆ k, (f₂.genEigenspace μ₂) ↑k ≤ ⨆ k, ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) ↑k

Tactic:
simp_rw [iSup_genEigenspace_eq]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
h : Commute f₁ f₂
⊢ f₁.maxGenEigenspace μ₁ ⊓ f₂.maxGenEigenspace μ₂ ≤ (f₁ + f₂).maxGenEigenspace (μ₁ + μ₂)