## Stream: general

### Topic: They're the same picture

#### Bolton Bailey (Mar 23 2022 at 18:21):

What is the difference between the following two tactic states, one of which is resolved by abel, and the other or which is not. They pretty-print the same, set_option pp.all true tells me they are different, yet inspecting the types in the infoview tells me they are all the same.

import data.fintype.basic
import group_theory.order_of_element
import tactic.zify

-- set_option pp.all true

example (p a : ℕ) : (((p ^ a * p) : ℕ) : ℤ) - ((1 : ℕ) : ℤ) = (((p ^ a * p) : ℕ) : ℤ) - (((p ^ a) : ℕ) : ℤ) + ((((p ^ a) : ℕ) : ℤ) - ((1 : ℕ) : ℤ)) :=
begin
abel,
-- goals accomplished
end

lemma sub_one_dvd_pow_sub_one (p α : ℕ) (one_le_p : 1 ≤ p) : (p - 1) ∣ (p^α - 1) :=
begin
induction α with a ih,
{ simp, },
{ rw dvd_iff_exists_eq_mul_left at *,
rcases ih with ⟨c, hc⟩,
use p^a + c,
rw ← hc,
rw mul_tsub,
rw mul_one,
zify,
rw int.coe_nat_sub (one_le_pow_of_one_le one_le_p a),
rw int.coe_nat_sub (le_mul_of_one_le_right' one_le_p),
rw int.coe_nat_sub (one_le_pow_of_one_le one_le_p (nat.succ a)),
rw pow_succ',
clear hc c one_le_p,
abel,
-- (-1) • ↑1 + ↑(p ^ a * p) = (-1) • ↑(p ^ a) + ((-1) • ↑1 + (↑(p ^ a) + ↑(p ^ a * p)))
},
end


#### Eric Rodriguez (Mar 23 2022 at 18:25):

norm_cast, abel solves it. my intuition says it's to do with the coerced ones, but not sure.

Last updated: Dec 20 2023 at 11:08 UTC