Simplify if statement

Stream: general

[Abdullah Uyu]

How can I replace the have simp_if : ... with a rw, simp or anything natural really? I wrote that have statement with aesop's suggestion. simp alone does not simplify that if statement.

import Mathlib.Tactic

namespace simpifly_if

variable [DecidableEq G]

class ProjectiveGeometry
  (G : Type u) where
  ell : G → G → G → Prop
  l1  : ∀ a b, ell a b a
  l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
  l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : G, ell q a c ∧ ell q b d

theorem rel_sym_cab
  {G : Type u}
  {PG : ProjectiveGeometry G}
  (a b c : G)
  (abc_col : PG.ell a b c) :
    PG.ell c a b := by
  obtain rfl | bc_neq := eq_or_ne b c
  · apply PG.l1 b a
  · apply PG.l2 c a b c
    · apply PG.l1 c b
    · exact abc_col
    · exact bc_neq

theorem rel_sym_bca
  {G : Type u}
  {PG : ProjectiveGeometry G}
  (a b c : G)
  (abc_col : PG.ell a b c) :
    PG.ell b c a := by
  apply rel_sym_cab c a b
  apply rel_sym_cab a b c
  exact abc_col

def star
  {PG : ProjectiveGeometry G} :
    G → G → Set G :=
  fun a b => if a = b then {a} else {c | PG.ell a b c}

theorem p_2
  {PG : ProjectiveGeometry G} :
    ∀ a b, a ∈ star (PG := PG) b a := by
  intro a b
  unfold star
  obtain rfl | ab_neq := eq_or_ne a b
  · simp
  · have simp_if :
        PG.ell b a a → a ∈ (if b = a then {b} else {c | PG.ell b a c}) := by
      aesop
    apply simp_if
    apply rel_sym_bca a b a
    apply PG.l1 a b

[Kevin Buzzard]

split is the tactic which makes progress with if.

[Abdullah Uyu]

Thank you. That worked pretty well.

theorem p_2
  {PG : ProjectiveGeometry G} :
    ∀ a b, a ∈ star (PG := PG) b a := by
  intro a b
  unfold star
  obtain rfl | _ := eq_or_ne a b
  · simp
  · split
    case inr.inl eq =>
      rw [eq]
      simp
    case inr.inr _ =>
      simp
      apply rel_sym_bca a b a
      apply PG.l1 a b