awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
x_1 : { a : α // ¬p a }
a : α
h : ¬p a
dsimp :
  (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
⊢ (if h_1 : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) (↑(Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) : α) h_1)
    else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) (↑(Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) : α) h_1)) =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)

Tactic:
dsimp only
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
x_1 : { a : α // ¬p a }
a : α
h : ¬p a
rw rw₁ : x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) = x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
⊢ (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
a : α
h : p a
⊢ (↑(((subtypePreimage p x₀).symm : (a : { a : α // ¬p a } → β) → { x : α → β // x ∘ Subtype.val = x₀ }) x) : α → β) a =
    x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h)

Tactic:
dif_pos h

Premises used: dif_pos, dite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
a : α
h : ¬p a
⊢ (↑(((subtypePreimage p x₀).symm : (a : { a : α // ¬p a } → β) → { x : α → β // x ∘ Subtype.val = x₀ }) x) : α → β) a =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)

Tactic:
dif_neg h

Premises used: dif_neg, dite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
β₁ : α → Sort u_9
β₂ : α → Sort u_10
F : (a : α) → Equiv.{u_9, u_10} (β₁ a) (β₂ a)
H : (a : α) → β₁ a
⊢ ∀ (x : α),
    Pi.map (α := β₂) (β := β₁) (fun (a : α) ↦ (⇑(F a).symm : (a_1 : β₂ a) → β₁ a))
        (Pi.map (α := β₁) (β := β₂) (fun (a : α) ↦ (⇑(F a) : (a_1 : β₁ a) → β₂ a)) H) x =
      H x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁_1 : Sort u_5
β₂_1 : Sort u_6
γ : Sort u_7
δ : Sort u_8
β₁ : α → Sort u_9
β₂ : α → Sort u_10
F : (a : α) → Equiv.{u_9, u_10} (β₁ a) (β₂ a)
H : (a : α) → β₂ a
⊢ ∀ (x : α),
    Pi.map (α := β₁) (β := β₂) (fun (a : α) ↦ (⇑(F a) : (a_1 : β₁ a) → β₂ a))
        (Pi.map (α := β₂) (β := β₁) (fun (a : α) ↦ (⇑(F a).symm : (a_1 : β₂ a) → β₁ a)) H) x =
      H x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : α → Sort u_9
⊢ Eq (α := ((a : α) → β a) ≃ ((a : α) → β a)) (piCongrRight (β₁ := β) (β₂ := β) fun (a : α) ↦ Equiv.refl (β a))
    (Equiv.refl ((a : α) → β a))

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
φ : α → β → Sort u_9
⊢ (piComm φ).symm = piComm (swap (φ := fun (a : α) (a_1 : β) ↦ Sort u_9) φ)

Tactic:
rfl

Premises used: Equiv.piComm, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_11
β : α → Type u_9
γ : (a : α) → β a → Type u_10
f : (x : (i : α) × β i) → γ (x.fst (β := fun (i : α) ↦ β i)) (x.snd (β := fun (i : α) ↦ β i))
⊢ (piCurry (β := β) γ : (a : (x : (i : α) × β i) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b) f =
    Sigma.curry (β := fun (i : α) ↦ β i) (γ := γ) f

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_11
β : α → Type u_9
γ : (a : α) → β a → Type u_10
f : (a : α) → (b : β a) → γ a b
⊢ ((piCurry (β := β) γ).symm : (a : (a : α) → (b : β a) → γ a b) → (x : (i : α) × β i) → γ x.fst x.snd) f =
    Sigma.uncurry (β := β) (γ := γ) f

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_13
β : Type u_14
γ : Type u_15
f : α → γ
g : β → γ
e : (c : γ) → Equiv.{u_13 + 1, u_14 + 1} { a : α // f a = c } { b : β // g b = c }
a : α
⊢ g ((ofFiberEquiv e : (a : α) → β) a) = f a

Tactic:
(_ : { b // g b = _ }).property

Premises used: Subtype.property
-- Module: Mathlib.Logic.Equiv.Basic
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
f : ℕ → Type u
x : f 0
⊢ Sum.elim (α := f 0) (β := (n : ℕ) × f (n + 1)) (Sigma.mk (β := f) 0)
      (Sigma.map (β₁ := fun (n : ℕ) ↦ f (n + 1)) (β₂ := fun (n : ℕ) ↦ f n) Nat.succ fun (x : ℕ) ↦ id)
      ((fun (x : (n : ℕ) × f n) ↦
          (Sigma.casesOn (β := f) (motive := fun (x : Sigma f) ↦ f 0 ⊕ (n : ℕ) × f (n + 1)) x fun (n : ℕ) ↦
              Nat.casesOn (motive := fun (i : ℕ) ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun (x : f 0) ↦ inl x)
                fun (n : ℕ) (x : f n.succ) ↦ inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x) :
            f 0 ⊕ (n : ℕ) × f (n + 1)))
        (Sigma.mk (β := fun (n : ℕ) ↦ f n) 0 x)) =
    Sigma.mk (β := fun (n : ℕ) ↦ f n) 0 x

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ Sum.elim (α := f 0) (β := (n : ℕ) × f (n + 1)) (Sigma.mk (β := f) 0)
      (Sigma.map (β₁ := fun (n : ℕ) ↦ f (n + 1)) (β₂ := fun (n : ℕ) ↦ f n) Nat.succ fun (x : ℕ) ↦ id)
      ((fun (x : (n : ℕ) × f n) ↦
          (Sigma.casesOn (β := f) (motive := fun (x : Sigma f) ↦ f 0 ⊕ (n : ℕ) × f (n + 1)) x fun (n : ℕ) ↦
              Nat.casesOn (motive := fun (i : ℕ) ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun (x : f 0) ↦ inl x)
                fun (n : ℕ) (x : f n.succ) ↦ inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x) :
            f 0 ⊕ (n : ℕ) × f (n + 1)))
        (Sigma.mk (β := fun (n : ℕ) ↦ f n) (n + 1) x)) =
    Sigma.mk (β := fun (n : ℕ) ↦ f n) (n + 1) x

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
f : ℕ → Type u
x : f 0
⊢ Eq (α := f 0 ⊕ (n : ℕ) × f (n + 1))
    ((fun (x : (n : ℕ) × f n) ↦
        (Sigma.casesOn (β := f) (motive := fun (x : Sigma f) ↦ f 0 ⊕ (n : ℕ) × f (n + 1)) x fun (n : ℕ) ↦
            Nat.casesOn (motive := fun (i : ℕ) ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun (x : f 0) ↦ inl x)
              fun (n : ℕ) (x : f n.succ) ↦ inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x) :
          f 0 ⊕ (n : ℕ) × f (n + 1)))
      (Sum.elim (β := (n : ℕ) × f (n + 1)) (Sigma.mk (β := f) 0)
        (Sigma.map (β₁ := fun (n : ℕ) ↦ f (n + 1)) (β₂ := fun (n : ℕ) ↦ f n) Nat.succ fun (x : ℕ) ↦ id) (inl x)))
    (inl x)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
f : ℕ → Type u
n : ℕ
x : f (n + 1)
⊢ Eq.{u + 1} (α := f 0 ⊕ (n : ℕ) × f (n + 1))
    ((fun (x : (n : ℕ) × f n) ↦
        (Sigma.casesOn (β := f) (motive := fun (x : Sigma f) ↦ f 0 ⊕ (n : ℕ) × f (n + 1)) x fun (n : ℕ) ↦
            Nat.casesOn (motive := fun (i : ℕ) ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun (x : f 0) ↦ inl x)
              fun (n : ℕ) (x : f n.succ) ↦ inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x) :
          f 0 ⊕ (n : ℕ) × f (n + 1)))
      (Sum.elim (α := f 0) (β := (n : ℕ) × f (n + 1)) (Sigma.mk (β := f) 0)
        (Sigma.map (β₁ := fun (n : ℕ) ↦ f (n + 1)) (β₂ := fun (n : ℕ) ↦ f n) Nat.succ fun (x : ℕ) ↦ id)
        (inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x))))
    (inr (Sigma.mk (β := fun (n : ℕ) ↦ f (n + 1)) n x))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
n : ℕ
zero :
  Sum.elim Nat.succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) 0) =
    0
succ :
  ∀ (n : ℕ),
    Sum.elim Nat.succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
        ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) (n + 1)) =
      n + 1
⊢ Sum.elim Nat.succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) n) =
    n

Tactic:
cases n
-- Module: Mathlib.Logic.Equiv.Basic
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
⊢ Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) 0) =
    0

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
n : ℕ
⊢ Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) (n + 1)) =
    n + 1

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
val : ℕ
⊢ Eq.{u_9 + 1} (α := ℕ ⊕ PUnit)
    ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit))
      (Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0) (inl val)))
    (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
val : PUnit
⊢ Eq (α := ℕ ⊕ PUnit)
    ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit))
      (Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0) (inr val)))
    (inr val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
m : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc
      ((fun (z : ℤ) ↦ (Int.casesOn (motive := fun (x : ℤ) ↦ ℕ ⊕ ℕ) z inl inr : ℕ ⊕ ℕ)) (Int.ofNat m)) =
    Int.ofNat m

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
n : ℕ
⊢ Sum.elim Int.ofNat Int.negSucc
      ((fun (z : ℤ) ↦ (Int.casesOn (motive := fun (x : ℤ) ↦ ℕ ⊕ ℕ) z inl inr : ℕ ⊕ ℕ)) (Int.negSucc n)) =
    Int.negSucc n

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
m : ℕ
⊢ Eq (α := ℕ ⊕ ℕ)
    ((fun (z : ℤ) ↦ (Int.casesOn (motive := fun (x : ℤ) ↦ ℕ ⊕ ℕ) z inl inr : ℕ ⊕ ℕ))
      (Sum.elim Int.ofNat Int.negSucc (inl m)))
    (inl m)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
n : ℕ
⊢ Eq (α := ℕ ⊕ ℕ)
    ((fun (z : ℤ) ↦ (Int.casesOn (motive := fun (x : ℤ) ↦ ℕ ⊕ ℕ) z inl inr : ℕ ⊕ ℕ))
      (Sum.elim Int.ofNat Int.negSucc (inr n)))
    (inr n)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
e : α ≃ β
⊢ IsEmpty α ↔ IsEmpty β

Tactic:
⟨fun h => @Function.isEmpty _ _ h e.symm, fun h => @Function.isEmpty _ _ h e⟩

Premises used: Function.isEmpty, Iff.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
e : α ≃ β
inst : IsEmpty β
⊢ IsEmpty α

Tactic:
e.isEmpty_congr.mpr ‹_›

Premises used: Iff.mpr, Equiv.isEmpty_congr
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
a : { a : α // p a }
⊢ (↑((fun (b : { b : β // q b }) ↦
            (Subtype.mk (p := fun (a : α) ↦ p a) ((e.symm : (a : β) → α) (↑b : β)) ⋯ : { a : α // p a }))
          ((fun (a : { a : α // p a }) ↦
              (Subtype.mk (p := fun (b : β) ↦ q b) ((e : (a : α) → β) (↑a : α)) ⋯ : { b : β // q b }))
            a)) :
      α) =
    (↑a : α)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
b : { b : β // q b }
⊢ (↑((fun (a : { a : α // p a }) ↦
            (Subtype.mk (p := fun (b : β) ↦ q b) ((e : (a : α) → β) (↑a : α)) ⋯ : { b : β // q b }))
          ((fun (b : { b : β // q b }) ↦
              (Subtype.mk (p := fun (a : α) ↦ p a) ((e.symm : (a : β) → α) (↑b : β)) ⋯ : { a : α // p a }))
            b)) :
      β) =
    (↑b : β)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
p : X → Prop
q : Y → Prop
e : X ≃ Y
h : ∀ (x : X), p x ↔ q ((e : (a : X) → Y) x)
⊢ Eq (α := (a : { a : X // p a }) → { b : Y // q b })
    (⇑(e.subtypeEquiv (p := p) (q := q) h) : (a : { a : X // p a }) → { b : Y // q b })
    (map (p := p) (q := q) (⇑e : (a : X) → Y) ⋯)

Tactic:
rfl

Premises used: Subtype.map, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α : (a : α) → α) a)
H :
  ∀ (x : { a : α // p a }),
    Eq.{u_1} (α := α)
      (↑(((Equiv.refl α).subtypeEquiv (p := p) (q := p) h : (a : { a : α // p a }) → { a : α // p a }) x) : α)
      (↑((Equiv.refl.{max 1 u_1} { a : α // p a } : (a : { a : α // p a }) → { a : α // p a }) x) : α)
⊢ Eq.{max 1 u_1} ((Equiv.refl α).subtypeEquiv (p := p) (q := p) h) (Equiv.refl.{max 1 u_1} { a : α // p a })

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α : (a : α) → α) a)
x : { a : α // p a }
⊢ Eq.{u_1} (α := α)
    (↑(((Equiv.refl α).subtypeEquiv (p := p) (q := p) h : (a : { a : α // p a }) → { a : α // p a }) x) : α)
    (↑((Equiv.refl.{max 1 u_1} { a : α // p a } : (a : { a : α // p a }) → { a : α // p a }) x) : α)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ ∀ (a : β), q a ↔ p ((e.symm : (a : β) → α) a)

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ ∀ (a : β), q a ↔ p ((e.symm : (a : β) → α) a)

Tactic:
as_aux_lemma => grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
⊢ Equiv.symm.{max 1 u_1, max 1 u_4} (e.subtypeEquiv (p := p) (q := q) h) = e.symm.subtypeEquiv (p := q) (q := p) ⋯

Tactic:
rfl

Premises used: Equiv.subtypeEquiv, Equiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
h' : ∀ (b : β), q b ↔ r ((f : (a : β) → γ) b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f : (a : α) → γ) a)

Tactic:
fun a => (h a).trans (h' <| e a)

Premises used: Iff.trans, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
h' : ∀ (b : β), q b ↔ r ((f : (a : β) → γ) b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f : (a : α) → γ) a)

Tactic:
exact fun a => (h a).trans (h' <| e a)

Premises used: Iff.trans, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
h' : ∀ (b : β), q b ↔ r ((f : (a : β) → γ) b)
⊢ ∀ (a : α), p a ↔ r ((e.trans f : (a : α) → γ) a)

Tactic:
as_aux_lemma => exact fun a => (h a).trans (h' <| e a)

Premises used: Iff.trans, DFunLike.coe
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
β : Sort u_4
γ : Sort u_7
p : α → Prop
q : β → Prop
r : γ → Prop
e : α ≃ β
f : β ≃ γ
h : ∀ (a : α), p a ↔ q ((e : (a : α) → β) a)
h' : ∀ (b : β), q b ↔ r ((f : (a : β) → γ) b)
⊢ Equiv.trans.{max 1 u_1, max 1 u_4, max 1 u_7} (e.subtypeEquiv (p := p) (q := q) h)
      (f.subtypeEquiv (p := q) (q := r) h') =
    (e.trans f).subtypeEquiv (p := p) (q := r) ⋯

Tactic:
rfl

Premises used: Equiv.subtypeEquiv, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p q : α → Prop
e : ∀ (x : α), p x ↔ q x
z : { x : α // p x }
⊢ Eq.{max 1 u_1} ((subtypeEquivRight (p := p) (q := q) e : (a : { x : α // p x }) → { x : α // q x }) z)
    (Subtype.mk (p := fun (x : α) ↦ q x) (↑z : α) ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
p q : α → Prop
e : ∀ (x : α), p x ↔ q x
z : { x : α // q x }
⊢ Eq.{max 1 u_1}
    ((Equiv.symm.{max 1 u_1, max 1 u_1} (subtypeEquivRight (p := p) (q := q) e) :
        (a : { x : α // q x }) → { x : α // p x })
      z)
    (Subtype.mk (p := fun (x : α) ↦ p x) (↑z : α) ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
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
p : β → Prop
e : α ≃ β
⊢ ∀ (a : α), p ((e : (a : α) → β) a) ↔ p ((e : (a : α) → β) a)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : Subtype p → Prop
a : Subtype.{max 1 u_1} q
rcases :
  ∀ (a : α) (hap : p a) (haq : q (Subtype.mk (p := p) a hap)),
    q (Subtype.mk (p := p) (↑(↑(Subtype.mk.{max 1 u_1} (p := q) (Subtype.mk (p := p) a hap) haq) : Subtype p) : α) ⋯)
⊢ q (Subtype.mk (p := p) (↑(↑a : Subtype p) : α) ⋯)

Tactic:
rcases a with ⟨⟨a, hap⟩, haq⟩
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : Subtype p → Prop
a : α
hap : p a
haq : q (Subtype.mk (p := p) a hap)
⊢ q (Subtype.mk (p := p) (↑(↑(Subtype.mk.{max 1 u_1} (p := q) (Subtype.mk (p := p) a hap) haq) : Subtype p) : α) ⋯)

Tactic:
haq
-- Module: Mathlib.Logic.Equiv.Basic
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
p : α → Prop
q : Subtype p → Prop
a : α
hap : p a
haq : q (Subtype.mk (p := p) a hap)
⊢ q (Subtype.mk (p := p) (↑(↑(Subtype.mk.{max 1 u_1} (p := q) (Subtype.mk (p := p) a hap) haq) : Subtype p) : α) ⋯)

Tactic:
exact haq
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
F : (a : Subtype q) → { x : α // f x = (↑a : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = a }
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }

Tactic:
apply sigmaCongrRight

Premises used: Equiv.sigmaCongrRight
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
F : { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y } ≃ { x : α // f x = (↑y : β) }
⊢ { x : α // f x = (↑y : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }

Tactic:
apply Equiv.symm

Premises used: Equiv.symm
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
F : ∀ (x : α), (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) ⋯ = y) ↔ f x = (↑y : β)
⊢ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y } ≃ { x : α // f x = (↑y : β) }

Tactic:
refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)

Premises used: Equiv.trans, Equiv.subtypeEquivRight, Equiv.subtypeSubtypeEquivSubtypeExists
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
x : α
⊢ (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) ⋯ = y) ↔ f x = (↑y : β)

Tactic:
⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩

Premises used: Iff.mpr, Equiv.sigmaSubtypeFiberEquivSubtype.match_1, Eq.rec, congr_arg, Iff.intro, Exists.intro, Eq.symm, Subtype.val, Eq, Subtype.property, Subtype.ext
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
x : α
⊢ (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) ⋯ = y) ↔ f x = (↑y : β)

Tactic:
exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩
-- Module: Mathlib.Logic.Equiv.Basic
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
F F₁ : (y : Subtype q) → { x : α // f x = (↑y : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
F₂ : (y : Subtype q) → { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y } ≃ { x : α // f x = (↑y : β) }
F₃ F₄ :
  ∀ (y : Subtype q) (x : α),
    (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) ⋯ = y) ↔ f x = (↑y : β)
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }

Tactic:
{
          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.ext h'⟩⟩ }

Premises used: Equiv.trans, Equiv.subtypeEquivRight, Equiv.subtypeSubtypeEquivSubtypeExists, Equiv.symm, Equiv.sigmaCongrRight
-- Module: Mathlib.Logic.Equiv.Basic
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
p : Option α → Type v
h : ∀ (a : p Option.none), False
x : Option α
none : ∀ (a : p Option.none), Option.isSome.{u_9} (α := α) Option.none = true
some : ∀ (val : α) (a : p (Option.some val)), (Option.some val).isSome = true
⊢ ∀ (a : p x), x.isSome = true

Tactic:
cases x
-- Module: Mathlib.Logic.Equiv.Basic
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
p : Option α → Type v
h : ∀ (a : p Option.none), False
n : p Option.none
none : False
⊢ Option.isSome.{u_9} (α := α) Option.none = true

Tactic:
exfalso
-- Module: Mathlib.Logic.Equiv.Basic
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
p : Option α → Type v
h : ∀ (a : p none), False
n : p none
⊢ False

Tactic:
h n