awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact h n
-- 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
val : α
a : p (some val)
⊢ (some val).isSome = true

Tactic:
rfl

Premises used: rfl
-- 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
val : α
a : p (some val)
⊢ (some val).isSome = true

Tactic:
exact 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
ι : Type u_10
π : ι → Type u_9
f : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }
i : ι
rw : π (((↑f : ι → (i : ι) × π i) i).fst (β := fun (i : ι) ↦ π i))
⊢ π i

Tactic:
rw [← f.2 i]

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
ι : Type u_10
π : ι → Type u_9
f : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }
i : ι
⊢ π (((↑f : ι → (i : ι) × π i) i).fst (β := fun (i : ι) ↦ π i))

Tactic:
exact (f.1 i).2

Premises used: Sigma.snd, Subtype.val
-- 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
ι : Type u_10
π : ι → Type u_9
x : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }
f : ι → (i : ι) × π i
hf : ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i
i : ι
⊢ HEq (α :=
    π
      (Sigma.fst (β := fun (a : ι) ↦ π a)
        ((↑((fun (f : (i : ι) → π i) ↦
                  (Subtype.mk (p := fun (f : ι → (i : ι) × π i) ↦ ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i)
                      (fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) i (f i)) ⋯ :
                    { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }))
                ((fun (f : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }) (i : ι) ↦
                    Eq.mpr ⋯ (((↑f : ι → (i : ι) × π i) i).snd (β := fun (i : ι) ↦ π i)))
                  (Subtype.mk (p := fun (f : ι → (i : ι) × π i) ↦ ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i) f
                    hf))) :
            ι → (i : ι) × π i)
          i)))
    (Sigma.snd (β := fun (a : ι) ↦ π a)
      ((↑((fun (f : (i : ι) → π i) ↦
                (Subtype.mk (p := fun (f : ι → (i : ι) × π i) ↦ ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i)
                    (fun (i : ι) ↦ Sigma.mk (β := fun (i : ι) ↦ π i) i (f i)) ⋯ :
                  { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }))
              ((fun (f : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }) (i : ι) ↦
                  Eq.mpr ⋯ (((↑f : ι → (i : ι) × π i) i).snd (β := fun (i : ι) ↦ π i)))
                (Subtype.mk (p := fun (f : ι → (i : ι) × π i) ↦ ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i) f
                  hf))) :
          ι → (i : ι) × π i)
        i))
    (((↑(Subtype.mk (p := fun (f : ι → (i : ι) × π i) ↦ ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i) f hf) :
            ι → (i : ι) × π i)
          i).snd
      (β := fun (a : ι) ↦ π a))

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

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : 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
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b : β a // p a b }
h :
  ∀ (a : α),
    Eq.{max 1 v}
      ((fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
          (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) ⋯ : { b : β a // p a b }))
        ((fun (f : (a : α) → { b : β a // p a b }) ↦
            (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) ⋯ :
              { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
          f)
        a)
      (f a)
⊢ (fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
        (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) ⋯ : { b : β a // p a b }))
      ((fun (f : (a : α) → { b : β a // p a b }) ↦
          (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) ⋯ :
            { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
        f) =
    f

Tactic:
funext a
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : 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
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b : β a // p a b }
a : α
⊢ Eq.{max 1 v}
    ((fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
        (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) ⋯ : { b : β a // p a b }))
      ((fun (f : (a : α) → { b : β a // p a b }) ↦
          (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) ⋯ :
            { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
        f)
      a)
    (f a)

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : 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
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b : β a // p a b }
a : α
⊢ Eq.{max 1 v}
    ((fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
        (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) ⋯ : { b : β a // p a b }))
      ((fun (f : (a : α) → { b : β a // p a b }) ↦
          (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) ⋯ :
            { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
        f)
      a)
    (f a)

Tactic:
exact Subtype.ext rfl

Premises used: rfl, 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
a_1 : α
x : { s : Sigma β // s.fst (β := β) = a_1 }
a : Sigma β
h : a.fst (β := β) = a_1
refl :
  ∀ (x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }),
    Eq (α := { s : Sigma β // s.fst (β := β) = a.fst (β := β) })
      ((fun (b : β (a.fst (β := β))) ↦
          Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) (Sigma.mk (β := β) (a.fst (β := β)) b)
            ⋯)
        ((fun (x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }) ↦
            (match (motive := { s : Sigma β // s.fst (β := β) = a.fst (β := β) } → β (a.fst (β := β))) x with
              | ⟨⟨fst, b⟩, h⟩ =>
                Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
              β (a.fst (β := β))))
          (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a ⋯)))
      (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a ⋯)
⊢ Eq (α := { s : Sigma β // s.fst (β := β) = a_1 })
    ((fun (b : β a_1) ↦ Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) (Sigma.mk (β := β) a_1 b) ⋯)
      ((fun (x : { s : Sigma β // s.fst (β := β) = a_1 }) ↦
          (match (motive := { s : Sigma β // s.fst (β := β) = a_1 } → β a_1) x with
            | ⟨⟨fst, b⟩, h⟩ =>
              Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
            β a_1))
        (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) a h)))
    (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) a h)

Tactic:
cases 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
a : Sigma β
x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }
⊢ Eq (α := { s : Sigma β // s.fst (β := β) = a.fst (β := β) })
    ((fun (b : β (a.fst (β := β))) ↦
        Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) (Sigma.mk (β := β) (a.fst (β := β)) b) ⋯)
      ((fun (x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }) ↦
          (match (motive := { s : Sigma β // s.fst (β := β) = a.fst (β := β) } → β (a.fst (β := β))) x with
            | ⟨⟨fst, b⟩, h⟩ =>
              Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
            β (a.fst (β := β))))
        (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a ⋯)))
    (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a ⋯)

Tactic:
simp
-- 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
a : α
b : β a
⊢ (fun (x : { s : Sigma β // s.fst (β := β) = a }) ↦
        (match (motive := { s : Sigma β // s.fst (β := β) = a } → β a) x with
          | ⟨⟨fst, b⟩, h⟩ => Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
          β a))
      ((fun (b : β a) ↦ Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a) (Sigma.mk (β := β) a b) ⋯) b) =
    b

Tactic:
simp
-- 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
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
s : (a : α) × (b : β a) × γ a b
⊢ (fun (x : (a : α) × (b : β a) × γ a b) ↦
        (match (motive := (a : α) × (b : β a) × γ a b → Prop) x with
          | ⟨a, ⟨b, c⟩⟩ => p (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
          Prop))
      s ↔
    (fun (x : (ab : (a : α) × β a) × γ (ab.fst (β := fun (a : α) ↦ β a)) (ab.snd (β := fun (a : α) ↦ β a))) ↦
        p
          (x.fst (β := fun (ab : (a : α) × β a) ↦
            γ (ab.fst (β := fun (a : α) ↦ β a)) (ab.snd (β := fun (a : α) ↦ β a)))))
      (((sigmaAssoc (β := β) γ).symm : (a : (a : α) × (b : β a) × γ a b) → (ab : (a : α) × β a) × γ ab.fst ab.snd) s)

Tactic:
simp [sigmaAssoc]

Premises used: Equiv.sigmaAssoc
-- 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
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
rw rw₁ :
  γ
      ((↑(Subtype.mk (p := fun (ab : (a : α) × β a) ↦ p ab) (Sigma.mk (β := fun (a : α) ↦ β a) a b) h) : Sigma β).fst
        (β := β))
      ((↑(Subtype.mk (p := fun (ab : (a : α) × β a) ↦ p ab) (Sigma.mk (β := fun (a : α) ↦ β a) a b) h) : Sigma β).snd
        (β := β)) =
    γ a b
⊢ γ (Sigma.fst (β := β) (↑default : Sigma β)) (Sigma.snd (β := β) (↑default : Sigma β)) = γ a b

Tactic:
rw [← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]

Premises used: Subtype.mk, Unique.uniq, Sigma.mk
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
c : γ a b
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
rw :
  c =
    (sigmaSigmaSubtype (β := β) (γ := γ) p h :
        (a_1 : { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ }) → γ a b)
      (Subtype.mk (p := fun (s : (a : α) × (b : β a) × γ a b) ↦
        p
          (Sigma.mk (β := fun (a : α) ↦ β a) (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))
            (s.snd (β := fun (a : α) ↦ (b : β a) × γ a b).fst (β :=
              fun (b : β (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))) ↦
              γ (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b)) b))))
        (Sigma.mk (β := fun (a : α) ↦ (b : β a) × γ a b) a (Sigma.mk (β := fun (b : β a) ↦ γ a b) b c)) h)
⊢ (Equiv.symm (sigmaSigmaSubtype (β := β) (γ := γ) p h) :
        (a : γ a b) → { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ })
      c =
    Subtype.mk (p := fun (s : (a : α) × (b : β a) × γ a b) ↦
      p
        (Sigma.mk (β := fun (a : α) ↦ β a) (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))
          (s.snd (β := fun (a : α) ↦ (b : β a) × γ a b).fst (β :=
            fun (b : β (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))) ↦
            γ (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b)) b))))
      (Sigma.mk (β := fun (a : α) ↦ (b : β a) × γ a b) a (Sigma.mk (β := fun (b : β a) ↦ γ a b) b c)) h

Tactic:
rw [Equiv.symm_apply_eq]

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
c : γ a b
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
⊢ c =
    (sigmaSigmaSubtype (β := β) (γ := γ) p h :
        (a_1 : { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ }) → γ a b)
      (Subtype.mk (p := fun (s : (a : α) × (b : β a) × γ a b) ↦
        p
          (Sigma.mk (β := fun (a : α) ↦ β a) (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))
            (s.snd (β := fun (a : α) ↦ (b : β a) × γ a b).fst (β :=
              fun (b : β (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))) ↦
              γ (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b)) b))))
        (Sigma.mk (β := fun (a : α) ↦ (b : β a) × γ a b) a (Sigma.mk (β := fun (b : β a) ↦ γ a b) b c)) h)

Tactic:
simp
-- 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
γ_1 : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a' : α
b' : β
⊢ Eq (α :=
    { x : (_ : α) × β //
      match (motive := (_ : α) × β → Prop) x with
      | ⟨a'_1, b'_1⟩ => a'_1 = a' ∧ b'_1 = b' })
    (Subtype.mk (p := fun (x : (_ : α) × β) ↦
      match (motive := (_ : α) × β → Prop) x with
      | ⟨a'_1, b'_1⟩ => a'_1 = a' ∧ b'_1 = b')
      (Sigma.mk (β := fun (x : α) ↦ β) a' b') ⋯)
    (Subtype.mk (p := fun (x : (_ : α) × β) ↦
      match (motive := (_ : α) × β → Prop) x with
      | ⟨a'_1, b'_1⟩ => a'_1 = a' ∧ b'_1 = b')
      (Sigma.mk (β := fun (x : α) ↦ β) a' b') ⋯)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
s :
  { s : (a : α) × (b : β) × γ a b //
    s.fst (β := fun (a : α) ↦ (b : β) × γ a b) = a ∧
      s.snd (β := fun (a : α) ↦ (b : β) × γ a b).fst (β := fun (b : β) ↦
          γ (s.fst (β := fun (a : α) ↦ (b : β) × γ a b)) b) =
        b }
⊢ (sigmaSigmaSubtypeEq (γ := γ) a b : (a_1 : { s : (a : α) × (b : β) × γ a b // s.fst = a ∧ s.snd.fst = b }) → γ a b)
      s =
    cast ⋯
      ((↑s : (a : α) × (b : β) × γ a b).snd (β := fun (a : α) ↦ (b : β) × γ a b).snd (β := fun (b_1 : β) ↦
        γ ((↑s : (a : α) × (b : β) × γ a b).fst (β := fun (a : α) ↦ (b : β) × γ a b)) b_1))

Tactic:
simp [sigmaSigmaSubtypeEq]

Premises used: Equiv.sigmaSigmaSubtypeEq
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
c : γ a b
⊢ Eq (α :=
    { s : (a : α) × (b : β) × γ a b //
      s.fst (β := fun (a : α) ↦ (b : β) × γ a b) = a ∧
        s.snd (β := fun (a : α) ↦ (b : β) × γ a b).fst (β := fun (b : β) ↦
            γ (s.fst (β := fun (a : α) ↦ (b : β) × γ a b)) b) =
          b })
    ((Equiv.symm (sigmaSigmaSubtypeEq (γ := γ) a b) :
          (a_1 : γ a b) → { s : (a : α) × (b : β) × γ a b // s.fst = a ∧ s.snd.fst = b })
        c :
      { s : (a : α) × (b : β) × γ a b //
        s.fst (β := fun (a : α) ↦ (b : β) × γ a b) = a ∧
          s.snd (β := fun (a : α) ↦ (b : β) × γ a b).fst (β := fun (b : β) ↦
              γ (s.fst (β := fun (a : α) ↦ (b : β) × γ a b)) b) =
            b })
    (Subtype.mk (p := fun (s : (a : α) × (b : β) × γ a b) ↦
        s.fst (β := fun (a : α) ↦ (b : β) × γ a b) = a ∧
          s.snd (β := fun (a : α) ↦ (b : β) × γ a b).fst (β := fun (b : β) ↦
              γ (s.fst (β := fun (a : α) ↦ (b : β) × γ a b)) b) =
            b)
        (Sigma.mk (β := fun (a : α) ↦ (b : β) × γ a b) a (Sigma.mk (β := fun (b : β) ↦ γ a b) b c)) ⋯ :
      { s : (a : α) × (b : β) × γ a b //
        s.fst (β := fun (a : α) ↦ (b : β) × γ a b) = a ∧
          s.snd (β := fun (a : α) ↦ (b : β) × γ a b).fst (β := fun (b : β) ↦
              γ (s.fst (β := fun (a : α) ↦ (b : β) × γ a b)) b) =
            b })

Tactic:
simp [sigmaSigmaSubtypeEq]

Premises used: Equiv.sigmaSigmaSubtypeEq
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
⊢ Eq (α := (a : { g : X → Y // g ∘ Subtype.val (p := fun (x' : X) ↦ x' ≠ x) = f }) → Y)
    (⇑(subtypeEquivCodomain f) : (a : { g : X → Y // g ∘ Subtype.val = f }) → Y)
    fun (g : { g : X → Y // g ∘ Subtype.val (p := fun (x' : X) ↦ x' ≠ x) = f }) ↦ (↑g : X → Y) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
g : { g : X → Y // g ∘ Subtype.val (p := fun (x' : X) ↦ x' ≠ x) = f }
⊢ (subtypeEquivCodomain f : (a : { g : X → Y // g ∘ Subtype.val = f }) → Y) g = (↑g : X → Y) x

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
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
y : Y
⊢ (fun (x' : X) ↦ if h : x' ≠ x then f (Subtype.mk (p := fun (x' : X) ↦ x' ≠ x) x' h) else y) ∘
      Subtype.val (p := fun (x' : X) ↦ x' ≠ x) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
⊢ Eq (α := (a : Y) → { g : X → Y // g ∘ Subtype.val (p := fun (x' : X) ↦ x' ≠ x) = f })
    (⇑(subtypeEquivCodomain f).symm : (a : Y) → { g : X → Y // g ∘ Subtype.val = f }) fun (y : Y) ↦
    Subtype.mk (p := fun (g : X → Y) ↦ g ∘ Subtype.val (p := fun (x' : X) ↦ x' ≠ x) = f)
      (fun (x' : X) ↦ if h : x' ≠ x then f (Subtype.mk (p := fun (x' : X) ↦ x' ≠ x) x' h) else y) ⋯

Tactic:
rfl

Premises used: Eq.mpr, uniqueElim, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
y : Y
x' : X
⊢ Eq.{u_10} (α := Y)
    ((↑(((subtypeEquivCodomain f).symm : (a : Y) → { g : X → Y // g ∘ Subtype.val = f }) y) : X → Y) x')
    (if h : x' ≠ x then f (Subtype.mk (p := fun (x' : X) ↦ x' ≠ x) x' h) else y)

Tactic:
rfl

Premises used: Eq.mpr, dite, uniqueElim, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
y : Y
⊢ (↑(((subtypeEquivCodomain f).symm : (a : Y) → { g : X → Y // g ∘ Subtype.val = f }) y) : X → Y) x = y

Tactic:
dif_neg (not_not.mpr rfl)

Premises used: Iff.mpr, Eq.mpr, Classical.not_not, dif_neg, dite, uniqueElim, rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
X : Sort u_9
Y : Sort u_10
inst : DecidableEq X
x : X
f : { x' : X // x' ≠ x } → Y
y : Y
x' : X
h : x' ≠ x
⊢ (↑(((subtypeEquivCodomain f).symm : (a : Y) → { g : X → Y // g ∘ Subtype.val = f }) y) : X → Y) x' =
    f (Subtype.mk (p := fun (x' : X) ↦ x' ≠ x) x' h)

Tactic:
dif_pos h

Premises used: dif_pos, dite
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
a : α'
⊢ Eq (α := β') ((e.extendDomain (p := p) f : (a : β') → β') (↑((f : (a : α') → Subtype p) a) : β') : β')
    ((↑((f : (a : α') → Subtype p) ((e : (a : α') → α') a)) : β') : β')

Tactic:
simp [Perm.extendDomain]

Premises used: Equiv.Perm.extendDomain
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
b : β'
h : p b
⊢ Eq (α := β') ((e.extendDomain (p := p) f : (a : β') → β') b : β')
    ((↑((f : (a : α') → Subtype p)
            ((e : (a : α') → α') ((f.symm : (a : Subtype p) → α') (Subtype.mk (p := p) b h) : α'))) :
        β') :
      β')

Tactic:
simp [Perm.extendDomain, h]

Premises used: Equiv.Perm.extendDomain
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
b : β'
h : ¬p b
⊢ (e.extendDomain (p := p) f : (a : β') → β') b = b

Tactic:
simp [Perm.extendDomain, h]

Premises used: Equiv.Perm.extendDomain
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
⊢ extendDomain (Equiv.refl α') (p := p) f = Equiv.refl β'

Tactic:
simp [Perm.extendDomain]

Premises used: Equiv.Perm.extendDomain
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
e : Perm α'
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
⊢ Equiv.symm (e.extendDomain (p := p) f) = extendDomain (Equiv.symm e) (p := p) f

Tactic:
rfl

Premises used: Equiv.Perm.extendDomain, Sum.map, Equiv.trans, Equiv.Perm.subtypeCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α' : Type u_9
β' : Type u_10
p : β' → Prop
inst : DecidablePred p
f : Equiv.{u_9 + 1, max 1 (u_10 + 1)} α' (Subtype p)
e e' : Perm α'
⊢ Equiv.trans (e.extendDomain (p := p) f) (e'.extendDomain (p := p) f) = extendDomain (Equiv.trans e e') (p := p) f

Tactic:
simp [Perm.extendDomain, permCongr_trans]

Premises used: Equiv.Perm.extendDomain, Equiv.permCongr_trans
-- 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
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a_1 : { x : Quotient s₁ // p₂ x }
a b : α
hab : a ≈ b
rw rw₁ : p₂ ⟦b⟧ = p₂ ⟦b⟧
⊢ p₂ ⟦a⟧ = p₂ ⟦b⟧

Tactic:
rw [Quotient.sound hab]

Premises used: Quotient.sound