michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library,hott): avoid rewrite with patterns of the form (?M ...)

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-09 14:21:33 -08:00
parent d4f0ce0eab
commit 5e14b4ebe8
18 changed files with 55 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/algebra/category/iso.hlean
View file

@ -378,8 +378,8 @@ namespace iso
variables (q)
theorem comp.cancel_left (H : q ∘ p = q ∘ p') : p = p' :=
by rewrite [-inverse_comp_cancel_left q, H, inverse_comp_cancel_left q]
by rewrite [-inverse_comp_cancel_left q p, H, inverse_comp_cancel_left q]
theorem comp.cancel_right (H : r ∘ q = r' ∘ q) : r = r' :=
by rewrite [-comp_inverse_cancel_right _ q, H, comp_inverse_cancel_right _ q]
by rewrite [-comp_inverse_cancel_right r q, H, comp_inverse_cancel_right _ q]
end
end iso

10
hott/algebra/field.hlean
View file

@ -58,7 +58,7 @@ section division_ring
absurd C1 zero_ne_one
theorem one_inv_eq : 1⁻¹ = (1:A) :=
by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))]
by rewrite [-mul_one ((1:A)⁻¹), inv_mul_cancel (ne.symm (@zero_ne_one A _))]
theorem div_one (a : A) : a / 1 = a :=
by rewrite [*division.def, one_inv_eq, mul_one]
@ -69,7 +69,7 @@ section division_ring
-- domain, but let's not define that class for now.
theorem division_ring.mul_ne_zero (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
assume H : a * b = 0,
have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
have C1 : a = 0, by rewrite [-(mul_one a), -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
absurd C1 Ha
theorem mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 :=
@ -190,7 +190,7 @@ section division_ring
theorem eq_div_iff_mul_eq (a : A) {b : A} (Hc : c ≠ 0) : a = b / c ↔ a * c = b :=
iff.intro
(suppose a = b / c, by rewrite [this, (!div_mul_cancel Hc)])
(suppose a * c = b, by rewrite [-(!mul_div_cancel Hc), this])
(suppose a * c = b, begin rewrite [-mul_div_cancel a Hc, this] end)
theorem eq_div_of_mul_eq (a b : A) {c : A} (Hc : c ≠ 0) : a * c = b → a = b / c :=
iff.mpr (!eq_div_iff_mul_eq Hc)
@ -278,7 +278,7 @@ section field
theorem mul_eq_mul_of_div_eq_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0)
(Hd : d ≠ 0) (H : a / b = c / d) : a * d = c * b :=
by rewrite [-mul_one, mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
by rewrite [-mul_one (a*d), mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
-(!field.div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div), (!div_mul_cancel Hd)]
theorem field.one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
@ -332,7 +332,7 @@ section discrete_field
decidable.by_cases
(suppose x = 0, sum.inl this)
(suppose x ≠ 0,
sum.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
sum.inr (by rewrite [-one_mul y, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
definition discrete_field.to_integral_domain [trans_instance] : integral_domain A :=
⦃ integral_domain, s,

2
hott/algebra/group.hlean
View file

@ -352,7 +352,7 @@ section add_group
by rewrite [add.assoc, add.left_inv, add_zero]
theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
by rewrite [-add_zero, -H, neg_add_cancel_left]
by rewrite [-add_zero (-a), -H, neg_add_cancel_left]
theorem neg_zero : -0 = (0 : A) := neg_eq_of_add_eq_zero (zero_add 0)

6
hott/types/int/hott.hlean
View file

@ -94,7 +94,7 @@ namespace eq
(λn IH, idp)
(λn IH, calc
power p (-succ n) ⬝ p
= (power p (-int.of_nat n) ⬝ p⁻¹) ⬝ p : by rewrite [↑power,-rec_nat_on_neg]
= (power p (-int.of_nat n) ⬝ p⁻¹) ⬝ p : by krewrite [↑power,rec_nat_on_neg]
... = power p (-int.of_nat n) : inv_con_cancel_right
... = power p (succ (-succ n)) : by rewrite -succ_neg_succ)
@ -106,7 +106,7 @@ namespace eq
... = power p (pred (succ n)) : by rewrite pred_nat_succ)
(λn IH, calc
power p (-int.of_nat (succ n)) ⬝ p⁻¹
= power p (-int.of_nat (succ (succ n))) : by rewrite [↑power,-rec_nat_on_neg]
= power p (-int.of_nat (succ (succ n))) : by krewrite [↑power,*rec_nat_on_neg]
... = power p (pred (-succ n)) : by rewrite -neg_succ)
definition con_power : p ⬝ power p b = power p (succ b) :=
@ -137,7 +137,7 @@ namespace eq
... = (p⁻¹ ⬝ power p (-int.of_nat n)) ⬝ p⁻¹ : con.assoc
... = power p (pred (-int.of_nat n)) ⬝ p⁻¹ : by rewrite IH
... = power p (-int.of_nat (succ n)) ⬝ p⁻¹ : by rewrite -neg_succ
... = power p (-succ (succ n)) : by rewrite [↑power,-rec_nat_on_neg]
... = power p (-succ (succ n)) : by krewrite [↑power,*rec_nat_on_neg]
... = power p (pred (-succ n)) : by rewrite -neg_succ)
definition power_con_power : Π(b : ℤ), power p b ⬝ power p c = power p (b + c) :=

10
library/algebra/field.lean
View file

@ -60,7 +60,7 @@ section division_ring
absurd C1 zero_ne_one
theorem one_inv_eq [simp] : 1⁻¹ = (1:A) :=
by rewrite [-mul_one, inv_mul_cancel (ne.symm (@zero_ne_one A _))]
by rewrite [-mul_one ((1:A)⁻¹), inv_mul_cancel (ne.symm (@zero_ne_one A _))]
theorem div_one [simp] (a : A) : a / 1 = a :=
by simp
@ -72,7 +72,7 @@ section division_ring
-- domain, but let's not define that class for now.
theorem division_ring.mul_ne_zero (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
assume H : a * b = 0,
have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
have C1 : a = 0, by rewrite [-mul_one a, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
absurd C1 Ha
theorem mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 :=
@ -176,7 +176,7 @@ section division_ring
theorem eq_div_iff_mul_eq (a : A) {b : A} (Hc : c ≠ 0) : a = b / c ↔ a * c = b :=
iff.intro
(suppose a = b / c, by rewrite [this, (!div_mul_cancel Hc)])
(suppose a * c = b, by rewrite [-(!mul_div_cancel Hc), this])
(suppose a * c = b, by rewrite [-(mul_div_cancel a Hc), this])
theorem eq_div_of_mul_eq (a b : A) {c : A} (Hc : c ≠ 0) : a * c = b → a = b / c :=
iff.mpr (!eq_div_iff_mul_eq Hc)
@ -257,7 +257,7 @@ section field
theorem mul_eq_mul_of_div_eq_div (a : A) {b : A} (c : A) {d : A} (Hb : b ≠ 0)
(Hd : d ≠ 0) (H : a / b = c / d) : a * d = c * b :=
by rewrite [-mul_one, mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
by rewrite [-mul_one (a*d), mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
-(!field.div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div), (!div_mul_cancel Hd)]
theorem field.one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
@ -311,7 +311,7 @@ section discrete_field
decidable.by_cases
(suppose x = 0, or.inl this)
(suppose x ≠ 0,
or.inr (by rewrite [-one_mul, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
or.inr (by rewrite [-one_mul y, -(inv_mul_cancel this), mul.assoc, H, mul_zero]))
definition discrete_field.to_integral_domain [trans_instance] :
integral_domain A :=

26
library/algebra/homomorphism.lean
View file

@ -49,7 +49,7 @@ is_add_hom.mk (take a₁ a₂, rfl)
proposition is_add_hom_comp [has_add A] [has_add B] [has_add C]
{f : B → C} {g : A → B} [is_add_hom f] [is_add_hom g] : is_add_hom (f ∘ g) :=
is_add_hom.mk (take a₁ a₂, by esimp; rewrite *hom_add)
is_add_hom.mk (take a₁ a₂, begin esimp, rewrite [hom_add g, hom_add f] end)
section add_group_A_B
variables [add_group A] [add_group B]
@ -61,26 +61,26 @@ section add_group_A_B
proposition hom_neg (f : A → B) [is_add_hom f] (a : A) :
f (- a) = - f a :=
have f (- a) + f a = 0, by rewrite [-hom_add f, add.left_inv, hom_zero],
have f (- a) + f a = 0, by rewrite [-hom_add f, add.left_inv, hom_zero f],
eq_neg_of_add_eq_zero this
proposition hom_sub (f : A → B) [is_add_hom f] (a₁ a₂ : A) :
f (a₁ - a₂) = f a₁ - f a₂ :=
by rewrite [*sub_eq_add_neg, *hom_add, hom_neg]
by rewrite [*sub_eq_add_neg, *(hom_add f), (hom_neg f)]
proposition injective_hom_add [add_group B] {f : A → B} [is_add_hom f]
(H : ∀ x, f x = 0 → x = 0) :
injective f :=
take x₁ x₂,
suppose f x₁ = f x₂,
have f (x₁ - x₂) = 0, by rewrite [hom_sub, this, sub_self],
have f (x₁ - x₂) = 0, by rewrite [hom_sub f, this, sub_self],
have x₁ - x₂ = 0, from H _ this,
eq_of_sub_eq_zero this
proposition eq_zero_of_injective_hom [add_group B] {f : A → B} [is_add_hom f]
(injf : injective f) {a : A} (fa0 : f a = 0) :
a = 0 :=
have f a = f 0, by rewrite [fa0, hom_zero],
have f a = f 0, by rewrite [fa0, hom_zero f],
show a = 0, from injf this
end add_group_A_B
@ -104,7 +104,7 @@ is_mul_hom.mk (take a₁ a₂, rfl)
proposition is_mul_hom_comp [has_mul A] [has_mul B] [has_mul C]
{f : B → C} {g : A → B} [is_mul_hom f] [is_mul_hom g] : is_mul_hom (f ∘ g) :=
is_mul_hom.mk (take a₁ a₂, by esimp; rewrite *hom_mul)
is_mul_hom.mk (take a₁ a₂, begin esimp, rewrite [hom_mul g, hom_mul f] end)
section group_A_B
variables [group A] [group B]
@ -116,7 +116,7 @@ section group_A_B
proposition hom_inv (f : A → B) [is_mul_hom f] (a : A) :
f (a⁻¹) = (f a)⁻¹ :=
have f (a⁻¹) * f a = 1, by rewrite [-hom_mul f, mul.left_inv, hom_one],
have f (a⁻¹) * f a = 1, by rewrite [-hom_mul f, mul.left_inv, hom_one f],
eq_inv_of_mul_eq_one this
proposition injective_hom_mul [group B] {f : A → B} [is_mul_hom f]
@ -124,14 +124,14 @@ section group_A_B
injective f :=
take x₁ x₂,
suppose f x₁ = f x₂,
have f (x₁ * x₂⁻¹) = 1, by rewrite [hom_mul, hom_inv, this, mul.right_inv],
have f (x₁ * x₂⁻¹) = 1, by rewrite [hom_mul f, hom_inv f, this, mul.right_inv],
have x₁ * x₂⁻¹ = 1, from H _ this,
eq_of_mul_inv_eq_one this
proposition eq_one_of_injective_hom [group B] {f : A → B} [is_mul_hom f]
(injf : injective f) {a : A} (fa1 : f a = 1) :
a = 1 :=
have f a = f 1, by rewrite [fa1, hom_one],
have f a = f 1, by rewrite [fa1, hom_one f],
show a = 1, from injf this
end group_A_B
@ -156,11 +156,11 @@ section module_hom
proposition is_module_hom_comp : is_module_hom R (g ∘ f) :=
is_module_hom.mk
(take a₁ a₂, by esimp; rewrite *hom_add)
(take a₁ a₂, begin esimp, rewrite [hom_add f, hom_add g] end)
(take r a, by esimp; rewrite [hom_smul f, hom_smul g])
proposition hom_smul_add_smul (a b : R) (u v : M₁) : f (a • u + b • v) = a • f u + b • f v :=
by rewrite [hom_add, +hom_smul f]
by rewrite [hom_add f, +hom_smul f]
end module_hom
/- rings -/
@ -177,9 +177,9 @@ section semiring
proposition is_ring_hom_comp : is_ring_hom (g ∘ f) :=
is_ring_hom.mk
(take a₁ a₂, by esimp; rewrite *hom_add)
(take a₁ a₂, begin esimp, rewrite [hom_add f, hom_add g] end)
(take r a, by esimp; rewrite [hom_mul f, hom_mul g])
proposition hom_mul_add_mul (a b c d : R₁) : f (a * b + c * d) = f a * f b + f c * f d :=
by rewrite [hom_add, +hom_mul]
by rewrite [hom_add f, +(hom_mul f)]
end semiring

2
library/data/finset/partition.lean
View file

@ -112,7 +112,7 @@ include deceqB
lemma binary_Union (f : A → finset B) {P : A → Prop} [decP : decidable_pred P] {s : finset A} :
Union s f = Union {a ∈ s | P a} f ∪ Union {a ∈ s | ¬P a} f :=
begin rewrite [binary_union P at {1}], apply Union_union, exact binary_inter_empty end
begin rewrite [@binary_union _ _ P _ s at {1}], apply Union_union, exact binary_inter_empty end
end

2
library/data/list/set.lean
View file

@ -27,7 +27,7 @@ rfl
lemma erase_cons_head (a : A) (l : list A) : erase a (a :: l) = l :=
show match H a a with | inl e := l | inr n := a :: erase a l end = l,
by rewrite decidable_eq_inl_refl
by rewrite (@decidable_eq_inl_refl A H)
lemma erase_cons_tail {a b : A} (l : list A) : a ≠ b → erase a (b::l) = b :: erase a l :=
assume h : a ≠ b,

2
library/data/nat/fact.lean
View file

@ -49,7 +49,7 @@ begin
{subst m},
{transitivity (fact n),
exact ih (le_of_lt_succ h₂),
rewrite [fact_succ, -one_mul at {1}],
rewrite [fact_succ, -one_mul (fact n) at {1}],
exact nat.mul_le_mul (succ_le_succ (zero_le n)) !le.refl}}
end
end nat

6
library/data/pnat.lean
View file

@ -196,7 +196,7 @@ begin
apply one_div_lt_one_div_of_lt,
apply rat_of_pnat_is_pos,
have H : n~ < (2 * n)~, begin
rewrite -pnat.one_mul at {1},
rewrite -(pnat.one_mul n) at {1},
rewrite -pnat.lt_def,
apply mul_lt_mul_left,
apply one_lt_two
@ -265,7 +265,7 @@ pnat.eq !add.assoc
protected theorem mul_le_mul_left (p q : ℕ+) : q ≤ p * q :=
begin
rewrite [-pnat.one_mul at {1}, pnat.mul_comm, pnat.mul_comm p],
rewrite [-pnat.one_mul q at {1}, pnat.mul_comm, pnat.mul_comm p],
apply pnat_mul_le_mul_left',
apply pone_le
end
@ -285,7 +285,7 @@ by rewrite rat.mul_comm; apply pnat.inv_cancel_left
theorem lt_add_left (p q : ℕ+) : p < p + q :=
begin
have H : p~ < p~ + q~, begin
rewrite -nat.add_zero at {1},
rewrite -(nat.add_zero (p~)) at {1},
apply nat.add_lt_add_left,
apply pnat_pos
end,

8
library/data/rat/order.lean
View file

@ -248,7 +248,7 @@ iff.intro
(suppose a = b, this ▸ !rat.le_refl))
private theorem to_nonneg : a ≥ 0 → nonneg a :=
by intros; rewrite -sub_zero; eassumption
by intros; rewrite -(sub_zero a); eassumption
protected theorem add_le_add_left (H : a ≤ b) (c : ℚ) : c + a ≤ c + b :=
have c + b - (c + a) = b - a,
@ -257,14 +257,14 @@ show nonneg (c + b - (c + a)), from this⁻¹ ▸ H
protected theorem mul_nonneg (H1 : a ≥ (0 : ℚ)) (H2 : b ≥ (0 : ℚ)) : a * b ≥ (0 : ℚ) :=
have nonneg (a * b), from nonneg_mul (to_nonneg H1) (to_nonneg H2),
begin rewrite -sub_zero at this, exact this end
begin rewrite -(sub_zero (a*b)) at this, exact this end
private theorem to_pos : a > 0 → pos a :=
by intros; rewrite -sub_zero; eassumption
by intros; rewrite -(sub_zero a); eassumption
protected theorem mul_pos (H1 : a > (0 : ℚ)) (H2 : b > (0 : ℚ)) : a * b > (0 : ℚ) :=
have pos (a * b), from pos_mul (to_pos H1) (to_pos H2),
begin rewrite -sub_zero at this, exact this end
begin rewrite -(sub_zero (a*b)) at this, exact this end
definition decidable_lt [instance] : decidable_rel rat.lt :=
take a b, decidable_pos (b - a)

4
library/data/real/basic.lean
View file

@ -758,8 +758,8 @@ theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t)
begin
rewrite [↑equiv, ↑smul],
intros,
rewrite [↑sneg, *sub_neg_eq_add, -neg_mul_eq_mul_neg, add.comm, *sneg_def,
*neg_bound2_eq_bound2, add.right_inv, abs_zero],
rewrite [↑sneg, *sub_neg_eq_add, -neg_mul_eq_mul_neg, add.comm],
rewrite [*sneg_def t, *neg_bound2_eq_bound2, add.right_inv, abs_zero],
apply add_invs_nonneg
end

2
library/data/real/complete.lean
View file

@ -816,7 +816,7 @@ private theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i
rewrite [if_neg Havg, ↑avg_seq, ↑avg],
apply rat.le_trans,
apply Ha,
rewrite -add_halves at {1},
rewrite -(add_halves (under_seq (i + a))) at {1},
apply add_le_add_right,
apply div_le_div_of_le_of_pos,
apply rat.le_of_lt,

11
library/data/set/basic.lean
View file

@ -95,7 +95,8 @@ section
apply forall_congr,
intro x,
rewrite not_and_iff_not_or_not,
rewrite imp_iff_not_or
symmetry,
apply imp_iff_not_or
end
lemma not_bounded_forall {A : Type} {S : set A} {P : A → Prop} :
@ -808,7 +809,7 @@ ext (take x, iff.intro
theorem sUnion_eq_compl_sInter_compl (S : set (set X)) :
⋃₀ S = - ⋂₀ (compl ' S) :=
by rewrite [-compl_compl, compl_sUnion]
by rewrite [-compl_compl (⋃₀ S), compl_sUnion]
theorem compl_sInter (S : set (set X)) :
- ⋂₀ S = ⋃₀ (compl ' S) :=
@ -816,7 +817,7 @@ by rewrite [sUnion_eq_compl_sInter_compl, compl_compl_image]
theorem sInter_eq_comp_sUnion_compl (S : set (set X)) :
⋂₀ S = -(⋃₀ (compl ' S)) :=
by rewrite [-compl_compl, compl_sInter]
by rewrite [-compl_compl (⋂₀ S), compl_sInter]
theorem inter_sUnion_nonempty_of_inter_nonempty {s t : set X} {S : set (set X)} (Hs : t ∈ S) (Hne : s ∩ t ≠ ∅) :
s ∩ ⋃₀ S ≠ ∅ :=
@ -870,10 +871,10 @@ theorem compl_Inter {X I : Type} (s : I → set X) : -(⋂ i, s i) = (⋃ i, - s
by rewrite [Inter_eq_sInter_image, compl_sInter, -image_comp, -Union_eq_sUnion_image]
theorem Union_eq_comp_Inter_comp {X I : Type} (s : I → set X) : (⋃ i, s i) = - (⋂ i, - s i) :=
by rewrite [-compl_compl, compl_Union]
by rewrite [-compl_compl (⋃ i, s i), compl_Union]
theorem Inter_eq_comp_Union_comp {X I : Type} (s : I → set X) : (⋂ i, s i) = - (⋃ i, -s i) :=
by rewrite [-compl_compl, compl_Inter]
by rewrite [-compl_compl (⋂ i, s i), compl_Inter]
lemma inter_distrib_Union_left {X I : Type} (s : I → set X) (a : set X) :
a ∩ (⋃ i, s i) = ⋃ i, a ∩ s i :=

2
library/data/set/card.lean
View file

@ -121,7 +121,7 @@ by rewrite [↑card, to_finset_image]; apply finset.card_image_le
theorem inj_on_of_card_image_eq {f : A → B} {s : set A} [finite s]
(H : card (image f s) = card s) : inj_on f s :=
begin
rewrite -to_set_to_finset,
rewrite -(to_set_to_finset s),
apply finset.inj_on_of_card_image_eq,
rewrite [-to_finset_to_set (finset.image _ _), finset.to_set_image, to_set_to_finset],
exact H

2
library/data/set/finite.lean
View file

@ -32,7 +32,7 @@ by rewrite [↑to_finset, dif_pos fins]; exact eq.symm (some_spec fins)
theorem mem_to_finset_eq (a : A) (s : set A) [finite s] :
(#finset a ∈ to_finset s) = (a ∈ s) :=
by rewrite [-to_set_to_finset at {2}]
by rewrite [-to_set_to_finset s at {2}]
theorem to_set_to_finset_of_not_finite {s : set A} (nfins : ¬ finite s) :
finset.to_set (to_finset s) = ∅ :=

8
library/data/stream.lean
View file

@ -116,10 +116,10 @@ theorem head_map (s : stream A) : head (map f s) = f (head s) :=
rfl
theorem map_eq (s : stream A) : map f s = f (head s) :: map f (tail s) :=
by rewrite [-stream.eta, tail_map, head_map]
by rewrite [-stream.eta (map f s), tail_map, head_map]
theorem map_cons (a : A) (s : stream A) : map f (a :: s) = f a :: map f s :=
by rewrite [-stream.eta, map_eq]
by rewrite [-stream.eta (map f (a :: s)), map_eq]
theorem map_id (s : stream A) : map id s = s :=
rfl
@ -151,7 +151,7 @@ theorem tail_zip (s₁ : stream A) (s₂ : stream B) : tail (zip f s₁ s₂) =
rfl
theorem zip_eq (s₁ : stream A) (s₂ : stream B) : zip f s₁ s₂ = f (head s₁) (head s₂) :: zip f (tail s₁) (tail s₂) :=
by rewrite [-stream.eta]
by rewrite [-stream.eta (zip f s₁ s₂)]
end zip
definition const (a : A) : stream A :=
@ -196,7 +196,7 @@ end
theorem iterate_eq (f : A → A) (a : A) : iterate f a = a :: iterate f (f a) :=
begin
rewrite [-stream.eta], congruence, exact !tail_iterate
rewrite [-stream.eta (iterate f a)], congruence, exact !tail_iterate
end
theorem nth_zero_iterate (f : A → A) (a : A) : nth 0 (iterate f a) = a :=

2
library/theories/number_theory/irrational_roots.lean
View file

@ -121,7 +121,7 @@ section
have ane0 : a ≠ 0, from
suppose aeq0 : a = 0,
have qeq0 : q = 0,
by rewrite [eq_num_div_denom, aeq0, of_int_zero, zero_div],
begin rewrite [eq_num_div_denom q, aeq0, of_int_zero, zero_div] end,
show false,
from qne0 qeq0,
have nat_abs a ≠ 0, from