harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma disjoint_sUnion_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    Disjoint t (⋃₀ hC.disjointOfDiff hs ht)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (s \ t)

Tactic:
exact disjoint_sdiff_right

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (⋃₀ ↑(hC.disjointOfDiff hs ht))

Tactic:
rw [hC.sUnion_disjointOfDiff]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (s \ t)
-- Mathlib/FieldTheory/IsAlgClosed/Classification.lean
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' [Nontrivial R]
    (hv : IsTranscendenceBasis R v') (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K') : #K' = #ι'

Proof state:
R : Type u
inst✝⁴ : CommRing R
K' : Type u
inst✝³ : Field K'
inst✝² : Algebra R K'
inst✝¹ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v'
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K'
⊢ #K' = #ι'

Tactic:
simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
theorem coe_smul {R} (r : R) (s : ℝ≥0) [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0]
    [IsScalarTower R ℝ≥0 ℝ≥0∞] : (↑(r • s) : ℝ≥0∞) = (r : R) • (s : ℝ≥0∞)

Proof state:
R : Type u_1
r : R
s : ℝ≥0
inst✝³ : SMul R ℝ≥0
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ ↑(r • s) = r • ↑s

Tactic:
rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
  one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem memLp_approxOn_range [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    [SeparableSpace (range f ∪ {0} : Set E)] (hf : MemLp f p μ) (n : ℕ) :
    MemLp (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) p μ :=
  memLp_approxOn fmeas hf (y₀ := 0) (by simp) MemLp.zero n

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/FractionalIdeal.lean
theorem det_basisOfFractionalIdeal_eq_absNorm (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
    (e : (Free.ChooseBasisIndex ℤ (𝓞 K)) ≃ (Free.ChooseBasisIndex ℤ I)) :
    |(integralBasis K).det ((basisOfFractionalIdeal K I).reindex e.symm)| =
      FractionalIdeal.absNorm I.1

Proof state:
case e_a.h.e_6.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ ⇑((basisOfFractionalIdeal K I).reindex e.symm) = Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)

Tactic:
ext

Result:
case e_a.h.e_6.h.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((basisOfFractionalIdeal K I).reindex e.symm) x✝ = (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)) x✝

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm ↑I

Tactic:
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1
  ((fractionalIdealBasis K I.1).reindex e.symm)]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| =
    |(Basis.localizationLocalization ℚ ℤ⁰ K (RingOfIntegers.basis K)).det
        (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm))|

Proof state:
case e_a.h.e_6.h.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((basisOfFractionalIdeal K I).reindex e.symm) x✝ = (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)) x✝

Tactic:
simpa using basisOfFractionalIdeal_apply K I _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ |(integralBasis K).det ⇑((basisOfFractionalIdeal K I).reindex e.symm)| =
    |(Basis.localizationLocalization ℚ ℤ⁰ K (RingOfIntegers.basis K)).det
        (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm))|

Tactic:
congr

Result:
case e_a.h.e_6.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
⊢ ⇑((basisOfFractionalIdeal K I).reindex e.symm) = Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)
-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} {τ τ' : F₁ ⟶ F₂}
    (h : ∀ X : C, τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ'

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
E : Type u_3
inst✝¹ : Category.{u_6, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
⊢ τ = τ'

Tactic:
haveI := essSurj L W

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
E : Type u_3
inst✝¹ : Category.{u_6, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
⊢ τ = τ'

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
E : Type u_3
inst✝¹ : Category.{u_6, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ.app Y = τ'.app Y

Tactic:
rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
E : Type u_3
inst✝¹ : Category.{u_6, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
⊢ τ = τ'

Tactic:
ext Y

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
E : Type u_3
inst✝¹ : Category.{u_6, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ.app Y = τ'.app Y
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
/-- Helper lemma for `integral_log`: case where `a = 0` and `b` is positive. -/
lemma integral_log_from_zero_of_pos (ht : 0 < b) : ∫ s in (0)..b, log s = b * log b - b

Proof state:
case hderiv
b : ℝ
ht : 0 < b
⊢ ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun x => x * log x - x) (log x) x

Tactic:
intro s ⟨hs, _ ⟩

Result:
case hderiv
b : ℝ
ht : 0 < b
s : ℝ
hs : 0 < s
right✝ : s < b
⊢ HasDerivAt (fun x => x * log x - x) (log s) s

Proof state:
b : ℝ
ht : 0 < b
⊢ ∫ (s : ℝ) in 0 ..b, log s = b * log b - b

Tactic:
rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
  (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]

Result:
b : ℝ
ht : 0 < b
⊢ b * log b - b - 0 = b * log b - b

case hab
b : ℝ
ht : 0 < b
⊢ 0 < b

case hderiv
b : ℝ
ht : 0 < b
⊢ ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun x => x * log x - x) (log x) x

case ha
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun x => x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

case hb
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun x => x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))

Proof state:
case ha
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun x => x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Tactic:
simpa [mul_comm] using ((tendsto_log_mul_rpow_nhds_zero zero_lt_one).sub
  (tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id))

Result:
no goals

Proof state:
b : ℝ
ht : 0 < b
⊢ ContinuousAt (fun x => x * log x - x) b

Tactic:
fun_prop

Result:
no goals

Proof state:
b : ℝ
ht : 0 < b
⊢ b * log b - b - 0 = b * log b - b

Tactic:
abel

Result:
no goals

Proof state:
case hb
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun x => x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Result:
no goals

Proof state:
case hab
b : ℝ
ht : 0 < b
⊢ 0 < b

Tactic:
exact ht

Result:
no goals

Proof state:
case hderiv
b : ℝ
ht : 0 < b
s : ℝ
hs : 0 < s
right✝ : s < b
⊢ HasDerivAt (fun x => x * log x - x) (log s) s

Tactic:
simpa using (hasDerivAt_mul_log hs.ne.symm).sub (hasDerivAt_id s)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma addLECancellable_iff_ne_bot [Nonempty α] [Preorder α]
    [ContravariantClass α α (· + ·) (· ≤ ·)] : AddLECancellable x ↔ x ≠ ⊥ where
  mp

Proof state:
α : Type u
inst✝³ : Add α
x : WithBot α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
⊢ AddLECancellable x → x ≠ ⊥

Tactic:
rintro h rfl

Result:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊥
⊢ False

Proof state:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊥
⊢ False

Tactic:
exact (bot_lt_coe <| Classical.arbitrary _).not_le <| h <| by simp

Result:
no goals

Proof state:
α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
h : AddLECancellable ⊥
⊢ ⊥ + ↑(Classical.arbitrary α) ≤ ⊥ + ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
lemma Ico_filter_dvd_eq :
    {x ∈ Ico a b | r ∣ x} =
      (Ico ⌈a / (r : ℚ)⌉ ⌈b / (r : ℚ)⌉).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩

Proof state:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ filter (fun x => r ∣ x) (Ico a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Tactic:
simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀,
  dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Result:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a ≤ x ∧ x < b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a ≤ a_1 * r ∧ a_1 * r < b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x

Proof state:
a b r : ℤ
hr : 0 < r
⊢ filter (fun x => r ∣ x) (Ico a b) = map { toFun := fun x => x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Tactic:
ext x

Result:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ x ∈ filter (fun x => r ∣ x) (Ico a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)

Proof state:
case h
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a ≤ x ∧ x < b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a ≤ a_1 * r ∧ a_1 * r < b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x

Tactic:
aesop

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
theorem solutionSetCondition_of_isRightAdjoint [G.IsRightAdjoint] : SolutionSetCondition G

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h

Tactic:
refine
  ⟨PUnit, fun _ => G.leftAdjoint.obj A, fun _ => (Adjunction.ofIsRightAdjoint G).unit.app A, ?_⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
⊢ SolutionSetCondition G

Tactic:
intro A

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Tactic:
intro B h

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) PUnit.unit ≫
      G.map (((Adjunction.ofIsRightAdjoint G).homEquiv A B).symm h) =
    h

Tactic:
rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Tactic:
refine ⟨PUnit.unit, ((Adjunction.ofIsRightAdjoint G).homEquiv _ _).symm h, ?_⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
D : Type u
inst✝¹ : Category.{v, u} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ (fun x => (Adjunction.ofIsRightAdjoint G).unit.app A) PUnit.unit ≫
      G.map (((Adjunction.ofIsRightAdjoint G).homEquiv A B).symm h) =
    h
-- Mathlib/Data/List/Sublists.lean
theorem length_sublistsLen :
    ∀ (n) (l : List α), length (sublistsLen n l) = Nat.choose (length l) n
  | 0, l => by simp
  | _ + 1, [] => by simp
  | n + 1, a :: l => by
    rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n+1) l,
      length_map, length_sublistsLen n l, length_cons, Nat.choose_succ_succ, Nat.add_comm]

Proof state:
α : Type u
l : List α
⊢ (sublistsLen 0 l).length = l.length.choose 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n✝ : ℕ
⊢ (sublistsLen (n✝ + 1) []).length = [].length.choose (n✝ + 1)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)

Tactic:
rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n+1) l,
  length_map, length_sublistsLen n l, length_cons, Nat.choose_succ_succ, Nat.add_comm]

Result:
no goals
-- Mathlib/RingTheory/Norm/Basic.lean
theorem PowerBasis.norm_gen_eq_coeff_zero_minpoly (pb : PowerBasis R S) :
    norm R pb.gen = (-1) ^ pb.dim * coeff (minpoly R pb.gen) 0

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
pb : PowerBasis R S
⊢ (norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0

Tactic:
rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix,
  Fintype.card_fin]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_of_mem_push_of_mem {a b : α} {l : Vector α n} : a ∈ l.push b → b ∈ l → a ∈ l

Proof state:
case mk
α : Type u_1
a b : α
l : Array α
⊢ a ∈ { toArray := l, size_toArray := ⋯ }.push b →
    b ∈ { toArray := l, size_toArray := ⋯ } → a ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simpa using Array.mem_of_mem_push_of_mem

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
⊢ a ∈ l.push b → b ∈ l → a ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a b : α
l : Array α
⊢ a ∈ { toArray := l, size_toArray := ⋯ }.push b →
    b ∈ { toArray := l, size_toArray := ⋯ } → a ∈ { toArray := l, size_toArray := ⋯ }
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.mul_neg (x y : BitVec w) : x * (~~~y + 1#w) = ~~~(x * y) + 1#w

Proof state:
w : Nat
x y : BitVec w
⊢ x * (~~~y + 1#w) = ~~~(x * y) + 1#w

Tactic:
rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.mul_neg]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma of_fac {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : f = eqToHom ha.symm ≫ p.map φ ≫ eqToHom hb) : p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
⊢ p.IsHomLift (eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯) φ

Tactic:
simp

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom hb
⊢ p.IsHomLift f φ

Tactic:
subst ha hb h

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
⊢ p.IsHomLift (eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯) φ
-- Mathlib/Computability/Primrec.lean
theorem natPair : Primrec₂ Nat.pair

Proof state:
⊢ Primrec₂ Nat.pair

Tactic:
simp [Primrec₂, Primrec]

Result:
⊢ Nat.Primrec fun n => n + 1

Proof state:
⊢ Nat.Primrec fun n => n + 1

Tactic:
constructor

Result:
no goals
-- Mathlib/Probability/Distributions/Geometric.lean
/-- The geometric pmf is positive for all natural numbers -/
lemma geometricPMFReal_pos {n : ℕ} (hp_pos : 0 < p) (hp_lt_one : p < 1) :
    0 < geometricPMFReal p n

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p

Tactic:
have : 0 < 1 - p := sub_pos.mpr hp_lt_one

Result:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
this : 0 < 1 - p
⊢ 0 < (1 - p) ^ n * p

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
this : 0 < 1 - p
⊢ 0 < (1 - p) ^ n * p

Tactic:
positivity

Result:
no goals

Proof state:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < geometricPMFReal p n

Tactic:
rw [geometricPMFReal]

Result:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pushforward_comp {f : Y ⟶ X} {g : Z ⟶ Y} (R : Sieve Z) :
    R.pushforward (g ≫ f) = (R.pushforward g).pushforward f :=
  Sieve.ext fun W h =>
    ⟨fun ⟨f₁, hq, hf₁⟩ => ⟨f₁ ≫ g, by simpa, f₁, rfl, hf₁⟩, fun ⟨y, hy, z, hR, hz⟩ =>
      ⟨z, by rw [← Category.assoc, hR]; tauto⟩⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward (g ≫ f) R).arrows h
f₁ : W ⟶ Z
hq : f₁ ≫ g ≫ f = h
hf₁ : R.arrows f₁
⊢ (f₁ ≫ g) ≫ f = h

Tactic:
simpa

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ z ≫ g ≫ f = h ∧ R.arrows z

Tactic:
rw [← Category.assoc, hR]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve Z
W : C
h : W ⟶ X
x✝ : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ y ≫ f = h ∧ R.arrows z
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_C_mul {x : F} (hx : x ≠ 0) :
    (C x * f).natSepDegree = f.natSepDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (C x * f).natSepDegree = f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (C x * f).natSepDegree = f.natSepDegree

Tactic:
classical
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_midpoint (x y : P) : Wbtw R x (midpoint R x y) y

Proof state:
case h.e'_10
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ y = (pointReflection R (midpoint R x y)) x

Tactic:
rw [pointReflection_midpoint_left]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R x (midpoint R x y) y

Tactic:
convert wbtw_pointReflection R (midpoint R x y) x

Result:
case h.e'_10
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ y = (pointReflection R (midpoint R x y)) x
-- Mathlib/Computability/Primrec.lean
theorem option_iget [Inhabited α] : Primrec (@Option.iget α _) :=
  (option_casesOn .id (const <| @default α _) .right).of_eq fun o => by cases o <;> rfl

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
inst✝ : Inhabited α
o : Option α
⊢ (Option.casesOn (id o) default fun b => b) = o.iget

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem inv_prodComparison_map_fst [IsIso (prodComparison F A B)] :
    inv (prodComparison F A B) ≫ F.map (fst _ _) = fst _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B)

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp]
lemma RightHomologyData.opcyclesIso_hom_comp_descQ :
    h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.hom ≫ h.descQ k hk = S.descOpcycles k hk

Tactic:
rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]

Result:
no goals