awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
pos : ∀ (h : p a), x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
⊢ (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x a) = x a
have neg : ¬p a → x a = x a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
h : p a
⊢ x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
have pos : (x ∘ Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
x_1 : { a : α // ¬p a }
a : α
h : ¬p a
⊢ (if h_1 : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) (↑(Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) : α) h_1)
    else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) (↑(Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) : α) h_1)) =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
have dsimp : (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
  x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x : { a : α // ¬p a } → β
x_1 : { a : α // ¬p a }
a : α
h : ¬p a
⊢ (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)) =
    x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
have rw : x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h) = x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h)
Tactic: rw [dif_neg h]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
n : ℕ
⊢ Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) n) =
    n
have zero : Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
    ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) 0) =
  0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
n : ℕ
zero :
  Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) 0) =
    0
⊢ Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) n) =
    n
have succ : ∀ (n : ℕ),
  Sum.elim succ (fun (x : PUnit.{u_9 + 1}) ↦ 0)
      ((fun (n : ℕ) ↦ (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ PUnit) n (inr PUnit.unit) inl : ℕ ⊕ PUnit)) (n + 1)) =
    n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ p ((Equiv.refl α : (a : α) → α) a)
⊢ Eq.{max 1 u_1} ((Equiv.refl α).subtypeEquiv (p := p) (q := p) h) (Equiv.refl.{max 1 u_1} { a : α // p a })
have H : ∀ (x : { a : α // p a }),
  Eq.{u_1} (α := α)
    (↑(((Equiv.refl α).subtypeEquiv (p := p) (q := p) h : (a : { a : α // p a }) → { a : α // p a }) x) : α)
    (↑((Equiv.refl.{max 1 u_1} { a : α // p a } : (a : { a : α // p a }) → { a : α // p a }) x) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p : α → Prop
q : Subtype p → Prop
a : Subtype.{max 1 u_1} q
⊢ q (Subtype.mk (p := p) (↑(↑a : Subtype p) : α) ⋯)
have rcases : ∀ (a : α) (hap : p a) (haq : q (Subtype.mk (p := p) a hap)),
  q (Subtype.mk (p := p) (↑(↑(Subtype.mk.{max 1 u_1} (p := q) (Subtype.mk (p := p) a hap) haq) : Subtype p) : α) sorry)
Tactic: rcases a with ⟨⟨a, hap⟩, haq⟩
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
have F : (a : Subtype q) → { x : α // f x = (↑a : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) sorry = a }
Tactic: apply sigmaCongrRight
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x : α // f x = (↑y : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
have F : { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) sorry = y } ≃ { x : α // f x = (↑y : β) }
Tactic: apply Equiv.symm
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
⊢ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y } ≃ { x : α // f x = (↑y : β) }
have F : ∀ (x : α), (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) sorry = y) ↔ f x = (↑y : β)
Tactic: refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
have F : (a : Subtype q) → { x : α // f x = (↑a : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) sorry = a }
Tactic: {
          apply sigmaCongrRight
          intro y
          apply Equiv.symm
          refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
          intro x
          exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩ }
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
F F₁ : (y : Subtype q) → { x : α // f x = (↑y : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
have F₂ : (y : Subtype q) → { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) sorry = y } ≃ { x : α // f x = (↑y : β) }
Tactic: {
          apply sigmaCongrRight
          intro y
          apply Equiv.symm
          refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
          intro x
          exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩ }
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : Type u_10
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
F F₁ : (y : Subtype q) → { x : α // f x = (↑y : β) } ≃ { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
F₂ : (y : Subtype q) → { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y } ≃ { x : α // f x = (↑y : β) }
⊢ (y : Subtype q) × { x : α // f x = (↑y : β) } ≃
    (y : Subtype q) × { x : Subtype p // Subtype.mk (p := q) (f (↑x : α)) ⋯ = y }
have F₃ : ∀ (y : Subtype q) (x : α),
  (∃ (h_1 : p x), Subtype.mk (p := q) (f (↑(Subtype.mk (p := p) x h_1) : α)) sorry = y) ↔ f x = (↑y : β)
Tactic: {
          apply sigmaCongrRight
          intro y
          apply Equiv.symm
          refine (subtypeSubtypeEquivSubtypeExists _ _).trans (subtypeEquivRight ?_)
          intro x
          exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩ }
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : Option α → Type v
h : ∀ (a : p none), False
x : Option α
⊢ ∀ (a : p x), x.isSome = true
have none : ∀ (a : p none), Option.isSome.{u_9} (α := α) none = true
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : Option α → Type v
h : ∀ (a : p Option.none), False
x : Option α
none : ∀ (a : p Option.none), Option.isSome.{u_9} (α := α) Option.none = true
⊢ ∀ (a : p x), x.isSome = true
have some : ∀ (val : α) (a : p (some val)), (some val).isSome = true
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : Option α → Type v
h : ∀ (a : p none), False
n : p none
⊢ Option.isSome.{u_9} (α := α) none = true
have none : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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_9
f : { f : ι → (i : ι) × π i // ∀ (i : ι), (f i).fst (β := fun (i : ι) ↦ π i) = i }
i : ι
⊢ π i
have rw : π (((↑f : ι → (i : ι) × π i) i).fst (β := fun (i : ι) ↦ π i))
Tactic: rw [← f.2 i]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
β : α → Sort v
p : (a : α) → β a → Prop
f : (a : α) → { b : β a // p a b }
⊢ (fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
        (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) ⋯ : { b : β a // p a b }))
      ((fun (f : (a : α) → { b : β a // p a b }) ↦
          (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) ⋯ :
            { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
        f) =
    f
have h : ∀ (a : α),
  Eq.{max 1 v}
    ((fun (f : { f : (a : α) → β a // ∀ (a : α), p a (f a) }) (a : α) ↦
        (Subtype.mk (p := fun (b : β a) ↦ p a b) ((↑f : (a : α) → β a) a) sorry : { b : β a // p a b }))
      ((fun (f : (a : α) → { b : β a // p a b }) ↦
          (Subtype.mk (p := fun (f : (a : α) → β a) ↦ ∀ (a : α), p a (f a)) (fun (a : α) ↦ (↑(f a) : β a)) sorry :
            { f : (a : α) → β a // ∀ (a : α), p a (f a) }))
        f)
      a)
    (f a)
Tactic: funext a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
β : α → Type u_10
a_1 : α
x : { s : Sigma β // s.fst (β := β) = a_1 }
a : Sigma β
h : a.fst (β := β) = a_1
⊢ Eq (α := { s : Sigma β // s.fst (β := β) = a_1 })
    ((fun (b : β a_1) ↦ Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) (Sigma.mk (β := β) a_1 b) ⋯)
      ((fun (x : { s : Sigma β // s.fst (β := β) = a_1 }) ↦
          (match (motive := { s : Sigma β // s.fst (β := β) = a_1 } → β a_1) x with
            | ⟨⟨fst, b⟩, h⟩ =>
              Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
            β a_1))
        (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) a h)))
    (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a_1) a h)
have refl : ∀ (x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }),
  Eq (α := { s : Sigma β // s.fst (β := β) = a.fst (β := β) })
    ((fun (b : β (a.fst (β := β))) ↦
        Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) (Sigma.mk (β := β) (a.fst (β := β)) b) sorry)
      ((fun (x : { s : Sigma β // s.fst (β := β) = a.fst (β := β) }) ↦
          (match (motive := { s : Sigma β // s.fst (β := β) = a.fst (β := β) } → β (a.fst (β := β))) x with
            | ⟨⟨fst, b⟩, h⟩ =>
              Eq.rec (motive := fun (x : α) (h : (Sigma.mk (β := β) fst b).fst (β := β) = x) ↦ β x) b h :
            β (a.fst (β := β))))
        (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a sorry)))
    (Subtype.mk (p := fun (s : Sigma β) ↦ s.fst (β := β) = a.fst (β := β)) a sorry)
Tactic: cases h
Cleared hypotheses: a_1, x, h
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
⊢ γ (Sigma.fst (β := β) (↑default : Sigma β)) (Sigma.snd (β := β) (↑default : Sigma β)) = γ a b
have rw : γ
    ((↑(Subtype.mk (p := fun (ab : (a : α) × β a) ↦ p ab) (Sigma.mk (β := fun (a : α) ↦ β a) a b) h) : Sigma β).fst
      (β := β))
    ((↑(Subtype.mk (p := fun (ab : (a : α) × β a) ↦ p ab) (Sigma.mk (β := fun (a : α) ↦ β a) a b) h) : Sigma β).snd
      (β := β)) =
  γ a b
Tactic: rw [← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab : (a : α) × β a // p ab }
a : α
b : β a
c : γ a b
h : p (Sigma.mk (β := fun (a : α) ↦ β a) a b)
⊢ (Equiv.symm (sigmaSigmaSubtype (β := β) (γ := γ) p h) :
        (a : γ a b) → { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ })
      c =
    Subtype.mk (p := fun (s : (a : α) × (b : β a) × γ a b) ↦
      p
        (Sigma.mk (β := fun (a : α) ↦ β a) (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))
          (s.snd (β := fun (a : α) ↦ (b : β a) × γ a b).fst (β :=
            fun (b : β (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))) ↦
            γ (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b)) b))))
      (Sigma.mk (β := fun (a : α) ↦ (b : β a) × γ a b) a (Sigma.mk (β := fun (b : β a) ↦ γ a b) b c)) h
have rw : c =
  (sigmaSigmaSubtype (β := β) (γ := γ) p h :
      (a_1 : { s : (a : α) × (b : β a) × γ a b // p ⟨s.fst, s.snd.fst⟩ }) → γ a b)
    (Subtype.mk (p := fun (s : (a : α) × (b : β a) × γ a b) ↦
      p
        (Sigma.mk (β := fun (a : α) ↦ β a) (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))
          (s.snd (β := fun (a : α) ↦ (b : β a) × γ a b).fst (β :=
            fun (b : β (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b))) ↦
            γ (s.fst (β := fun (a : α) ↦ (b : β a) × γ a b)) b))))
      (Sigma.mk (β := fun (a : α) ↦ (b : β a) × γ a b) a (Sigma.mk (β := fun (b : β a) ↦ γ a b) b c)) h)
Tactic: rw [Equiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a_1 : { x : Quotient s₁ // p₂ x }
a b : α
hab : a ≈ b
⊢ p₂ ⟦a⟧ = p₂ ⟦b⟧
have rw : p₂ ⟦b⟧ = p₂ ⟦b⟧
Tactic: rw [Quotient.sound hab]
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : { x : Quotient s₁ // p₂ x }
⊢ Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        a))
    a
have obtain : ∀ (a : Quotient s₁) (ha : p₂ a),
  Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ sorry) sorry :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a sorry⟧) sorry sorry :
            Quotient.{max 1 u_1} s₂))
        (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)))
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)
Tactic: obtain ⟨a, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : Quotient s₁
ha : p₂ a
⊢ Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
            Quotient.{max 1 u_1} s₂))
        (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)))
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) a ha)
have h₁ : ∀ (a : α) (ha : p₂ ⟦a⟧),
  Eq.{max 1 u_1}
    ((fun (a : Quotient.{max 1 u_1} s₂) ↦
        (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
            (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ sorry) sorry :
          { x : Quotient s₁ // p₂ x }))
      ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
          (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
              (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a sorry⟧) sorry sorry :
            Quotient.{max 1 u_1} s₂))
        (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)))
    (Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦a⟧ ha)
Tactic: induction a using Quotient.inductionOn
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (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
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid.{max 1 u_1} (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), (s₂ : Subtype p₁ → Subtype p₁ → Prop) x y ↔ (s₁ : α → α → Prop) (↑x : α) (↑y : α)
a : Quotient.{max 1 u_1} s₂
⊢ Eq.{max 1 u_1}
    ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
        (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
            (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a ⋯⟧) ⋯ ⋯ :
          Quotient.{max 1 u_1} s₂))
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ ⋯) ⋯ :
            { x : Quotient s₁ // p₂ x }))
        a))
    a
have h₁ : ∀ (a : Subtype p₁),
  Eq.{max 1 u_1}
    ((fun (a : { x : Quotient s₁ // p₂ x }) ↦
        (Quotient.hrecOn (motive := fun (x : Quotient s₁) ↦ p₂ x → Quotient.{max 1 u_1} s₂) (↑a : Quotient s₁)
            (fun (a : α) (h : p₂ ⟦a⟧) ↦ ⟦Subtype.mk (p := p₁) a sorry⟧) sorry sorry :
          Quotient.{max 1 u_1} s₂))
      ((fun (a : Quotient.{max 1 u_1} s₂) ↦
          (Quotient.liftOn.{max 1 u_1, max 1 u_1} a
              (fun (a : Subtype p₁) ↦ Subtype.mk (p := fun (x : Quotient s₁) ↦ p₂ x) ⟦(↑a : α)⟧ sorry) sorry :
            { x : Quotient s₁ // p₂ x }))
        ⟦a⟧))
    ⟦a⟧
Tactic: induction a using Quotient.inductionOn
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
⊢ swapCore a a r = r
have unfold : (if r = a then a else if r = a then a else r) = r
Tactic: unfold swapCore
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
⊢ (if r = a then a else if r = a then a else r) = r
have pos : r = a → a = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a : α
pos : r = a → a = r
⊢ (if r = a then a else if r = a then a else r) = r
have neg : ¬r = a → r = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
⊢ swapCore a b (swapCore a b r) = r
have unfold : (if (if r = a then b else if r = b then a else r) = a then b
  else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
  r
Tactic: unfold swapCore
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have pos : r = a → b = a → b = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have pos₁ : r = a → ¬b = a → b = b → a = r
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
α : Sort u_1
inst : DecidableEq α
r a b : α
pos : r = a → b = a → b = r
pos₁ : r = a → ¬b = a → b = b → a = r
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
have neg : r = a → ¬b = a → ¬b = b → b = r
Tactic: split_ifs