harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Derivation.lean
theorem C_smul_derivation_apply (D : Derivation R R[X] A) (a : R) (f : R[X]) :
    C a • D f = a • D f

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Tactic:
rw [this, C_mul', D.map_smul]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = a • D f

Tactic:
have : C a • D f = D (C a * f) := by simp

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = D (C a * f)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Ioc_update_union (x y : ∀ i, α i) (i₀ : ι) (m : α i₀) (hm : m ∈ Icc (x i₀) (y i₀)) :
    ((pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) ∪
        pi univ fun i ↦ Ioc (update x i₀ m i) (y i)) =
      pi univ fun i ↦ Ioc (x i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((univ.pi fun i => Ioc (x i) (update y i₀ m i)) ∪ univ.pi fun i => Ioc (update x i₀ m i) (y i)) =
    univ.pi fun i => Ioc (x i) (y i)

Tactic:
simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
  ← setOf_or, le_or_lt, setOf_true, univ_inter]

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem sup_eq_ringConGen (c d : RingCon R) : c ⊔ d = ringConGen fun x y => c x y ∨ d x y

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ c ⊔ d = sInf {s | ∀ (x y : R), c x y ∨ d x y → s x y}

Tactic:
apply congr_arg sInf

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : R), c x y ∨ d x y → s x y}

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : R), c x y ∨ d x y → s x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ c ⊔ d = ringConGen fun x y => c x y ∨ d x y

Tactic:
rw [ringConGen_eq]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ c ⊔ d = sInf {s | ∀ (x y : R), c x y ∨ d x y → s x y}
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem algHom_eval₂_algebraMap {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
    [Algebra R A] [Algebra R B] (p : R[X]) (f : A →ₐ[R] B) (a : A) :
    f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

Proof state:
R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ f (∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * a ^ n) = ∑ n ∈ p.support, (algebraMap R B) (p.coeff n) * f a ^ n

Tactic:
simp only [map_sum, map_mul, map_pow, eq_intCast, map_intCast, AlgHom.commutes]

Result:
no goals

Proof state:
R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

Tactic:
simp only [eval₂_eq_sum, sum_def]

Result:
R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ f (∑ n ∈ p.support, (algebraMap R A) (p.coeff n) * a ^ n) = ∑ n ∈ p.support, (algebraMap R B) (p.coeff n) * f a ^ n
-- Mathlib/Order/Filter/Prod.lean
theorem map_const_principal_coprod_map_id_principal {α β ι : Type*} (a : α) (b : β) (i : ι) :
    (map (fun _ => b) (𝓟 {a})).coprod (map id (𝓟 {i})) =
      𝓟 ((({b} : Set β) ×ˢ univ) ∪ (univ ×ˢ ({i} : Set ι)))

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ (map (fun x => b) (𝓟 {a})).coprod (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})

Tactic:
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton,
  image_id, prod_univ, univ_prod, id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem length_pushn (c : Char) (n : Nat) : (pushn s c n).length = s.length + n

Proof state:
s : String
c : Char
n : Nat
⊢ (Nat.repeat (fun s => s.push c) n s).length = s.length + n

Tactic:
induction n <;> simp [Nat.repeat, Nat.add_assoc, *]

Result:
no goals

Proof state:
s : String
c : Char
n : Nat
⊢ (s.pushn c n).length = s.length + n

Tactic:
unfold pushn

Result:
s : String
c : Char
n : Nat
⊢ (Nat.repeat (fun s => s.push c) n s).length = s.length + n
-- Mathlib/Data/Fin/Tuple/Reflection.lean
theorem seq_eq : ∀ {m} (f : Fin m → α → β) (v : Fin m → α), seq f v = fun i => f i (v i)
  | 0, _, _ => Subsingleton.elim _ _
  | n + 1, f, v =>
    funext fun i => by
      simp_rw [seq, seq_eq]
      refine i.cases ?_ fun i => ?_
      · rfl
      · rw [Matrix.cons_val_succ]
        rfl

Proof state:
case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)

Tactic:
simp_rw [seq, seq_eq]

Result:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)

Tactic:
refine i.cases ?_ fun i => ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)

case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i.succ = f i.succ (v i.succ)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i => Matrix.vecTail f i (Matrix.vecTail v i)) i.succ = f i.succ (v i.succ)

Tactic:
rw [Matrix.cons_val_succ]

Result:
case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)
-- Mathlib/Topology/ContinuousOn.lean
theorem Function.LeftInverse.map_nhds_eq {f : α → β} {g : β → α} {x : β}
    (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (range g) (g x))
    (hg : ContinuousAt g x) : map g (𝓝 x) = 𝓝[range g] g x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ map g (𝓝 x) = 𝓝[range g] g x

Tactic:
simpa only [nhdsWithin_univ, image_univ] using
  (h.leftInvOn univ).map_nhdsWithin_eq (h x) (by rwa [image_univ]) hg.continuousWithinAt

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
h : LeftInverse f g
hf : ContinuousWithinAt f (range g) (g x)
hg : ContinuousAt g x
⊢ ContinuousWithinAt f (g '' univ) (g x)

Tactic:
rwa [image_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_eq_bif : or o o' = bif o.isSome then o else o'

Proof state:
α✝ : Type u_1
o o' : Option α✝
⊢ o.or o' = bif o.isSome then o else o'

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

Tactic:
simp [mem_iff_contains, contains_insertIfNew]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.inner_single_left (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
    ⟪EuclideanSpace.single i (a : 𝕜), v⟫ = conj a * v i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ inner (single i a) v = (starRingEnd 𝕜) a * v i

Tactic:
simp [apply_ite conj]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem mul_fin_three [AddCommMonoid α] [Mul α]
    (a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α) :
    !![a₁₁, a₁₂, a₁₃;
       a₂₁, a₂₂, a₂₃;
       a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃;
                           b₂₁, b₂₂, b₂₃;
                           b₃₁, b₃₂, b₃₃] =
    !![a₁₁*b₁₁ + a₁₂*b₂₁ + a₁₃*b₃₁, a₁₁*b₁₂ + a₁₂*b₂₂ + a₁₃*b₃₂, a₁₁*b₁₃ + a₁₂*b₂₃ + a₁₃*b₃₃;
       a₂₁*b₁₁ + a₂₂*b₂₁ + a₂₃*b₃₁, a₂₁*b₁₂ + a₂₂*b₂₂ + a₂₃*b₃₂, a₂₁*b₁₃ + a₂₂*b₂₃ + a₂₃*b₃₃;
       a₃₁*b₁₁ + a₃₂*b₂₁ + a₃₃*b₃₁, a₃₁*b₁₂ + a₃₂*b₂₂ + a₃₃*b₃₂, a₃₁*b₁₃ + a₃₂*b₂₃ + a₃₃*b₃₃]

Proof state:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ !![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
      a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
      a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j

Proof state:
case a
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ (!![a₁₁, a₁₂, a₁₃; a₂₁, a₂₂, a₂₃; a₃₁, a₃₂, a₃₃] * !![b₁₁, b₁₂, b₁₃; b₂₁, b₂₂, b₂₃; b₃₁, b₃₂, b₃₃]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃;
        a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃;
        a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]
      i j

Tactic:
fin_cases i <;> fin_cases j
  <;> simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Basic.lean
theorem stream_isSeq (v : K) : (IntFractPair.stream v).IsSeq

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
hyp : IntFractPair.stream v n✝ = none
⊢ IntFractPair.stream v (n✝ + 1) = none

Tactic:
simp [IntFractPair.stream, hyp]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
⊢ (IntFractPair.stream v).IsSeq

Tactic:
intro _ hyp

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n✝ : ℕ
hyp : IntFractPair.stream v n✝ = none
⊢ IntFractPair.stream v (n✝ + 1) = none
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
/-- Guessing rule for the `bound` tactic: when trying to prove `x ^ y ≤ x ^ z`, we can either assume
`1 ≤ x` or `0 < x ≤ 1`. -/
@[bound] lemma rpow_le_rpow_of_exponent_le_or_ge {x y z : ℝ}
    (h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y) : x ^ y ≤ x ^ z

Proof state:
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩

Result:
case inl.intro
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

case inr.intro.intro
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Proof state:
case inl.intro
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
exact Real.rpow_le_rpow_of_exponent_le x1 yz

Result:
no goals

Proof state:
case inr.intro.intro
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_formula (n : ℕ) :
    log (stirlingSeq n) = Real.log n ! - 1 / 2 * Real.log (2 * n) - n * log (n / exp 1)

Proof state:
n : ℕ
⊢ Real.log (stirlingSeq n) = Real.log ↑n ! - 1 / 2 * Real.log (2 * ↑n) - ↑n * Real.log (↑n / rexp 1)

Tactic:
cases n

Result:
case zero

⊢ Real.log (stirlingSeq 0) = Real.log ↑0! - 1 / 2 * Real.log (2 * ↑0) - ↑0 * Real.log (↑0 / rexp 1)

case succ
n✝ : ℕ
⊢ Real.log (stirlingSeq (n✝ + 1)) =
    Real.log ↑(n✝ + 1)! - 1 / 2 * Real.log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * Real.log (↑(n✝ + 1) / rexp 1)

Proof state:
case zero

⊢ Real.log (stirlingSeq 0) = Real.log ↑0! - 1 / 2 * Real.log (2 * ↑0) - ↑0 * Real.log (↑0 / rexp 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n✝ : ℕ
⊢ Real.log (stirlingSeq (n✝ + 1)) =
    Real.log ↑(n✝ + 1)! - 1 / 2 * Real.log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * Real.log (↑(n✝ + 1) / rexp 1)

Tactic:
rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
  <;> positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem go_get (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
    (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig lhs rhs curr hcurr cin s).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig lhs rhs curr hcurr cin s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig lhs rhs curr hcurr cin s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig lhs rhs curr hcurr cin s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefVec curr
lhs rhs : aig.RefVec w
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig lhs rhs curr hcurr cin s).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_of_mul_eq_mul_left {a b c : Int} (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
  have : a * b - a * c = 0 := Int.sub_eq_zero_of_eq h
  have : a * (b - c) = 0

Proof state:
a b c : Int
ha : a ≠ 0
h : a * b = a * c
this : a * b - a * c = 0
⊢ a * (b - c) = 0

Tactic:
rw [Int.mul_sub, this]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_intCast_eq_padic_norm (z : ℤ) : ‖(z : ℤ_[p])‖ = ‖(z : ℚ_[p])‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = ‖↑z‖

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_neg_self (n : ℕ) : multichoose (-n : ℤ) n = (-1)^n

Proof state:
n : ℕ
⊢ multichoose (-↑n) n = (-1) ^ n

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
  factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
  Nat.cast_comm]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma ofTensorProductInvOfPiFintype_comp_ofTensorProduct :
    ofTensorProductInvOfPiFintype I ι ∘ₗ ofTensorProduct I (ι → R) = LinearMap.id

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ
      ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) =
    LinearMap.id

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ
      ofTensorProduct I (ι → R) =
    LinearMap.id

Tactic:
rw [LinearEquiv.coe_trans, LinearMap.comp_assoc, piEquivOfFintype_comp_ofTensorProduct_eq]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ
      ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) =
    LinearMap.id

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) ∘ₗ ofTensorProduct I (ι → R) = LinearMap.id

Tactic:
dsimp only [ofTensorProductInvOfPiFintype]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ
      ofTensorProduct I (ι → R) =
    LinearMap.id
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_sub_two (n : ℤ) : S R (n - 2) = X * S R (n - 1) - S R n

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (n - 2) = X * S R (n - 1) - S R n

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 2)

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem norm_approxOn_zero_le [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E}
    (h₀ : (0 : E) ∈ s) [SeparableSpace s] (x : β) (n : ℕ) :
    ‖approxOn f hf s 0 h₀ n x‖ ≤ ‖f x‖ + ‖f x‖

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
h₀ : 0 ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ ‖(approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖

Tactic:
simpa [enorm, edist_eq_enorm_sub, ← ENNReal.coe_add, norm_sub_rev]
  using edist_approxOn_y0_le hf h₀ x n

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Free.lean
theorem basis_repr_symm_apply (a : A) (i : ι) :
    (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ b.repr.symm (Finsupp.single i 1)

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ (basisAux A b).invFun (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

Tactic:
simp [Equiv.uniqueProd_symm_apply, basisAux]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)

Tactic:
rw [basis, LinearEquiv.coe_symm_mk]

Result:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
i : ι
⊢ (basisAux A b).invFun (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.scomp_of_eq
    (hg : HasDerivAt g₁ g₁' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
    HasDerivAt (g₁ ∘ h) (h' • g₁') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
exact hg.scomp x hh

Result:
no goals