Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂