internlm/Lean-Github huggingface dataset:
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rw [Kaplansky.set_def, ← Ne.def] at ha₂
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rcases Set.nonempty_iff_ne_empty.2 (ha₂ hP) with ⟨x, ⟨hx, hx₂⟩⟩
Proof state after:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
cases' Ideal.mem_span_singleton'.1 (SetLike.mem_coe.1 hx) with b hb
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
hx₂ : x ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
rw [← hb, mul_comm] at hx₂
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
have hsubset : Submonoid.closure {r : R | Prime r} ≤
    Submonoid.closure {r : R | IsUnit r ∨ Prime r} := by
  refine' Submonoid.closure_mono (Set.setOf_subset_setOf.2 (fun _ ha => _))
  right
  exact ha
Proof state after:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
hsubset : Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
case intro.intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
hsubset : Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
Tactic:
exact exists_prime_factors_of_exists_multiset a (Submonoid.exists_multiset_of_mem_closure
  (Submonoid.closure_mem_of_prod_mem _ _ (hsubset hx₂)))
Proof state after:
no goals
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
Tactic:
refine' Submonoid.closure_mono (Set.setOf_subset_setOf.2 (fun _ ha => _))
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ IsUnit x✝ ∨ Prime x✝
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ IsUnit x✝ ∨ Prime x✝
Tactic:
right
Proof state after:
case h
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ Prime x✝
Theorem: uniqueFactorizationMonoid_of_exists_prime
Proof state before:
case h
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha✝ : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → ↑(Ideal.span {a}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
x✝ : R
ha : Prime x✝
⊢ Prime x✝
Tactic:
exact ha
Proof state after:
no goals
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
Tactic:
classical
constructor
intro _ _ hI hI₂
exact Ideal.IsPrime.exists_mem_prime_of_ne_bot hI₂ hI
intro H
exact uniqueFactorizationMonoid_of_exists_prime H hP
Proof state after:
no goals
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R ↔ ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R → ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ UniqueFactorizationMonoid R → ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
intro _ _ hI hI₂
Proof state after:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
a✝ : UniqueFactorizationMonoid R
I✝ : Ideal R
hI : I✝ ≠ ⊥
hI₂ : Ideal.IsPrime I✝
⊢ ∃ x ∈ I✝, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
case mp
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
a✝ : UniqueFactorizationMonoid R
I✝ : Ideal R
hI : I✝ ≠ ⊥
hI₂ : Ideal.IsPrime I✝
⊢ ∃ x ∈ I✝, Prime x

case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
exact Ideal.IsPrime.exists_mem_prime_of_ne_bot hI₂ hI
Proof state after:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
⊢ (∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x) → UniqueFactorizationMonoid R
Tactic:
intro H
Proof state after:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R
Theorem: uniqueFactorizationMonoid_iff
Proof state before:
case mpr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
hP : Set.Nonempty {r | Prime r}
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
⊢ UniqueFactorizationMonoid R
Tactic:
exact uniqueFactorizationMonoid_of_exists_prime H hP
Proof state after:
no goals
Theorem: STG4.mem_pair
Proof state before:
U : Type
t A B : U
⊢ t ∈ {A, B} ↔ t = A ∨ t = B
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.iterate_eq_Nat_iterate
Proof state before:
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
⊢ iterate f a i = f^[i] a
Tactic:
induction' i with i ih
Proof state after:
case zero
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
⊢ iterate f a Nat.zero = f^[Nat.zero] a

case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ iterate f a (Nat.succ i) = f^[Nat.succ i] a
Theorem: Stream'.iterate_eq_Nat_iterate
Proof state before:
case zero
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
⊢ iterate f a Nat.zero = f^[Nat.zero] a
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.iterate_eq_Nat_iterate
Proof state before:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ iterate f a (Nat.succ i) = f^[Nat.succ i] a
Tactic:
unfold iterate Nat.iterate
Proof state after:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ f (iterate f a i) = f^[i] (f a)
Theorem: Stream'.iterate_eq_Nat_iterate
Proof state before:
case succ
α : Type ?u.15
σ : Stream' α
α✝ : Type u_1
f : α✝ → α✝
a : α✝
i : ℕ
ih : iterate f a i = f^[i] a
⊢ f (iterate f a i) = f^[i] (f a)
Tactic:
rw [ih, Function.Commute.iterate_self]
Proof state after:
no goals
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ iterate (fun s i => s (f i)) σ i j = σ (f^[i] j)
Tactic:
rw [iterate_eq_Nat_iterate]
Proof state after:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
α : Type u_1
σ✝ : Stream' α
i j : ℕ
σ : Stream' α
f : ℕ → ℕ
⊢ (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
Tactic:
induction' i with i ih generalizing σ
Proof state after:
case zero
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.zero] σ j = σ (f^[Nat.zero] j)

case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.succ i] σ j = σ (f^[Nat.succ i] j)
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
case zero
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.zero] σ j = σ (f^[Nat.zero] j)
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ (fun s i => s (f i))^[Nat.succ i] σ j = σ (f^[Nat.succ i] j)
Tactic:
simp [ih]
Proof state after:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ σ (f (f^[i] j)) = σ (f^[i] (f j))
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
case succ
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ σ (f (f^[i] j)) = σ (f^[i] (f j))
Tactic:
congr
Proof state after:
case succ.e_a
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ f (f^[i] j) = f^[i] (f j)
Theorem: Stream'.iterate_stream_eq_index_iterate
Proof state before:
case succ.e_a
α : Type u_1
σ✝¹ : Stream' α
j : ℕ
σ✝ : Stream' α
f : ℕ → ℕ
i : ℕ
ih : ∀ (σ : Stream' α), (fun s i => s (f i))^[i] σ j = σ (f^[i] j)
σ : Stream' α
⊢ f (f^[i] j) = f^[i] (f j)
Tactic:
exact (Function.iterate_succ_apply' f i j).symm
Proof state after:
no goals
Theorem: Stream'.corec_succ
Proof state before:
α : Type ?u.5702
σ : Stream' α
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
g : α✝¹ → α✝¹
x : α✝¹
i : ℕ
⊢ corec f g x (i + 1) = corec f g (g x) i
Tactic:
simp only [corec, map, nth, iterate_eq_Nat_iterate, Function.iterate_succ, Function.comp_apply]
Proof state after:
no goals
Theorem: Stream'.tail_corec
Proof state before:
α : Type ?u.6271
σ : Stream' α
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
g : α✝¹ → α✝¹
x : α✝¹
⊢ tail (corec f g x) = corec f g (g x)
Tactic:
simp only [tail, nth, corec_succ]
Proof state after:
no goals
Theorem: Stream'.corec_bisim
Proof state before:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
⊢ ∀ {a : α} {a' : α'}, R a a' → corec f g a = corec f' g' a'
Tactic:
intro a a' hR
Proof state after:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ corec f g a = corec f' g' a'
Theorem: Stream'.corec_bisim
Proof state before:
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ corec f g a = corec f' g' a'
Tactic:
funext i
Proof state after:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ corec f g a i = corec f' g' a' i
Theorem: Stream'.corec_bisim
Proof state before:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ corec f g a i = corec f' g' a' i
Tactic:
simp [corec, map, nth]
Proof state after:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ f (iterate g a i) = f' (iterate g' a' i)
Theorem: Stream'.corec_bisim
Proof state before:
case h
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ f (iterate g a i) = f' (iterate g' a' i)
Tactic:
apply hf
Proof state after:
case h.a
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ R (iterate g a i) (iterate g' a' i)
Theorem: Stream'.corec_bisim
Proof state before:
case h.a
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
⊢ R (iterate g a i) (iterate g' a' i)
Tactic:
induction' i with i ih
Proof state after:
case h.a.zero
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ R (iterate g a Nat.zero) (iterate g' a' Nat.zero)

case h.a.succ
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
ih : R (iterate g a i) (iterate g' a' i)
⊢ R (iterate g a (Nat.succ i)) (iterate g' a' (Nat.succ i))
Theorem: Stream'.corec_bisim
Proof state before:
case h.a.zero
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
⊢ R (iterate g a Nat.zero) (iterate g' a' Nat.zero)
Tactic:
exact hR
Proof state after:
no goals
Theorem: Stream'.corec_bisim
Proof state before:
case h.a.succ
α : Type u_3
σ : Stream' α
β : Type u_1
α' : Type u_2
f : α → β
g : α → α
f' : α' → β
g' : α' → α'
R : α → α' → Prop
hf : ∀ (a : α) (a' : α'), R a a' → f a = f' a'
hg : ∀ (a : α) (a' : α'), R a a' → R (g a) (g' a')
a : α
a' : α'
hR : R a a'
i : ℕ
ih : R (iterate g a i) (iterate g' a' i)
⊢ R (iterate g a (Nat.succ i)) (iterate g' a' (Nat.succ i))
Tactic:
exact hg _ _ ih
Proof state after:
no goals
Theorem: Stream'.fun_to_corec
Proof state before:
α : Type u_1
σ✝ σ : Stream' α
⊢ σ = corec σ (fun x => x + 1) 0
Tactic:
funext i
Proof state after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ i = corec σ (fun x => x + 1) 0 i
Theorem: Stream'.fun_to_corec
Proof state before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ i = corec σ (fun x => x + 1) 0 i
Tactic:
suffices ∀ j,
  σ (i+j) = corec σ _ j i
from this 0
Proof state after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
Theorem: Stream'.fun_to_corec
Proof state before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
Tactic:
intro j
Proof state after:
case h
α : Type u_1
σ✝ σ : Stream' α
i j : ℕ
⊢ σ (i + j) = corec σ (fun x => x + 1) j i
Theorem: Stream'.fun_to_corec
Proof state before:
case h
α : Type u_1
σ✝ σ : Stream' α
i j : ℕ
⊢ σ (i + j) = corec σ (fun x => x + 1) j i
Tactic:
induction' i with i ih generalizing j
Proof state after:
case h.zero
α : Type u_1
σ✝ σ : Stream' α
j✝ j : ℕ
⊢ σ (Nat.zero + j) = corec σ (fun x => x + 1) j Nat.zero

case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i : ℕ
ih : ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
j : ℕ
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Theorem: Stream'.fun_to_corec
Proof state before:
case h.zero
α : Type u_1
σ✝ σ : Stream' α
j✝ j : ℕ
⊢ σ (Nat.zero + j) = corec σ (fun x => x + 1) j Nat.zero
Tactic:
simp only [Nat.zero_eq, zero_add, corec_zero]
Proof state after:
no goals
Theorem: Stream'.fun_to_corec
Proof state before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i : ℕ
ih : ∀ (j : ℕ), σ (i + j) = corec σ (fun x => x + 1) j i
j : ℕ
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
specialize ih (j+1)
Proof state after:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + (j + 1)) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Theorem: Stream'.fun_to_corec
Proof state before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + (j + 1)) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
rw [←Nat.add_assoc] at ih
Proof state after:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + j + 1) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Theorem: Stream'.fun_to_corec
Proof state before:
case h.succ
α : Type u_1
σ✝ σ : Stream' α
j✝ i j : ℕ
ih : σ (i + j + 1) = corec σ (fun x => x + 1) (j + 1) i
⊢ σ (Nat.succ i + j) = corec σ (fun x => x + 1) j (Nat.succ i)
Tactic:
simp only [Nat.succ_add, ih, corec_succ]
Proof state after:
no goals
Theorem: Stream'.take_append_drop_take
Proof state before:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ take i σ ++ take j (drop i σ) = take (i + j) σ
Tactic:
simp only [drop, nth]
Proof state after:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ