harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/PrimeFin.lean
lemma primeFactors_pow_succ (n k : ℕ) : (n ^ (k + 1)).primeFactors = n.primeFactors

Proof state:
n k : ℕ
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0

case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Proof state:
case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ (n ^ (0 + 1)).primeFactors = n.primeFactors

Tactic:
simp

Result:
no goals

Proof state:
case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
induction' k with k ih

Result:
case inr.zero
n : ℕ
hn : n ≠ 0
⊢ (n ^ (0 + 1)).primeFactors = n.primeFactors

case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors

Proof state:
case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors

Tactic:
rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_le_max (a b : Cardinal) : a * b ≤ max (max a b) ℵ₀

Proof state:
case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

Result:
no goals

Proof state:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]

Result:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb0]

Result:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ b with hb | hb

Result:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ a with ha | ha

Result:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

case inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases eq_or_ne b 0 with (rfl | hb0)

Result:
case inr.inl
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ a ⊔ 0 ⊔ ℵ₀

case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
a b : Cardinal.{u_1}
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases eq_or_ne a 0 with (rfl | ha0)

Result:
case inl
b : Cardinal.{u_1}
⊢ 0 * b ≤ 0 ⊔ b ⊔ ℵ₀

case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inl
b : Cardinal.{u_1}
⊢ 0 * b ≤ 0 ⊔ b ⊔ ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
case inr.inl
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ a ⊔ 0 ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_sub_left : neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g₁ g₂ : Π₀ (a : α), N a
⊢ (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂

Tactic:
simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_add {α} [AddCommMonoid α] (l r tl tr t)
    (prl : (l : α) = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma basis_apply (n : Fin 2) :
    CoordinateRing.basis W n = (AdjoinRoot.powerBasis' W.monic_polynomial).gen ^ (n : ℕ)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
  PowerBasis.basis_eq_pow]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (AdjoinRoot.powerBasis' ⋯).gen ^ ↑((finCongr ⋯).symm n) = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
a✝ : Nontrivial R
⊢ (AdjoinRoot.powerBasis' ⋯).gen ^ ↑((finCongr ⋯).symm n) = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
classical
nontriviality R
rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
  PowerBasis.basis_eq_pow]
rfl

Result:
no goals
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem le_algebraicClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsAlgebraic F x) :
    L ≤ algebraicClosure F E := fun x h ↦ by
  simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
    Algebra.id.map_eq_id, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsAlgebraic F x
x : E
h : x ∈ L
⊢ x ∈ algebraicClosure F E

Tactic:
simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
  Algebra.id.map_eq_id, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [MeasurableSpace F]
    [BorelSpace F] (f : 𝕜 → F) : Measurable (deriv f)

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : MeasurableSpace 𝕜
inst✝² : OpensMeasurableSpace 𝕜
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : 𝕜 → F
⊢ Measurable (deriv f)

Tactic:
simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_le_of_le_directed {α : Type*} [SemilatticeSup α] [OrderBot α] (s : Set α)
    (hs : s.Nonempty) (hdir : DirectedOn (· ≤ ·) s) (t : Finset α) :
    (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Proof state:
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
t : Finset α
⊢ (∀ x ∈ t, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, t.sup id ≤ x

Tactic:
induction' t using Finset.induction_on with a r _ ih h

Result:
case empty
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ (∀ x ∈ ∅, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, ∅.sup id ≤ x

case insert
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
⊢ (∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, (insert a r).sup id ≤ x
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem complementedLattice_iff_isAtomistic : ComplementedLattice α ↔ IsAtomistic α

Proof state:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α

Tactic:
constructor <;> intros

Result:
case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α

Proof state:
case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

Tactic:
exact isAtomistic_of_complementedLattice

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
exact complementedLattice_of_isAtomistic

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
/-- See also `Order.pred_eq_of_covBy`. -/
lemma pred_le_of_wcovBy (h : a ⩿ b) : pred b ≤ a

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ pred b ≤ a

Tactic:
exact (pred_le _).trans hba

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬pred b ≤ a
⊢ False

Tactic:
exact h.2 (hab.lt.le_pred.lt_of_not_le hba) (pred_lt_of_not_isMin hab.lt.not_isMin)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
⊢ pred b ≤ a

Tactic:
obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le

Result:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ pred b ≤ a

case inr.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ pred b ≤ a

Proof state:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ pred b ≤ a

Tactic:
by_contra hba

Result:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬pred b ≤ a
⊢ False
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_ext_iff {l₁ l₂ : List α} : l₁ <+~ l₂ ↔ ∀ x ∈ l₁, count x l₁ ≤ count x l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ l₂.diff l₁ ++ l₁
⊢ l₁ <+~ l₂

Tactic:
refine this.trans (Perm.subperm ?_)

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ l₂.diff l₁ ++ l₁
⊢ l₂.diff l₁ ++ l₁ ~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ l₂.diff l₁ ++ l₁
⊢ l₂.diff l₁ ++ l₁ ~ l₂

Tactic:
exact perm_append_comm.trans (subperm_append_diff_self_of_count_le h)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂

Tactic:
refine ⟨fun h x _ => h.count_le x, fun h => ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
⊢ l₁ <+~ l₂

Tactic:
have : l₁ <+~ l₂.diff l₁ ++ l₁ := (subperm_append_right l₁).mpr nil_subperm

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ∀ (x : α), x ∈ l₁ → count x l₁ ≤ count x l₂
this : l₁ <+~ l₂.diff l₁ ++ l₁
⊢ l₁ <+~ l₂
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem bell_eq (m : Multiset ℕ) :
    m.bell = m.sum ! / ((m.map (fun j ↦ j !)).prod *
      ∏ j ∈ (m.toFinset.erase 0), (m.count j)!)

Proof state:
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero]

Result:
m : Multiset ℕ
⊢ 0 < (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!

Proof state:
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

Tactic:
rw [← bell_mul_eq, mul_assoc]

Result:
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣
    m.bell * ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)

Proof state:
m : Multiset ℕ
⊢ 0 < (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
apply Nat.mul_pos

Result:
case ha
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod > 0

case hb
m : Multiset ℕ
⊢ ∏ j ∈ m.toFinset.erase 0, (count j m)! > 0

Proof state:
m : Multiset ℕ
⊢ m.bell * (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Tactic:
exact bell_mul_eq m

Result:
no goals

Proof state:
case ha
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod > 0

Tactic:
simp only [gt_iff_lt, CanonicallyOrderedAdd.multiset_prod_pos, mem_map,
forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
case ha
m : Multiset ℕ
⊢ ∀ a ∈ m, 0 < a !

Proof state:
m : Multiset ℕ
⊢ m.bell * ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

Tactic:
rw [← mul_assoc]

Result:
m : Multiset ℕ
⊢ m.bell * (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Proof state:
case hb
m : Multiset ℕ
⊢ ∏ j ∈ m.toFinset.erase 0, (count j m)! > 0

Tactic:
apply Finset.prod_pos

Result:
case hb.h0
m : Multiset ℕ
⊢ ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!

Proof state:
case hb.h0
m : Multiset ℕ
⊢ ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!

Tactic:
exact fun _ _ ↦ Nat.factorial_pos _

Result:
no goals

Proof state:
case ha
m : Multiset ℕ
⊢ ∀ a ∈ m, 0 < a !

Tactic:
exact fun _ _ ↦ Nat.factorial_pos _

Result:
no goals

Proof state:
m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣
    m.bell * ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
apply Nat.dvd_mul_left

Result:
no goals

Proof state:
m : Multiset ℕ
⊢ m.bell = m.sum ! / ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]

Result:
m : Multiset ℕ
⊢ m.bell * ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ∣ m.sum !

m : Multiset ℕ
⊢ (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! ≠ 0
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma le_smul_of_one_le_left [SMulPosMono α β] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a • b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
hb : 0 ≤ b
h : 1 ≤ a
⊢ b ≤ a • b

Tactic:
simpa only [one_smul] using smul_le_smul_of_nonneg_right h hb

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsConnected.lean
theorem zigzag_of_eqvGen_quot_rel (F : C ⥤ Type w) (c d : Σ j, F.obj j)
    (h : Relation.EqvGen (Quot.Rel F) c d) : Zigzag c.1 d.1

Proof state:
case refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ : (j : C) × F.obj j
⊢ Zigzag x✝.fst x✝.fst

Tactic:
exact Zigzag.refl _

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d : (j : C) × F.obj j
h : Relation.EqvGen (Quot.Rel F) c d
⊢ Zigzag c.fst d.fst

Tactic:
induction h with
| rel _ _ h => exact Zigzag.of_hom <| Exists.choose h
| refl _ => exact Zigzag.refl _
| symm _ _ _ ih => exact zigzag_symmetric ih
| trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

Result:
no goals

Proof state:
case rel
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ : (j : C) × F.obj j
h : Quot.Rel F x✝ y✝
⊢ Zigzag x✝.fst y✝.fst

Tactic:
exact Zigzag.of_hom <| Exists.choose h

Result:
no goals

Proof state:
case trans
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ z✝ : (j : C) × F.obj j
a✝¹ : Relation.EqvGen (Quot.Rel F) x✝ y✝
a✝ : Relation.EqvGen (Quot.Rel F) y✝ z✝
ih₁ : Zigzag x✝.fst y✝.fst
ih₂ : Zigzag y✝.fst z✝.fst
⊢ Zigzag x✝.fst z✝.fst

Tactic:
exact ih₁.trans ih₂

Result:
no goals

Proof state:
case symm
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d x✝ y✝ : (j : C) × F.obj j
a✝ : Relation.EqvGen (Quot.Rel F) x✝ y✝
ih : Zigzag x✝.fst y✝.fst
⊢ Zigzag y✝.fst x✝.fst

Tactic:
exact zigzag_symmetric ih

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
@[simp] lemma mul_modEq_mul_right (hc : c ≠ 0) : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD (p / c)]

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a b c p : α
hc : c ≠ 0
⊢ a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD p / c]

Tactic:
rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).rootSet S = ∅

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).rootSet S = ∅

Tactic:
classical
rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

Result:
no goals

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).rootSet S = ∅

Tactic:
rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

Result:
no goals
-- Mathlib/RepresentationTheory/Invariants.lean
theorem invariants_eq_inter : (invariants ρ).carrier = ⋂ g : G, Function.fixedPoints (ρ g)

Proof state:
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ x✝ ∈ ρ.invariants.carrier ↔ x✝ ∈ ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
simp [Function.IsFixedPt]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
ext

Result:
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ x✝ ∈ ρ.invariants.carrier ↔ x✝ ∈ ⋂ g, Function.fixedPoints ⇑(ρ g)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrable_indicator_iff (hs : MeasurableSet s) :
    Integrable (indicator s f) μ ↔ IntegrableOn f s μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ

Tactic:
simp_rw [IntegrableOn, Integrable, hasFiniteIntegral_iff_enorm,
  enorm_indicator_eq_indicator_enorm, lintegral_indicator hs,
  aestronglyMeasurable_indicator_iff hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/HashMap.lean
theorem HashMapBucket.size_update {α : Type u} {β : Type v} (data : HashMapBucket α β) (i : USize) (d : AssocList α β)
    (h : i.toNat < data.val.size) : (data.update i d h).val.size = data.val.size

Proof state:
α : Type u
β : Type v
data : HashMapBucket α β
i : USize
d : AssocList α β
h : i.toNat < data.val.size
⊢ (data.update i d h).val.size = data.val.size

Tactic:
simp [update, Array.uset]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p

Proof state:
r p : ℝ≥0
h : r ≠ 0
⊢ r⁻¹ ≤ p ↔ 1 ≤ r * p

Tactic:
rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
/-- If the cokernel comparison map for `G` at `f` is an isomorphism, then `G` preserves the
cokernel of `f`.
-/
lemma PreservesCokernel.of_iso_comparison [i : IsIso (cokernelComparison f G)] :
    PreservesColimit (parallelPair f 0) G

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (CokernelCofork.ofπ (G.map (cokernel.π f)) ⋯)

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (cokernelIsCokernel (G.map f)) i

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))

Tactic:
apply (isColimitMapCoconeCoforkEquiv' G (cokernel.condition f)).symm _

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (CokernelCofork.ofπ (G.map (cokernel.π f)) ⋯)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
i : IsIso (cokernelComparison f G)
⊢ IsColimit (G.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))