[GOAL]
α : Sort ?u.394
β : Sort ?u.393
γ : Sort ?u.398
δ : Sort ?u.397
e₁ : α ≃ β
e₂ : γ ≃ δ
x✝ : PProd α γ
x : α
y : γ
⊢ (fun x => { fst := ↑e₁.symm x.fst, snd := ↑e₂.symm x.snd })
      ((fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd }) { fst := x, snd := y }) =
    { fst := x, snd := y }
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.394
β : Sort ?u.393
γ : Sort ?u.398
δ : Sort ?u.397
e₁ : α ≃ β
e₂ : γ ≃ δ
x✝ : PProd β δ
x : β
y : δ
⊢ (fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd })
      ((fun x => { fst := ↑e₁.symm x.fst, snd := ↑e₂.symm x.snd }) { fst := x, snd := y }) =
    { fst := x, snd := y }
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.3831
α₂ : Type ?u.3833
β₁ : Type ?u.3830
β₂ : Type ?u.3832
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x✝ : α₁ × β₁
a : α₁
b : β₁
⊢ Prod.map (↑e₁.symm) (↑e₂.symm) (Prod.map ↑e₁ ↑e₂ (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.3831
α₂ : Type ?u.3833
β₁ : Type ?u.3830
β₂ : Type ?u.3832
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x✝ : α₂ × β₂
a : α₂
b : β₂
⊢ Prod.map (↑e₁) (↑e₂) (Prod.map ↑e₁.symm ↑e₂.symm (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.12786
β : Type ?u.12785
s : α ⊕' β
⊢ Sum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) s) = s
[PROOFSTEP]
cases s
[GOAL]
case inl
α : Type ?u.12786
β : Type ?u.12785
val✝ : α
⊢ Sum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.12786
β : Type ?u.12785
val✝ : β
⊢ Sum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.12786
β : Type ?u.12785
s : α ⊕ β
⊢ (fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = s
[PROOFSTEP]
cases s
[GOAL]
case inl
α : Type ?u.12786
β : Type ?u.12785
val✝ : α
⊢ (fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.12786
β : Type ?u.12785
val✝ : β
⊢ (fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
α₁ : Type ?u.13193
α₂ : Type ?u.13195
β₁ : Type ?u.13192
β₂ : Type ?u.13194
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₁ ⊕ β₁
⊢ Sum.map (↑ea.symm) (↑eb.symm) (Sum.map (↑ea) (↑eb) x) = x
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.13193
α₂ : Type ?u.13195
β₁ : Type ?u.13192
β₂ : Type ?u.13194
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
x : α₂ ⊕ β₂
⊢ Sum.map (↑ea) (↑eb) (Sum.map (↑ea.symm) (↑eb.symm) x) = x
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
    PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
x : α
⊢ (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
      ((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inl x)) =
    PSum.inl x
[PROOFSTEP]
simp
[GOAL]
case inr
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
x : γ
⊢ (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
      ((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inr x)) =
    PSum.inr x
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ Function.RightInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
    PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
x : β
⊢ (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
      ((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inl x)) =
    PSum.inl x
[PROOFSTEP]
simp
[GOAL]
case inr
α : Sort ?u.14682
β : Sort ?u.14681
γ : Sort ?u.14686
δ : Sort ?u.14685
e₁ : α ≃ β
e₂ : γ ≃ δ
x : δ
⊢ (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
      ((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inr x)) =
    PSum.inr x
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)
[PROOFSTEP]
ext i
[GOAL]
case H
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) i
[PROOFSTEP]
cases i
[GOAL]
case H.inl
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₁
⊢ ↑((sumCongr e f).trans (sumCongr g h)) (inl val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case H.inr
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
val✝ : α₂
⊢ ↑((sumCongr e f).trans (sumCongr g h)) (inr val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
⊢ sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
[PROOFSTEP]
ext i
[GOAL]
case H
α : Type u_1
β : Type u_2
i : α ⊕ β
⊢ ↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) i
[PROOFSTEP]
cases i
[GOAL]
case H.inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ ↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inl val✝) = ↑(Equiv.refl (α ⊕ β)) (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ ↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inr val✝) = ↑(Equiv.refl (α ⊕ β)) (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
⊢ LeftInverse
    (fun c =>
      match c with
      | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
      | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
    fun c =>
    match h : ↑c with
    | inl a => inl { val := a, property := (_ : p (inl a)) }
    | inr b => inr { val := b, property := (_ : p (inr b)) }
[PROOFSTEP]
rintro ⟨a | b, h⟩
[GOAL]
case mk.inl
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
a : α
h : p (inl a)
⊢ (fun c =>
        match c with
        | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
        | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
      ((fun c =>
          match h : ↑c with
          | inl a => inl { val := a, property := (_ : p (inl a)) }
          | inr b => inr { val := b, property := (_ : p (inr b)) })
        { val := inl a, property := h }) =
    { val := inl a, property := h }
[PROOFSTEP]
rfl
[GOAL]
case mk.inr
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
b : β
h : p (inr b)
⊢ (fun c =>
        match c with
        | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
        | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
      ((fun c =>
          match h : ↑c with
          | inl a => inl { val := a, property := (_ : p (inl a)) }
          | inr b => inr { val := b, property := (_ : p (inr b)) })
        { val := inr b, property := h }) =
    { val := inr b, property := h }
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
⊢ Function.RightInverse
    (fun c =>
      match c with
      | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
      | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
    fun c =>
    match h : ↑c with
    | inl a => inl { val := a, property := (_ : p (inl a)) }
    | inr b => inr { val := b, property := (_ : p (inr b)) }
[PROOFSTEP]
rintro (a | b)
[GOAL]
case inl
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
a : { a // p (inl a) }
⊢ (fun c =>
        match h : ↑c with
        | inl a => inl { val := a, property := (_ : p (inl a)) }
        | inr b => inr { val := b, property := (_ : p (inr b)) })
      ((fun c =>
          match c with
          | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
          | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
        (inl a)) =
    inl a
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.20147
β : Type ?u.20146
p : α ⊕ β → Prop
b : { b // p (inr b) }
⊢ (fun c =>
        match h : ↑c with
        | inl a => inl { val := a, property := (_ : p (inl a)) }
        | inr b => inr { val := b, property := (_ : p (inr b)) })
      ((fun c =>
          match c with
          | inl a => { val := inl ↑a, property := (_ : p (inl ↑a)) }
          | inr b => { val := inr ↑b, property := (_ : p (inr ↑b)) })
        (inr b)) =
    inr b
[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ Sum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ Sum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ Sum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) true) = true
[PROOFSTEP]
rfl
[GOAL]
s : PUnit ⊕ PUnit
⊢ (fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) s) = s
[PROOFSTEP]
rcases s with (⟨⟨⟩⟩ | ⟨⟨⟩⟩)
[GOAL]
case inl.unit
⊢ (fun b => bif b then inr PUnit.unit else inl PUnit.unit)
      (Sum.elim (fun x => false) (fun x => true) (inl PUnit.unit)) =
    inl PUnit.unit
[PROOFSTEP]
rfl
[GOAL]
case inr.unit
⊢ (fun b => bif b then inr PUnit.unit else inl PUnit.unit)
      (Sum.elim (fun x => false) (fun x => true) (inr PUnit.unit)) =
    inr PUnit.unit
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
⊢ LeftInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))
[PROOFSTEP]
rintro (⟨_ | _⟩ | _)
[GOAL]
case inl.inl
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : α
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =
    inl (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : β
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =
    inl (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : γ
⊢ Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) =
    inr val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
⊢ Function.RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr))
    (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))
[PROOFSTEP]
rintro (_ | ⟨_ | _⟩)
[GOAL]
case inl
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : α
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val✝)) =
    inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : β
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val✝))) =
    inr (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α : Type ?u.22761
β : Type ?u.22760
γ : Type ?u.22758
val✝ : γ
⊢ Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inr val✝))) =
    inr (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.24508
β : Type ?u.24507
inst✝ : IsEmpty β
s : α ⊕ β
⊢ inl (Sum.elim id (fun a => isEmptyElim a) s) = s
[PROOFSTEP]
rcases s with (_ | x)
[GOAL]
case inl
α : Type ?u.24508
β : Type ?u.24507
inst✝ : IsEmpty β
val✝ : α
⊢ inl (Sum.elim id (fun a => isEmptyElim a) (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.24508
β : Type ?u.24507
inst✝ : IsEmpty β
x : β
⊢ inl (Sum.elim id (fun a => isEmptyElim a) (inr x)) = inr x
[PROOFSTEP]
exact isEmptyElim x
[GOAL]
α : Type ?u.25254
o : Option α
⊢ (fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) o) = o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type ?u.25254
⊢ (fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) none) = none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type ?u.25254
val✝ : α
⊢ (fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) (some val✝)) = some val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.25254
s : α ⊕ PUnit
⊢ (fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) s) = s
[PROOFSTEP]
rcases s with (_ | ⟨⟨⟩⟩)
[GOAL]
case inl
α : Type ?u.25254
val✝ : α
⊢ (fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.unit
α : Type ?u.25254
⊢ (fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inr PUnit.unit)) =
    inr PUnit.unit
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.27010
β : Option α → Type u_1
f : (a : Option α) → β a
a : Option α
⊢ (fun x a => Option.casesOn a x.fst x.snd) ((fun f => (f none, fun a => f (some a))) f) a = f a
[PROOFSTEP]
cases a
[GOAL]
case none
α : Type ?u.27010
β : Option α → Type u_1
f : (a : Option α) → β a
⊢ (fun x a => Option.casesOn a x.fst x.snd) ((fun f => (f none, fun a => f (some a))) f) none = f none
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type ?u.27010
β : Option α → Type u_1
f : (a : Option α) → β a
val✝ : α
⊢ (fun x a => Option.casesOn a x.fst x.snd) ((fun f => (f none, fun a => f (some a))) f) (some val✝) = f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.27010
β : Option α → Type u_1
x : β none × ((a : α) → β (some a))
⊢ (fun f => (f none, fun a => f (some a))) ((fun x a => Option.casesOn a x.fst x.snd) x) = x
[PROOFSTEP]
simp
[GOAL]
α β : Type u
s : α ⊕ β
⊢ (fun s =>
        match s with
        | { fst := true, snd := a } => inl a
        | { fst := false, snd := b } => inr b)
      ((fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s) s) =
    s
[PROOFSTEP]
cases s
[GOAL]
case inl
α β : Type u
val✝ : α
⊢ (fun s =>
        match s with
        | { fst := true, snd := a } => inl a
        | { fst := false, snd := b } => inr b)
      ((fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s) (inl val✝)) =
    inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β : Type u
val✝ : β
⊢ (fun s =>
        match s with
        | { fst := true, snd := a } => inl a
        | { fst := false, snd := b } => inr b)
      ((fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s) (inr val✝)) =
    inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β : Type u
s : (b : Bool) × bif b then α else β
⊢ (fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s)
      ((fun s =>
          match s with
          | { fst := true, snd := a } => inl a
          | { fst := false, snd := b } => inr b)
        s) =
    s
[PROOFSTEP]
rcases s with ⟨_ | _, _⟩
[GOAL]
case mk.false
α β : Type u
snd✝ : bif false then α else β
⊢ (fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s)
      ((fun s =>
          match s with
          | { fst := true, snd := a } => inl a
          | { fst := false, snd := b } => inr b)
        { fst := false, snd := snd✝ }) =
    { fst := false, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
case mk.true
α β : Type u
snd✝ : bif true then α else β
⊢ (fun s => Sum.elim (fun x => { fst := true, snd := x }) (fun x => { fst := false, snd := x }) s)
      ((fun s =>
          match s with
          | { fst := true, snd := a } => inl a
          | { fst := false, snd := b } => inr b)
        { fst := true, snd := snd✝ }) =
    { fst := true, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
⊢ LeftInverse (fun a => if h : p a then Sum.inl { val := a, property := h } else Sum.inr { val := a, property := h })
    (Sum.elim Subtype.val Subtype.val)
[PROOFSTEP]
rintro (⟨x, hx⟩ | ⟨x, hx⟩)
[GOAL]
case inl.mk
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (fun a => if h : p a then Sum.inl { val := a, property := h } else Sum.inr { val := a, property := h })
      (Sum.elim Subtype.val Subtype.val (Sum.inl { val := x, property := hx })) =
    Sum.inl { val := x, property := hx }
[PROOFSTEP]
dsimp
[GOAL]
case inr.mk
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (fun a => if h : p a then Sum.inl { val := a, property := h } else Sum.inr { val := a, property := h })
      (Sum.elim Subtype.val Subtype.val (Sum.inr { val := x, property := hx })) =
    Sum.inr { val := x, property := hx }
[PROOFSTEP]
dsimp
[GOAL]
case inl.mk
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : p x
⊢ (if h : p x then Sum.inl { val := x, property := h } else Sum.inr { val := x, property := h }) =
    Sum.inl { val := x, property := hx }
[PROOFSTEP]
rw [dif_pos]
[GOAL]
case inr.mk
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (if h : p x then Sum.inl { val := x, property := h } else Sum.inr { val := x, property := h }) =
    Sum.inr { val := x, property := hx }
[PROOFSTEP]
rw [dif_neg]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val
      ((fun a => if h : p a then Sum.inl { val := a, property := h } else Sum.inr { val := a, property := h }) a) =
    a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ Sum.elim Subtype.val Subtype.val
      (if h : p a then Sum.inl { val := a, property := h } else Sum.inr { val := a, property := h }) =
    a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inl { val := a, property := h✝ }) = a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
h✝ : ¬p a
⊢ Sum.elim Subtype.val Subtype.val (Sum.inr { val := a, property := h✝ }) = a
[PROOFSTEP]
rfl
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
⊢ ↑(subtypeCongr ep en) a = if h : p a then ↑(↑ep { val := a, property := h }) else ↑(↑en { val := a, property := h })
[PROOFSTEP]
by_cases h : p a
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
h : p a
⊢ ↑(subtypeCongr ep en) a = if h : p a then ↑(↑ep { val := a, property := h }) else ↑(↑en { val := a, property := h })
[PROOFSTEP]
simp [Perm.subtypeCongr, h]
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ ↑(subtypeCongr ep en) a = if h : p a then ↑(↑ep { val := a, property := h }) else ↑(↑en { val := a, property := h })
[PROOFSTEP]
simp [Perm.subtypeCongr, h]
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
h : p a
⊢ ↑(subtypeCongr ep en) a = ↑(↑ep { val := a, property := h })
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h]
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ ↑(subtypeCongr ep en) a = ↑(↑en { val := a, property := h })
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h]
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε
[PROOFSTEP]
ext x
[GOAL]
case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = ↑(Equiv.refl ε) x
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ ↑(subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = ↑(Equiv.refl ε) x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ ↑(subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = ↑(Equiv.refl ε) x
[PROOFSTEP]
simp [h]
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ (subtypeCongr ep en).symm = subtypeCongr ep.symm en.symm
[PROOFSTEP]
ext x
[GOAL]
case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
[PROOFSTEP]
have : p (ep.symm ⟨x, h⟩) := Subtype.property _
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(↑ep.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
[PROOFSTEP]
have : ¬p (en.symm ⟨x, h⟩) := Subtype.property (en.symm _)
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(↑en.symm { val := x, property := h })
⊢ ↑(subtypeCongr ep en).symm x = ↑(subtypeCongr ep.symm en.symm) x
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]
[GOAL]
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
⊢ (subtypeCongr ep en).trans (subtypeCongr ep' en') = subtypeCongr (ep.trans ep') (en.trans en')
[PROOFSTEP]
ext x
[GOAL]
case H
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
[PROOFSTEP]
have : p (ep ⟨x, h⟩) := Subtype.property _
[GOAL]
case pos
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑(↑ep { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h, this]
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
[PROOFSTEP]
have : ¬p (en ⟨x, h⟩) := Subtype.property (en _)
[GOAL]
case neg
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑(↑en { val := x, property := h })
⊢ ↑((subtypeCongr ep en).trans (subtypeCongr ep' en')) x = ↑(subtypeCongr (ep.trans ep') (en.trans en')) x
[PROOFSTEP]
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]
[GOAL]
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ ↑((fun x =>
            { val := fun a => if h : p a then x₀ { val := a, property := h } else x { val := a, property := h },
              property :=
                (_ :
                  (fun a => if h : p a then x₀ { val := a, property := h } else x { val := a, property := h }) ∘
                      Subtype.val =
                    x₀) })
          ((fun x a => ↑x ↑a) { val := x, property := hx }))
      a =
    ↑{ val := x, property := hx } a
[PROOFSTEP]
dsimp only
[GOAL]
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
⊢ (if h : p a then x₀ { val := a, property := h } else x a) = x a
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ x₀ { val := a, property := h✝ } = x a
[PROOFSTEP]
rw [← hx]
[GOAL]
case pos
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ (x ∘ Subtype.val) { val := a, property := h✝ } = x a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : ¬p a
⊢ x a = x a
[PROOFSTEP]
rfl
[GOAL]
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h_1 : p a then (fun h_2 => x₀ { val := ↑{ val := a, property := h }, property := h_2 }) h_1
    else (fun h_2 => x { val := ↑{ val := a, property := h }, property := h_2 }) h_1) =
    x { val := a, property := h }
[PROOFSTEP]
dsimp only
[GOAL]
α : Sort ?u.40681
β : Sort ?u.40703
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x : { a // ¬p a } → β
x✝ : { a // ¬p a }
a : α
h : ¬p a
⊢ (if h : p a then x₀ { val := a, property := h } else x { val := a, property := h }) = x { val := a, property := h }
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
α : Sort ?u.43789
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₁ a
⊢ ∀ (x : α), (fun H a => ↑(F a).symm (H a)) ((fun H a => ↑(F a) (H a)) H) x = H x
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.43789
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₂ a
⊢ ∀ (x : α), (fun H a => ↑(F a) (H a)) ((fun H a => ↑(F a).symm (H a)) H) x = H x
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.45975
β₁ : Type ?u.45976
β₂ : Type ?u.45978
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab => (↑(e ab.snd).symm ab.fst, ab.snd)) fun ab => (↑(e ab.snd) ab.fst, ab.snd)
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α₁ : Type ?u.45975
β₁ : Type ?u.45976
β₂ : Type ?u.45978
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ (fun ab => (↑(e ab.snd).symm ab.fst, ab.snd)) ((fun ab => (↑(e ab.snd) ab.fst, ab.snd)) (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.45975
β₁ : Type ?u.45976
β₂ : Type ?u.45978
e : α₁ → β₁ ≃ β₂
⊢ Function.RightInverse (fun ab => (↑(e ab.snd).symm ab.fst, ab.snd)) fun ab => (↑(e ab.snd) ab.fst, ab.snd)
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α₁ : Type ?u.45975
β₁ : Type ?u.45976
β₂ : Type ?u.45978
e : α₁ → β₁ ≃ β₂
a : β₂
b : α₁
⊢ (fun ab => (↑(e ab.snd) ab.fst, ab.snd)) ((fun ab => (↑(e ab.snd).symm ab.fst, ab.snd)) (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_3
β₁ : Type u_1
β₂ : Type u_2
e✝ : α₁ → β₁ ≃ β₂
e : β₁ ≃ β₂
⊢ prodCongr e (Equiv.refl α₁) = prodCongrLeft fun x => e
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_3
β₁ : Type u_1
β₂ : Type u_2
e✝ : α₁ → β₁ ≃ β₂
e : β₁ ≃ β₂
a : β₁
b : α₁
⊢ ↑(prodCongr e (Equiv.refl α₁)) (a, b) = ↑(prodCongrLeft fun x => e) (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.47651
β₁ : Type ?u.47650
β₂ : Type ?u.47652
e : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun ab => (ab.fst, ↑(e ab.fst).symm ab.snd)) fun ab => (ab.fst, ↑(e ab.fst) ab.snd)
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α₁ : Type ?u.47651
β₁ : Type ?u.47650
β₂ : Type ?u.47652
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ (fun ab => (ab.fst, ↑(e ab.fst).symm ab.snd)) ((fun ab => (ab.fst, ↑(e ab.fst) ab.snd)) (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.47651
β₁ : Type ?u.47650
β₂ : Type ?u.47652
e : α₁ → β₁ ≃ β₂
⊢ Function.RightInverse (fun ab => (ab.fst, ↑(e ab.fst).symm ab.snd)) fun ab => (ab.fst, ↑(e ab.fst) ab.snd)
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α₁ : Type ?u.47651
β₁ : Type ?u.47650
β₂ : Type ?u.47652
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₂
⊢ (fun ab => (ab.fst, ↑(e ab.fst) ab.snd)) ((fun ab => (ab.fst, ↑(e ab.fst).symm ab.snd)) (a, b)) = (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_3
β₁ : Type u_1
β₂ : Type u_2
e✝ : α₁ → β₁ ≃ β₂
e : β₁ ≃ β₂
⊢ prodCongr (Equiv.refl α₁) e = prodCongrRight fun x => e
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_3
β₁ : Type u_1
β₂ : Type u_2
e✝ : α₁ → β₁ ≃ β₂
e : β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑(prodCongr (Equiv.refl α₁) e) (a, b) = ↑(prodCongrRight fun x => e) (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ ↑((prodCongrLeft e).trans (prodComm β₂ α₁)) (a, b) = ↑((prodComm β₁ α₁).trans (prodCongrRight e)) (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_3
β₁ : Type u_2
β₂ : Type u_1
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ↑((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
e : α₁ → β₁ ≃ β₂
⊢ (sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂) = (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑((sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)) { fst := a, snd := b } =
    ↑((sigmaEquivProd α₁ β₁).trans (prodCongrRight e)) { fst := a, snd := b }
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
e : α₁ → β₁ ≃ β₂
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm
[PROOFSTEP]
ext ⟨a, b⟩ : 1
[GOAL]
case H.mk
α₁ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ↑((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) =
    ↑((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)
[PROOFSTEP]
simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]
[GOAL]
case H.mk
α₁ : Type u_1
β₁ : Type u_2
β₂ : Type u_3
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ { fst := (↑(sigmaEquivProd α₁ β₁).symm (a, b)).fst,
      snd := ↑(e (↑(sigmaEquivProd α₁ β₁).symm (a, b)).fst) (↑(sigmaEquivProd α₁ β₁).symm (a, b)).snd } =
    ↑(sigmaEquivProd α₁ β₂).symm (a, ↑(e a) b)
[PROOFSTEP]
rfl
[GOAL]
α₁ : Type ?u.53326
β₁ : Type ?u.53325
β₂ : Type ?u.53327
e : α₁ → β₁ ≃ β₂
α₂ : Type ?u.53328
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ LeftInverse (fun y => (↑e₁.symm y.fst, ↑(e₂ (↑e₁.symm y.fst)).symm y.snd)) fun x => (↑e₁ x.fst, ↑(e₂ x.fst) x.snd)
[PROOFSTEP]
rintro ⟨x₁, y₁⟩
[GOAL]
case mk
α₁ : Type ?u.53326
β₁ : Type ?u.53325
β₂ : Type ?u.53327
e : α₁ → β₁ ≃ β₂
α₂ : Type ?u.53328
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
x₁ : α₁
y₁ : β₁
⊢ (fun y => (↑e₁.symm y.fst, ↑(e₂ (↑e₁.symm y.fst)).symm y.snd)) ((fun x => (↑e₁ x.fst, ↑(e₂ x.fst) x.snd)) (x₁, y₁)) =
    (x₁, y₁)
[PROOFSTEP]
simp only [symm_apply_apply]
[GOAL]
α₁ : Type ?u.53326
β₁ : Type ?u.53325
β₂ : Type ?u.53327
e : α₁ → β₁ ≃ β₂
α₂ : Type ?u.53328
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ Function.RightInverse (fun y => (↑e₁.symm y.fst, ↑(e₂ (↑e₁.symm y.fst)).symm y.snd)) fun x =>
    (↑e₁ x.fst, ↑(e₂ x.fst) x.snd)
[PROOFSTEP]
rintro ⟨x₁, y₁⟩
[GOAL]
case mk
α₁ : Type ?u.53326
β₁ : Type ?u.53325
β₂ : Type ?u.53327
e : α₁ → β₁ ≃ β₂
α₂ : Type ?u.53328
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
x₁ : α₂
y₁ : β₂
⊢ (fun x => (↑e₁ x.fst, ↑(e₂ x.fst) x.snd)) ((fun y => (↑e₁.symm y.fst, ↑(e₂ (↑e₁.symm y.fst)).symm y.snd)) (x₁, y₁)) =
    (x₁, y₁)
[PROOFSTEP]
simp only [apply_symm_apply]
[GOAL]
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ LeftInverse (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
[PROOFSTEP]
rintro ⟨k', x⟩
[GOAL]
case mk
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
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) (k', x)) =
    (k', x)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
⊢ (if (if k' = a then (a, ↑e x) else (k', x)).fst = a then (a, ↑e.symm (if k' = a then (a, ↑e x) else (k', x)).snd)
    else if k' = a then (a, ↑e x) else (k', x)) =
    (k', x)
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : k' = a
h₂ : (a, ↑e x).fst = a
⊢ (a, ↑e.symm (a, ↑e x).snd) = (k', x)
[PROOFSTEP]
simp [h₁]
[GOAL]
case neg
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : k' = a
h₂ : ¬(a, ↑e x).fst = a
⊢ (a, ↑e x) = (k', x)
[PROOFSTEP]
simp at h₂
[GOAL]
case neg
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : ¬k' = a
⊢ (k', x) = (k', x)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ Function.RightInverse (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
[PROOFSTEP]
rintro ⟨k', x⟩
[GOAL]
case mk
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
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) (k', x)) =
    (k', x)
[PROOFSTEP]
dsimp only
[GOAL]
case mk
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
⊢ (if (if k' = a then (a, ↑e.symm x) else (k', x)).fst = a then (a, ↑e (if k' = a then (a, ↑e.symm x) else (k', x)).snd)
    else if k' = a then (a, ↑e.symm x) else (k', x)) =
    (k', x)
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : k' = a
h₂ : (a, ↑e.symm x).fst = a
⊢ (a, ↑e (a, ↑e.symm x).snd) = (k', x)
[PROOFSTEP]
simp [h₁]
[GOAL]
case neg
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : k' = a
h₂ : ¬(a, ↑e.symm x).fst = a
⊢ (a, ↑e.symm x) = (k', x)
[PROOFSTEP]
simp at h₂
[GOAL]
case neg
α₁ : Type ?u.54842
β₁ : Type ?u.54841
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
k' : α₁
x : β₁
h₁ : ¬k' = a
⊢ (k', x) = (k', x)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_2
β₁ : Type u_1
inst✝ : DecidableEq α₁
a✝ : α₁
e✝ e : Perm β₁
a a' : α₁
b : β₁
h : ↑(prodExtendRight a e) (a', b) ≠ (a', b)
⊢ a' = a
[PROOFSTEP]
contrapose! h
[GOAL]
α₁ : Type u_2
β₁ : Type u_1
inst✝ : DecidableEq α₁
a✝ : α₁
e✝ e : Perm β₁
a a' : α₁
b : β₁
h : a' ≠ a
⊢ ↑(prodExtendRight a e) (a', b) = (a', b)
[PROOFSTEP]
exact prodExtendRight_apply_ne _ h _
[GOAL]
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ (↑(prodExtendRight a e) ab).fst = ab.fst
[PROOFSTEP]
rw [prodExtendRight]
[GOAL]
α₁ : 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
[PROOFSTEP]
dsimp
[GOAL]
α₁ : 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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ab.fst = a
⊢ (a, ↑e ab.snd).fst = ab.fst
[PROOFSTEP]
rw [h]
[GOAL]
case neg
α₁ : Type u_1
β₁ : Type u_2
inst✝ : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
h : ¬ab.fst = a
⊢ ab.fst = ab.fst
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : (γ → α) × (γ → β)
⊢ (fun f => (fun c => (f c).fst, fun c => (f c).snd)) ((fun p c => (Prod.fst p c, Prod.snd p c)) p) = p
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝ : γ → α
snd✝ : γ → β
⊢ (fun f => (fun c => (f c).fst, fun c => (f c).snd)) ((fun p c => (Prod.fst p c, Prod.snd p c)) (fst✝, snd✝)) =
    (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β → γ
⊢ (fun p => Sum.elim p.fst p.snd) ((fun f => (f ∘ inl, f ∘ inr)) f) = f
[PROOFSTEP]
ext ⟨⟩
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β → γ
val✝ : α
⊢ (fun p => Sum.elim p.fst p.snd) ((fun f => (f ∘ inl, f ∘ inr)) f) (inl val✝) = f (inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β → γ
val✝ : β
⊢ (fun p => Sum.elim p.fst p.snd) ((fun f => (f ∘ inl, f ∘ inr)) f) (inr val✝) = f (inr val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : (α → γ) × (β → γ)
⊢ (fun f => (f ∘ inl, f ∘ inr)) ((fun p => Sum.elim p.fst p.snd) p) = p
[PROOFSTEP]
cases p
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
fst✝ : α → γ
snd✝ : β → γ
⊢ (fun f => (f ∘ inl, f ∘ inr)) ((fun p => Sum.elim p.fst p.snd) (fst✝, snd✝)) = (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
⊢ LeftInverse (fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p =>
    Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst
[PROOFSTEP]
rintro ⟨_ | _, _⟩
[GOAL]
case mk.inl
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
snd✝ : γ
val✝ : α
⊢ (fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p => Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst) (inl val✝, snd✝)) =
    (inl val✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case mk.inr
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
snd✝ : γ
val✝ : β
⊢ (fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s)
      ((fun p => Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst) (inr val✝, snd✝)) =
    (inr val✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
⊢ Function.RightInverse (fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p =>
    Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst
[PROOFSTEP]
rintro (⟨_, _⟩ | ⟨_, _⟩)
[GOAL]
case inl.mk
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
fst✝ : α
snd✝ : γ
⊢ (fun p => Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst)
      ((fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inl (fst✝, snd✝))) =
    inl (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case inr.mk
α : Type ?u.60919
β : Type ?u.60918
γ : Type ?u.60916
fst✝ : β
snd✝ : γ
⊢ (fun p => Sum.map (fun x => (x, p.snd)) (fun x => (x, p.snd)) p.fst)
      ((fun s => Sum.elim (Prod.map inl id) (Prod.map inr id) s) (inr (fst✝, snd✝))) =
    inr (fst✝, snd✝)
[PROOFSTEP]
rfl
[GOAL]
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
p : (i : ι) × (α i ⊕ β i)
⊢ Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr)
      ((fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) p) =
    p
[PROOFSTEP]
rcases p with ⟨i, a | b⟩
[GOAL]
case mk.inl
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
i : ι
a : α i
⊢ Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr)
      ((fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) { fst := i, snd := inl a }) =
    { fst := i, snd := inl a }
[PROOFSTEP]
rfl
[GOAL]
case mk.inr
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
i : ι
b : β i
⊢ Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr)
      ((fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd) { fst := i, snd := inr b }) =
    { fst := i, snd := inr b }
[PROOFSTEP]
rfl
[GOAL]
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
p : (i : ι) × α i ⊕ (i : ι) × β i
⊢ (fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr) p) =
    p
[PROOFSTEP]
rcases p with (⟨i, a⟩ | ⟨i, b⟩)
[GOAL]
case inl.mk
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
i : ι
a : α i
⊢ (fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr) (inl { fst := i, snd := a })) =
    inl { fst := i, snd := a }
[PROOFSTEP]
rfl
[GOAL]
case inr.mk
ι : Type ?u.63850
α : ι → Type u_1
β : ι → Type u_2
i : ι
b : β i
⊢ (fun p => Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd)
      (Sum.elim (Sigma.map id fun x => inl) (Sigma.map id fun x => inr) (inr { fst := i, snd := b })) =
    inr { fst := i, snd := b }
[PROOFSTEP]
rfl
[GOAL]
ι : Type ?u.64658
α : ι → Type u_1
β : Type u_2
p : ((i : ι) × α i) × β
⊢ (fun p => ({ fst := p.fst, snd := p.snd.fst }, p.snd.snd))
      ((fun p => { fst := p.fst.fst, snd := (p.fst.snd, p.snd) }) p) =
    p
[PROOFSTEP]
rcases p with ⟨⟨_, _⟩, _⟩
[GOAL]
case mk.mk
ι : Type ?u.64658
α : ι → Type u_1
β : Type u_2
snd✝¹ : β
fst✝ : ι
snd✝ : α fst✝
⊢ (fun p => ({ fst := p.fst, snd := p.snd.fst }, p.snd.snd))
      ((fun p => { fst := p.fst.fst, snd := (p.fst.snd, p.snd) }) ({ fst := fst✝, snd := snd✝ }, snd✝¹)) =
    ({ fst := fst✝, snd := snd✝ }, snd✝¹)
[PROOFSTEP]
rfl
[GOAL]
ι : Type ?u.64658
α : ι → Type u_1
β : Type u_2
p : (i : ι) × α i × β
⊢ (fun p => { fst := p.fst.fst, snd := (p.fst.snd, p.snd) })
      ((fun p => ({ fst := p.fst, snd := p.snd.fst }, p.snd.snd)) p) =
    p
[PROOFSTEP]
rcases p with ⟨_, ⟨_, _⟩⟩
[GOAL]
case mk.mk
ι : Type ?u.64658
α : ι → Type u_1
β : Type u_2
fst✝¹ : ι
fst✝ : α fst✝¹
snd✝ : β
⊢ (fun p => { fst := p.fst.fst, snd := (p.fst.snd, p.snd) })
      ((fun p => ({ fst := p.fst, snd := p.snd.fst }, p.snd.snd)) { fst := fst✝¹, snd := (fst✝, snd✝) }) =
    { fst := fst✝¹, snd := (fst✝, snd✝) }
[PROOFSTEP]
rfl
[GOAL]
f : ℕ → Type u
⊢ LeftInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id)) fun x =>
    Sigma.casesOn x fun n =>
      Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
        inr { fst := n, snd := x }
[PROOFSTEP]
rintro ⟨n | n, x⟩
[GOAL]
case mk.zero
f : ℕ → Type u
x : f Nat.zero
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id)
      ((fun x =>
          Sigma.casesOn x fun n =>
            Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
              inr { fst := n, snd := x })
        { fst := Nat.zero, snd := x }) =
    { fst := Nat.zero, snd := x }
[PROOFSTEP]
rfl
[GOAL]
case mk.succ
f : ℕ → Type u
n : ℕ
x : f (Nat.succ n)
⊢ Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id)
      ((fun x =>
          Sigma.casesOn x fun n =>
            Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
              inr { fst := n, snd := x })
        { fst := Nat.succ n, snd := x }) =
    { fst := Nat.succ n, snd := x }
[PROOFSTEP]
rfl
[GOAL]
f : ℕ → Type u
⊢ Function.RightInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id)) fun x =>
    Sigma.casesOn x fun n =>
      Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
        inr { fst := n, snd := x }
[PROOFSTEP]
rintro (x | ⟨n, x⟩)
[GOAL]
case inl
f : ℕ → Type u
x : f 0
⊢ (fun x =>
        Sigma.casesOn x fun n =>
          Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
            inr { fst := n, snd := x })
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id) (inl x)) =
    inl x
[PROOFSTEP]
rfl
[GOAL]
case inr.mk
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ (fun x =>
        Sigma.casesOn x fun n =>
          Nat.casesOn (motive := fun i => f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x => inl x) fun n x =>
            inr { fst := n, snd := x })
      (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x => id) (inr { fst := n, snd := x })) =
    inr { fst := n, snd := x }
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.66028
⊢ LeftInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p => bif p.fst then inr p.snd else inl p.snd
[PROOFSTEP]
rintro ⟨_ | _, _⟩
[GOAL]
case mk.false
α : Type ?u.66028
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p => bif p.fst then inr p.snd else inl p.snd) (false, snd✝)) =
    (false, snd✝)
[PROOFSTEP]
rfl
[GOAL]
case mk.true
α : Type ?u.66028
snd✝ : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true) ((fun p => bif p.fst then inr p.snd else inl p.snd) (true, snd✝)) =
    (true, snd✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.66028
⊢ Function.RightInverse (Sum.elim (Prod.mk false) (Prod.mk true)) fun p => bif p.fst then inr p.snd else inl p.snd
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case inl
α : Type ?u.66028
val✝ : α
⊢ (fun p => bif p.fst then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type ?u.66028
val✝ : α
⊢ (fun p => bif p.fst then inr p.snd else inl p.snd) (Sum.elim (Prod.mk false) (Prod.mk true) (inr val✝)) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Sum.elim succ (fun x => 0) ((fun n => Nat.casesOn n (inr PUnit.unit) inl) n) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Sum.elim succ (fun x => 0) ((fun n => Nat.casesOn n (inr PUnit.unit) inl) zero) = zero
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ Sum.elim succ (fun x => 0) ((fun n => Nat.casesOn n (inr PUnit.unit) inl) (succ n✝)) = succ n✝
[PROOFSTEP]
rfl
[GOAL]
⊢ Function.RightInverse (Sum.elim succ fun x => 0) fun n => Nat.casesOn n (inr PUnit.unit) inl
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case inl
val✝ : ℕ
⊢ (fun n => Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x => 0) (inl val✝)) = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
val✝ : PUnit
⊢ (fun n => Nat.casesOn n (inr PUnit.unit) inl) (Sum.elim succ (fun x => 0) (inr val✝)) = inr val✝
[PROOFSTEP]
rfl
[GOAL]
⊢ LeftInverse (Sum.elim Int.ofNat Int.negSucc) fun z => Int.casesOn z inl inr
[PROOFSTEP]
rintro (m | n)
[GOAL]
case ofNat
m : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z => Int.casesOn z inl inr) (Int.ofNat m)) = Int.ofNat m
[PROOFSTEP]
rfl
[GOAL]
case negSucc
n : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc ((fun z => Int.casesOn z inl inr) (Int.negSucc n)) = Int.negSucc n
[PROOFSTEP]
rfl
[GOAL]
⊢ Function.RightInverse (Sum.elim Int.ofNat Int.negSucc) fun z => Int.casesOn z inl inr
[PROOFSTEP]
rintro (m | n)
[GOAL]
case inl
m : ℕ
⊢ (fun z => Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inl m)) = inl m
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
⊢ (fun z => Int.casesOn z inl inr) (Sum.elim Int.ofNat Int.negSucc (inr n)) = inr n
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.67366
β : Type ?u.67367
e : α ≃ β
l : List α
⊢ List.map (↑e.symm) (List.map (↑e) l) = l
[PROOFSTEP]
rw [List.map_map, e.symm_comp_self, List.map_id]
[GOAL]
α : Type ?u.67366
β : Type ?u.67367
e : α ≃ β
l : List β
⊢ List.map (↑e) (List.map (↑e.symm) l) = l
[PROOFSTEP]
rw [List.map_map, e.self_comp_symm, List.map_id]
[GOAL]
α : Sort ?u.68590
β : Sort ?u.68594
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : { a // p a }
⊢ ↑((fun b => { val := ↑e.symm ↑b, property := (_ : p (↑e.symm ↑b)) })
        ((fun a => { val := ↑e ↑a, property := (_ : q (↑e ↑a)) }) a)) =
    ↑a
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.68590
β : Sort ?u.68594
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
b : { b // q b }
⊢ ↑((fun a => { val := ↑e ↑a, property := (_ : q (↑e ↑a)) })
        ((fun b => { val := ↑e.symm ↑b, property := (_ : p (↑e.symm ↑b)) }) b)) =
    ↑b
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)
⊢ subtypeEquiv (Equiv.refl α) h = Equiv.refl { a // p a }
[PROOFSTEP]
ext
[GOAL]
case H.a
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p (↑(Equiv.refl α) a)) (_ : ∀ (a : α), p a ↔ p a)
x✝ : { a // p a }
⊢ ↑(↑(subtypeEquiv (Equiv.refl α) h) x✝) = ↑(↑(Equiv.refl { a // p a }) x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Sort ?u.69934
β : Sort ?u.69938
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : β
⊢ q a ↔ p (↑e.symm a)
[PROOFSTEP]
convert (h <| e.symm a).symm
[GOAL]
case h.e'_1.h.e'_1
α : Sort ?u.69934
β : Sort ?u.69938
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (↑e a)
a : β
⊢ a = ↑e (↑e.symm a)
[PROOFSTEP]
exact (e.apply_symm_apply a).symm
[GOAL]
β : Sort ?u.72782
α : Sort ?u.72787
p : β → Prop
e : α ≃ β
⊢ ∀ (a : α), p (↑e a) ↔ p (↑e a)
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.74025
p : α → Prop
q : Subtype p → Prop
a : Subtype q
⊢ q { val := ↑↑a, property := (_ : p ↑↑a) }
[PROOFSTEP]
rcases a with ⟨⟨a, hap⟩, haq⟩
[GOAL]
case mk.mk
α : Sort ?u.74025
p : α → Prop
q : Subtype p → Prop
a : α
hap : p a
haq : q { val := a, property := hap }
⊢ q
    { val := ↑↑{ val := { val := a, property := hap }, property := haq },
      property := (_ : p ↑↑{ val := { val := a, property := hap }, property := haq }) }
[PROOFSTEP]
exact haq
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (y : Subtype q) × { x // f x = ↑y } ≃ (y : Subtype q) × { x // { val := f ↑x, property := (_ : q (f ↑x)) } = y }
[PROOFSTEP]
{ apply sigmaCongrRight
  intro y
  apply Equiv.symm
  refine' (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight _)
  intro x
  exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2), Subtype.eq h'⟩⟩
}
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (y : Subtype q) × { x // f x = ↑y } ≃ (y : Subtype q) × { x // { val := f ↑x, property := (_ : q (f ↑x)) } = y }
[PROOFSTEP]
apply sigmaCongrRight
[GOAL]
case F
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (a : Subtype q) → { x // f x = ↑a } ≃ { x // { val := f ↑x, property := (_ : q (f ↑x)) } = a }
[PROOFSTEP]
intro y
[GOAL]
case F
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x // f x = ↑y } ≃ { x // { val := f ↑x, property := (_ : q (f ↑x)) } = y }
[PROOFSTEP]
apply Equiv.symm
[GOAL]
case F.e
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x // { val := f ↑x, property := (_ : q (f ↑x)) } = y } ≃ { x // f x = ↑y }
[PROOFSTEP]
refine' (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight _)
[GOAL]
case F.e
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ ∀ (x : α),
    (∃ h_1, { val := f ↑{ val := x, property := h_1 }, property := (_ : q (f ↑{ val := x, property := h_1 })) } = y) ↔
      f x = ↑y
[PROOFSTEP]
intro x
[GOAL]
case F.e
α : Type u_1
β : Type u_2
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
x : α
⊢ (∃ h_1, { val := f ↑{ val := x, property := h_1 }, property := (_ : q (f ↑{ val := x, property := h_1 })) } = y) ↔
    f x = ↑y
[PROOFSTEP]
exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2), Subtype.eq h'⟩⟩
[GOAL]
α : Type ?u.79450
p : Option α → Type v
h : p none → False
⊢ ∀ (x : Option α), p x → Option.isSome x = true
[PROOFSTEP]
intro x
[GOAL]
α : Type ?u.79450
p : Option α → Type v
h : p none → False
x : Option α
⊢ p x → Option.isSome x = true
[PROOFSTEP]
cases x
[GOAL]
case none
α : Type ?u.79450
p : Option α → Type v
h : p none → False
⊢ p none → Option.isSome none = true
[PROOFSTEP]
intro n
[GOAL]
case none
α : Type ?u.79450
p : Option α → Type v
h : p none → False
n : p none
⊢ Option.isSome none = true
[PROOFSTEP]
exfalso
[GOAL]
case none.h
α : Type ?u.79450
p : Option α → Type v
h : p none → False
n : p none
⊢ False
[PROOFSTEP]
exact h n
[GOAL]
case some
α : Type ?u.79450
p : Option α → Type v
h : p none → False
val✝ : α
⊢ p (some val✝) → Option.isSome (some val✝) = true
[PROOFSTEP]
intro _
[GOAL]
case some
α : Type ?u.79450
p : Option α → Type v
h : p none → False
val✝ : α
a✝ : p (some val✝)
⊢ Option.isSome (some val✝) = true
[PROOFSTEP]
exact rfl
[GOAL]
ι : Type ?u.79857
π : ι → Type u_1
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π i
[PROOFSTEP]
rw [← f.2 i]
[GOAL]
ι : Type ?u.79857
π : ι → Type u_1
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst
[PROOFSTEP]
exact (f.1 i).2
[GOAL]
ι : Type ?u.79857
π : ι → Type u_1
x✝ : { f // ∀ (i : ι), (f i).fst = i }
f : ι → (i : ι) × π i
hf : ∀ (i : ι), (f i).fst = i
i : ι
⊢ HEq
    (↑((fun f =>
              { val := fun i => { fst := i, snd := f i },
                property :=
                  (_ :
                    ∀ (i : ι),
                      ((fun i => { fst := i, snd := f i }) i).fst = ((fun i => { fst := i, snd := f i }) i).fst) })
            ((fun f i => Eq.mpr (_ : π i = π (↑f i).fst) (↑f i).snd) { val := f, property := hf }))
        i).snd
    (↑{ val := f, property := hf } i).snd
[PROOFSTEP]
simp
[GOAL]
α : Sort ?u.80907
β : α → Sort v
p : (a : α) → β a → Prop
⊢ LeftInverse (fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), p a ↑(f a)) }) fun f a =>
    { val := ↑f a, property := (_ : p a (↑f a)) }
[PROOFSTEP]
rintro ⟨f, h⟩
[GOAL]
case mk
α : Sort ?u.80907
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → β a
h : ∀ (a : α), p a (f a)
⊢ (fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), p a ↑(f a)) })
      ((fun f a => { val := ↑f a, property := (_ : p a (↑f a)) }) { val := f, property := h }) =
    { val := f, property := h }
[PROOFSTEP]
rfl
[GOAL]
α : Sort ?u.80907
β : α → Sort v
p : (a : α) → β a → Prop
⊢ Function.RightInverse (fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), p a ↑(f a)) }) fun f a =>
    { val := ↑f a, property := (_ : p a (↑f a)) }
[PROOFSTEP]
rintro f
[GOAL]
α : Sort ?u.80907
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b // p a b }
⊢ (fun f a => { val := ↑f a, property := (_ : p a (↑f a)) })
      ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), p a ↑(f a)) }) f) =
    f
[PROOFSTEP]
funext a
[GOAL]
case h
α : Sort ?u.80907
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b // p a b }
a : α
⊢ (fun f a => { val := ↑f a, property := (_ : p a (↑f a)) })
      ((fun f => { val := fun a => ↑(f a), property := (_ : ∀ (a : α), p a ↑(f a)) }) f) a =
    f a
[PROOFSTEP]
exact Subtype.ext_val rfl
[GOAL]
α : Type ?u.82438
β : Type ?u.82437
p : α → β → Prop
x : { x // p x.fst x.snd }
⊢ (fun x => { val := (x.fst, ↑x.snd), property := (_ : p x.fst ↑x.snd) })
      ((fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, property := (_ : p (↑x).fst (↑x).snd) } }) x) =
    x
[PROOFSTEP]
ext
[GOAL]
case a.h₁
α : Type ?u.82438
β : Type ?u.82437
p : α → β → Prop
x : { x // p x.fst x.snd }
⊢ (↑((fun x => { val := (x.fst, ↑x.snd), property := (_ : p x.fst ↑x.snd) })
          ((fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, property := (_ : p (↑x).fst (↑x).snd) } }) x))).fst =
    (↑x).fst
[PROOFSTEP]
rfl
[GOAL]
case a.h₂
α : Type ?u.82438
β : Type ?u.82437
p : α → β → Prop
x : { x // p x.fst x.snd }
⊢ (↑((fun x => { val := (x.fst, ↑x.snd), property := (_ : p x.fst ↑x.snd) })
          ((fun x => { fst := (↑x).fst, snd := { val := (↑x).snd, property := (_ : p (↑x).fst (↑x).snd) } }) x))).snd =
    (↑x).snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : α) → β i
⊢ (fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
      ((fun f => (fun x => f ↑x, fun x => f ↑x)) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : α) → β i
x : α
⊢ (fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
      ((fun f => (fun x => f ↑x, fun x => f ↑x)) f) x =
    f x
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : α) → β i
x : α
h : p x
⊢ (fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
      ((fun f => (fun x => f ↑x, fun x => f ↑x)) f) x =
    f x
[PROOFSTEP]
simp only [h, dif_neg, dif_pos, not_false_iff]
[GOAL]
case neg
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : α) → β i
x : α
h : ¬p x
⊢ (fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
      ((fun f => (fun x => f ↑x, fun x => f ↑x)) f) x =
    f x
[PROOFSTEP]
simp only [h, dif_neg, dif_pos, not_false_iff]
[GOAL]
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
⊢ Function.RightInverse
    (fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
    fun f => (fun x => f ↑x, fun x => f ↑x)
[PROOFSTEP]
rintro ⟨f, g⟩
[GOAL]
case mk
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (fun f => (fun x => f ↑x, fun x => f ↑x))
      ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
        (f, g)) =
    (f, g)
[PROOFSTEP]
ext1
[GOAL]
case mk.h₁
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g))).fst =
    (f, g).fst
[PROOFSTEP]
ext y
[GOAL]
case mk.h₁.h
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
y : { x // p x }
⊢ Prod.fst
      ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g)))
      y =
    Prod.fst (f, g) y
[PROOFSTEP]
rcases y with ⟨val, property⟩
[GOAL]
case mk.h₁.h.mk
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
val : α
property : p val
⊢ Prod.fst
      ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g)))
      { val := val, property := property } =
    Prod.fst (f, g) { val := val, property := property }
[PROOFSTEP]
simp only [property, dif_pos, dif_neg, not_false_iff, Subtype.coe_mk]
[GOAL]
case mk.h₂
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g))).snd =
    (f, g).snd
[PROOFSTEP]
ext y
[GOAL]
case mk.h₂.h
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
y : { x // ¬p x }
⊢ Prod.snd
      ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g)))
      y =
    Prod.snd (f, g) y
[PROOFSTEP]
rcases y with ⟨val, property⟩
[GOAL]
case mk.h₂.h.mk
α : Type u_1
p : α → Prop
β : α → Type u_2
inst✝ : DecidablePred p
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
val : α
property : ¬p val
⊢ Prod.snd
      ((fun f => (fun x => f ↑x, fun x => f ↑x))
        ((fun f x => if h : p x then Prod.fst f { val := x, property := h } else Prod.snd f { val := x, property := h })
          (f, g)))
      { val := val, property := property } =
    Prod.snd (f, g) { val := val, property := property }
[PROOFSTEP]
simp only [property, dif_pos, dif_neg, not_false_iff, Subtype.coe_mk]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : (j : α) → β j
⊢ (fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h })
      ((fun f => (f i, fun j => f ↑j)) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : (j : α) → β j
x : α
⊢ (fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h })
      ((fun f => (f i, fun j => f ↑j)) f) x =
    f x
[PROOFSTEP]
dsimp only
[GOAL]
case h
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : (j : α) → β j
x : α
⊢ (if h : x = i then (_ : i = x) ▸ f i else f x) = f x
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : (j : α) → β j
x : α
h : x = i
⊢ (_ : i = x) ▸ f i = f x
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
f : (j : α) → β j
x : α
⊢ (_ : x = x) ▸ f x = f x
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : (j : α) → β j
x : α
h : ¬x = i
⊢ f x = f x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ (fun f => (f i, fun j => f ↑j))
      ((fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h }) f) =
    f
[PROOFSTEP]
ext x
[GOAL]
case h₁
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : β i × ((j : { j // j ≠ i }) → β ↑j)
⊢ ((fun f => (f i, fun j => f ↑j))
        ((fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h }) f)).fst =
    f.fst
case h₂.h
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : β i × ((j : { j // j ≠ i }) → β ↑j)
x : { j // j ≠ i }
⊢ Prod.snd
      ((fun f => (f i, fun j => f ↑j))
        ((fun f j => if h : j = i then (_ : i = j) ▸ f.fst else Prod.snd f { val := j, property := h }) f))
      x =
    Prod.snd f x
[PROOFSTEP]
exacts [dif_pos rfl, (dif_neg x.2).trans (by cases x; rfl)]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : β i × ((j : { j // j ≠ i }) → β ↑j)
x : { j // j ≠ i }
⊢ (fun h => Prod.snd f { val := ↑x, property := h }) (_ : ↑x ≠ i) = Prod.snd f x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
inst✝ : DecidableEq α
i : α
β : α → Type u_2
f : β i × ((j : { j // j ≠ i }) → β ↑j)
val✝ : α
property✝ : val✝ ≠ i
⊢ (fun h => Prod.snd f { val := ↑{ val := val✝, property := property✝ }, property := h })
      (_ : ↑{ val := val✝, property := property✝ } ≠ i) =
    Prod.snd f { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
X : Sort ?u.89087
inst✝ : DecidableEq X
x : X
Y : Sort ?u.89123
f : { x' // x' ≠ x } → Y
y : Y
⊢ (fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val = f
[PROOFSTEP]
funext x'
[GOAL]
case h
X : Sort ?u.89087
inst✝ : DecidableEq X
x : X
Y : Sort ?u.89123
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ((fun x' => if h : x' ≠ x then f { val := x', property := h } else y) ∘ Subtype.val) x' = f x'
[PROOFSTEP]
simp only [ne_eq, dite_not, comp_apply, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
[GOAL]
case h
X : Sort ?u.89087
inst✝ : DecidableEq X
x : X
Y : Sort ?u.89123
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ↑x' = x → y = f x'
[PROOFSTEP]
intro w
[GOAL]
case h
X : Sort ?u.89087
inst✝ : DecidableEq X
x : X
Y : Sort ?u.89123
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ y = f x'
[PROOFSTEP]
exfalso
[GOAL]
case h.h
X : Sort ?u.89087
inst✝ : DecidableEq X
x : X
Y : Sort ?u.89123
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ False
[PROOFSTEP]
exact x'.property w
[GOAL]
α' : Type u_1
β' : Type u_2
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
a : α'
⊢ ↑(extendDomain e f) ↑(↑f a) = ↑(↑f (↑e a))
[PROOFSTEP]
simp [Perm.extendDomain]
[GOAL]
α' : Type u_1
β' : Type u_2
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
b : β'
h : p b
⊢ ↑(extendDomain e f) b = ↑(↑f (↑e (↑f.symm { val := b, property := h })))
[PROOFSTEP]
simp [Perm.extendDomain, h]
[GOAL]
α' : Type u_1
β' : Type u_2
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
b : β'
h : ¬p b
⊢ ↑(extendDomain e f) b = b
[PROOFSTEP]
simp [Perm.extendDomain, h]
[GOAL]
α' : Type u_1
β' : Type u_2
e : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
⊢ extendDomain (Equiv.refl α') f = Equiv.refl β'
[PROOFSTEP]
simp [Perm.extendDomain]
[GOAL]
α' : Type u_1
β' : Type u_2
e✝ : Perm α'
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
e e' : Perm α'
⊢ (extendDomain e f).trans (extendDomain e' f) = extendDomain (e.trans e') f
[PROOFSTEP]
simp [Perm.extendDomain, permCongr_trans]
[GOAL]
α : Sort ?u.97068
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ (Quotient.mk s₁ a)
h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y
a✝ : { x // p₂ x }
a b : α
hab : a ≈ b
⊢ p₂ (Quotient.mk s₁ a) = p₂ (Quotient.mk s₁ b)
[PROOFSTEP]
rw [Quotient.sound hab]
[GOAL]
α : Sort ?u.97068
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ (Quotient.mk s₁ a)
h : ∀ (x y : Subtype p₁), Setoid.r x y ↔ ↑x ≈ ↑y
⊢ LeftInverse
    (fun a =>
      Quotient.liftOn a (fun a => { val := Quotient.mk s₁ ↑a, property := (_ : p₂ (Quotient.mk s₁ ↑a)) })
        (_ :
          ∀ (a b : Subtype p₁),
            a ≈ b →
              (fun a => { val := Quotient.mk s₁ ↑a, property := (_ : p₂ (Quotient.mk s₁ ↑a)) }) a =
                (fun a => { val := Quotient.mk s₁ ↑a, property := (_ : p₂ (Quotient.mk s₁ ↑a)) }) b))
    fun a =>
    Quotient.hrecOn (motive := fun x => p₂ x → Quotient s₂) (↑a)
      (fun a h => Quotient.mk s₂ { val := a, property := (_ : p₁ a) })
      (_ : ∀ (a_1 b : α), a_1 ≈ b → HEq (?m.97417 a a_1) (?m.97418 a b)) (_ : p₂ ↑a)
[PROOFSTEP]
exact fun ⟨a, ha⟩ => Quotient.inductionOn a (fun b hb => rfl) ha
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ swapCore a a r = r
[PROOFSTEP]
unfold swapCore
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : r = a
⊢ a = r
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : ¬r = a
⊢ r = r
[PROOFSTEP]
simp [*]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b (swapCore a b r) = r
[PROOFSTEP]
unfold swapCore
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
[PROOFSTEP]
split_ifs with h₁ h₂ h₃ h₄ h₅
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : b = a
⊢ b = r
[PROOFSTEP]
subst h₁
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : b = r
⊢ b = r
[PROOFSTEP]
exact h₂
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : b = b
⊢ a = r
[PROOFSTEP]
subst h₁
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₃ : b = b
h₂ : ¬b = r
⊢ r = r
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬b = a
h₃ : ¬b = b
⊢ b = r
[PROOFSTEP]
cases h₃ rfl
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : a = a
⊢ b = r
[PROOFSTEP]
exact h₄.symm
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : a = b
⊢ a = r
[PROOFSTEP]
cases h₅ rfl
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : r = b
h₅ : ¬a = a
h✝ : ¬a = b
⊢ a = r
[PROOFSTEP]
cases h₅ rfl
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₄ : ¬r = b
⊢ r = r
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b r = swapCore b a r
[PROOFSTEP]
unfold swapCore
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
[PROOFSTEP]
split_ifs with h₁ h₂ h₃
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : r = b
⊢ b = a
[PROOFSTEP]
try simp
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : r = b
⊢ b = a
[PROOFSTEP]
simp
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬r = b
⊢ b = b
[PROOFSTEP]
try simp
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : ¬r = b
⊢ b = b
[PROOFSTEP]
simp
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₃ : r = b
⊢ a = a
[PROOFSTEP]
try simp
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₃ : r = b
⊢ a = a
[PROOFSTEP]
simp
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₃ : ¬r = b
⊢ r = r
[PROOFSTEP]
try simp
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : ¬r = a
h₃ : ¬r = b
⊢ r = r
[PROOFSTEP]
simp
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
h₁ : r = a
h₂ : r = b
⊢ b = a
[PROOFSTEP]
cases h₁
[GOAL]
case pos.refl
α : Sort u_1
inst✝ : DecidableEq α
r b : α
h₂ : r = b
⊢ b = r
[PROOFSTEP]
cases h₂
[GOAL]
case pos.refl.refl
α : Sort u_1
inst✝ : DecidableEq α
r : α
⊢ r = r
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
a b : α
⊢ ↑(swap a b) b = a
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b : α
h : b = a
⊢ ↑(swap a b) b = a
[PROOFSTEP]
simp [swap_apply_def, h]
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b : α
h : ¬b = a
⊢ ↑(swap a b) b = a
[PROOFSTEP]
simp [swap_apply_def, h]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ x ≠ a → x ≠ b → ↑(swap a b) x = x
[PROOFSTEP]
simp (config := { contextual := true }) [swap_apply_def]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
x y : α
⊢ swap x y = Equiv.refl α ↔ x = y
[PROOFSTEP]
refine' ⟨fun h => (Equiv.refl _).injective _, fun h => h ▸ swap_self _⟩
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
x y : α
h : swap x y = Equiv.refl α
⊢ ↑(Equiv.refl α) x = ↑(Equiv.refl α) y
[PROOFSTEP]
rw [← h, swap_apply_left, h, refl_apply]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
π : Perm α
⊢ ↑(π.trans (swap a b)) x = if ↑π x = a then b else if ↑π x = b then a else ↑π x
[PROOFSTEP]
cases π
[GOAL]
case mk
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
toFun✝ invFun✝ : α → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ ↑({ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (swap a b)) x =
    if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = a then b
    else
      if ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x = b then a
      else ↑{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } x
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
i j x : α
⊢ ↑(swap i j) x = update (update id j i) i j x
[PROOFSTEP]
rw [update_apply _ i j, update_apply _ j i, Equiv.swap_apply_def, id.def]
[GOAL]
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
i j : α
f : α → β
⊢ f ∘ ↑(swap i j) = update (update f j (f i)) i (f j)
[PROOFSTEP]
rw [swap_eq_update, comp_update, comp_update, comp.right_id]
[GOAL]
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
⊢ ↑((e.symm.trans (swap a b)).trans e) x = ↑(swap (↑e a) (↑e b)) x
[PROOFSTEP]
have : ∀ a, e.symm x = a ↔ x = e a := fun a =>
  by
  rw [@eq_comm _ (e.symm x)]
  constructor <;> intros <;> simp_all
[GOAL]
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ ↑e.symm x = a ↔ x = ↑e a
[PROOFSTEP]
rw [@eq_comm _ (e.symm x)]
[GOAL]
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ a = ↑e.symm x ↔ x = ↑e a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ a = ↑e.symm x → x = ↑e a
[PROOFSTEP]
intros
[GOAL]
case mpr
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝ b : α
e : α ≃ β
x : β
a : (fun x => α) x
⊢ x = ↑e a → a = ↑e.symm x
[PROOFSTEP]
intros
[GOAL]
case mp
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝¹ b : α
e : α ≃ β
x : β
a : (fun x => α) x
a✝ : a = ↑e.symm x
⊢ x = ↑e a
[PROOFSTEP]
simp_all
[GOAL]
case mpr
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a✝¹ b : α
e : α ≃ β
x : β
a : (fun x => α) x
a✝ : x = ↑e a
⊢ a = ↑e.symm x
[PROOFSTEP]
simp_all
[GOAL]
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑((e.symm.trans (swap a b)).trans e) x = ↑(swap (↑e a) (↑e b)) x
[PROOFSTEP]
simp [trans_apply, swap_apply_def, this]
[GOAL]
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
⊢ ↑e (if x = ↑e a then b else if x = ↑e b then a else ↑e.symm x) =
    if x = ↑e a then ↑e b else if x = ↑e b then ↑e a else x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
h✝ : x = ↑e a
⊢ ↑e b = ↑e b
[PROOFSTEP]
simp
[GOAL]
case pos
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
h✝¹ : ¬x = ↑e a
h✝ : x = ↑e b
⊢ ↑e a = ↑e a
[PROOFSTEP]
simp
[GOAL]
case neg
α : Sort u_2
inst✝¹ : DecidableEq α
β : Sort u_1
inst✝ : DecidableEq β
a b : α
e : α ≃ β
x : β
this : ∀ (a : (fun x => α) x), ↑e.symm x = a ↔ x = ↑e a
h✝¹ : ¬x = ↑e a
h✝ : ¬x = ↑e b
⊢ ↑e (↑e.symm x) = x
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
i j a : α
⊢ ↑(swap i j) (↑(swap i j) a) = a
[PROOFSTEP]
rw [← Equiv.trans_apply, Equiv.swap_swap, Equiv.refl_apply]
[GOAL]
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v (↑(swap i j) k) = v k
[PROOFSTEP]
by_cases hi : k = i
[GOAL]
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : k = i
⊢ v (↑(swap i j) k) = v k
[PROOFSTEP]
rw [hi, swap_apply_left, hv]
[GOAL]
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
⊢ v (↑(swap i j) k) = v k
[PROOFSTEP]
by_cases hj : k = j
[GOAL]
case pos
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : k = j
⊢ v (↑(swap i j) k) = v k
[PROOFSTEP]
rw [hj, swap_apply_right, hv]
[GOAL]
case neg
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
v : α → β
i j : α
hv : v i = v j
k : α
hi : ¬k = i
hj : ¬k = j
⊢ v (↑(swap i j) k) = v k
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne hi hj]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
x y z w : α
⊢ ↑(swap x y) z = w ↔ z = ↑(swap x y) w
[PROOFSTEP]
rw [apply_eq_iff_eq_symm_apply, symm_swap]
[GOAL]
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
by_cases hab : a = b
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : a = b
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
simp [hab]
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
by_cases hax : x = a
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : x = a
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
simp [hax, eq_comm]
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
by_cases hbx : x = b
[GOAL]
case pos
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : x = b
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
simp [hbx]
[GOAL]
case neg
α : Sort u_1
inst✝ : DecidableEq α
a b x : α
hab : ¬a = b
hax : ¬x = a
hbx : ¬x = b
⊢ ↑(swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)
[PROOFSTEP]
simp [hab, hax, hbx, swap_apply_of_ne_of_ne]
[GOAL]
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
⊢ sumCongr (swap i j) (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)
[PROOFSTEP]
ext x
[GOAL]
case H
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
x : α ⊕ β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) x = ↑(swap (Sum.inl i) (Sum.inl j)) x
[PROOFSTEP]
cases x
[GOAL]
case H.inl
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inl val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inl val✝)
[PROOFSTEP]
simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp.right_id, Sum.elim_inl, comp_apply, swap_apply_def,
  Sum.inl.injEq]
[GOAL]
case H.inl
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
⊢ Sum.inl (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inl j else if val✝ = j then Sum.inl i else Sum.inl val✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
h✝ : val✝ = i
⊢ Sum.inl j = Sum.inl j
[PROOFSTEP]
rfl
[GOAL]
case pos
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
h✝¹ : ¬val✝ = i
h✝ : val✝ = j
⊢ Sum.inl i = Sum.inl i
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : α
h✝¹ : ¬val✝ = i
h✝ : ¬val✝ = j
⊢ Sum.inl val✝ = Sum.inl val✝
[PROOFSTEP]
rfl
[GOAL]
case H.inr
α✝ : Sort ?u.117935
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : α
val✝ : β
⊢ ↑(sumCongr (swap i j) (Equiv.refl β)) (Sum.inr val✝) = ↑(swap (Sum.inl i) (Sum.inl j)) (Sum.inr val✝)
[PROOFSTEP]
simp [Sum.map, swap_apply_of_ne_of_ne]
[GOAL]
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
⊢ sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)
[PROOFSTEP]
ext x
[GOAL]
case H
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
x : α ⊕ β
⊢ ↑(sumCongr (Equiv.refl α) (swap i j)) x = ↑(swap (Sum.inr i) (Sum.inr j)) x
[PROOFSTEP]
cases x
[GOAL]
case H.inl
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j : β
val✝ : α
⊢ ↑(sumCongr (Equiv.refl α) (swap i j)) (Sum.inl val✝) = ↑(swap (Sum.inr i) (Sum.inr j)) (Sum.inl val✝)
[PROOFSTEP]
simp [Sum.map, swap_apply_of_ne_of_ne]
[GOAL]
case H.inr
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ ↑(sumCongr (Equiv.refl α) (swap i j)) (Sum.inr val✝) = ↑(swap (Sum.inr i) (Sum.inr j)) (Sum.inr val✝)
[PROOFSTEP]
simp only [Equiv.sumCongr_apply, Sum.map, coe_refl, comp.right_id, Sum.elim_inr, comp_apply, swap_apply_def,
  Sum.inr.injEq]
[GOAL]
case H.inr
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
⊢ Sum.inr (if val✝ = i then j else if val✝ = j then i else val✝) =
    if val✝ = i then Sum.inr j else if val✝ = j then Sum.inr i else Sum.inr val✝
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
h✝ : val✝ = i
⊢ Sum.inr j = Sum.inr j
[PROOFSTEP]
rfl
[GOAL]
case pos
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
h✝¹ : ¬val✝ = i
h✝ : val✝ = j
⊢ Sum.inr i = Sum.inr i
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Sort ?u.122347
inst✝² : DecidableEq α✝
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
i j val✝ : β
h✝¹ : ¬val✝ = i
h✝ : ¬val✝ = j
⊢ Sum.inr val✝ = Sum.inr val✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
inst✝ : DecidableEq α
β : Sort u_1
f : α ≃ β
a : α
b : β
⊢ ↑(setValue f a b) a = b
[PROOFSTEP]
simp [setValue, swap_apply_left]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f (↑(Equiv.swap x y) z) = ↑(Equiv.swap (f x) (f y)) (f z)
[PROOFSTEP]
conv_rhs => rw [Equiv.swap_apply_def]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
| ↑(Equiv.swap (f x) (f y)) (f z)
[PROOFSTEP]
rw [Equiv.swap_apply_def]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
| ↑(Equiv.swap (f x) (f y)) (f z)
[PROOFSTEP]
rw [Equiv.swap_apply_def]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
| ↑(Equiv.swap (f x) (f y)) (f z)
[PROOFSTEP]
rw [Equiv.swap_apply_def]
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f (↑(Equiv.swap x y) z) = if f z = f x then f y else if f z = f y then f x else f z
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : f z = f x
⊢ f (↑(Equiv.swap x y) z) = f y
[PROOFSTEP]
rw [hf h₁, Equiv.swap_apply_left]
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : f z = f y
⊢ f (↑(Equiv.swap x y) z) = f x
[PROOFSTEP]
rw [hf h₂, Equiv.swap_apply_right]
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
h₁ : ¬f z = f x
h₂ : ¬f z = f y
⊢ f (↑(Equiv.swap x y) z) = f z
[PROOFSTEP]
rw [Equiv.swap_apply_of_ne_of_ne (mt (congr_arg f) h₁) (mt (congr_arg f) h₂)]
[GOAL]
α : Sort ?u.129173
β : Sort ?u.129177
P✝ : α → Sort w
e✝ : α ≃ β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
x : α
⊢ ∀ {y : α} (h : y = x), h ▸ f y = f x
[PROOFSTEP]
rintro _ rfl
[GOAL]
α : Sort ?u.129173
β : Sort ?u.129177
P✝ : α → Sort w
e✝ : α ≃ β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
y✝ : α
⊢ (_ : y✝ = y✝) ▸ f y✝ = f y✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort ?u.129173
β : Sort ?u.129177
P✝ : α → Sort w
e✝ : α ≃ β
P : α → Sort u_1
e : α ≃ β
f : (b : β) → P (↑e.symm b)
x : β
⊢ ∀ {y : β} (h : y = x), (_ : ↑e.symm y = ↑e.symm x) ▸ f y = f x
[PROOFSTEP]
rintro _ rfl
[GOAL]
α : Sort ?u.129173
β : Sort ?u.129177
P✝ : α → Sort w
e✝ : α ≃ β
P : α → Sort u_1
e : α ≃ β
f : (b : β) → P (↑e.symm b)
y✝ : β
⊢ (_ : ↑e.symm y✝ = ↑e.symm y✝) ▸ f y✝ = f y✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ↑(piCongr h₁ h₂) f (↑h₁ a) = ↑(h₂ a) (f a)
[PROOFSTEP]
change Eq.ndrec _ _ = _
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ (_ : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a) ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
[PROOFSTEP]
generalize_proofs hZa
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a
⊢ hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
[PROOFSTEP]
revert hZa
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm (↑h₁.symm (↑h₁ a)) = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f (↑h₁.symm (↑h₁ a)) = ↑(h₂ a) (f a)
[PROOFSTEP]
rw [h₁.symm_apply_apply a]
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ∀ (hZa : ↑h₁.symm.symm a = ↑h₁ a), hZa ▸ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
[PROOFSTEP]
simp
[GOAL]
α : Sort u_2
β : Sort u_1
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (↑h₁ a)
f : (a : α) → W a
a : α
⊢ ↑(piCongrRight h₂) f a = ↑(h₂ a) (f a)
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ↑(piCongr' h₁ h₂).symm f (↑h₁.symm b) = ↑(h₂ b).symm (f b)
[PROOFSTEP]
change Eq.ndrec _ _ = _
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ (_ : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b) ▸
      ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) =
    ↑(h₂ b).symm (f b)
[PROOFSTEP]
generalize_proofs hWb
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b
⊢ hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
[PROOFSTEP]
revert hWb
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm (↑h₁.symm.symm (↑h₁.symm b)) = ↑h₁.symm b),
    hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f (↑h₁.symm.symm (↑h₁.symm b)) = ↑(h₂ b).symm (f b)
[PROOFSTEP]
generalize hb : h₁ (h₁.symm b) = b'
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : ↑h₁ (↑h₁.symm b) = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
[PROOFSTEP]
rw [h₁.apply_symm_apply b] at hb
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b b' : β
hb : b = b'
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b' = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b' = ↑(h₂ b).symm (f b)
[PROOFSTEP]
subst hb
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ∀ (hWb : ↑h₁.symm.symm.symm b = ↑h₁.symm b), hWb ▸ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
β : Sort u_2
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (b : β) → W (↑h₁.symm b) ≃ Z b
f : (b : β) → Z b
b : β
⊢ ↑(piCongrRight fun b => (h₂ b).symm) f b = ↑(h₂ b).symm (f b)
[PROOFSTEP]
rfl
[GOAL]
α₁ : Type u_2
β₁ : Type u_1
e : α₁ ≃ β₁
f✝ : α₁ → α₁ → α₁
f : α₁ → α₁
x : α₁
⊢ ↑e (f x) = ↑(conj e) f (↑e x)
[PROOFSTEP]
simp
[GOAL]
α₁ : Type u_2
β₁ : Type u_1
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
x y : α₁
⊢ ↑e (f x y) = ↑(arrowCongr e (conj e)) f (↑e x) (↑e y)
[PROOFSTEP]
simp [arrowCongr]
[GOAL]
α₁ : Type ?u.139208
β₁ : Type ?u.139213
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
inst✝ : IsLeftCancel α₁ f
x y z : α₁
⊢ ↑(arrowCongr e (arrowCongr e e)) f (↑e x) (↑e y) = ↑(arrowCongr e (arrowCongr e e)) f (↑e x) (↑e z) → ↑e y = ↑e z
[PROOFSTEP]
simpa using @IsLeftCancel.left_cancel _ f _ x y z
[GOAL]
α₁ : Type ?u.141095
β₁ : Type ?u.141100
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
inst✝ : IsRightCancel α₁ f
x y z : α₁
⊢ ↑(arrowCongr e (arrowCongr e e)) f (↑e x) (↑e y) = ↑(arrowCongr e (arrowCongr e e)) f (↑e z) (↑e y) → ↑e x = ↑e z
[PROOFSTEP]
simpa using @IsRightCancel.right_cancel _ f _ x y z
[GOAL]
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
[PROOFSTEP]
by_cases hx : z = x
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
[PROOFSTEP]
by_cases hy : z = y
[GOAL]
case pos
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
[PROOFSTEP]
simp [hy]
[GOAL]
case neg
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
hx : ¬z = x
hy : ¬z = y
⊢ ↑(Equiv.swap (f x) (f y)) (f z) = f (↑(Equiv.swap x y) z)
[PROOFSTEP]
rw [Equiv.swap_apply_of_ne_of_ne hx hy, Equiv.swap_apply_of_ne_of_ne (hf.ne hx) (hf.ne hy)]
[GOAL]
α' : Sort u_1
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ↑g = update (f ∘ ↑g) (↑g.symm a) v
[PROOFSTEP]
rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]
[GOAL]
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
⊢ ↑(Equiv.piCongrLeft' P e) (update f (↑e.symm b) x) = update (↑(Equiv.piCongrLeft' P e) f) b x
[PROOFSTEP]
ext b'
[GOAL]
case h
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
⊢ ↑(Equiv.piCongrLeft' P e) (update f (↑e.symm b) x) b' = update (↑(Equiv.piCongrLeft' P e) f) b x b'
[PROOFSTEP]
rcases eq_or_ne b' b with (rfl | h)
[GOAL]
case h.inl
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b' : β
x : P (↑e.symm b')
⊢ ↑(Equiv.piCongrLeft' P e) (update f (↑e.symm b') x) b' = update (↑(Equiv.piCongrLeft' P e) f) b' x b'
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
h : b' ≠ b
⊢ ↑(Equiv.piCongrLeft' P e) (update f (↑e.symm b) x) b' = update (↑(Equiv.piCongrLeft' P e) f) b x b'
[PROOFSTEP]
simp only [Equiv.piCongrLeft'_apply, ne_eq, h, not_false_iff, update_noteq]
[GOAL]
case h.inr
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
h : b' ≠ b
⊢ update f (↑e.symm b) x (↑e.symm b') = f (↑e.symm b')
[PROOFSTEP]
rw [update_noteq _]
[GOAL]
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
h : b' ≠ b
⊢ ↑e.symm b' ≠ ↑e.symm b
[PROOFSTEP]
rw [ne_eq]
[GOAL]
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
h : b' ≠ b
⊢ ¬↑e.symm b' = ↑e.symm b
[PROOFSTEP]
intro h'
[GOAL]
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (a : α) → P a
b : β
x : P (↑e.symm b)
b' : β
h : b' ≠ b
h' : ↑e.symm b' = ↑e.symm b
⊢ False
[PROOFSTEP]
cases e.symm.injective h' |> h
[GOAL]
α : Sort u_2
β : Sort u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_1
e : α ≃ β
f : (b : β) → P (↑e.symm b)
b : β
x : P (↑e.symm b)
⊢ ↑(Equiv.piCongrLeft' P e).symm (update f b x) = update (↑(Equiv.piCongrLeft' P e).symm f) (↑e.symm b) x
[PROOFSTEP]
simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]