Proof is symmetric. How to get rid of duplication?

Stream: new members

[Abdullah Uyu]

In the proof of the theorem cen_proj_bij, there is two parts, showing the existence of a left inverse, and then a right inverse. The second part is exactly the same as the first part, except that I swap x with y; a with b and z with ⟨z, zp_sym⟩.

import Mathlib.Data.Set.Card

open Set

namespace Basic

variable {G : Type*}
variable {ell : G → G → G → Prop}

theorem rel_sym_acb
  (a b c : G)
  (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)
  (abc_col : ell a b c) :
    ell a c b := by
  sorry

theorem rel_sym_cab
  (a b c : G)
  (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)
  (abc_col : ell a b c) :
    ell c a b := by
  sorry

theorem rel_sym_bca
  (a b c : G)
  (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)
  (abc_col : ell a b c) :
    ell b c a := by
  sorry

class ProjectiveGeometry
  (G : Type*)
  (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 [PG : ProjectiveGeometry G ell]

syntax "rel_sym" : tactic

macro_rules
| `(tactic| rel_sym) => `(tactic| first
  | assumption
  | apply rel_sym_acb _ _ _ PG.l1 PG.l2 <;> assumption
  | apply rel_sym_cab _ _ _ PG.l1 PG.l2 <;> assumption
  | apply rel_sym_bca _ _ _ PG.l1 PG.l2 <;> assumption
  | apply rel_sym_bac _ _ _ PG.l1 PG.l2 <;> assumption
  | apply rel_sym_cba _ _ _ PG.l1 PG.l2 <;> assumption)

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}

theorem p_5
  (a b c : G)
  (a_in_bc : a ∈ star ell b c) :
    star ell a b ⊆ star ell b c := by
  sorry

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

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

theorem star_nempty_and_neq_imp_sing
  (a b c d : G)
  (nempty : star ell a b ∩ star ell c d ≠ ∅)
  (neq : star ell a b ≠ star ell c d) :
    ∃ y, star ell a b ∩ star ell c d = {y} := by
  sorry

theorem abc_inter_sing
  (a b c : G)
  (abc_ncol : ¬ ell a b c) :
    star ell a b ∩ star ell a c = {a} := by
  sorry

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

variable (a b c : G)
variable (z : star ell a b)
variable [CPQ : CentralProjectionQuadruple a b c z]

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

theorem nin_arm :
    z.val ∉ star ell a c := by
  sorry

theorem nin_wall :
    z.val ∉ star ell c b := by
  sorry

variable (x : star ell a c)

theorem elbow_center_neq :
    x.val ≠ z.val := by
  sorry

theorem shadow_exists :
    star ell x.val z ∩ star ell c b ≠ ∅ := by
  sorry

theorem cen_proj_sing :
    ∃ y, central_projection a b c z x = {y} := by
  sorry

noncomputable def cen_proj_map :
    star ell b c :=
  Exists.choose (cen_proj_sing a b c z x)

theorem cen_proj_map_property :
    cen_proj_map a b c z x ∈ Subtype.val ⁻¹' star ell x z := by
  sorry

theorem cen_proj_arg_col :
    ell (cen_proj_map a b c z x) x z := by
  sorry
theorem shadow_in_light :
    (cen_proj_map a b c z x).val ∈ star ell x z := by
  sorry

theorem shadow_center_neq :
    (cen_proj_map a b c z x).val ≠ z.val := by
  sorry

theorem cen_proj_bij :
    Function.Bijective (cen_proj_map 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 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 y_in_xz : y.val ∈ star ell x z := by exact shadow_in_light a b c z x
    have ac_yz_inter_sing := by apply cen_proj_sing b a c ⟨z, zp_sym⟩ y
    have yz_neq : y.val ≠ z := by exact shadow_center_neq a b c z x
    unfold central_projection at ac_yz_inter_sing
    cases ac_yz_inter_sing with
    | intro yy yy_sing =>
      simp only [preimage] at yy_sing
      have x_in_yy : x ∈ ({yy} : Set _)  := by
        rw [<- yy_sing]
        simp
        split
        next yz_eq => exact False.elim (yz_neq yz_eq)
        next _ =>
          have yxz_col : ell y x z := by apply cen_proj_arg_col
          rel_sym
      have ψy_in_yy : ψ y ∈ ({yy} : Set _)  := by
        rw [<- yy_sing]
        simp
        split
        next yz_eq => exact False.elim (yz_neq yz_eq)
        next _=>
          have foo := by apply cen_proj_arg_col (ell := ell) b a c ⟨z, zp_sym⟩ y
          rel_sym
      have x_eq_yy : x = yy := by exact x_in_yy
      have ψy_eq_yy : ψ y = yy := by exact ψy_in_yy
      rw [<- x_eq_yy] at ψy_eq_yy
      exact ψy_eq_yy
  · intro y
    set x := ψ y
    have x_in_yz : x.val ∈ star ell y z := by exact shadow_in_light b a c ⟨z, zp_sym⟩ y
    have bc_xz_inter_sing := by apply cen_proj_sing a b c z x
    have xz_neq : x.val ≠ z := by exact shadow_center_neq b a c ⟨z, zp_sym⟩ y
    unfold central_projection at bc_xz_inter_sing
    cases bc_xz_inter_sing with
    | intro xx xx_sing =>
      simp only [preimage] at xx_sing
      have y_in_xx : y ∈ ({xx} : Set _)  := by
        rw [<- xx_sing]
        simp
        split
        next xz_eq => exact False.elim (xz_neq xz_eq)
        next _ =>
          have xyz_col : ell x y z := by apply cen_proj_arg_col b a c ⟨z, zp_sym⟩
          rel_sym
      have φx_in_xx : φ x ∈ ({xx} : Set _)  := by
        rw [<- xx_sing]
        simp
        split
        next xz_eq => exact False.elim (xz_neq xz_eq)
        next _=>
          have foo := by apply cen_proj_arg_col (ell := ell) a b c z x
          rel_sym
      have y_eq_xx : y = xx := by exact y_in_xx
      have φx_eq_xx : φ x = xx := by exact φx_in_xx
      rw [<- y_eq_xx] at φx_eq_xx
      exact φx_eq_xx

end Basic

I suspect there should be a way to avoid this duplication.

[Vlad]

Extract the first branch into a new theorem:

theorem cen_proj_left_inverse [PG : ProjectiveGeometry G ell]
  (a b c : G) (z : ↑(star ell a b)) [CPQ : CentralProjectionQuadruple a b c z] :
  let φ := cen_proj_map a b c z;
  ∀ (zp_sym : ↑z ∈ star ell b a),
  let ψ := cen_proj_map b a c ⟨↑z, zp_sym⟩;
  Function.LeftInverse ψ φ := by sorry

Then replace both branches with constructor <;> apply cen_proj_left_inverse in the main theorem.

[Abdullah Uyu]

Perfect, thank you!