harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/IsLUB.lean
theorem IsLUB.exists_seq_monotone_tendsto {t : Set α} {x : α} [IsCountablyGenerated (𝓝 x)]
    (htx : IsLUB t x) (ht : t.Nonempty) :
    ∃ u : ℕ → α, Monotone u ∧ (∀ n, u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ n, u n ∈ t

Proof state:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
rcases htx.exists_seq_strictMono_tendsto_of_not_mem h ht with ⟨u, hu⟩

Result:
case neg.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Proof state:
case neg.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
by_cases h : x ∈ t

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) :
    (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ)

Proof state:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑(Pi.single i j x) * m ^ ↑x = 0

Tactic:
rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Result:
no goals

Proof state:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i

Tactic:
rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]

Result:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0

Proof state:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0

Tactic:
rintro x hx

Result:
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑(Pi.single i j x) * m ^ ↑x = 0
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem Algebra.isIntegral_iSup {ι} (S : ι → Subalgebra R A) :
    Algebra.IsIntegral R ↑(iSup S) ↔ ∀ i, Algebra.IsIntegral R (S i)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Sort u_5
S : ι → Subalgebra R A
⊢ Algebra.IsIntegral R ↥(iSup S) ↔ ∀ (i : ι), Algebra.IsIntegral R ↥(S i)

Tactic:
simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_and' (p : ι' → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p y ∧ q x y → Set α) :
    ⋃ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h =
      ⋃ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y ⟨hy, hx⟩

Proof state:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋃ x, ⋃ y, ⋃ (h : p y ∧ q x y), s x y h = ⋃ y, ⋃ (hy : p y), ⋃ x, ⋃ (hx : q x y), s x y ⋯

Tactic:
simp only [iUnion_and, @iUnion_comm _ ι]

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma hom_inv_apply {M N : CommMonCat} (e : M ≅ N) (s : N) : e.hom (e.inv s) = s

Proof state:
M N : CommMonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem div_surjective (z : K) :
    ∃ x y : A, y ∈ nonZeroDivisors A ∧ algebraMap _ _ x / algebraMap _ _ y = z :=
  let ⟨x, ⟨y, hy⟩, h⟩ := mk'_surjective (nonZeroDivisors A) z
  ⟨x, y, hy, by rwa [mk'_eq_div] at h⟩

Proof state:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
z : K
x y : A
hy : y ∈ nonZeroDivisors A
h : mk' K x ⟨y, hy⟩ = z
⊢ (algebraMap A K) x / (algebraMap A K) y = z

Tactic:
rwa [mk'_eq_div] at h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem append_eq_of_isPrefixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : List α}
    (h : xs.isPrefixOf? ys = some zs) : xs ++ zs = ys

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs ys zs : List α
h : xs.isPrefixOf? ys = some zs
⊢ xs ++ zs = ys

Tactic:
simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_subsingleton_apply [Subsingleton n] (A : Matrix n n α) (b : n → α) (i : n) :
    cramer A b i = b i

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Subsingleton n
A : Matrix n n α
b : n → α
i : n
⊢ A.cramer b i = b i

Tactic:
rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem vecAppend_eq_ite {α : Type*} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) :
    vecAppend ho u v = fun i : Fin o =>
      if h : (i : ℕ) < m then u ⟨i, h⟩ else v ⟨(i : ℕ) - m, by omega⟩

Proof state:
case h.e_e.h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩

Tactic:
simp only [eq_rec_constant]

Result:
case h.e_e.h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩

Proof state:
case h.e_e.h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun i => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
ext i

Result:
case h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Proof state:
case h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ vecAppend ho u v i = if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]

Result:
case h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(Fin.cast ho i) < m then ⋯ ▸ u ((Fin.cast ho i).castLT hi)
    else ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) =
    if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Proof state:
α✝ : Type u
m n o✝ : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
h : ¬↑i < m
⊢ ↑i - m < n

Tactic:
omega

Result:
no goals

Proof state:
case h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
⊢ (if hi : ↑(Fin.cast ho i) < m then ⋯ ▸ u ((Fin.cast ho i).castLT hi)
    else ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯)) =
    if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
congr with hi

Result:
case h.e_e.h
m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
hi : ¬↑(Fin.cast ho i) < m
⊢ ⋯ ▸ v (Fin.subNat m (Fin.cast ⋯ (Fin.cast ho i)) ⋯) = v ⟨↑i - m, ⋯⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_comm [LawfulBEq α] (a b : α) (l : Array α) :
    (l.erase a).erase b = (l.erase b).erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : Array α
⊢ (l.erase a).erase b = (l.erase b).erase a

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
⊢ ({ toList := l }.erase a).erase b = ({ toList := l }.erase b).erase a

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
⊢ ({ toList := l }.erase a).erase b = ({ toList := l }.erase b).erase a

Tactic:
simpa using List.erase_comm a b l

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem isLeast_leastExt (i : ι) : IsLeast {k | b k ∉ E⟮<i⟯} (φ i)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ IsLeast {k | b k ∉ adjoin F (⇑b ∘ φ '' Iio i)} (φ i)

Tactic:
rw [image_eq_range, leastExt, wellFounded_lt.fix_eq]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
⊢ IsLeast
    {k |
      b k ∉
        adjoin F
          (range fun x =>
            (⇑b ∘
                ⋯.fix fun i ih =>
                  let s := range fun j => b (ih ↑j ⋯);
                  ⋯.min {k | b k ∉ adjoin F s} ⋯)
              ↑x)}
    (let s :=
      range fun j =>
        b
          ((fun y x =>
              ⋯.fix
                (fun i ih =>
                  let s := range fun j => b (ih ↑j ⋯);
                  ⋯.min {k | b k ∉ adjoin F s} ⋯)
                y)
            ↑j ⋯);
    ⋯.min {k | b k ∉ adjoin F s} ⋯)
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_neg_of_lt {n k : ℕ} (h : n < k) :
    smeval (ascPochhammer ℕ k) (-n : ℤ) = 0

Proof state:
n k : ℕ
h : n < k
⊢ (ascPochhammer ℕ k).smeval (-↑n) = 0

Tactic:
rw [show k = n + (k - n - 1) + 1 by omega, smeval_ascPochhammer_neg_add]

Result:
no goals

Proof state:
n k : ℕ
h : n < k
⊢ k = n + (k - n - 1) + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem lt_one_of_mul_lt_right [MulLeftReflectLT α] {a b : α} (h : a * b < a) :
    b < 1 :=
  lt_of_mul_lt_mul_left' (a := a) <| by simpa only [mul_one]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a * b < a
⊢ a * b < a * 1

Tactic:
simpa only [mul_one]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Filter.Tendsto.subseq_mem_entourage {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α}
    {a : α} (hu : Tendsto u atTop (𝓝 a)) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧
      ∀ n, (u <| φ (n + 1), u <| φ n) ∈ V (n + 1)

Proof state:
case intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφV : ∀ (n_1 : ℕ), ((u ∘ fun a => a + n) (φ (n_1 + 1)), (u ∘ fun a => a + n) (φ n_1)) ∈ V (n_1 + 1)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
exact ⟨fun k => φ k + n, φ_mono.add_const _, hn _ le_add_self, hφV⟩

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
rcases mem_atTop_sets.1 (hu (ball_mem_nhds a (symm_le_uniformity <| hV 0))) with ⟨n, hn⟩

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)

Tactic:
rcases (hu.comp (tendsto_add_atTop_nat n)).cauchySeq.subseq_mem fun n => hV (n + 1) with
  ⟨φ, φ_mono, hφV⟩

Result:
case intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
a : α
hu : Tendsto u atTop (𝓝 a)
n : ℕ
hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφV : ∀ (n_1 : ℕ), ((u ∘ fun a => a + n) (φ (n_1 + 1)), (u ∘ fun a => a + n) (φ n_1)) ∈ V (n_1 + 1)
⊢ ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_zero : normEDS b c d 0 = 0

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 0 = 0

Tactic:
erw [normEDS_ofNat, preNormEDS'_zero, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem coeff_prod_of_natDegree_le (f : ι → R[X]) (n : ℕ) (h : ∀ p ∈ s, natDegree (f p) ≤ n) :
    coeff (∏ i ∈ s, f i) (#s * n) = ∏ i ∈ s, coeff (f i) n

Proof state:
case h.e'_2.h.e'_4.h.e'_5
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ #{ val := l, nodup := hl } = (Multiset.map f l).card

Tactic:
simp

Result:
no goals

Proof state:
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ (∏ i ∈ { val := l, nodup := hl }, f i).coeff (#{ val := l, nodup := hl } * n) =
    ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n

Tactic:
convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_

Result:
case h.e'_2.h.e'_4.h.e'_5
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ #{ val := l, nodup := hl } = (Multiset.map f l).card

case h.e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p => p.coeff n) (Multiset.map f l)).prod

case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
h : ∀ p ∈ s, (f p).natDegree ≤ n
⊢ (∏ i ∈ s, f i).coeff (#s * n) = ∏ i ∈ s, (f i).coeff n

Tactic:
obtain ⟨l, hl⟩ := s

Result:
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ (∏ i ∈ { val := l, nodup := hl }, f i).coeff (#{ val := l, nodup := hl } * n) =
    ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n

Proof state:
case h.e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p => p.coeff n) (Multiset.map f l)).prod

Tactic:
simp

Result:
no goals

Proof state:
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem self_symm_id_assoc (α : X ≅ Y) (β : X ≅ Z) : α ≪≫ α.symm ≪≫ β = β

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
α : X ≅ Y
β : X ≅ Z
⊢ α ≪≫ α.symm ≪≫ β = β

Tactic:
rw [← trans_assoc, self_symm_id, refl_trans]

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem traverse_map {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _}
    (g : α → β) (h : β → G γ) (x : Multiset α) : traverse h (map g x) = traverse (h ∘ g) x

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ ∀ (a : List α), traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧

Tactic:
intro

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ traverse h (map g ⟦a✝⟧) = traverse (h ∘ g) ⟦a✝⟧

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ traverse h (map g ⟦a✝⟧) = traverse (h ∘ g) ⟦a✝⟧

Tactic:
simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ ofList <$> Traversable.traverse h (List.map g a✝) = ofList <$> Traversable.traverse (h ∘ g) a✝

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ traverse h (map g x) = traverse (h ∘ g) x

Tactic:
refine Quotient.inductionOn x ?_

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
⊢ ∀ (a : List α), traverse h (map g ⟦a⟧) = traverse (h ∘ g) ⟦a⟧

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
x : Multiset α
a✝ : List α
⊢ ofList <$> Traversable.traverse h (List.map g a✝) = ofList <$> Traversable.traverse (h ∘ g) a✝

Tactic:
rw [← Traversable.traverse_map h g, List.map_eq_map]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Idempotents.lean
lemma isIdempotentElem_idempotent (i : I) : IsIdempotentElem (idempotent V i : R)

Proof state:
R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
i : I
⊢ IsIdempotentElem (idempotent V i)

Tactic:
rw [IsIdempotentElem, ← decompose_eq_mul_idempotent, idempotent, decompose_coe, of_eq_same]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sUnion_singleton {x : ZFSet.{u}} : ⋃₀ ({x} : ZFSet) = x :=
  ext fun y => by simp_rw [mem_sUnion, mem_singleton, exists_eq_left]

Proof state:
x y : ZFSet.{u}
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x

Tactic:
simp_rw [mem_sUnion, mem_singleton, exists_eq_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_mkVector {n : Nat} {a : α} {k : Nat} {h} :
    (mkVector n a).eraseIdx k = mkVector (n - 1) a

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ { toArray := (mkArray n a).eraseIdx k ⋯, size_toArray := ⋯ } = mkVector (n - 1) a

Tactic:
simp [Array.eraseIdx_mkArray, *]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ (mkVector n a).eraseIdx k h = mkVector (n - 1) a

Tactic:
rw [mkVector_eq_mk_mkArray, eraseIdx_mk]

Result:
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ { toArray := (mkArray n a).eraseIdx k ⋯, size_toArray := ⋯ } = mkVector (n - 1) a
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α}
    {c : Set ι} (hn : c.Nonempty) (hc : DirectedOn (fun i j => f i ⊆ f j) c) {s : Finset α}
    (hs : (s : Set α) ⊆ ⋃ i ∈ c, f i) : ∃ i ∈ c, (s : Set α) ⊆ f i

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
rw [Set.biUnion_eq_iUnion] at hs

Result:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
⊢ ∃ i ∈ c, ↑s ⊆ f i

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
haveI := hn.coe_sort

Result:
α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ x, f ↑x
this : Nonempty ↑c
⊢ ∃ i ∈ c, ↑s ⊆ f i
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem coeff_add (A B : HVertexOperator Γ R V W) : (A + B).coeff = A.coeff + B.coeff

Proof state:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A B : HVertexOperator Γ R V W
⊢ (A + B).coeff = A.coeff + B.coeff

Tactic:
ext

Result:
case h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A B : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ ((A + B).coeff x✝¹) x✝ = ((A.coeff + B.coeff) x✝¹) x✝

Proof state:
case h.h
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A B : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ ((A + B).coeff x✝¹) x✝ = ((A.coeff + B.coeff) x✝¹) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem le_card_iff_exists_subset_card : n ≤ #s ↔ ∃ t ⊆ s, #t = n

Proof state:
α : Type u_1
s : Finset α
n : ℕ
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n

Tactic:
refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩

Result:
α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Proof state:
α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
exact exists_subset_card_eq h

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem one_lt_card_iff_nontrivial (α : Type*) : 1 < card α ↔ Nontrivial α

Proof state:
α : Type u_1
⊢ 1 < card α ↔ Nontrivial α

Tactic:
rw [← Cardinal.one_lt_iff_nontrivial]

Result:
α : Type u_1
⊢ 1 < card α ↔ 1 < #α

Proof state:
α : Type u_1
⊢ 1 < card α ↔ 1 < #α

Tactic:
conv_rhs => rw [← Nat.cast_one]

Result:
α : Type u_1
⊢ 1 < card α ↔ ↑1 < #α

Proof state:
α : Type u_1
⊢ 1 < card α ↔ ↑1 < toPartENat #α

Tactic:
simp only [PartENat.card, Nat.cast_one]

Result:
no goals

Proof state:
α : Type u_1
⊢ 1 < card α ↔ ↑1 < #α

Tactic:
rw [← natCast_lt_toPartENat_iff]

Result:
α : Type u_1
⊢ 1 < card α ↔ ↑1 < toPartENat #α
-- Mathlib/Data/Set/Prod.lean
theorem univ_prod {t : Set β} : (univ : Set α) ×ˢ t = Prod.snd ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
t : Set β
⊢ univ ×ˢ t = Prod.snd ⁻¹' t

Tactic:
simp [prod_eq]

Result:
no goals