unfold class

Stream: general

[blackxv]

hello everyone,
lemma Q2b : ¬is_total (set ℤ) (λ A B, A ⊆ B)
how to unfold is_total?
thank you in advance!

[Kevin Buzzard]

Does unfold is_total (in tactic mode) work?

[Alex J. Best]

is_total is a class, but you can do

lemma Q2b : ¬is_total (set ℤ) (λ A B, A ⊆ B) := begin
  intro h,
  cases h,
end

[Kevin Buzzard]

If not then try cases h if h : is_total ...

[blackxv]

cases h works, thank you!

lemma Q2b : ¬is_total (set ℤ) (λ A B, A ⊆ B) := begin
  intro h,
  cases h,
end

Are there some addional plugs to install in order to show lean code in a special style here?

ok yeah, ```works.

[Alex Peattie]

Code formatting is explained here: #backticks :smile: