α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (↑{ toFun := fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab,
            invFun := fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab,
            left_inv :=
              (_ :
                ∀ (x : α₁ × β₁),
                  (fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab)
                      ((fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : α₁ × β₁),
                  (fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab)
                      ((fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab) x) =
                    x) }
        ab).fst =
    ab.fst
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (↑(prodExtendRight a e) ab).fst = ab.fst
rw [prodExtendRight]
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (if ab.fst = a then (a, ↑e ab.snd) else ab).fst = ab.fst
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (↑{ toFun := fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab,
            invFun := fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab,
            left_inv :=
              (_ :
                ∀ (x : α₁ × β₁),
                  (fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab)
                      ((fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : α₁ × β₁),
                  (fun ab => if ab.fst = a then (a, ↑e ab.snd) else ab)
                      ((fun ab => if ab.fst = a then (a, ↑e.symm ab.snd) else ab) x) =
                    x) }
        ab).fst =
    ab.fst
dsimp
case inl
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ab.fst = a
⊢ (a, ↑e ab.snd).fst = ab.fst

case inr
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ¬ab.fst = a
⊢ ab.fst = ab.fst
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (if ab.fst = a then (a, ↑e ab.snd) else ab).fst = ab.fst
split_ifs with h
no goals
case inl
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ab.fst = a
⊢ (a, ↑e ab.snd).fst = ab.fst
rw [h]
no goals
case inr
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ¬ab.fst = a
⊢ ab.fst = ab.fst
rfl