tactic 'split' failed

Stream: new members

[Abdullah Uyu]

import Mathlib.Data.Set.Card

set_option trace.split.failure true

open Set

class ProjectiveGeometry
  (G : Type u)
  (ell : G → G → G → Prop) where
  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, ell q a c ∧ ell q b d

variable [DecidableEq G]
@[simp]
def star
  (ell : G → G → G → Prop)
  (a b : G) :
    Set G :=
  {c : G | if a = b then c = a else ell a b c}

class CentralProjectionQuadruple
  (ell : G → G → G → Prop)
  (a b c : G)
  (z : star ell a b) where
  abc_ncol : ¬ ell a b c
  az_neq : a ≠ z
  bz_neq : b ≠ z

def central_projection
  (a b c z : G)
  (ell : G → G → G → Prop)
  (x : star ell a c) :
    Set (star ell b c) :=
  Subtype.val ⁻¹' (star ell x z ∩ star ell b c)

theorem cen_proj_sing
  [PG : ProjectiveGeometry G ell]
  (a b c : G)
  (z : star ell a b)
  (x : star ell a c)
  (abc_ncol : ¬ ell a b c)
  (az_neq : a ≠ z)
  (bz_neq : b ≠ z) :
    ∃ y, central_projection a b c z ell x = {y} := by sorry

noncomputable def cen_proj_map
  [PG : ProjectiveGeometry G ell]
  (a b c : G)
  (z : star ell a b)
  [CPQ : CentralProjectionQuadruple ell a b c z]
  (x : star ell a c) :
    star ell b c :=
  Exists.choose (cen_proj_sing (PG := PG) a b c z x CPQ.abc_ncol CPQ.az_neq CPQ.bz_neq)

theorem p_6
  [ProjectiveGeometry G ell]
  (a b : G) :
    star ell a b = star ell b a := by sorry

instance cpq_symmetry
  [PG : ProjectiveGeometry G ell]
  [CPQ : CentralProjectionQuadruple ell a b c z] :
    have zp_sym :
        z.val ∈ star ell b a := by
      rw [<- p_6 (ell := ell) a b]
      exact z.property
    CentralProjectionQuadruple ell b a c ⟨z.val, zp_sym⟩ where
  abc_ncol := by sorry
  az_neq := by sorry
  bz_neq := by sorry

theorem cen_proj_bij
  [PG : ProjectiveGeometry G ell]
  [CPQ : CentralProjectionQuadruple ell a b c z] :
    Function.Bijective (cen_proj_map (ell := ell) a b c z) := by
  set φ := cen_proj_map a b c z
  have zp_sym :
      z.val ∈ star ell b a := by
    rw [<- p_6 (ell := ell) a b]
    exact z.property
  set ψ := (cen_proj_map b a c ⟨z, zp_sym⟩)
  rw [Function.bijective_iff_has_inverse]
  use ψ
  constructor
  · intro x
    set y := φ x
    have ψ_sing : ∃ y_1, central_projection b a c z ell y = {y_1} := by sorry
    unfold central_projection at ψ_sing
    choose y' yz_ac_inter using ψ_sing
    have ψ_eq_y' : ψ y = y' := by sorry
    have x_eq_y' : x = y' := by
      rw [<- Set.singleton_eq_singleton_iff]
      rw [<- yz_ac_inter]
      rw [Subset.antisymm_iff]
      constructor
      · simp
        constructor
        split
        -- tactic 'split' failed, consider using `set_option trace.split.failure true`
        · sorry
        · sorry
      · sorry
    sorry
  sorry

In line 100, why can't I split?

[Aaron Liu]

I don't get this error, but maybe you can try using split_ifs instead?

[Abdullah Uyu]

Well, it's splitting in online Lean, yes. Then maybe it's because my Lean is old, I will update it. But, to your suggestion: split_ifs adds h : b = c to context and leaves the goal unchanged.

[Abdullah Uyu]

Yep, that was because of an old version of Lean. Working fine now.

[Aaron Liu]

You can also use by_cases and docs#if_pos / docs#dif_pos and docs#if_neg / docs#dif_neg to split it.