How to solve a theorem with 'match'

Stream: lean4

[Hannah Santos]

I'm trying to prove that this relation is a congruence relation, but I got stuck on this part with the match. How can I proceed?

def iso (α β : Type) : Prop :=
  ∃ (f : α → β) (g : β → α), (∀ (b : β), (f ∘ g) b = b) ∧ (∀ (a : α), (g ∘ f) a = a)

def F : (α → α') → (β → β') → (Sum α β) → (Sum α' β')
  | f, _, (.inl a) => .inl (f a)
  | _, g, (.inr b) => .inr (g b)

def respects_sum : Prop :=
  ∀α α' β β', iso α α' ∧ iso β β' → iso (Sum α β) (Sum α' β')

theorem sum:
  respects_sum :=
by
  intro α α' β β' h
  apply (h.1).elim
  intro fa h'
  apply h'.elim
  intro ga hfga
  apply (h.2).elim
  intro fb h''
  apply h''.elim
  intro gb hfgb
  apply Exists.intro (F fa fb)
  apply Exists.intro (F ga gb)
  apply And.intro
  intro ab'
  rw [Function.comp, F, F]
  cases ab'
  · case Sum.inl a' =>
  · case Sum.inr b' =>

/-
Tactic state
3 goals
case left.inl
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
val✝ : α'
⊢ (match fa, fb,
    match ga, gb, Sum.inl val✝ with
    | f, x, Sum.inl a => Sum.inl (f a)
    | x, g, Sum.inr b => Sum.inr (g b) with
  | f, x, Sum.inl a => Sum.inl (f a)
  | x, g, Sum.inr b => Sum.inr (g b)) =
  Sum.inl val✝
case left.inr
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
val✝ : β'
⊢ (match fa, fb,
    match ga, gb, Sum.inr val✝ with
    | f, x, Sum.inl a => Sum.inl (f a)
    | x, g, Sum.inr b => Sum.inr (g b) with
  | f, x, Sum.inl a => Sum.inl (f a)
  | x, g, Sum.inr b => Sum.inr (g b)) =
  Sum.inr val✝
case right
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
⊢ ∀ (a : α ⊕ β), (F ga gb ∘ F fa fb) a = a
Expected type
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
ab' : α' ⊕ β'
⊢ α' ⊕ β'
Messages (1)
Help.lean:13:0
unsolved goals
case left.inr
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
val✝ : β'
⊢ (match fa, fb,
    match ga, gb, Sum.inr val✝ with
    | f, x, Sum.inl a => Sum.inl (f a)
    | x, g, Sum.inr b => Sum.inr (g b) with
  | f, x, Sum.inl a => Sum.inl (f a)
  | x, g, Sum.inr b => Sum.inr (g b)) =
  Sum.inr val✝


case right
α α' β β' : Type
h : iso α α' ∧ iso β β'
fa : α → α'
h' : ∃ g, (∀ (b : α'), (fa ∘ g) b = b) ∧ ∀ (a : α), (g ∘ fa) a = a
ga : α' → α
hfga : (∀ (b : α'), (fa ∘ ga) b = b) ∧ ∀ (a : α), (ga ∘ fa) a = a
fb : β → β'
h'' : ∃ g, (∀ (b : β'), (fb ∘ g) b = b) ∧ ∀ (a : β), (g ∘ fb) a = a
gb : β' → β
hfgb : (∀ (b : β'), (fb ∘ gb) b = b) ∧ ∀ (a : β), (gb ∘ fb) a = a
⊢ ∀ (a : α ⊕ β), (F ga gb ∘ F fa fb) a = a
All Messages (2)
-/

[Adam Topaz]

dsimp might get rid of the match, if you case split enough ahead of time (at least for the goal with the match in the comments you mentioned, it looks like it has already been split up enough)
... here's a much shorter solution (behind a spoiler, in case you're doing this as an exercise).

def iso (α β : Type) : Prop :=
  ∃ (f : α → β) (g : β → α), (∀ (b : β), (f ∘ g) b = b) ∧ (∀ (a : α), (g ∘ f) a = a)

def F : (α → α') → (β → β') → (Sum α β) → (Sum α' β')
  | f, _, (.inl a) => .inl (f a)
  | _, g, (.inr b) => .inr (g b)

def respects_sum : Prop :=
  ∀α α' β β', iso α α' ∧ iso β β' → iso (Sum α β) (Sum α' β')

theorem sum : respects_sum := by
  rintro α α' β β' ⟨⟨f,g,hf1,hf2⟩,⟨f',g',hg1,hg2⟩⟩
  refine ⟨F f f', F g g', ?_, ?_⟩
  · rintro (a|a)
    · simpa [F] using hf1 a
    · simpa [F] using hg1 a
  · rintro (a|a)
    · simpa [F] using hf2 a
    · simpa [F] using hg2 a

[Hannah Santos]

Wow, so many things I hadn't seen before. :open_mouth:

[Hannah Santos]

It's kind of an exercise, but I can write the proof on paper, I'm just trying to translate it to lean, so it's a bit of a syntax problem.

[Hannah Santos]

Anyway, thank you, that helps, I'll study these tactics a bit to understand them.

[Adam Topaz]

No problem. By the way, it may be easier to phrase iso rather as

def iso (α β : Type) : Prop :=
  ∃ (f : α → β) (g : β → α), (∀ (b : β), f (g b) = b) ∧ (∀ (a : α), g (f a) = a)

[Kyle Miller]

Adam's proof can be shortened using <;> (though it's not clearer using it!)

theorem sum : respects_sum := by
  rintro α α' β β' ⟨⟨f,g,hf1,hf2⟩, ⟨f',g',hg1,hg2⟩⟩
  dsimp only [Function.comp] at *
  refine ⟨F f f', F g g', ?_, ?_⟩
    <;> rintro (a|a) <;> simp [*,F]

[Kyle Miller]

Here's handling the point you got to in your original code:

def respects_sum : Prop :=
  ∀α α' β β', iso α α' ∧ iso β β' → iso (Sum α β) (Sum α' β')
theorem sum:
  respects_sum :=
by
  intro α α' β β' h
  apply (h.1).elim
  intro fa h'
  apply h'.elim
  intro ga hfga
  apply (h.2).elim
  intro fb h''
  apply h''.elim
  intro gb hfgb
  apply Exists.intro (F fa fb)
  apply Exists.intro (F ga gb)
  apply And.intro
  intro ab'
  rw [Function.comp]
  unfold F -- had to switch to this in a newer version of Lean
  cases ab' with
  | inl a' => simp; apply hfga.1
  | inr b' => simp; apply hfgb.1
  sorry

[Kyle Miller]

There was something a bit wrong with the cases syntax, with putting each case in a focus dot, but I switched it over to using the cases ... with | ... syntax.

[Hannah Santos]

I put the dot from something else I read, I'll switch it up right away, thank you.

[Hannah Santos]

Thank you for your pointers, guys. I've mixed and matched, basically, what you said and I wrote something that I understood.

def iso (α β : Type) : Prop :=
  ∃ (f : α → β) (g : β → α), (∀ (b : β), (f ∘ g) b = b) ∧ (∀ (a : α), (g ∘ f) a = a)

def F : (α → α') → (β → β') → (Sum α β) → (Sum α' β')
  | f, _, (.inl a) => .inl (f a)
  | _, g, (.inr b) => .inr (g b)

def respects_sum : Prop :=
  ∀α α' β β', iso α α' ∧ iso β β' → iso (Sum α β) (Sum α' β')

theorem comp_def {α β γ: Type}:
  ∀ (f : α → β) (g : β → γ), ∀ (a : α), (g ∘ f) a = g (f a) :=
by
  intro f g a
  rw [Function.comp]

theorem sum :
  respects_sum :=
by
  intro α α' β β' ⟨⟨fa, fa', ha⟩,⟨gb, gb', hb⟩⟩
  refine ⟨F fa gb, F fa' gb', ?_, ?_⟩
  intro ab'
  unfold F
  cases ab' with
  | inl a' => simp; rw [← comp_def fa' fa, ha.1]
  | inr b' => simp; rw [← comp_def gb' gb, hb.1]
  intro ab
  unfold F
  cases ab with
  | inl a => simp; rw [← comp_def fa fa', ha.2]
  | inr b => simp; rw [← comp_def gb gb', hb.2]