awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p ((e.symm : (a : β) → α) b) ↔ q b
⊢ (∃! b : β, p ((e.symm : (a : β) → α) b)) ↔ ∃! b : β, q b

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : Equiv.{max 1 u, max 1 v} { a : α // p a } { b : β // q b }
⊢ (∃! a : α, p a) ↔ ∃! b : β, q b

Tactic:
simp [← unique_subtype_iff_existsUnique, unique_iff_subsingleton_and_nonempty,
        nonempty_congr e, subsingleton_congr e]

Premises used: Equiv.subsingleton_congr, unique_iff_subsingleton_and_nonempty, unique_subtype_iff_existsUnique, Equiv.nonempty_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
β₁ : Sort u_3
β₂ : Sort u_4
p : α₁ → β₁ → Prop
q : α₂ → β₂ → Prop
eα : α₁ ≃ α₂
eβ : β₁ ≃ β₂
h : ∀ {x : α₁} {y : β₁}, p x y ↔ q ((eα : (a : α₁) → α₂) x) ((eβ : (a : β₁) → β₂) y)
⊢ (∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y

Tactic:
eα.forall_congr fun _ ↦ eβ.forall_congr <| @h _

Premises used: Equiv.forall_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
β₁ : Sort u_3
β₂ : Sort u_4
p : α₁ → β₁ → Prop
q : α₂ → β₂ → Prop
eα : α₁ ≃ α₂
eβ : β₁ ≃ β₂
h : ∀ {x : α₂} {y : β₂}, p ((eα.symm : (a : α₂) → α₁) x) ((eβ.symm : (a : β₂) → β₁) y) ↔ q x y
⊢ (∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y

Tactic:
(Equiv.forall₂_congr eα.symm eβ.symm h.symm).symm

Premises used: Equiv.symm, Equiv.forall₂_congr, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
β₁ : Sort u_3
β₂ : Sort u_4
γ₁ : Sort u_5
γ₂ : Sort u_6
p : α₁ → β₁ → γ₁ → Prop
q : α₂ → β₂ → γ₂ → Prop
eα : α₁ ≃ α₂
eβ : β₁ ≃ β₂
eγ : γ₁ ≃ γ₂
h : ∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z ↔ q ((eα : (a : α₁) → α₂) x) ((eβ : (a : β₁) → β₂) y) ((eγ : (a : γ₁) → γ₂) z)
⊢ (∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z

Tactic:
Equiv.forall₂_congr _ _ <| Equiv.forall_congr _ <| @h _ _

Premises used: Equiv.forall_congr, Equiv.forall₂_congr
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α₁ : Sort u_1
α₂ : Sort u_2
β₁ : Sort u_3
β₂ : Sort u_4
γ₁ : Sort u_5
γ₂ : Sort u_6
p : α₁ → β₁ → γ₁ → Prop
q : α₂ → β₂ → γ₂ → Prop
eα : α₁ ≃ α₂
eβ : β₁ ≃ β₂
eγ : γ₁ ≃ γ₂
h :
  ∀ {x : α₂} {y : β₂} {z : γ₂},
    p ((eα.symm : (a : α₂) → α₁) x) ((eβ.symm : (a : β₂) → β₁) y) ((eγ.symm : (a : γ₂) → γ₁) z) ↔ q x y z
⊢ (∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z

Tactic:
(Equiv.forall₃_congr eα.symm eβ.symm eγ.symm h.symm).symm

Premises used: Equiv.symm, Equiv.forall₃_congr, Iff.symm
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Bijective f
⊢ (⇑(ofBijective f hf) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α ≃ β
⊢ ofBijective (⇑f : (a : α) → β) ⋯ = f

Tactic:
Equiv.ext (congrFun rfl)

Premises used: Equiv.ext, congrFun, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Bijective f
x : β
⊢ f (((ofBijective f hf).symm : (a : β) → α) x) = x

Tactic:
(ofBijective f hf).apply_symm_apply x

Premises used: Equiv.apply_symm_apply, Equiv.ofBijective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
f : α → β
hf : Bijective f
x : α
⊢ ((ofBijective f hf).symm : (a : β) → α) (f x) = x

Tactic:
(ofBijective f hf).symm_apply_apply x

Premises used: Equiv.symm_apply_apply, Equiv.ofBijective
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x : α ≃ β
H :
  ∀ (x_1 : α),
    Eq.{v} (α := β)
      (((fun (f : { f : α → β // Bijective f }) ↦ ofBijective (↑f : α → β) ⋯)
              ((fun (f : α ≃ β) ↦ Subtype.mk (p := fun (f : α → β) ↦ Bijective f) (⇑f : (a : α) → β) ⋯) x) :
            (a : α) → β)
          x_1 :
        β)
      ((x : (a : α) → β) x_1 : β)
⊢ (fun (f : { f : α → β // Bijective f }) ↦ ofBijective (↑f : α → β) ⋯)
      ((fun (f : α ≃ β) ↦ Subtype.mk (p := fun (f : α → β) ↦ Bijective f) (⇑f : (a : α) → β) ⋯) x) =
    x

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x : α ≃ β
x_1 : α
⊢ Eq.{v} (α := β)
    (((fun (f : { f : α → β // Bijective f }) ↦ ofBijective (↑f : α → β) ⋯)
            ((fun (f : α ≃ β) ↦ Subtype.mk (p := fun (f : α → β) ↦ Bijective f) (⇑f : (a : α) → β) ⋯) x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb ((e : (a : α) → β) a₁) ((e : (a : α) → β) a₂)
x : Quot ra
a : α
⊢ Quot.map (ra := rb) (rb := ra) (⇑e.symm : (a : β) → α) ⋯
      (Quot.map (ra := ra) (rb := rb) (⇑e : (a : α) → β) ⋯ (mk ra a)) =
    mk ra a

Tactic:
simp only [Quot.map, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Quot.map
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb ((e : (a : α) → β) a₁) ((e : (a : α) → β) a₂)
x : Quot rb
a : β
⊢ Quot.map (ra := ra) (rb := rb) (⇑e : (a : α) → β) ⋯
      (Quot.map (ra := rb) (rb := ra) (⇑e.symm : (a : β) → α) ⋯ (mk rb a)) =
    mk rb a

Tactic:
simp only [Quot.map, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Quot.map
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb ((e : (a : α) → β) a₁) ((e : (a : α) → β) a₂)
a : α
⊢ (Quot.congr (ra := ra) (rb := rb) e eq : (a : Quot ra) → Quot rb) (mk ra a) = mk rb ((e : (a : α) → β) a)

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
r : α → α → Prop
e : α ≃ β
x x_1 : α
⊢ r x x_1 ↔ r ((e.symm : (a : β) → α) ((e : (a : α) → β) x : β)) ((e.symm : (a : β) → α) ((e : (a : α) → β) x_1 : β))

Tactic:
simp only [e.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
ra : Setoid α
rb : Setoid β
e : α ≃ β
eq :
  ∀ (a₁ a₂ : α), (ra : α → α → Prop) a₁ a₂ ↔ (rb : β → β → Prop) ((e : (a : α) → β) a₁ : β) ((e : (a : α) → β) a₂ : β)
a : α
⊢ (Quotient.congr e eq : (a : Quotient ra) → Quotient rb) ⟦a⟧ = ⟦(e : (a : α) → β) a⟧

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
i : Fin 2
⊢ (fun (b : Bool) ↦ (bif b then 1 else 0 : Fin 2)) ((fun (i : Fin 2) ↦ i == 1) i) = i

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun (i : Fin 2) ↦ i == 1) ((fun (b : Bool) ↦ (bif b then 1 else 0 : Fin 2)) b) = b

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : LE β
a b : α
⊢ LE.le.{u_2} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : LT β
a b : α
⊢ LT.lt.{u_2} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Max β
a b : α
⊢ max a b = (e.symm : (a : β) → α) (max ((e : (a : α) → β) a) ((e : (a : α) → β) b) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Min β
a b : α
⊢ min a b = (e.symm : (a : β) → α) (min ((e : (a : α) → β) a) ((e : (a : α) → β) b) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Ord β
a b : α
⊢ compare a b = compare.{u_2} (α := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
rw :
  ∀ ⦃a : γ⦄,
    Membership.mem (γ := Set γ)
        (Set.range.{u_3, u_1 + 1} (ι := α)
          (⇑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).1 : (a : α) → γ))
        a →
      ¬Membership.mem (γ := Set γ)
          (Set.range.{u_3, u_2 + 1} (ι := β)
            (⇑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).2 : (a : β) → γ))
          a
⊢ Disjoint.{u_3} (α := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (⇑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β)
      (⇑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).2 : (a : β) → γ))

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h :
  Eq.{u_3 + 1} (α := γ) ((Function.Embedding.trans inl f : (a : α) → γ) a : γ)
    ((Function.Embedding.trans inr f : (a : β) → γ) b : γ)
⊢ Sum.inl a = Sum.inr b

Tactic:
have : Sum.inl a = Sum.inr b := f.injective h
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h :
  Eq.{u_3 + 1} (α := γ) ((Function.Embedding.trans inl f : (a : α) → γ) a : γ)
    ((Function.Embedding.trans inr f : (a : β) → γ) b : γ)
this : Sum.inl a = Sum.inr b
⊢ False

Tactic:
simp only [reduceCtorEq] at this

Premises used: reduceCtorEq
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
a₁ a₂ : α
f_eq : Eq.{u_3 + 1} (α := γ) ((f : (a : α) → γ) a₁ : γ) ((f : (a : α) → γ) a₂ : γ)
inl inl₁ : Eq (α := α ⊕ β) (Sum.inl a₂) (Sum.inl a₂)
⊢ Eq (α := α ⊕ β) (Sum.inl a₁) (Sum.inl a₂)

Tactic:
rw [f.injective f_eq]

Premises used: Function.Embedding.injective
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
a₁ : α
b₂ : β
f_eq : Eq.{u_3 + 1} (α := γ) ((f : (a : α) → γ) a₁ : γ) ((g : (a : β) → γ) b₂ : γ)
inl : False
⊢ Sum.inl a₁ = Sum.inr b₂

Tactic:
exfalso
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
a₁ : α
b₂ : β
f_eq : Eq.{u_3 + 1} (α := γ) ((f : (a : α) → γ) a₁ : γ) ((g : (a : β) → γ) b₂ : γ)
⊢ Eq.{u_3 + 1} (α := γ) (((f, g).2 : (a : β) → γ) b₂ : γ) ((g : (a : β) → γ) b₂ : γ)

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
a₁ : α
b₂ : β
f_eq : Eq.{u_3 + 1} (α := γ) ((f : (a : α) → γ) a₁ : γ) ((g : (a : β) → γ) b₂ : γ)
⊢ False

Tactic:
exact disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp⟩⟩

Premises used: Disjoint.le_bot, And.intro, Exists.intro
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
b₁ : β
a₂ : α
f_eq : Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) b₁ : γ) ((f : (a : α) → γ) a₂ : γ)
inr : False
⊢ Sum.inr b₁ = Sum.inl a₂

Tactic:
exfalso
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
b₁ : β
a₂ : α
f_eq : Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) b₁ : γ) ((f : (a : α) → γ) a₂ : γ)
⊢ False

Tactic:
disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
b₁ : β
a₂ : α
f_eq : Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) b₁ : γ) ((f : (a : α) → γ) a₂ : γ)
⊢ False

Tactic:
exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩

Premises used: Disjoint.le_bot, And.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
disj :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
b₁ b₂ : β
f_eq : Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) b₁ : γ) ((g : (a : β) → γ) b₂ : γ)
inr inr₁ : Eq (α := α ⊕ β) (Sum.inr b₂) (Sum.inr b₂)
⊢ Eq (α := α ⊕ β) (Sum.inr b₁) (Sum.inr b₂)

Tactic:
rw [g.injective f_eq]

Premises used: Function.Embedding.injective
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
h :
  ∀ (x : α ⊕ β),
    Eq.{u_3 + 1} (α := γ)
      (({
              toFun := fun (x : α ⊕ β) ↦
                match (motive := α ⊕ β → γ) x with
                | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
                | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
              inj' := ⋯ } :
            (a : α ⊕ β) → γ)
          x :
        γ)
      ((f : (a : α ⊕ β) → γ) x : γ)
⊢ {
      toFun := fun (x : α ⊕ β) ↦
        match (motive := α ⊕ β → γ) x with
        | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
        | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
      inj' := ⋯ } =
    f

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ)
      (({
              toFun := fun (x : α ⊕ β) ↦
                match (motive := α ⊕ β → γ) x with
                | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
                | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
              inj' := ⋯ } :
            (a : α ⊕ β) → γ)
          (Sum.inl val) :
        γ)
      ((f : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ)
      (({
              toFun := fun (x : α ⊕ β) ↦
                match (motive := α ⊕ β → γ) x with
                | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
                | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
              inj' := ⋯ } :
            (a : α ⊕ β) → γ)
          (Sum.inr val) :
        γ)
      ((f : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ Eq.{u_3 + 1} (α := γ)
    (({
            toFun := fun (x : α ⊕ β) ↦
              match (motive := α ⊕ β → γ) x with
              | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
              | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
            inj' := ⋯ } :
          (a : α ⊕ β) → γ)
        x :
      γ)
    ((f : (a : α ⊕ β) → γ) x : γ)

Tactic:
cases x
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val : α
⊢ Eq.{u_3 + 1} (α := γ)
    (({
            toFun := fun (x : α ⊕ β) ↦
              match (motive := α ⊕ β → γ) x with
              | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
              | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
            inj' := ⋯ } :
          (a : α ⊕ β) → γ)
        (Sum.inl val) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp!
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val : β
⊢ Eq.{u_3 + 1} (α := γ)
    (({
            toFun := fun (x : α ⊕ β) ↦
              match (motive := α ⊕ β → γ) x with
              | Sum.inl a => (Function.Embedding.trans inl f : (a : α) → γ) a
              | Sum.inr b => (Function.Embedding.trans inr f : (a : β) → γ) b,
            inj' := ⋯ } :
          (a : α ⊕ β) → γ)
        (Sum.inr val) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp!
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x :
  { f : (α ↪ γ) × (β ↪ γ) //
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) }
f : α ↪ γ
g : β ↪ γ
property :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑(f, g).1 : (a : α) → γ))
    (Set.range.{u_3, u_2 + 1} (ι := β) (⇑(f, g).2 : (a : β) → γ))
⊢ Eq (α :=
    { f : (α ↪ γ) × (β ↪ γ) //
      Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
        (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)) })
    (Subtype.mk (p := fun (f : (α ↪ γ) × (β ↪ γ)) ↦
      Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
        (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)))
      (Function.Embedding.trans inl
          {
            toFun := fun (x : α ⊕ β) ↦
              match (motive := α ⊕ β → γ) x with
              | Sum.inl a => (f : (a : α) → γ) a
              | Sum.inr b => (g : (a : β) → γ) b,
            inj' := ⋯ : α ⊕ β ↪ γ },
        Function.Embedding.trans inr
          {
            toFun := fun (x : α ⊕ β) ↦
              match (motive := α ⊕ β → γ) x with
              | Sum.inl a => (f : (a : α) → γ) a
              | Sum.inr b => (g : (a : β) → γ) b,
            inj' := ⋯ : α ⊕ β ↪ γ })
      ⋯)
    (Subtype.mk (p := fun (f : (α ↪ γ) × (β ↪ γ)) ↦
      Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑f.1 : (a : α) → γ))
        (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f.2 : (a : β) → γ)))
      (f, g) property)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
h :
  ∀ (f : β ↪ γ),
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
        (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
      ∀ (a_1 : β),
        Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
          ((f : (a : β) → γ) a_1 : γ)
⊢ Eq (α := (β ↪ γ) → Prop)
    (fun (b : β ↪ γ) ↦
      Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
        (Set.range.{u_3, u_2 + 1} (ι := β) (⇑b : (a : β) → γ)))
    fun (f : β ↪ γ) ↦
    ∀ (a_1 : β),
      Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
        ((f : (a : β) → γ) a_1 : γ)

Tactic:
ext f
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
h :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    Subset.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
h₁ :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
h₂ h₃ :
  Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ)) ↔
    Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ))
      (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
⊢ Disjoint.{u_3} (α := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))
      (Set.range.{u_3, u_2 + 1} (ι := β) (⇑f : (a : β) → γ)) ↔
    ∀ (a_1 : β),
      Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ) (Set.range.{u_3, u_1 + 1} (ι := α) (⇑a : (a : α) → γ))ᶜ
        ((f : (a : β) → γ) a_1 : γ)

Tactic:
rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]

Premises used: Set.subset_compl_iff_disjoint_right, disjoint_comm, Set.range_subset_iff
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x : α ↪ β
h :
  ∀ (x_1 : α),
    Eq.{u_2 + 1} (α := β)
      (((fun (x : β) ↦ ({ toFun := fun (x_2 : α) ↦ x, inj' := ⋯ } : α ↪ β))
              ((fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β)) x) :
            (a : α) → β)
          x_1 :
        β)
      ((x : (a : α) → β) x_1 : β)
⊢ (fun (x : β) ↦ ({ toFun := fun (x_1 : α) ↦ x, inj' := ⋯ } : α ↪ β))
      ((fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β)) x) =
    x

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

Tactic:
simp_rw [Function.Embedding.coeFn_mk]

Premises used: Function.Embedding.coeFn_mk
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x_1 : α ↪ β
x : α
h : default = x
⊢ Eq.{u_2 + 1} (α := β) ((x_1 : (a : α) → β) default : β) ((x_1 : (a : α) → β) x : β)

Tactic:
congr 1
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x_1 : α ↪ β
x : α
⊢ default = x

Tactic:
Subsingleton.elim _ x

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x_1 : α ↪ β
x : α
⊢ default = x

Tactic:
exact Subsingleton.elim _ x

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Equiv.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : Unique α
x : β
⊢ (fun (f : α ↪ β) ↦ ((f : (a : α) → β) default : β))
      ((fun (x : β) ↦ ({ toFun := fun (x_1 : α) ↦ x, inj' := ⋯ } : α ↪ β)) x) =
    x

Tactic:
simp