awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
a : α
h : ¬p a
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (((sumCompl p).symm : (a : α) → { a : α // p a } ⊕ { a : α // ¬p a }) a : { a : α // p a } ⊕ { a : α // ¬p a })
    (Sum.inr (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) : { a : α // p a } ⊕ { a : α // ¬p a })

Tactic:
dif_neg h

Premises used: dif_neg, dite
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : { x : α // p x }
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (((sumCompl p).symm : (a : α) → { a : α // p a } ⊕ { a : α // ¬p a }) (↑x : α) :
      { a : α // p a } ⊕ { a : α // ¬p a })
    (Sum.inl x : { x : α // p x } ⊕ { a : α // ¬p a })

Tactic:
sumCompl_symm_apply_of_pos x.2

Premises used: Subtype.property, Equiv.sumCompl_symm_apply_of_pos
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
p : α → Prop
inst : DecidablePred p
x : { x : α // ¬p x }
⊢ Eq (α := { a : α // p a } ⊕ { a : α // ¬p a })
    (((sumCompl p).symm : (a : α) → { a : α // p a } ⊕ { a : α // ¬p a }) (↑x : α) :
      { a : α // p a } ⊕ { a : α // ¬p a })
    (Sum.inr x : { a : α // p a } ⊕ { x : α // ¬p x })

Tactic:
sumCompl_symm_apply_of_neg x.2

Premises used: Equiv.sumCompl_symm_apply_of_neg, Subtype.property
-- Module: Mathlib.Logic.Equiv.Sum
Goal:
α : Type u_9
β : Type u_10
γ : Type u_11
a : α
b : β
⊢ Eq (α := α × β ⊕ α × γ) ((prodSumDistrib α β γ : (a : α × (β ⊕ γ)) → α × β ⊕ α × γ) (a, inl b) : α × β ⊕ α × γ)
    (inl (a, b) : α × β ⊕ α × γ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)
inl :
  ∀ (i : ι) (a : α i),
    Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
      (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inr)
        ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
            Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inl a))))
      (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inl a))
inr :
  ∀ (i : ι) (b : β i),
    Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
      (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inr)
        ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
            Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
              (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inr b))))
      (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (Sum.inr b))
⊢ Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        p) =
    p

Tactic:
rcases p with ⟨i, a | b⟩
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
i : ι
a : α i
⊢ Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
    (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inl a))))
    (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inl a))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
i : ι
b : β i
⊢ Eq (α := (i : ι) × Sum.{u_9, u_10} (α i) (β i))
    (Sum.elim (α := (i : ι) × α i) (β := (i : ι) × β i)
      (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
      (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inr b))))
    (Sigma.mk (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) i (inr b))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
p : (i : ι) × α i ⊕ (i : ι) × β i
inl :
  ∀ (i : ι) (a : α i),
    Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sum.elim (β := (i : ι) × β i)
          (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦
            Sum.inl)
          (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦
            Sum.inr)
          (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))))
      (Sum.inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))
inr :
  ∀ (i : ι) (b : β i),
    Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
      ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
          Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
            (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
        (Sum.elim (α := (i : ι) × α i)
          (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦
            Sum.inl)
          (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦
            Sum.inr)
          (Sum.inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))))
      (Sum.inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))
⊢ (fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ Sum.inr)
        p) =
    p

Tactic:
rcases p with (⟨i, a⟩ | ⟨i, b⟩)
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
i : ι
a : α i
⊢ Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
    ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim (β := (i : ι) × β i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        (inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))))
    (inl (Sigma.mk (β := fun (i : ι) ↦ α i) i a))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_11
α : ι → Type u_9
β : ι → Type u_10
i : ι
b : β i
⊢ Eq (α := (i : ι) × α i ⊕ (i : ι) × β i)
    ((fun (p : (i : ι) × Sum.{u_9, u_10} (α i) (β i)) ↦
        Sum.map (Sigma.mk (β := fun (i : ι) ↦ α i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (Sigma.mk (β := fun (i : ι) ↦ β i) (p.fst (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
          (p.snd (β := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i))))
      (Sum.elim (α := (i : ι) × α i)
        (Sigma.map (β₁ := fun (i : ι) ↦ α i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inl)
        (Sigma.map (β₁ := fun (i : ι) ↦ β i) (β₂ := fun (i : ι) ↦ Sum.{u_9, u_10} (α i) (β i)) id fun (x : ι) ↦ inr)
        (inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))))
    (inr (Sigma.mk (β := fun (i : ι) ↦ β i) i b))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Sum
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_10
β : Type u_11
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ Sum.elim
      (fun (a : (i : α) × t (inl i)) ↦
        Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl (a.fst (β := fun (i : α) ↦ t (inl i))))
          (a.snd (β := fun (i : α) ↦ t (inl i))))
      (fun (b : (i : β) × t (inr i)) ↦
        Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr (b.fst (β := fun (i : β) ↦ t (inr i))))
          (b.snd (β := fun (i : β) ↦ t (inr i))))
      ((fun (x : (i : α ⊕ β) × t i) ↦
          (match (motive := (i : α ⊕ β) × t i → (i : α) × t (inl i) ⊕ (i : β) × t (inr i)) x with
            | ⟨inl x, y⟩ => inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y)
            | ⟨inr x, y⟩ => inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y) :
            (i : α) × t (inl i) ⊕ (i : β) × t (inr i)))
        (Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl x) y)) =
    Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl x) y

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
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_10
β : Type u_11
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ Sum.elim
      (fun (a : (i : α) × t (inl i)) ↦
        Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl (a.fst (β := fun (i : α) ↦ t (inl i))))
          (a.snd (β := fun (i : α) ↦ t (inl i))))
      (fun (b : (i : β) × t (inr i)) ↦
        Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr (b.fst (β := fun (i : β) ↦ t (inr i))))
          (b.snd (β := fun (i : β) ↦ t (inr i))))
      ((fun (x : (i : α ⊕ β) × t i) ↦
          (match (motive := (i : α ⊕ β) × t i → (i : α) × t (inl i) ⊕ (i : β) × t (inr i)) x with
            | ⟨inl x, y⟩ => inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y)
            | ⟨inr x, y⟩ => inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y) :
            (i : α) × t (inl i) ⊕ (i : β) × t (inr i)))
        (Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr x) y)) =
    Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr x) y

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
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_10
β : Type u_11
t : α ⊕ β → Type u_9
x : α
y : t (inl x)
⊢ Eq (α := (i : α) × t (inl i) ⊕ (i : β) × t (inr i))
    ((fun (x : (i : α ⊕ β) × t i) ↦
        (match (motive := (i : α ⊕ β) × t i → (i : α) × t (inl i) ⊕ (i : β) × t (inr i)) x with
          | ⟨inl x, y⟩ => inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y)
          | ⟨inr x, y⟩ => inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y) :
          (i : α) × t (inl i) ⊕ (i : β) × t (inr i)))
      (Sum.elim
        (fun (a : (i : α) × t (inl i)) ↦
          Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl (a.fst (β := fun (i : α) ↦ t (inl i))))
            (a.snd (β := fun (i : α) ↦ t (inl i))))
        (fun (b : (i : β) × t (inr i)) ↦
          Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr (b.fst (β := fun (i : β) ↦ t (inr i))))
            (b.snd (β := fun (i : β) ↦ t (inr i))))
        (inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y))))
    (inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y))

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Sum
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_10
β : Type u_11
t : α ⊕ β → Type u_9
x : β
y : t (inr x)
⊢ Eq (α := (i : α) × t (inl i) ⊕ (i : β) × t (inr i))
    ((fun (x : (i : α ⊕ β) × t i) ↦
        (match (motive := (i : α ⊕ β) × t i → (i : α) × t (inl i) ⊕ (i : β) × t (inr i)) x with
          | ⟨inl x, y⟩ => inl (Sigma.mk (β := fun (i : α) ↦ t (inl i)) x y)
          | ⟨inr x, y⟩ => inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y) :
          (i : α) × t (inl i) ⊕ (i : β) × t (inr i)))
      (Sum.elim
        (fun (a : (i : α) × t (inl i)) ↦
          Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inl (a.fst (β := fun (i : α) ↦ t (inl i))))
            (a.snd (β := fun (i : α) ↦ t (inl i))))
        (fun (b : (i : β) × t (inr i)) ↦
          Sigma.mk (β := fun (i : α ⊕ β) ↦ t i) (inr (b.fst (β := fun (i : β) ↦ t (inr i))))
            (b.snd (β := fun (i : β) ↦ t (inr i))))
        (inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y))))
    (inr (Sigma.mk (β := fun (i : β) ↦ t (inr i)) x y))

Tactic:
simp
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Prop
w : α
h₁ : p w
h₂ : ∀ (y : α), p y → y = w
⊢ ∃! x : α, p x

Tactic:
⟨w, h₁, h₂⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Prop
b : Prop
h₂ : ∃! x : α, p x
h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = x) → b
⊢ b

Tactic:
Exists.elim h₂ (fun w hw ↦ h₁ w (And.left hw) (And.right hw))

Premises used: And.right, And.left, Exists.elim
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Prop
hex : ∃ (x : α), p x
hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂
⊢ ∃! x : α, p x

Tactic:
Exists.elim hex (fun x px ↦ ExistsUnique.intro x px (fun y (h : p y) ↦ hunique y x h px))

Premises used: ExistsUnique.intro, Exists.elim
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Prop
h : ∃! x : α, p x
y₁ y₂ : α
py₁ : p y₁
py₂ : p y₂
⊢ y₁ = y₂

Tactic:
let ⟨_, _, hy⟩ := h; (hy _ py₁).trans (hy _ py₂).symm

Premises used: _private.0.ExistsUnique.unique.match_1, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Prop
a : α
h : ∃! x : α, p x
⊢ Exists.choose (p := fun (x : α) ↦ (fun (x : α) ↦ p x) x ∧ ∀ (y : α), (fun (x : α) ↦ p x) y → y = x) h = a ↔ p a

Tactic:
⟨fun ha ↦ ha ▸ h.choose_spec.left, h.unique h.choose_spec.left⟩

Premises used: Exists.choose_spec, Eq.rec, And.left, Iff.intro, ExistsUnique.unique
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p q : α → Prop
h : ∀ (a : α), p a ↔ q a
⊢ (∃! a : α, p a) ↔ ∃! a : α, q a

Tactic:
exists_congr fun _ ↦ and_congr (h _) <| forall_congr' fun _ ↦ imp_congr_left (h _)

Premises used: imp_congr_left, exists_congr, ExistsUnique, forall_congr', and_congr
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
inst : Subsingleton α
p : α → Prop
⊢ (∃! x : α, p x) ↔ ∃ (x : α), p x

Tactic:
⟨fun h ↦ h.exists, Exists.imp fun x hx ↦ ⟨hx, fun y _ ↦ Subsingleton.elim y x⟩⟩

Premises used: ExistsUnique.exists, Exists.imp, And.intro, Iff.intro, Subsingleton.elim
-- Module: Mathlib.Logic.ExistsUnique
Goal:
b : Prop
α : Sort u_2
i : Nonempty α
inst : Subsingleton α
⊢ (∃! x : α, b) ↔ b

Tactic:
simp
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
a' : α
⊢ ∃! a : α, a = a'

Tactic:
simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']

Premises used: and_self, forall_eq', eq_comm, exists_eq', ExistsUnique
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
a' : α
⊢ ∃! a : α, a' = a

Tactic:
simp only [ExistsUnique, and_self, forall_eq', exists_eq']

Premises used: and_self, forall_eq', exists_eq', ExistsUnique
-- Module: Mathlib.Logic.ExistsUnique
Goal:
p q : Prop
⊢ (∃! x : p, q) ↔ p ∧ q

Tactic:
simp
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
⊢ ¬∃! x : α, False

Tactic:
fun ⟨_, h, _⟩ ↦ h

Premises used: False, _private.0.existsUnique_false.match_1, Not
-- Module: Mathlib.Logic.ExistsUnique
Goal:
p : Prop
q : p → Prop
h : p
⊢ (∃! h' : p, q h') ↔ q h

Tactic:
@existsUnique_const (q h) p ⟨h⟩ _

Premises used: existsUnique_const
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x : α, ∃! h : p x, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ ∃! x : α, ∃ (h : p x), q x h

Tactic:
simp only [existsUnique_iff_exists] at h₂

Premises used: existsUnique_iff_exists
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x : α, ∃ (h : p x), q x h
apply : ∀ (x : α), (∃ (h : p x), q x h) → (∀ (y : α), (∃ (h : p y), q y h) → y = x) → b
⊢ b

Tactic:
apply h₂.elim

Premises used: ExistsUnique.elim
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x : α, ∃ (h : p x), q x h
⊢ ∀ (x : α), (∃ (h : p x), q x h) → (∀ (y : α), (∃ (h : p y), q y h) → y = x) → b

Tactic:
fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩

Premises used: Exists.intro, _private.0.ExistsUnique.elim₂.match_1
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x : α, ∃ (h : p x), q x h
⊢ ∀ (x : α), (∃ (h : p x), q x h) → (∀ (y : α), (∃ (h : p y), q y h) → y = x) → b

Tactic:
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
simp : ∃! x : α, ∃ (hx : p x), q x hx
⊢ ∃! x : α, ∃! hx : p x, q x hx

Tactic:
simp only [existsUnique_iff_exists]

Premises used: existsUnique_iff_exists
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x : α, ∃ (hx : p x), q x hx

Tactic:
ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

Premises used: ExistsUnique.intro, Exists.intro, Eq, _private.0.ExistsUnique.elim₂.match_1
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x : α, ∃ (hx : p x), q x hx

Tactic:
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq

Premises used: ExistsUnique.intro
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
q : (x : α) → p x → Prop
h : ∃! x : α, ∃! hx : p x, q x hx
⊢ ∃ (x : α), ∃ (hx : p x), q x hx

Tactic:
h.exists.imp fun _ hx ↦ hx.exists

Premises used: ExistsUnique.exists, Exists.imp
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
h : ∃! x : α, ∃! hx : p x, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ ∃! x : α, ∃ (hx : p x), q x hx

Tactic:
simp only [existsUnique_iff_exists] at h

Premises used: existsUnique_iff_exists
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x : α, ∃ (hx : p x), q x hx
⊢ y₁ = y₂

Tactic:
h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Premises used: Exists.intro, ExistsUnique.unique
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α : Sort u_1
p : α → Sort u_2
inst : ∀ (x : α), Subsingleton.{u_2} (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x : α, ∃ (hx : p x), q x hx
⊢ y₁ = y₂

Tactic:
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩

Premises used: Exists.intro, ExistsUnique.unique
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α_1 : Sort u_1
α : Type u_2
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
⊢ ¬∃! x : α, Membership.mem (γ := List α) [] x ∧ p x

Tactic:
simp
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α_1 : Sort u_1
α : Type u_2
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
x : α
xs : List α
hx : p x
h : ∀ (y : α), y ∈ xs → p y → x = y
⊢ (fun (x_1 : α) ↦ x_1 ∈ x :: xs ∧ p x_1) x ∧ ∀ (y : α), (fun (x_1 : α) ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = x

Tactic:
grind
-- Module: Mathlib.Logic.ExistsUnique
Goal:
α_1 : Sort u_1
α : Type u_2
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
x : α
xs : List α
hx : p x
h_1 : ∃! x_1 : α, x_1 ∈ x :: xs ∧ p x_1
y : α
hy : y ∈ xs
hp : p y
z : α
h : (fun (x_1 : α) ↦ x_1 ∈ x :: xs ∧ p x_1) z ∧ ∀ (y : α), (fun (x_1 : α) ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = z
⊢ z = y

Tactic:
grind