prove goal for specific values

Stream: new members

[Alena Gusakov]

Is it possible to take a goal and split it into two cases, e.g. proving something for n = 0 in one way and proving the same thing for general n in another?

[Bryan Gin-ge Chen]

cases n or induction n?

[Alena Gusakov]

I mean it's a different proof completely for 0 vs other n

[Bryan Gin-ge Chen]

#mwe ?

[Alena Gusakov]

import algebra.group.basic
import data.real.basic

noncomputable theory
open_locale classical


def star_set := set.Ico (0:ℝ) 1

#check star_set


section star_group


#check has_coe_to_sort
#check semigroup

def star : ℝ → ℝ → ℝ
| x y := x + y - ⌊ x + y ⌋


notation x`⋆`y := star x y
variables (x y : ℝ) (A : Type*)

#check star_set


lemma star_inverses {a : ℝ} (ha : a ∈ star_set) : ∃ (b : ℝ), (a ⋆ b) = 0 ∧ b ∈ star_set :=
begin
    use (1 - a),
    split,
    unfold star,
    simp,
    unfold star_set,
    unfold star_set at ha,
    rw set.mem_Ico at ha,
    rw set.mem_Ico,
    cases ha with h0 h1,
    split,
end

end star_group

[Yakov Pechersky]

by_cases (n = 0)

[Alena Gusakov]

Ohh okay, that's exactly what I needed. Thank you!

[Bryan Gin-ge Chen]

(Note that the first and final ``` should be on their own lines for syntax highlighting to work properly.)

[Yakov Pechersky]

I guess cases or induction wouldn't work here due to working in \R