awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P ((e.symm : (a : β) → α) b)
b' : β
⊢ Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))
have h : ∀ (x : P ((e.symm : (a : β) → α) b')),
  Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b') x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b' x b' :
      P ((e.symm : (a : β) → α) b'))
Tactic: rcases eq_or_ne b' b with (rfl | h)
Cleared hypotheses: b, x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
β : Sort u_4
inst : DecidableEq α
inst_1 : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P ((e.symm : (a : β) → α) b)
b' : β
h :
  ∀ (x : P ((e.symm : (a : β) → α) b')),
    Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
      ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
          (update (β := P) f ((e.symm : (a : β) → α) b') x) b' :
        P ((e.symm : (a : β) → α) b'))
      (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
          ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b' x b' :
        P ((e.symm : (a : β) → α) b'))
⊢ Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))
have h₁ : ∀ (h : b' ≠ b),
  Eq.{u_10} (α := P ((e.symm : (a : β) → α) b'))
    ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b))
        (update (β := P) f ((e.symm : (a : β) → α) b) x) b' :
      P ((e.symm : (a : β) → α) b'))
    (update (β := fun (a : β) ↦ P ((e.symm : (a : β) → α) a))
        ((Equiv.piCongrLeft' P e : (a : (a : α) → P a) → (b : β) → P ((e.symm : (a : β) → α) b)) f) b x b' :
      P ((e.symm : (a : β) → α) b'))
Tactic: rcases eq_or_ne b' b with (rfl | h)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
⊢ e₁ = e₂
have mk : ∀ (toFun : α → β) (invFun : β → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun)
  (h₁ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun = e₂.toFun)
  (h₂ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun = e₂.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } = e₂
Tactic: cases e₁
Cleared hypotheses: e₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun : α → β
invFun : β → α
left_inv : LeftInverse invFun toFun
right_inv : RightInverse invFun toFun
h₁ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun = e₂.toFun
h₂ : { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun = e₂.invFun
⊢ { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } = e₂
have mk : ∀ (toFun_1 : α → β) (invFun_1 : β → α) (left_inv_1 : LeftInverse invFun_1 toFun_1)
  (right_inv_1 : RightInverse invFun_1 toFun_1)
  (h₁ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.toFun =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.toFun)
  (h₂ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β }.invFun =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
Tactic: cases e₂
Cleared hypotheses: e₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Type u_1
inst : Subsingleton α
e : Perm α
⊢ Eq (α := (a : α) → α) (⇑e : (a : α) → α) id
have rw : Eq (α := (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) id
Tactic: rw [Perm.subsingleton_eq_refl e, coe_refl]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Type u_1
inst : Subsingleton α
e : Perm α
rw : Eq (α := (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) id
⊢ Eq (α := (a : α) → α) (⇑e : (a : α) → α) id
have rw₁ : Eq.{u_1 + 1} (α := (a : α) → α) id id
Tactic: rw [Perm.subsingleton_eq_refl e, coe_refl]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ Eq (α := γ) ((Equiv.cast ⋯ : (a : α) → γ) x : γ) (((Equiv.cast h).trans (Equiv.cast h2) : (a : α) → γ) x : γ)
have substs : Eq (α := α) ((Equiv.cast sorry : (a : α) → α) x : α) (((Equiv.cast sorry).trans (Equiv.cast sorry) : (a : α) → α) x : α)
Tactic: substs h h2
Cleared hypotheses: β, γ, h, h2
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h : (a : α) → β) a = b ↔ a ≍ b
have subst : ∀ {b : α}, (Equiv.cast sorry : (a : α) → α) a = b ↔ a ≍ b
Tactic: subst h
Cleared hypotheses: β, h, b
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
e : α ≃ β
⊢ (Equiv.refl α).trans e = e
have mk : ∀ (toFun : α → β) (invFun : β → α) (left_inv : LeftInverse invFun toFun) (right_inv : RightInverse invFun toFun),
  (Equiv.refl α).trans { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : α ≃ β } =
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv }
Tactic: cases e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
⊢ extend (⇑f : (a : α) → β) g e' b = g ((f.symm : (a : β) → α) b)
have rw : extend (⇑f : (a : α) → β) g e' ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α)) =
  g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
Tactic: rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
rw :
  extend (⇑f : (a : α) → β) g e' ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α)) =
    g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
⊢ extend (⇑f : (a : α) → β) g e' b = g ((f.symm : (a : β) → α) b)
have rw₁ : g ((f.symm : (a : β) → α) b) = g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
Tactic: rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
f : α ≃ β
g : α → γ
e' : β → γ
b : β
rw :
  extend (⇑f : (a : α) → β) g e' ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α)) =
    g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
rw₁ : g ((f.symm : (a : β) → α) b) = g ((f.symm : (a : β) → α) ((f : (a : α) → β) ((f.symm : (a : β) → α) b : α) : β))
⊢ extend (⇑f : (a : α) → β) g e' b = g ((f.symm : (a : β) → α) b)
have rw₂ : g ((f.symm : (a : β) → α) b) = g ((f.symm : (a : β) → α) b)
Tactic: rw [← f.apply_symm_apply b, f.injective.extend_apply, apply_symm_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm
have H : ∀ (x : β ≃ δ) (x_1 : α),
  Eq.{w} (α := γ) (((((ab.equivCongr cd).symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)
    ((((ab.symm.equivCongr cd.symm : (a : β ≃ δ) → α ≃ γ) x : α ≃ γ) : (a : α) → γ) x_1 : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw₁ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
    (⇑(Equiv.refl α) : (a : α) → α) ↔
  f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
rw₁ :
  Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
      (⇑(Equiv.refl α) : (a : α) → α) ↔
    f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw₂ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β)) id ↔ f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
rw₁ :
  Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
      (⇑(Equiv.refl α) : (a : α) → α) ↔
    f = g.symm
rw₂ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β)) id ↔ f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw₃ : Eq (α := α → β) (⇑f : (a : α) → β) ((⇑g.symm : (a : α) → β) ∘ id) ↔ f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
rw₁ :
  Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
      (⇑(Equiv.refl α) : (a : α) → α) ↔
    f = g.symm
rw₂ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β)) id ↔ f = g.symm
rw₃ : Eq (α := α → β) (⇑f : (a : α) → β) ((⇑g.symm : (a : α) → β) ∘ id) ↔ f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw₄ : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g.symm : (a : α) → β) ↔ f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
rw : Eq.{u} (α := (a : α) → α) (⇑(f.trans g) : (a : α) → α) (⇑(Equiv.refl α) : (a : α) → α) ↔ f = g.symm
rw₁ :
  Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β))
      (⇑(Equiv.refl α) : (a : α) → α) ↔
    f = g.symm
rw₂ : Eq.{u} (α := (a : α) → α) (comp.{u, v, u} (β := β) (⇑g : (a : β) → α) (⇑f : (a : α) → β)) id ↔ f = g.symm
rw₃ : Eq (α := α → β) (⇑f : (a : α) → β) ((⇑g.symm : (a : α) → β) ∘ id) ↔ f = g.symm
rw₄ : Eq (α := α → β) (⇑f : (a : α) → β) (⇑g.symm : (a : α) → β) ↔ f = g.symm
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f = g.symm
have rw₅ : f = g.symm ↔ f = g.symm
Tactic: rw [← Equiv.coe_inj, coe_trans, coe_refl, ← eq_symm_comp, comp_id, Equiv.coe_inj]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ Eq.{max 1 u} (f.trans g) (Equiv.refl α) ↔ f.symm = g
have rw : f = g.symm ↔ f.symm = g
Tactic: rw [trans_eq_refl_iff_eq_symm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
inst : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) = f
have h : ∀ (i : α), uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) i = f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β_1 : Sort v
γ : Sort w
inst : Unique α
β : α → Sort u_1
f : (i : α) → β i
i : α
⊢ uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) i = f i
have h : Eq (α := β default) (uniqueElim (α := β) ((fun (f : (i : α) → β i) ↦ (f default : β default)) f) default) (f default)
Tactic: cases Unique.eq_default i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Logic.Equiv.Defs (goal)
Goal:
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x : α ≃ β
⊢ (fun (f : { f : α → β // Bijective f }) ↦ ofBijective (↑f : α → β) ⋯)
      ((fun (f : α ≃ β) ↦ Subtype.mk (p := fun (f : α → β) ↦ Bijective f) (⇑f : (a : α) → β) ⋯) x) =
    x
have H : ∀ (x_1 : α),
  Eq.{v} (α := β)
    (((fun (f : { f : α → β // Bijective f }) ↦ ofBijective (↑f : α → β) sorry)
            ((fun (f : α ≃ β) ↦ Subtype.mk (p := fun (f : α → β) ↦ Bijective f) (⇑f : (a : α) → β) sorry) x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ 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 : β) → γ))
have 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
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (hypothesis)
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 : γ)
⊢ False
have this : Sum.inl a = Sum.inr b
Tactic: have : Sum.inl a = Sum.inr b := f.injective h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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₂ : γ)
⊢ Eq (α := α ⊕ β) (Sum.inl a₁) (Sum.inl a₂)
have inl : Eq (α := α ⊕ β) (Sum.inl a₂) (Sum.inl a₂)
Tactic: rw [f.injective f_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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₂ : γ)
⊢ Sum.inl a₁ = Sum.inr b₂
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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₂ : γ)
⊢ Sum.inr b₁ = Sum.inl a₂
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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₂ : γ)
⊢ Eq (α := α ⊕ β) (Sum.inr b₁) (Sum.inr b₂)
have inr : Eq (α := α ⊕ β) (Sum.inr b₂) (Sum.inr b₂)
Tactic: rw [g.injective f_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ {
      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
have 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' := sorry } :
          (a : α ⊕ β) → γ)
        x :
      γ)
    ((f : (a : α ⊕ β) → γ) x : γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
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 : γ)
have 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' := sorry } :
          (a : α ⊕ β) → γ)
        (Sum.inl val) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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) : γ)
⊢ 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 : γ)
have 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' := sorry } :
          (a : α ⊕ β) → γ)
        (Sum.inr val) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
⊢ 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 : γ)
have 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 : γ)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
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 : γ)
have 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 : α) → γ))ᶜ
Tactic: rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Embedding (goal)
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 : α) → γ))ᶜ
⊢ 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 : γ)
have 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 : α) → γ))
Tactic: rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]