awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
hs :
  (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁ :
  (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₂ hs₃ :
  x ∈ e.source →
    y ∈ e'.source →
      (↑e : α → β) x ∈ f.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₄ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₅ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
hs₆ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
hs₇ :
  x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
hs₈ hs₉ :
  x ∈ e.source →
    (↑e : α → β) x ∈ f.source →
      y ∈ e'.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁₀ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₁₁ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source ↔
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
have hs₁₂ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
hs :
  (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁ :
  (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source →
    (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₂ hs₃ :
  x ∈ e.source →
    y ∈ e'.source →
      (↑e : α → β) x ∈ f.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₄ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₅ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
hs₆ : x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
hs₇ :
  x ∈ e.source → y ∈ e'.source → (↑e : α → β) x ∈ f.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
hs₈ hs₉ :
  x ∈ e.source →
    (↑e : α → β) x ∈ f.source →
      y ∈ e'.source →
        (↑e' : δ → η) y ∈ f'.source →
          (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source
hs₁₀ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → x ∈ e.source
hs₁₁ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → y ∈ e'.source
hs₁₂ :
  x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → (↑e : α → β) x ∈ f.source
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ (↑e : α → β) x ∈ f.source ∧ (↑e' : δ → η) y ∈ f'.source ↔
    (x ∈ e.source ∧ (↑e : α → β) x ∈ f.source) ∧ y ∈ e'.source ∧ (↑e' : δ → η) y ∈ f'.source
have hs₁₃ : x ∈ e.source → (↑e : α → β) x ∈ f.source → y ∈ e'.source → (↑e' : δ → η) y ∈ f'.source → (↑e' : δ → η) y ∈ f'.source
Tactic: tauto
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
⊢ Eq (α := PartialEquiv ((i : ι) → αi i) ((i : ι) → αi i))
    (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) (PartialEquiv.refl ((i : ι) → αi i))
have h : ∀ (x : (i : ι) → αi i) (x_1 : ι),
  (↑(PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) : ((i : ι) → αi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.refl ((i : ι) → αi i)) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑(PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) :
          ((i : ι) → αi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.refl ((i : ι) → αi i)) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
⊢ Eq (α := PartialEquiv ((i : ι) → αi i) ((i : ι) → αi i))
    (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) (PartialEquiv.refl ((i : ι) → αi i))
have hsymm : ∀ (x : (i : ι) → αi i) (x_1 : ι),
  (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) :
        ((i : ι) → αi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.symm (PartialEquiv.refl ((i : ι) → αi i))) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑(PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) :
          ((i : ι) → αi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.refl ((i : ι) → αi i)) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
hsymm :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) :
          ((i : ι) → αi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.symm (PartialEquiv.refl ((i : ι) → αi i))) : ((i : ι) → αi i) → (i : ι) → αi i) x x_1
⊢ Eq (α := PartialEquiv ((i : ι) → αi i) ((i : ι) → αi i))
    (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i)) (PartialEquiv.refl ((i : ι) → αi i))
have hs : ∀ (x : (i : ι) → αi i),
  Membership.mem (γ := Set ((i : ι) → αi i))
      (source (β := (i : ι) → αi i) (PartialEquiv.pi (αi := αi) (βi := αi) fun (i : ι) ↦ PartialEquiv.refl (αi i))) x ↔
    Membership.mem (γ := Set ((i : ι) → αi i)) (source (PartialEquiv.refl ((i : ι) → αi i))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
⊢ (PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei') =
    PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)
have h : ∀ (x : (i : ι) → αi i) (x_1 : ι),
  (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')) :
        ((i : ι) → αi i) → (i : ι) → γi i)
      x x_1 =
    (↑(PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)) : ((i : ι) → αi i) → (i : ι) → γi i) x
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')) :
          ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1 =
      (↑(PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)) : ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1
⊢ (PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei') =
    PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)
have hsymm : ∀ (x : (i : ι) → γi i) (x_1 : ι),
  (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).symm :
        ((i : ι) → γi i) → (i : ι) → αi i)
      x x_1 =
    (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) :
        ((i : ι) → γi i) → (i : ι) → αi i)
      x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
Goal:
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv.{u_6, u_7} (αi i) (βi i)
ei' : (i : ι) → PartialEquiv.{u_7, u_8} (βi i) (γi i)
h :
  ∀ (x : (i : ι) → αi i) (x_1 : ι),
    (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')) :
          ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1 =
      (↑(PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)) : ((i : ι) → αi i) → (i : ι) → γi i)
        x x_1
hsymm :
  ∀ (x : (i : ι) → γi i) (x_1 : ι),
    (↑((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).symm :
          ((i : ι) → γi i) → (i : ι) → αi i)
        x x_1 =
      (↑(PartialEquiv.symm (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) :
          ((i : ι) → γi i) → (i : ι) → αi i)
        x x_1
⊢ (PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei') =
    PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i)
have hs : ∀ (x : (i : ι) → αi i),
  x ∈ ((PartialEquiv.pi (αi := αi) (βi := βi) ei).trans (PartialEquiv.pi (αi := βi) (βi := γi) ei')).source ↔
    Membership.mem (γ := Set ((i : ι) → αi i))
      (source (β := (i : ι) → γi i) (PartialEquiv.pi (αi := αi) (βi := γi) fun (i : ι) ↦ (ei i).trans (ei' i))) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrLeft e).trans (prodComm β₂ α₁) = (prodComm β₁ α₁).trans (prodCongrRight e)
have H : ∀ (a : β₁) (b : α₁),
  Eq (α := α₁ × β₂) (((prodCongrLeft e).trans (prodComm β₂ α₁) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)
    (((prodComm β₁ α₁).trans (prodCongrRight e) : (a : β₁ × α₁) → α₁ × β₂) (a, b) : α₁ × β₂)
Tactic: ext ⟨a, b⟩ : 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (prodCongrRight e).trans (prodComm α₁ β₂) = (prodComm α₁ β₁).trans (prodCongrLeft e)
have H : ∀ (a : α₁) (b : β₁),
  Eq (α := β₂ × α₁) (((prodCongrRight e).trans (prodComm α₁ β₂) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)
    (((prodComm α₁ β₁).trans (prodCongrLeft e) : (a : α₁ × β₁) → β₂ × α₁) (a, b) : β₂ × α₁)
Tactic: ext ⟨a, b⟩ : 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaCongrRight (β₁ := fun (a : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e).trans (sigmaEquivProd α₁ β₂) =
    (sigmaEquivProd α₁ β₁).trans (prodCongrRight e)
have H : ∀ (a : α₁) (b : β₁),
  Eq (α := α₁ × β₂)
    (((sigmaCongrRight (β₁ := fun (a : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e).trans (sigmaEquivProd α₁ β₂) :
          (a : (_ : α₁) × β₁) → α₁ × β₂)
        (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
      α₁ × β₂)
    (((sigmaEquivProd α₁ β₁).trans (prodCongrRight e) : (a : (_ : α₁) × β₁) → α₁ × β₂)
        (Sigma.mk (β := fun (a : α₁) ↦ β₁) a b) :
      α₁ × β₂)
Tactic: ext ⟨a, b⟩ : 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) =
    (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm
have H : ∀ (a : α₁) (b : β₁),
  Eq (α := (_ : α₁) × β₂)
    (((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) :
          (a : α₁ × β₁) → (_ : α₁) × β₂)
        (a, b) :
      (_ : α₁) × β₂)
    (((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₁) → (_ : α₁) × β₂) (a, b) : (_ : α₁) × β₂)
Tactic: ext ⟨a, b⟩ : 1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ Eq (α := (_ : α₁) × β₂)
    (((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight (β₁ := fun (x : α₁) ↦ β₁) (β₂ := fun (a : α₁) ↦ β₂) e) :
          (a : α₁ × β₁) → (_ : α₁) × β₂)
        (a, b) :
      (_ : α₁) × β₂)
    (((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₁) → (_ : α₁) × β₂) (a, b) : (_ : α₁) × β₂)
have H : Eq (α := (_ : α₁) × β₂)
  (Sigma.mk (β := fun (a : α₁) ↦ β₂)
      (Sigma.fst (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)))
      ((e (Sigma.fst (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b))) :
          (a : β₁) → β₂)
        (Sigma.snd (β := fun (a : α₁) ↦ β₁) (((sigmaEquivProd α₁ β₁).symm : (a : α₁ × β₁) → (_ : α₁) × β₁) (a, b)) :
          β₁)) :
    (_ : α₁) × β₂)
  (((sigmaEquivProd α₁ β₂).symm : (a : α₁ × β₂) → (_ : α₁) × β₂) (a, (e a : (a : β₁) → β₂) b) : (_ : α₁) × β₂)
Tactic: simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
Goal:
α₁ : Type u_9
β₁ : Type u_10
inst : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) ≠ (a', b)
⊢ a' = a
have contrapose! : ∀ (h : a' ≠ a), (prodExtendRight a e : (a : α₁ × β₁) → α₁ × β₁) (a', b) = (a', b)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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_11
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
⊢ (fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f) =
    f
have h : ∀ (i : ι),
  Eq (α := π (inl i))
    ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f)
      (inl i))
    (f (inl i))
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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_11
π : ι ⊕ ι' → Type u_9
f : (i : ι ⊕ ι') → π i
h :
  ∀ (i : ι),
    Eq (α := π (inl i))
      ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
          Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
        ((fun (f : (i : ι ⊕ ι') → π i) ↦
            ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
          f)
        (inl i))
      (f (inl i))
⊢ (fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f) =
    f
have h₁ : ∀ (i : ι'),
  Eq (α := π (inr i))
    ((fun (g : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))) (t : ι ⊕ ι') ↦
        Sum.rec (motive := fun (x : ι ⊕ ι') ↦ π x) g.fst g.snd t)
      ((fun (f : (i : ι ⊕ ι') → π i) ↦
          ((fun (i : ι) ↦ f (inl i), fun (i' : ι') ↦ f (inr i')) : ((i : ι) → π (inl i)) × ((i' : ι') → π (inr i'))))
        f)
      (inr i))
    (f (inr i))
Tactic: ext (i | i)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
f : α ⊕ β → γ
⊢ (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) = f
have h : ∀ (val : α),
  (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inl val) =
    f (inl val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
f : α ⊕ β → γ
h :
  ∀ (val : α),
    (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inl val) =
      f (inl val)
⊢ (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) = f
have h₁ : ∀ (val : β),
  (fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) ((fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) f) (inr val) =
    f (inr val)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
p : (α → γ) × (β → γ)
⊢ (fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) ((fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) p) = p
have mk : ∀ (fst : α → γ) (snd : β → γ),
  (fun (f : α ⊕ β → γ) ↦ (f ∘ inl, f ∘ inr)) ((fun (p : (α → γ) × (β → γ)) ↦ Sum.elim p.fst p.snd) (fst, snd)) =
    (fst, snd)
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
⊢ (fun (f : (i : α) → β i) ↦
        ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
          ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
          (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
            else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
            β x))
        (f, g)) =
    (f, g)
have fst : Prod.fst (β := (i : { x : α // ¬p x }) → β (↑i : α))
    ((fun (f : (i : α) → β i) ↦
        ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
          ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
          (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
            else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
            β x))
        (f, g))) =
  (f, g).fst
Tactic: ext1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
fst :
  Prod.fst (β := (i : { x : α // ¬p x }) → β (↑i : α))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
            (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
              else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
              β x))
          (f, g))) =
    (f, g).fst
⊢ (fun (f : (i : α) → β i) ↦
        ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
          ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
          (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
            else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
            β x))
        (f, g)) =
    (f, g)
have snd : Prod.snd (α := (i : { x : α // p x }) → β (↑i : α))
    ((fun (f : (i : α) → β i) ↦
        ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
          ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
          (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
            else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
            β x))
        (f, g))) =
  (f, g).snd
Tactic: ext1
-- Lean 4 proof step from Mathlib.Logic.Equiv.Prod (goal)
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
inst : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))
⊢ (fun (f : (j : α) → β j) ↦
        ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
      ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
          (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
            else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
            β j))
        f) =
    f
have fst : Prod.fst (β := (j : { j : α // j ≠ i }) → β (↑j : α))
    ((fun (f : (j : α) → β j) ↦
        ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
      ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
          (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst sorry
            else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
            β j))
        f)) =
  f.fst
Tactic: ext x