awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ RightInverse (fun (ab : α₁ × β₂) ↦ (ab.fst, ((e ab.fst).symm : (a : β₂) → β₁) ab.snd)) fun (ab : α₁ × β₁) ↦
    (ab.fst, (e ab.fst : (a : β₁) → β₂) ab.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ Eq (α := α₁ × β₂) ((prodCongrRight e : (a : α₁ × β₁) → α₁ × β₂) (a, b) : α₁ × β₂)
    ((a, (e a : (a : β₁) → β₂) b) : α₁ × β₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
⊢ (Equiv.refl α₁).prodCongr e = prodCongrRight fun (x : α₁) ↦ e

Tactic:
rfl

Premises used: Equiv.prodCongrRight, Prod.map, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).symm = prodCongrRight (Equiv.symm ∘ e)

Tactic:
rfl

Premises used: Equiv.prodCongrRight, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
H :
  ∀ (a : β₁) (b : α₁),
    Eq (α := α₁ × β₂) (((prodCongrLeft e).trans (prodComm β₂ α₁) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)
      (((prodComm β₁ α₁).trans (prodCongrRight e) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)

Tactic:
ext ⟨a, b⟩ : 1
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ Eq (α := α₁ × β₂) (((prodCongrLeft e).trans (prodComm β₂ α₁) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)
    (((prodComm β₁ α₁).trans (prodCongrRight e) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
H :
  ∀ (a : α₁) (b : β₁),
    Eq (α := β₂ × α₁) (((prodCongrRight e).trans (prodComm α₁ β₂) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)
      (((prodComm α₁ β₁).trans (prodCongrLeft e) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)

Tactic:
ext ⟨a, b⟩ : 1
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ Eq (α := β₂ × α₁) (((prodCongrRight e).trans (prodComm α₁ β₂) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)
    (((prodComm α₁ β₁).trans (prodCongrLeft e) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
H :
  ∀ (a : α₁) (b : β₁),
    Eq (α := α₁ × β₂)
      (((sigmaCongrRight (β₁ := fun (a : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e).trans (sigmaEquivProd α₁ β₂) :
            (a : (_ : α₁) × β₁) → α₁ × β₂)
          (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
        α₁ × β₂)
      (((sigmaEquivProd α₁ β₁).trans (prodCongrRight e) : (a : (_ : α₁) × β₁) → α₁ × β₂)
          (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
        α₁ × β₂)
⊢ (sigmaCongrRight (β₁ := fun (a : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e).trans (sigmaEquivProd α₁ β₂) =
    (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)

Tactic:
ext ⟨a, b⟩ : 1
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ Eq (α := α₁ × β₂)
    (((sigmaCongrRight (β₁ := fun (a : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e).trans (sigmaEquivProd α₁ β₂) :
          (a : (_ : α₁) × β₁) → α₁ × β₂)
        (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
      α₁ × β₂)
    (((sigmaEquivProd α₁ β₁).trans (prodCongrRight e) : (a : (_ : α₁) × β₁) → α₁ × β₂)
        (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
      α₁ × β₂)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
H :
  ∀ (a : α₁) (b : β₁),
    Eq (α := (_ : α₁) × β₂)
      (((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) :
            (a : α₁ × β₁) → (_ : α₁) × β₂)
          (a, b) :
        (_ : α₁) × β₂)
      (((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₁) → (_ : α₁) × β₂) (a, b) : (_ : α₁) × β₂)
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) =
    (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm

Tactic:
ext ⟨a, b⟩ : 1
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
H :
  Eq (α := (_ : α₁) × β₂)
    (Sigma.mk (β := fun (a : α₁) ↦ β₂)
        (Sigma.fst (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)))
        ((e
              (Sigma.fst (β := fun (a : α₁) ↦ β₁)
                (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b))) :
            (a : β₁) → β₂)
          (Sigma.snd (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)) :
            β₁)) :
      (_ : α₁) × β₂)
    (((sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₂) → (_ : α₁) × β₂) (a, (e a : (a : β₁) → β₂) b) : (_ : α₁) × β₂)
⊢ Eq (α := (_ : α₁) × β₂)
    (((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) :
          (a : α₁ × β₁) → (_ : α₁) × β₂)
        (a, b) :
      (_ : α₁) × β₂)
    (((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₁) → (_ : α₁) × β₂) (a, b) : (_ : α₁) × β₂)

Tactic:
simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]

Premises used: Equiv.trans_apply, Equiv.sigmaCongrRight_apply, Equiv.prodCongrRight_apply
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ Eq (α := (_ : α₁) × β₂)
    (Sigma.mk (β := fun (a : α₁) ↦ β₂)
        (Sigma.fst (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)))
        ((e
              (Sigma.fst (β := fun (a : α₁) ↦ β₁)
                (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b))) :
            (a : β₁) → β₂)
          (Sigma.snd (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)) :
            β₁)) :
      (_ : α₁) × β₂)
    (((sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₂) → (_ : α₁) × β₂) (a, (e a : (a : β₁) → β₂) b) : (_ : α₁) × β₂)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ LeftInverse
    (fun (y : α₂ × β₂) ↦
      ((e₁.symm : (a : α₂) → α₁) y.fst, ((e₂ ((e₁.symm : (a : α₂) → α₁) y.fst)).symm : (a : β₂) → β₁) y.snd))
    fun (x : α₁ × β₁) ↦ ((e₁ : (a : α₁) → α₂) x.fst, (e₂ x.fst : (a : β₁) → β₂) x.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂_1 : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
e₁ : α₁ ≃ α₂
e₂ : α₁ → β₁ ≃ β₂
⊢ RightInverse
    (fun (y : α₂ × β₂) ↦
      ((e₁.symm : (a : α₂) → α₁) y.fst, ((e₂ ((e₁.symm : (a : α₂) → α₁) y.fst)).symm : (a : β₂) → β₁) y.snd))
    fun (x : α₁ × β₁) ↦ ((e₁ : (a : α₁) → α₂) x.fst, (e₂ x.fst : (a : β₁) → β₂) x.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ LeftInverse (fun (ab : α₁ × β₁) ↦ if ab.fst = a then (a, (Equiv.symm e : (a : β₁) → β₁) ab.snd) else ab)
    fun (ab : α₁ × β₁) ↦ if ab.fst = a then (a, (e : (a : β₁) → β₁) ab.snd) else ab

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁_1 : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
a : α₁
e : Perm β₁
⊢ RightInverse (fun (ab : α₁ × β₁) ↦ if ab.fst = a then (a, (Equiv.symm e : (a : β₁) → β₁) ab.snd) else ab)
    fun (ab : α₁ × β₁) ↦ if ab.fst = a then (a, (e : (a : β₁) → β₁) ab.snd) else ab

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
a : α₁
e : Perm β₁
b : β₁
⊢ Eq (α := α₁ × β₁) ((prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a, b) : α₁ × β₁)
    ((a, (e : (a : β₁) → β₁) b) : α₁ × β₁)

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
e : Perm β₁
a a' : α₁
h : a' ≠ a
b : β₁
⊢ (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) = (a', b)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) ≠ (a', b)
contrapose! : ∀ (h : a' ≠ a), (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) = (a', b)
⊢ a' = a

Tactic:
contrapose! h
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : a' ≠ a
⊢ (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) = (a', b)

Tactic:
prodExtendRight_apply_ne _ h _

Premises used: Equiv.Perm.prodExtendRight_apply_ne
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : a' ≠ a
⊢ (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) = (a', b)

Tactic:
exact prodExtendRight_apply_ne _ h _

Premises used: Equiv.Perm.prodExtendRight_apply_ne
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
a : α₁
e : Perm β₁
ab : α₁ × β₁
⊢ Prod.fst.{u_9, u_10} (β := β₁) ((prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) ab) = ab.fst

Tactic:
grind [prodExtendRight]

Premises used: Equiv.Perm.prodExtendRight
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_10
ι' : Type u_11
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
h :
  ∀ (i : ι),
    Eq (α := π (inl i))
      ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
          Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
        ((fun (f : (i : ι ⊕ ι') → π i) ↦
            ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
          f)
        (inl i))
      (f (inl i))
h₁ :
  ∀ (i : ι'),
    Eq (α := π (inr i))
      ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
          Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
        ((fun (f : (i : ι ⊕ ι') → π i) ↦
            ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
          f)
        (inr i))
      (f (inr i))
⊢ (fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f) =
    f

Tactic:
ext (i | i)
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_10
ι' : Type u_11
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
i : ι
⊢ Eq (α := π (inl i))
    ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f)
      (inl i))
    (f (inl i))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_10
ι' : Type u_11
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
i : ι'
⊢ Eq (α := π (inr i))
    ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f)
      (inr i))
    (f (inr i))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
h :
  ∀ (val : α),
    (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inl val) =
      f (inl val)
h₁ :
  ∀ (val : β),
    (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inr val) =
      f (inr val)
⊢ (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) = f

Tactic:
ext ⟨⟩
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
val : α
⊢ (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inl val) =
    f (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
val : β
⊢ (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inr val) =
    f (inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
p : (α → γ) × (β → γ)
mk :
  ∀ (fst : α → γ) (snd : β → γ),
    (fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) ((fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) (fst, snd)) =
      (fst, snd)
⊢ (fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) ((fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) p) = p

Tactic:
cases p
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
fst : α → γ
snd : β → γ
⊢ (fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) ((fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) (fst, snd)) =
    (fst, snd)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
a : α
⊢ Prod.fst (β := β → γ) ((sumArrowEquivProdArrow α β γ : (a : α ⊕ β → γ) → (α → γ) × (β → γ)) f) a = f (inl a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
f : α ⊕ β → γ
b : β
⊢ Prod.snd (α := α → γ) ((sumArrowEquivProdArrow α β γ : (a : α ⊕ β → γ) → (α → γ) × (β → γ)) f) b = f (inr b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
f : α → γ
g : β → γ
a : α
⊢ ((sumArrowEquivProdArrow α β γ).symm : (a : (α → γ) × (β → γ)) → α ⊕ β → γ) (f, g) (inl a) = f a

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
f : α → γ
g : β → γ
b : β
⊢ ((sumArrowEquivProdArrow α β γ).symm : (a : (α → γ) × (β → γ)) → α ⊕ β → γ) (f, g) (inr b) = g b

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
snd : γ
val : α
⊢ Eq (α := (α ⊕ β) × γ)
    ((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)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
snd : γ
val : β
⊢ Eq (α := (α ⊕ β) × γ)
    ((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)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
fst : α
snd : γ
⊢ Eq (α := α × γ ⊕ β × γ)
    ((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))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : Type u_11
fst : β
snd : γ
⊢ Eq (α := α × γ ⊕ β × γ)
    ((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))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
a : α
c : γ
⊢ Eq (α := α × γ ⊕ β × γ) ((sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (inl a, c) : α × γ ⊕ β × γ)
    (inl (a, c) : α × γ ⊕ β × γ)

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
b : β
c : γ
⊢ Eq (α := α × γ ⊕ β × γ) ((sumProdDistrib α β γ : (a : (α ⊕ β) × γ) → α × γ ⊕ β × γ) (inr b, c) : α × γ ⊕ β × γ)
    (inr (b, c) : α × γ ⊕ β × γ)

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
a : α × γ
⊢ Eq (α := (α ⊕ β) × γ) (((sumProdDistrib α β γ).symm : (a : α × γ ⊕ β × γ) → (α ⊕ β) × γ) (inl a) : (α ⊕ β) × γ)
    ((inl a.fst, a.snd) : (α ⊕ β) × γ)

Tactic:
rfl

Premises used: Prod.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
b : β × γ
⊢ Eq (α := (α ⊕ β) × γ) (((sumProdDistrib α β γ).symm : (a : α × γ ⊕ β × γ) → (α ⊕ β) × γ) (inr b) : (α ⊕ β) × γ)
    ((inr b.fst, b.snd) : (α ⊕ β) × γ)

Tactic:
rfl

Premises used: Prod.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_9
α : ι → Type u_10
β : Type u_11
⊢ LeftInverse
    (fun (p : (i : ι) × Prod.{u_10, u_11} (α i) β) ↦
      (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β))
          p.snd (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β).fst,
        p.snd (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β).snd))
    fun (p : ((i : ι) × α i) × β) ↦
    Sigma.mk (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β) (p.fst.fst (β := fun (i : ι) ↦ α i))
      (p.fst.snd (β := fun (i : ι) ↦ α i), p.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type u_9
α : ι → Type u_10
β : Type u_11
⊢ RightInverse
    (fun (p : (i : ι) × Prod.{u_10, u_11} (α i) β) ↦
      (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β))
          p.snd (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β).fst,
        p.snd (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β).snd))
    fun (p : ((i : ι) × α i) × β) ↦
    Sigma.mk (β := fun (i : ι) ↦ Prod.{u_10, u_11} (α i) β) (p.fst.fst (β := fun (i : ι) ↦ α i))
      (p.fst.snd (β := fun (i : ι) ↦ α i), p.snd)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
snd : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true)
      ((fun (p : Bool × α) ↦ if p.fst = true then inr p.snd else inl p.snd) (false, snd)) =
    (false, snd)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
snd : α
⊢ Sum.elim (Prod.mk false) (Prod.mk true)
      ((fun (p : Bool × α) ↦ if p.fst = true then inr p.snd else inl p.snd) (true, snd)) =
    (true, snd)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
val : α
⊢ Eq (α := α ⊕ α)
    ((fun (p : Bool × α) ↦ if p.fst = true then inr p.snd else inl p.snd)
      (Sum.elim (Prod.mk false) (Prod.mk true) (inl val)))
    (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
val : α
⊢ Eq (α := α ⊕ α)
    ((fun (p : Bool × α) ↦ if p.fst = true then inr p.snd else inl p.snd)
      (Sum.elim (Prod.mk false) (Prod.mk true) (inr val)))
    (inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
x : Bool → α
⊢ (fun (p : α × α) (b : Bool) ↦ if b = true then p.snd else p.fst) ((fun (f : Bool → α) ↦ (f false, f true)) x) = x

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : α) → β i
⊢ (fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
        (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
          else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
          β x))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        f) =
    f

Tactic:
grind