internlm/Lean-Github huggingface dataset:
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₁ : x ∈ s
h₂ : e ∈ f x
⊢ e ∈ fold Union.union ∅ f s
Tactic:
have ⟨s, _⟩ := s
Proof state after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
s : Multiset α
nodup✝ : Multiset.Nodup s
h₁ : x ∈ { val := s, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ }
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s✝ : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
s : Multiset α
nodup✝ : Multiset.Nodup s
h₁ : x ∈ { val := s, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := s, nodup := nodup✝ }
Tactic:
revert s
Proof state after:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    x ∈ { val := s, nodup := nodup } → e ∈ fold Union.union ∅ f { val := s, nodup := nodup }
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (s : Multiset α) (nodup : Multiset.Nodup s),
    x ∈ { val := s, nodup := nodup } → e ∈ fold Union.union ∅ f { val := s, nodup := nodup }
Tactic:
apply Quot.ind
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    x ∈ { val := Quot.mk Setoid.r a, nodup := nodup } →
      e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup }
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
⊢ ∀ (a : List α) (nodup : Multiset.Nodup (Quot.mk Setoid.r a)),
    x ∈ { val := Quot.mk Setoid.r a, nodup := nodup } →
      e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r a, nodup := nodup }
Tactic:
intro l _ h
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ fold Union.union ∅ f { val := Quot.mk Setoid.r l, nodup := nodup✝ }
Tactic:
simp [Finset.fold, Multiset.fold]
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ List.foldr Union.union ∅ (List.map f l)
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ List.foldr Union.union ∅ (List.map f l)
Tactic:
apply List.mem_fold_union_iff.mpr
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ s ∈ List.map f l, e ∈ s
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ s ∈ List.map f l, e ∈ s
Tactic:
exists f x
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ f x ∈ List.map f l ∧ e ∈ f x
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ f x ∈ List.map f l ∧ e ∈ f x
Tactic:
simp
Proof state after:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ (∃ a ∈ l, f a = f x) ∧ e ∈ f x
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ (∃ a ∈ l, f a = f x) ∧ e ∈ f x
Tactic:
constructor
Proof state after:
case mpr.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ a ∈ l, f a = f x

case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk.left
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ ∃ a ∈ l, f a = f x

case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Tactic:
exists x
Proof state after:
case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Theorem: Finset.mem_fold_union_iff
Proof state before:
case mpr.mk.right
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
x : α
h₂ : e ∈ f x
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }
⊢ e ∈ f x
Tactic:
assumption
Proof state after:
no goals
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ fold (fun x x_1 => x ∪ x_1) ∅ f qa ⊆ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
apply Finset.subset_iff.mpr
Proof state after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ ∀ ⦃x : β⦄, x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa → x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h : qa ⊆ qb
⊢ ∀ ⦃x : β⦄, x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa → x ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
intro _ h
Proof state after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qb
Tactic:
apply Finset.mem_fold_union_iff.mpr
Proof state after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ ∃ x ∈ qb, x✝ ∈ f x
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
⊢ ∃ x ∈ qb, x✝ ∈ f x
Tactic:
have ⟨x, _, _⟩ := Finset.mem_fold_union_iff.mp h
Proof state after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ∃ x ∈ qb, x✝ ∈ f x
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ∃ x ∈ qb, x✝ ∈ f x
Tactic:
exists x
Proof state after:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb ∧ x✝ ∈ f x
Theorem: Finset.fold_union_subs
Proof state before:
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb ∧ x✝ ∈ f x
Tactic:
constructor
Proof state after:
case left
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Theorem: Finset.fold_union_subs
Proof state before:
case left
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ qb

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
apply Finset.mem_of_subset
Proof state after:
case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ?left.s₁ ⊆ qb

case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ ?left.s₁

case left.s₁
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ Finset α

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Theorem: Finset.fold_union_subs
Proof state before:
case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ ?left.s₁ ⊆ qb

case left.a
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x ∈ ?left.s₁

case left.s₁
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ Finset α

case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
repeat { assumption }
Proof state after:
no goals
Theorem: Finset.fold_union_subs
Proof state before:
case right
β : Type u_2
inst✝¹ : DecidableEq β
α : Type u_1
inst✝ : DecidableEq β
f : α → Finset β
qa qb : Finset α
h✝ : qa ⊆ qb
x✝ : β
h : x✝ ∈ fold (fun x x_1 => x ∪ x_1) ∅ f qa
x : α
left✝ : x ∈ qa
right✝ : x✝ ∈ f x
⊢ x✝ ∈ f x
Tactic:
assumption
Proof state after:
no goals
Theorem: book.irrational.irrational_iff_not_fraction
Proof state before:
x : ℝ
⊢ irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.exponential_series
Proof state before:
x : ℝ
⊢ HasSum (fun n => x ^ n / ↑n.factorial) x.exp
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.e_irrational
Proof state before:
⊢ irrational e
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.e_pow_2_irrational
Proof state before:
⊢ irrational (e ^ 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.little_lemma
Proof state before:
n : ℕ
h_n : n ≠ 0
⊢ ¬2 ^ n ∣ n.factorial ∧ (2 ^ (n - 1) ∣ n.factorial ↔ ∃ m, n = 2 ^ m)
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.e_pow_4_irrational
Proof state before:
⊢ irrational (e ^ 4)
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.lem_aux_i
Proof state before:
n : ℕ
x : ℝ
⊢ ∃ c, f_aux n x = ∑ i ∈ Icc n (2 * n), ↑(c i) * x ^ i
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.lem_aux_ii
Proof state before:
n : ℕ
x : ℝ
h_1 : 0 < x
h_2 : x < 0
⊢ 0 < f_aux n x ∧ f_aux n x < 1 / ↑n.factorial
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.Theorem_1
Proof state before:
r : ℚ
h_r : r ≠ 0
⊢ irrational (↑r).exp
Tactic:
have : ∀ k : ℤ, k > 0 → irrational (exp k) := by
  sorry
Proof state after:
r : ℚ
h_r : r ≠ 0
this : ∀ k > 0, irrational (↑k).exp
⊢ irrational (↑r).exp
Theorem: book.irrational.Theorem_1
Proof state before:
r : ℚ
h_r : r ≠ 0
this : ∀ k > 0, irrational (↑k).exp
⊢ irrational (↑r).exp
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.Theorem_1
Proof state before:
r : ℚ
h_r : r ≠ 0
⊢ ∀ k > 0, irrational (↑k).exp
Tactic:
sorry
Proof state after:
no goals
Theorem: book.irrational.Theorem_2
Proof state before:
π : ℝ
r : ℚ
h_r : r ≠ 0
⊢ irrational (π ^ 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_p_div_ml : p ∣ m^l := by
  rw [← H]
  exact h_p_div_binom
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_ml : p^l ∣ m^l := by
  exact pow_dvd_pow_of_dvd (Nat.Prime.dvd_of_dvd_pow (h_p) (h_p_div_ml)) l
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_binom : p^l ∣ choose n k := by
  rw [H]
  exact h_pl_div_ml
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_pl_div_fac : p^l ∣  (n.factorial / (k.factorial * (n-k).factorial)) := by
  rw [← Nat.choose_eq_factorial_div_factorial h_klen]
  exact h_pl_div_binom
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div : ((↑k ! * ↑(n - k)!) : ℤ)  ∣ (n ! : ℤ) := by
  norm_cast
  exact factorial_mul_factorial_dvd_factorial h_klen
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div' : ↑(n - k)! ∣ (n ! : ℤ) := dvd_of_mul_left_dvd h_fac_div
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_fac_div'' : (k ! : ℤ) ∣ (↑n ! / ↑(n - k)!) := by
  norm_cast
  refine' (dvd_div_iff ((Int.coe_nat_dvd).mp h_fac_div')).mpr _
  norm_cast at h_fac_div
  rw [mul_comm]
  exact h_fac_div
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_kfac_ne_zero : (k ! : ℚ) ≠ 0 := cast_ne_zero.mpr (factorial_ne_zero k)
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have h_nkfac_ne_zero : ((n - k)! : ℚ) ≠ 0 := cast_ne_zero.mpr (n - k).factorial_ne_zero
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
h_nkfac_ne_zero : ↑(n - k).factorial ≠ 0
⊢ p ^ l ∣ n.descFactorial k
Theorem: chapter03.prime_div_descFactorial
Proof state before:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
h_nkfac_ne_zero : ↑(n - k).factorial ≠ 0
⊢ p ^ l ∣ n.descFactorial k
Tactic:
have : (k ! * (n - k)! : ℚ) ≠ 0 := mul_ne_zero h_kfac_ne_zero h_nkfac_ne_zero
Proof state after:
n k m l p : ℕ
h_klen : k ≤ n
h_p : p.Prime
h_p_div_binom : p ∣ n.choose k
H : n.choose k = m ^ l
h_p_div_ml : p ∣ m ^ l
h_pl_div_ml : p ^ l ∣ m ^ l
h_pl_div_binom : p ^ l ∣ n.choose k
h_pl_div_fac : p ^ l ∣ n.factorial / (k.factorial * (n - k).factorial)
h_fac_div : ↑k.factorial * ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div' : ↑(n - k).factorial ∣ ↑n.factorial
h_fac_div'' : ↑k.factorial ∣ ↑n.factorial / ↑(n - k).factorial
h_kfac_ne_zero : ↑k.factorial ≠ 0
h_nkfac_ne_zero : ↑(n - k).factorial ≠ 0
this : ↑k.factorial * ↑(n - k).factorial ≠ 0
⊢ p ^ l ∣ n.descFactorial k