awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
β : Sort u_1
b : β
h : Eq.{u_1} (α := β) ((fun (x : PUnit.{u_2}) ↦ b) PUnit.unit) ((fun (x : PUnit.{u_2}) ↦ b) PUnit.unit)
⊢ PUnit.unit = PUnit.unit

Tactic:
rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
one : Type u_1
α : Type u_2
inst : Unique one
a : α
x y : one
h : Eq.{u_2 + 1} (α := α) ((fun (x : one) ↦ a) x) ((fun (x : one) ↦ a) y)
⊢ x = y

Tactic:
simp [Unique.uniq inferInstance]

Premises used: inferInstance, Unique.uniq
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
one : Type u_1
α : Type u_2
inst : Unique one
f : one ↪ α
h :
  ∀ (x : one),
    Eq.{u_2 + 1} (α := α)
      (((fun (a : α) ↦ ({ toFun := fun (x : one) ↦ a, inj' := ⋯ } : one ↪ α))
              ((fun (f : one ↪ α) ↦ ((f : (a : one) → α) default : α)) f) :
            (a : one) → α)
          x :
        α)
      ((f : (a : one) → α) x : α)
⊢ (fun (a : α) ↦ ({ toFun := fun (x : one) ↦ a, inj' := ⋯ } : one ↪ α))
      ((fun (f : one ↪ α) ↦ ((f : (a : one) → α) default : α)) f) =
    f

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
one : Type u_1
α : Type u_2
inst : Unique one
f : one ↪ α
x : one
⊢ Eq.{u_2 + 1} (α := α)
    (((fun (a : α) ↦ ({ toFun := fun (x : one) ↦ a, inj' := ⋯ } : one ↪ α))
            ((fun (f : one ↪ α) ↦ ((f : (a : one) → α) default : α)) f) :
          (a : one) → α)
        x :
      α)
    ((f : (a : one) → α) x : α)

Tactic:
simp [Unique.uniq]

Premises used: Unique.uniq
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Eq (α := (a : α × γ) → β × δ) (⇑(e₁.prodMap e₂) : (a : α × γ) → β × δ)
    (Prod.map (⇑e₁ : (a : α) → β) (⇑e₂ : (a : γ) → δ))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Eq (α := (a : α ⊕ γ) → β ⊕ δ) (⇑(e₁.sumMap e₂) : (a : α ⊕ γ) → β ⊕ δ)
    (Sum.map (⇑e₁ : (a : α) → β) (⇑e₂ : (a : γ) → δ))

Tactic:
rfl

Premises used: Sum.map, rfl, Sum.elim
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
e : α ↪ β
f : γ → α
⊢ Eq (α := γ → β) ((e.arrowCongrRight : (a : γ → α) → γ → β) f : γ → β) ((⇑e : (a : α) → β) ∘ f : γ → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Inhabited γ
e : α ↪ β
f₁ f₂ : α → γ
h :
  Eq (α := β → γ) ((fun (f : α → γ) ↦ (extend (⇑e : (a : α) → β) f default : β → γ)) f₁)
    ((fun (f : α → γ) ↦ (extend (⇑e : (a : α) → β) f default : β → γ)) f₂)
x : α
⊢ f₁ x = f₂ x

Tactic:
simpa only [e.injective.extend_apply] using congr_fun h (e x)

Premises used: Function.Injective.extend_apply, Function.Embedding.injective, congr_fun, DFunLike.coe
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
β : Sort v
γ : Sort w
inst : Inhabited γ
e : α ↪ β
f : α → γ
⊢ Eq (α := β → γ) ((e.arrowCongrLeft : (a : α → γ) → β → γ) f : β → γ) (extend (⇑e : (a : α) → β) f default : β → γ)

Tactic:
rfl

Premises used: dite, Function.extend, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
γ : Sort w
inst : Inhabited γ
h :
  ∀ (x : α → γ) (x_1 : α),
    Eq.{w} (α := γ) (((Embedding.refl α).arrowCongrLeft : (a : α → γ) → α → γ) x x_1 : γ)
      ((Embedding.refl (α → γ) : (a : α → γ) → α → γ) x x_1 : γ)
⊢ Eq (α := (α → γ) ↪ α → γ) (Embedding.refl α).arrowCongrLeft (Embedding.refl (α → γ))

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u
γ : Sort w
inst : Inhabited γ
x : α → γ
x_1 : α
⊢ Eq.{w} (α := γ) (((Embedding.refl α).arrowCongrLeft : (a : α → γ) → α → γ) x x_1 : γ)
    ((Embedding.refl (α → γ) : (a : α → γ) → α → γ) x x_1 : γ)

Tactic:
simp [coe_refl]

Premises used: Function.Embedding.coe_refl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
h :
  ∀ (f : α₁ → γ) (a : α₃),
    Eq.{w} (α := γ) ((Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
      (((e₁₂.trans e₂₃).arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
⊢ Eq (α := (α₁ → γ) ↪ α₃ → γ) (Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft) (e₁₂.trans e₂₃).arrowCongrLeft

Tactic:
ext f a
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
h :
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend (comp.{u, v, x} (β := α₂) (⇑e₂₃ : (a : α₂) → α₃) (⇑e₁₂ : (a : α₁) → α₂)) f (fun (a : α₃) ↦ default) a
⊢ Eq.{w} (α := γ) ((Embedding.trans e₁₂.arrowCongrLeft e₂₃.arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)
    (((e₁₂.trans e₂₃).arrowCongrLeft : (a : α₁ → γ) → α₃ → γ) f a : γ)

Tactic:
simp only [trans_apply, arrowCongrLeft_apply, Pi.default_def, coe_trans]

Premises used: Function.Embedding.arrowCongrLeft_apply, Function.Embedding.trans_apply, Pi.default_def, Function.Embedding.coe_trans
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
h :
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃)
      (extend (⇑e₁₂ : (a : α₁) → α₂) f ((fun (a : α₃) ↦ default) ∘ (⇑e₂₃ : (a : α₂) → α₃))) (fun (a : α₃) ↦ default) a
h₁ h₂ :
  extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (x : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a
⊢ extend.{v, x, w} (α := α₂) (⇑e₂₃ : (a : α₂) → α₃) (extend (⇑e₁₂ : (a : α₁) → α₂) f fun (a : α₂) ↦ default)
      (fun (a : α₃) ↦ default) a =
    extend (comp.{u, v, x} (β := α₂) (⇑e₂₃ : (a : α₂) → α₃) (⇑e₁₂ : (a : α₁) → α₂)) f (fun (a : α₃) ↦ default) a

Tactic:
rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]

Premises used: Function.comp_def, Function.Embedding.injective, Function.Injective.extend_comp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
x y z : α
⊢ Eq (α := β)
    (((Equiv.swap ((f : (a : α) → β) x) ((f : (a : α) → β) y) : Equiv.Perm β) : (a : β) → β) ((f : (a : α) → β) z : β) :
      β)
    ((f : (a : α) → β) ((Equiv.swap x y : (a : α) → α) z : α) : β)

Tactic:
f.injective.swap_apply x y z

Premises used: Function.Injective.swap_apply, Function.Embedding.injective
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
x y : α
⊢ Eq (α := α → β)
    (comp (β := β) (⇑(Equiv.swap ((f : (a : α) → β) x) ((f : (a : α) → β) y) : Equiv.Perm β) : (a : β) → β)
      (⇑f : (a : α) → β))
    (comp (β := α) (⇑f : (a : α) → β) (⇑(Equiv.swap x y) : (a : α) → α))

Tactic:
f.injective.swap_comp x y

Premises used: Function.Embedding.injective, Function.Injective.swap_comp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
h₁ :
  ∀ (x_1 : α),
    Eq.{u_3} (α := γ)
      (((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) ((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) x) :
            (a : α) → γ)
          x_1 :
        γ)
      ((x : (a : α) → γ) x_1 : γ)
⊢ (fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) ((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) x) = x

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
x_1 : α
⊢ Eq.{u_3} (α := γ)
    (((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) ((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) x) : (a : α) → γ)
        x_1 :
      γ)
    ((x : (a : α) → γ) x_1 : γ)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
h₁ :
  ∀ (x_1 : β),
    Eq.{u_4} (α := δ)
      (((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) ((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) x) :
            (a : β) → δ)
          x_1 :
        δ)
      ((x : (a : β) → δ) x_1 : δ)
⊢ (fun (f : α ↪ γ) ↦ Embedding.congr h h' f) ((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) x) = x

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
x_1 : β
⊢ Eq.{u_4} (α := δ)
    (((fun (f : α ↪ γ) ↦ Embedding.congr h h' f) ((fun (f : β ↪ δ) ↦ Embedding.congr h.symm h'.symm f) x) : (a : β) → δ)
        x_1 :
      δ)
    ((x : (a : β) → δ) x_1 : δ)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).embeddingCongr (Equiv.refl β) = Equiv.refl (α ↪ β)

Tactic:
rfl

Premises used: Equiv.embeddingCongr, Function.Embedding.trans, Function.Embedding.congr, Equiv.refl, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
α₃ : Sort u_5
β₃ : Sort u_6
e₁ : α₁ ≃ α₂
e₁' : β₁ ≃ β₂
e₂ : α₂ ≃ α₃
e₂' : β₂ ≃ β₃
⊢ (e₁.trans e₂).embeddingCongr (e₁'.trans e₂') = (e₁.embeddingCongr e₁').trans (e₂.embeddingCongr e₂')

Tactic:
rfl

Premises used: Equiv.trans, Equiv.embeddingCongr, Function.Embedding.trans, Function.Embedding.congr, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
⊢ (e₁.embeddingCongr e₂).symm = e₁.symm.embeddingCongr e₂.symm

Tactic:
rfl

Premises used: Equiv.embeddingCongr, Function.Embedding.trans, Function.Embedding.congr, Equiv.symm, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
h :
  ∀ (x : α₂),
    Eq.{u_6} (α := γ₂)
      ((((ea.embeddingCongr ec : (a : α₁ ↪ γ₁) → α₂ ↪ γ₂) (f.trans g) : α₂ ↪ γ₂) : (a : α₂) → γ₂) x : γ₂)
      ((Embedding.trans.{u_4, u_5, u_6} (β := β₂) ((ea.embeddingCongr eb : (a : α₁ ↪ β₁) → α₂ ↪ β₂) f)
              ((eb.embeddingCongr ec : (a : β₁ ↪ γ₁) → β₂ ↪ γ₂) g) :
            (a : α₂) → γ₂)
          x :
        γ₂)
⊢ Eq (α := α₂ ↪ γ₂) ((ea.embeddingCongr ec : (a : α₁ ↪ γ₁) → α₂ ↪ γ₂) (f.trans g) : α₂ ↪ γ₂)
    (Embedding.trans.{u_4, u_5, u_6} (β := β₂) ((ea.embeddingCongr eb : (a : α₁ ↪ β₁) → α₂ ↪ β₂) f)
        ((eb.embeddingCongr ec : (a : β₁ ↪ γ₁) → β₂ ↪ γ₂) g) :
      α₂ ↪ γ₂)

Tactic:
ext
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x : α₂
⊢ Eq.{u_6} (α := γ₂) ((((ea.embeddingCongr ec : (a : α₁ ↪ γ₁) → α₂ ↪ γ₂) (f.trans g) : α₂ ↪ γ₂) : (a : α₂) → γ₂) x : γ₂)
    ((Embedding.trans.{u_4, u_5, u_6} (β := β₂) ((ea.embeddingCongr eb : (a : α₁ ↪ β₁) → α₂ ↪ β₂) f)
            ((eb.embeddingCongr ec : (a : β₁ ↪ γ₁) → β₂ ↪ γ₂) g) :
          (a : α₂) → γ₂)
        x :
      γ₂)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
⊢ (Equiv.refl α).toEmbedding = Embedding.refl α

Tactic:
rfl

Premises used: Function.Embedding.refl, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
f : β ≃ γ
⊢ (e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding

Tactic:
rfl

Premises used: Function.Embedding.trans, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
pos :
  ∀ (h : p (↑x : α)) (h_1 : p (↑y : α)),
    Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
      x = y
neg : p (↑x : α) → ¬p (↑y : α) → False → x = y
pos₁ : ¬p (↑x : α) → p (↑y : α) → False → x = y
neg₁ :
  ∀ (h : ¬p (↑x : α)) (h_1 : ¬p (↑y : α)),
    Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
      x = y
⊢ Eq.{u_1 + 1} (α := { x : α // p x } ⊕ { x : α // q x })
      (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (if h : p (↑y : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y

Tactic:
split_ifs
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
h : p (↑x : α)
h_1 : p (↑y : α)
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
    x = y

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
h : p (↑x : α)
h_1 : ¬p (↑y : α)
⊢ False → x = y

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
h : ¬p (↑x : α)
h_1 : p (↑y : α)
⊢ False → x = y

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
h : ¬p (↑x : α)
h_1 : ¬p (↑y : α)
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x : { x : α // p x ∨ q x }
hx : p (↑x : α)
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x }) x :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) hx) : { x : α // p x } ⊕ { x : α // q x })

Tactic:
dif_pos hx

Premises used: dif_pos, dite
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x : { x : α // p x ∨ q x }
hx : ¬p (↑x : α)
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x }) x :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯) : { x : α // p x } ⊕ { x : α // q x })

Tactic:
dif_neg hx

Premises used: dif_neg, dite
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x : { x : α // p x ∨ q x }
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x }) x :
      { x : α // p x } ⊕ { x : α // q x })
    (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯) :
      { x : α // p x } ⊕ { x : α // q x })

Tactic:
rfl

Premises used: dite, rfl
-- Module: Mathlib.Logic.Embedding.Basic
Goal:
α : Type u_1
p q : α → Prop
h : ∀ (x : α), p x → q x
x y : { x : α // p x }
⊢ Eq.{u_1 + 1} (α := { x : α // q x }) ((fun (x : { x : α // p x }) ↦ mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯) x)
      ((fun (x : { x : α // p x }) ↦ mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯) y) →
    x = y

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Sort u_1
β : Type u_2
p : β → Prop
e : Equiv.{u_1, u_2 + 1} α (Subtype p)
x : β
hs : x ∈ setOf p
⊢ (e.asEmbedding (p := p) : (a : α) → β) ((e.symm : (a : Subtype p) → α) (Subtype.mk (p := p) x hs) : α) = x

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
β : Type u_2
f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (f : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) ↦
              f.fst (β := fun (f : α ↪ β) ↦
                    (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)).optionElim
                (↑(f.snd (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))) :
                  β)
                ⋯)
            ((fun (f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
                    (Embedding.trans Embedding.some f)
                    (Subtype.mk (p := fun (x : β) ↦
                      Membership.mem (γ := Set β)
                        (range.{u_2, u_1 + 1} (ι := α) (⇑(Embedding.trans Embedding.some f) : (a : α) → β))ᶜ x)
                      ((f : (a : Option α) → β) none) ⋯) :
                  (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)))
              f) :
          (a : Option α) → β)
        none :
      β)
    ((f : (a : Option α) → β) none : β)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
β : Type u_2
f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β
val : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (f : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) ↦
              f.fst (β := fun (f : α ↪ β) ↦
                    (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)).optionElim
                (↑(f.snd (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))) :
                  β)
                ⋯)
            ((fun (f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
                    (Embedding.trans Embedding.some f)
                    (Subtype.mk (p := fun (x : β) ↦
                      Membership.mem (γ := Set β)
                        (range.{u_2, u_1 + 1} (ι := α) (⇑(Embedding.trans Embedding.some f) : (a : α) → β))ᶜ x)
                      ((f : (a : Option α) → β) none) ⋯) :
                  (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)))
              f) :
          (a : Option α) → β)
        (some val) :
      β)
    ((f : (a : Option α) → β) (some val) : β)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
β : Type u_2
x : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)
f : α ↪ β
y : β
hy : Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ y
x_1 : α
⊢ Eq.{u_2 + 1} (α := β)
    ((Sigma.fst (β := fun (a : α ↪ β) ↦
            { x : β // Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑a : (a : α) → β))ᶜ x })
            ((fun (f : Embedding.{u_1 + 1, u_2 + 1} (Option α) β) ↦
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))
                    (Embedding.trans Embedding.some f)
                    (Subtype.mk (p := fun (x : β) ↦
                      Membership.mem (γ := Set β)
                        (range.{u_2, u_1 + 1} (ι := α) (⇑(Embedding.trans Embedding.some f) : (a : α) → β))ᶜ x)
                      ((f : (a : Option α) → β) none) ⋯) :
                  (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)))
              ((fun (f : (f : α ↪ β) × (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) ↦
                  f.fst (β := fun (f : α ↪ β) ↦
                        (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)).optionElim
                    (↑(f.snd (β := fun (f : α ↪ β) ↦
                          (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2))) :
                      β)
                    ⋯)
                (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) f
                  (Subtype.mk (p := fun (x : β) ↦
                    Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ x) y hy)))) :
          (a : α) → β)
        x_1 :
      β)
    ((Sigma.fst (β := fun (a : α ↪ β) ↦
            { x : β // Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑a : (a : α) → β))ᶜ x })
            (Sigma.mk (β := fun (f : α ↪ β) ↦ (↑(range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ : Type u_2)) f
              (Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))ᶜ x) y hy)) :
          (a : α) → β)
        x_1 :
      β)

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Sort u_1
β : Type u_2
p : Set β
f : α ↪ β
H : ∀ (a : α), Membership.mem (α := β) p ((f : (a : α) → β) a : β)
a : α
⊢ Eq.{u_2 + 1} (α := (↑p : Type u_2)) ((codRestrict p f H : (a : α) → (↑p : Type u_2)) a : (↑p : Type u_2))
    (Subtype.mk (p := fun (x : β) ↦ x ∈ p) ((f : (a : α) → β) a) ⋯ : { x : β // x ∈ p })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t : Set α
h_1 : s ⊆ t
x_1 x_2 : (↑s : Type u_1)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  Eq.{u_1 + 1} (α := (↑t : Type u_1))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy))
e_val : x = y
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

Tactic:
congr
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t : Set α
h_1 : s ⊆ t
x_1 x_2 : (↑s : Type u_1)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  Eq.{u_1 + 1} (α := (↑t : Type u_1))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy))
⊢ x = y

Tactic:
injection h
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // p x ∨ q x }
⊢ Sum.elim (α := { x : α // p x }) (β := { x : α // q x })
      (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
      (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
      ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x }) x) =
    x

Tactic:
grind
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // p x }
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        (Sum.elim (β := { x : α // q x })
          (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
          (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
          (Sum.inl x)) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inl x : { x : α // p x } ⊕ { x : α // q x })

Tactic:
grind