harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem sublist_cons_iff {a : α} {l l'} :
    l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Proof state:
α : Type u_1
a : α
l l' : List α
⊢ l <+ a :: l' ↔ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Tactic:
constructor

Result:
case mp
α : Type u_1
a : α
l l' : List α
⊢ l <+ a :: l' → l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

case mpr
α : Type u_1
a : α
l l' : List α
⊢ (l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l') → l <+ a :: l'

Proof state:
case mp
α : Type u_1
a : α
l l' : List α
⊢ l <+ a :: l' → l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Tactic:
intro h

Result:
case mp
α : Type u_1
a : α
l l' : List α
h : l <+ a :: l'
⊢ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Proof state:
case mpr
α : Type u_1
a : α
l l' : List α
⊢ (l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l') → l <+ a :: l'

Tactic:
rintro (h | ⟨r, rfl, h⟩)

Result:
case mpr.inl
α : Type u_1
a : α
l l' : List α
h : l <+ l'
⊢ l <+ a :: l'

case mpr.inr.intro.intro
α : Type u_1
a : α
l' r : List α
h : r <+ l'
⊢ a :: r <+ a :: l'

Proof state:
case mp.cons₂
α : Type u_1
a : α
l' l₁✝ : List α
h : l₁✝ <+ l'
⊢ a :: l₁✝ <+ l' ∨ ∃ r, a :: l₁✝ = a :: r ∧ r <+ l'

Tactic:
exact Or.inr ⟨_, rfl, h⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
a : α
l l' : List α
h : l <+ a :: l'
⊢ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Tactic:
cases h with
| cons _ h => exact Or.inl h
| cons₂ _ h => exact Or.inr ⟨_, rfl, h⟩

Result:
no goals

Proof state:
case mpr.inl
α : Type u_1
a : α
l l' : List α
h : l <+ l'
⊢ l <+ a :: l'

Tactic:
exact h.cons _

Result:
no goals

Proof state:
case mp.cons
α : Type u_1
a : α
l l' : List α
h : l <+ l'
⊢ l <+ l' ∨ ∃ r, l = a :: r ∧ r <+ l'

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case mpr.inr.intro.intro
α : Type u_1
a : α
l' r : List α
h : r <+ l'
⊢ a :: r <+ a :: l'

Tactic:
exact h.cons₂ _

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_succ {n : ℕ} (hs : s.Finite

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
⊢ s.ncard = t.ncard + 1

Tactic:
rw [← h, ncard_insert_of_not_mem hat (hs.subset ((subset_insert a t).trans_eq h))]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
n : ℕ
hs : autoParam s.Finite _auto✝
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1

Tactic:
rintro ⟨a, t, hat, h, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
⊢ s.ncard = t.ncard + 1

Proof state:
α : Type u_1
s : Set α
n : ℕ
hs : autoParam s.Finite _auto✝
⊢ s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
refine ⟨eq_insert_of_ncard_eq_succ, ?_⟩

Result:
α : Type u_1
s : Set α
n : ℕ
hs : autoParam s.Finite _auto✝
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometric_radius_top_of_neg_nat₃ {k : ℕ} :
    (ordinaryHypergeometricSeries 𝔸 a b (-(k : 𝕂))).radius = ⊤

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 a b (-↑k) (n + (1 + k)) = 0

Tactic:
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat a b (-(k : 𝕂)) (by aesop) (by omega)

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
omega

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 a b (-↑k)).radius = ⊤

Tactic:
refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 a b (-↑k) (n + (1 + k)) = 0

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a b : 𝕂
k n : ℕ
⊢ ↑?m.69462 = -a ∨ ↑?m.69462 = -b ∨ ↑?m.69462 = - -↑k

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_homology_iso_zero [S.HasHomology] [HasZeroObject C] :
    S.Exact ↔ Nonempty (S.homology ≅ 0)

Proof state:
case mpr.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
e : S.homology ≅ 0
⊢ IsZero S.homology

Tactic:
exact IsZero.of_iso (isZero_zero C) e

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology → Nonempty (S.homology ≅ 0)

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
h : IsZero S.homology
⊢ Nonempty (S.homology ≅ 0)

Proof state:
case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology

Tactic:
rintro ⟨e⟩

Result:
case mpr.intro
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
e : S.homology ≅ 0
⊢ IsZero S.homology

Proof state:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
h : IsZero S.homology
⊢ Nonempty (S.homology ≅ 0)

Tactic:
exact ⟨h.isoZero⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ S.Exact ↔ Nonempty (S.homology ≅ 0)

Tactic:
rw [exact_iff_isZero_homology]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology ↔ Nonempty (S.homology ≅ 0)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology ↔ Nonempty (S.homology ≅ 0)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology → Nonempty (S.homology ≅ 0)

case mpr
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] protected lemma sdiff_eq_left : s.sdiff t = s ↔ Disjoint ↑s t

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s) t

Tactic:
simp [← SetLike.coe_set_eq]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean
theorem counit_C_mul_T (a : A) (n : ℤ) :
    Coalgebra.counit (R := R) (C a * T n) = Coalgebra.counit (R := R) a

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
n : ℤ
⊢ CoalgebraStruct.counit (C a * T n) = CoalgebraStruct.counit a

Tactic:
simp [← single_eq_C_mul_T]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem of_nat_toZNumNeg (n : ℕ) : Num.toZNumNeg n = -n

Proof state:
n : ℕ
⊢ (↑n).toZNumNeg = -↑n

Tactic:
rw [← of_nat_toZNum, Num.zneg_toZNum]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Basic.lean
theorem not_isCyclic_of_denselyOrdered [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α

Proof state:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Result:
case intro.inl.intro.intro.intro
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
⊢ a⁻¹ ^ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < a⁻¹ ^ 1

Proof state:
α : Type u_1
inst✝² : LinearOrderedCommGroup α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x => a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x => a ^ x) k
hb : (fun x => a ^ x) k < 1
this : 0 < k ∧ k < 1
⊢ False

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_one {a : G} [Decidable (a = 1)] :
    (1 : SkewMonoidAlgebra k G).coeff a = if a = 1 then 1 else 0

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
inst✝² : One G
inst✝¹ : One k
a : G
inst✝ : Decidable (a = 1)
⊢ coeff 1 a = if 1 = a then 1 else 0

Tactic:
simpa using coeff_single_apply

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
inst✝² : One G
inst✝¹ : One k
a : G
inst✝ : Decidable (a = 1)
⊢ coeff 1 a = if a = 1 then 1 else 0

Tactic:
classical
simp_rw [eq_comm (a := a) (b := 1)]
simpa using coeff_single_apply

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
inst✝² : One G
inst✝¹ : One k
a : G
inst✝ : Decidable (a = 1)
⊢ coeff 1 a = if a = 1 then 1 else 0

Tactic:
simp_rw [eq_comm (a := a) (b := 1)]

Result:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
inst✝² : One G
inst✝¹ : One k
a : G
inst✝ : Decidable (a = 1)
⊢ coeff 1 a = if 1 = a then 1 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem isEqv_eq [DecidableEq α] {l₁ l₂ : Vector α n} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂)

Proof state:
α : Type u_1
n : Nat
inst✝ : DecidableEq α
l₁ l₂ : Vector α n
⊢ ((l₁.isEqv l₂ fun x1 x2 => x1 == x2) = true) = (l₁ = l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (({ toArray := toArray✝, size_toArray := size_toArray✝ }.isEqv l₂ fun x1 x2 => x1 == x2) = true) =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } = l₂)

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (({ toArray := toArray✝, size_toArray := size_toArray✝ }.isEqv l₂ fun x1 x2 => x1 == x2) = true) =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } = l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.isEqv
        { toArray := toArray✝, size_toArray := size_toArray✝ } fun x1 x2 => x1 == x2) =
      true) =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ })

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝ : DecidableEq α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.isEqv
        { toArray := toArray✝, size_toArray := size_toArray✝ } fun x1 x2 => x1 == x2) =
      true) =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_reverse {l : Array α} {i} (h : i < l.size) :
    l.reverse[i]? = l[l.size - 1 - i]?

Proof state:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ { toList := toList✝ }.reverse[i]? = { toList := toList✝ }[{ toList := toList✝ }.size - 1 - i]?

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l.reverse[i]? = l[l.size - 1 - i]?

Tactic:
cases l

Result:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ { toList := toList✝ }.reverse[i]? = { toList := toList✝ }[{ toList := toList✝ }.size - 1 - i]?
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_recurrence {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) :
    u * betaIntegral u (v + 1) = v * betaIntegral (u + 1) v

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
⊢ F 0 = 0

Tactic:
simp only [F, mul_eq_zero, ofReal_zero, cpow_eq_zero_iff, eq_self_iff_true, Ne,
  true_and, sub_zero, one_cpow, one_ne_zero, or_false]

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x => u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0 ..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
⊢ ¬u = 0

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
⊢ 0 < (u + 1).re

Tactic:
rw [add_re, one_re]

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x => ↑x ^ u * (1 - ↑x) ^ v
⊢ 0 < u.re + 1
-- Mathlib/Data/Sym/Sym2.lean
theorem inductionOn₂ {f : Sym2 α → Sym2 β → Prop} (i : Sym2 α) (j : Sym2 β)
    (hf : ∀ a₁ a₂ b₁ b₂, f s(a₁, a₂) s(b₁, b₂)) : f i j :=
  Quot.induction_on₂ i j <| by
    intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩
    exact hf _ _ _ _

Proof state:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
⊢ ∀ (a : α × α) (b : β × β), f (Quot.mk (Rel α) a) (Quot.mk (Rel β) b)

Tactic:
intro ⟨a₁, a₂⟩ ⟨b₁, b₂⟩

Result:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))

Proof state:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
a₁ a₂ : α
b₁ b₂ : β
⊢ f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) (b₁, b₂))

Tactic:
exact hf _ _ _ _

Result:
no goals
-- Mathlib/Data/Nat/Choose/Vandermonde.lean
theorem Nat.add_choose_eq (m n k : ℕ) :
    (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Proof state:
m n k : ℕ
⊢ (m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
calc
  (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, Nat.cast_id]
  _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
  _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
    rw [coeff_mul, Finset.sum_congr rfl]
    simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]

Result:
no goals

Proof state:
m n k : ℕ
⊢ ((X + 1) ^ (m + n)).coeff k = ((X + 1) ^ m * (X + 1) ^ n).coeff k

Tactic:
rw [pow_add]

Result:
no goals

Proof state:
m n k : ℕ
⊢ ((X + 1) ^ m * (X + 1) ^ n).coeff k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
rw [coeff_mul, Finset.sum_congr rfl]

Result:
m n k : ℕ
⊢ ∀ x ∈ antidiagonal k, ((X + 1) ^ m).coeff x.1 * ((X + 1) ^ n).coeff x.2 = m.choose x.1 * n.choose x.2

Proof state:
m n k : ℕ
⊢ (m + n).choose k = ((X + 1) ^ (m + n)).coeff k

Tactic:
rw [coeff_X_add_one_pow, Nat.cast_id]

Result:
no goals

Proof state:
m n k : ℕ
⊢ ∀ x ∈ antidiagonal k, ((X + 1) ^ m).coeff x.1 * ((X + 1) ^ n).coeff x.2 = m.choose x.1 * n.choose x.2

Tactic:
simp only [coeff_X_add_one_pow, Nat.cast_id, eq_self_iff_true, imp_true_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpIndSMul_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y : G) :
    condExpIndSMul hm hs hμs (x + y) = condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x y : G
⊢ condExpIndSMul hm hs hμs (x + y) = condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y

Tactic:
simp_rw [condExpIndSMul]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x y : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ (x + y))) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
      (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x y : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ (x + y))) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) +
      (compLpL 2 μ (toSpanSingleton ℝ y)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Tactic:
rw [toSpanSingleton_add, add_compLpL, add_apply]

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem card_of_mem_right {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) : 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b

Tactic:
have w₂ := fst_pred_mem_erase_of_mem_right h

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ 2 ≤ Finset.card b

Tactic:
have w₁ : m ∈ b := (Finset.mem_inter.1 h).1

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
⊢ 2 ≤ Finset.card b

Tactic:
have i₁ := Finset.card_erase_lt_of_mem w₁

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
⊢ 2 ≤ Finset.card b

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
i₂ : 0 < (Finset.erase b m).card
⊢ 2 ≤ Finset.card b

Tactic:
exact Nat.lt_of_le_of_lt i₂ i₁

Result:
no goals

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
⊢ 2 ≤ Finset.card b

Tactic:
have i₂ := Nat.lt_of_le_of_lt (Nat.zero_le _) (Finset.card_erase_lt_of_mem w₂)

Result:
b : Board
m : ℤ × ℤ
h : m ∈ right b
w₁ : m ∈ b
w₂ : (m.1 - 1, m.2) ∈ Finset.erase b m
i₁ : (Finset.erase b m).card < Finset.card b
i₂ : 0 < (Finset.erase b m).card
⊢ 2 ≤ Finset.card b
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem omega0_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o :=
  ⟨fun h n => (nat_lt_omega0 _).le.trans h, fun H =>
    le_of_forall_lt fun a h => by
      let ⟨n, e⟩ := lt_omega0.1 h
      rw [e, ← succ_le_iff]; exact H (n + 1)⟩

Proof state:
o : Ordinal.{u_1}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_1}
h : a < ω
⊢ a < o

Tactic:
let ⟨n, e⟩ := lt_omega0.1 h

Result:
o : Ordinal.{u_1}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_1}
h : a < ω
n : ℕ
e : a = ↑n
⊢ a < o

Proof state:
o : Ordinal.{u_1}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_1}
h : a < ω
n : ℕ
e : a = ↑n
⊢ succ ↑n ≤ o

Tactic:
exact H (n + 1)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_1}
h : a < ω
n : ℕ
e : a = ↑n
⊢ a < o

Tactic:
rw [e, ← succ_le_iff]

Result:
o : Ordinal.{u_1}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_1}
h : a < ω
n : ℕ
e : a = ↑n
⊢ succ ↑n ≤ o
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_leftUnitor_hom_snd (X : C₁ × C₂) :
    ((λ_ X).hom : 𝟙_ _ ⊗ X ⟶ X).2 = (λ_ X.2).hom

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).hom.2 = (λ_ X.2).hom

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.2 = (λ_ (fst✝, snd✝).2).hom

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).hom.2 = (λ_ (fst✝, snd✝).2).hom

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_add_mod_self_right (a b c : Nat) : (a * b + c) % b = c % b

Proof state:
a b c : Nat
⊢ (a * b + c) % b = c % b

Tactic:
rw [Nat.add_comm, Nat.add_mul_mod_self_right]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
/-- The last element of a nonempty Dyck word is `D`. -/
lemma getLast_eq_D (p : DyckWord) (h) : p.toList.getLast h = D

Proof state:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ↑p = count D ↑p
⊢ False

Tactic:
rw [← dropLast_append_getLast h, (dichotomy _).resolve_right f] at s

Result:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False

Proof state:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
⊢ False

Tactic:
have s := p.count_U_eq_count_D

Result:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ↑p = count D ↑p
⊢ False

Proof state:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
⊢ False

Tactic:
have := p.count_D_le_count_U (p.toList.length - 1)

Result:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
this : count D (take ((↑p).length - 1) ↑p) ≤ count U (take ((↑p).length - 1) ↑p)
⊢ False

Proof state:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U ((↑p).dropLast ++ [U]) = count D ((↑p).dropLast ++ [U])
⊢ False

Tactic:
simp_rw [dropLast_eq_take, count_append, count_singleton', ite_true, reduceCtorEq, ite_false] at s

Result:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
⊢ False

Proof state:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
this : count D (take ((↑p).length - 1) ↑p) ≤ count U (take ((↑p).length - 1) ↑p)
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
p : DyckWord
h : ↑p ≠ []
⊢ (↑p).getLast h = D

Tactic:
by_contra f

Result:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
⊢ False
-- Mathlib/Data/Finset/Image.lean
theorem map_refl : s.map (Embedding.refl _) = s :=
  ext fun _ => by simpa only [mem_map, exists_prop] using exists_eq_right

Proof state:
α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ map (Embedding.refl α) s ↔ x✝ ∈ s

Tactic:
simpa only [mem_map, exists_prop] using exists_eq_right

Result:
no goals