Zulip Chat Archive

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 add_mul,
    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: Aug 03 2023 at 10:10 UTC