awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ Eq (α := Option Bool) (decode n) none
have suffices : Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
Tactic: suffices decodeSum n = none by
    change (decodeSum n).bind _ = none
    rw [this]
    rfl
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
rw : HMul.hMul (α := ℕ) 1 2 ≤ n
⊢ 1 ≤ n / 2
have rw₁ : LT.lt (α := ℕ) 0 2
Tactic: rw [Nat.le_div_iff_mul_le]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (hypothesis)
Goal:
n : ℕ
h : 2 ≤ n
⊢ Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
have this : 1 ≤ n / 2
Tactic: have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
have obtain : ∀ (m : ℕ) (e : n / 2 = m.succ), Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
Tactic: obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) n.bodd, n / 2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))
have false : Eq (α := Option (Unit ⊕ Unit))
  (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) false, n / 2 with
    | false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m) :
    Option (Unit ⊕ Unit))
  (none : Option (Unit ⊕ Unit))
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
false :
  Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) Bool.false, n / 2 with
      | Bool.false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))
⊢ Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) n.bodd, n / 2 with
      | Bool.false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))
have true : Eq (α := Option (Unit ⊕ Unit))
  (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) true, n / 2 with
    | Bool.false, m => Option.map Sum.inl (decode m)
    | x, m => Option.map Sum.inr (decode m) :
    Option (Unit ⊕ Unit))
  (none : Option (Unit ⊕ Unit))
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
⊢ Eq (α := Option (α × β)) (decode n)
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have simp : Eq (α := Option (α × β))
  (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
    (Option.bind (decode (unpair n).1) fun (a : α) ↦
      Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
  (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
Tactic: simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind (decode (unpair n).1) fun (a : α) ↦
        Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have none : Eq (α := Option (α × β))
  (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
    (Option.bind none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
  (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
Tactic: cases (decode n.unpair.1 : Option α)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
none :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind (decode (unpair n).1) fun (a : α) ↦
        Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have some : ∀ (val : α),
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
Tactic: cases (decode n.unpair.1 : Option α)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have none : Eq (α := Option (α × β))
  (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
    (Option.bind none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
  (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) none)
Tactic: cases (decode n.unpair.2 : Option β)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
none :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) Option.none))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) Option.none)
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have none₁ : ∀ (val : β),
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (some val)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (some val))
Tactic: cases (decode n.unpair.2 : Option β)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : α
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have some : Eq (α := Option (α × β))
  (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
    ((some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
  ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)
Tactic: cases (decode n.unpair.2 : Option β)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : α
some :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
    ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
have some₁ : ∀ (val_1 : β),
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (Option.some val_1)))
    ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (Option.some val_1))
Tactic: cases (decode n.unpair.2 : Option β)
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
⊢ encode a = encode (↑a : α)
have mk : ∀ (val : α) (property : P val),
  encode (Subtype.mk (p := P) val property) = encode (↑(Subtype.mk (p := P) val property) : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence (r := r) f hf n)) (f (Directed.sequence (r := r) f hf (n + 1)))
have dsimp : r (f (Directed.sequence (r := r) f hf n))
  (f
    (match (motive := Option α → α) decode n with
    | none =>
      Classical.choose (p := fun (x : α) ↦
        r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f (Directed.sequence (r := r) f hf n)) (f x)) sorry
    | some a =>
      Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f a) (f x)) sorry))
Tactic: dsimp [Directed.sequence]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence (r := r) f hf n))
    (f
      (match (motive := Option α → α) decode n with
      | none =>
        Classical.choose (p := fun (x : α) ↦
          r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f (Directed.sequence (r := r) f hf n)) (f x)) ⋯
      | some a =>
        Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f a) (f x)) ⋯))
have generalize : ∀ (p : α),
  r (f p)
    (f
      (match (motive := Option α → α) decode n with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) sorry
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) sorry))
Tactic: generalize hf.sequence f n = p
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match (motive := Option α → α) decode n with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
have none : r (f p)
  (f
    (match (motive := Option α → α) none with
    | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) sorry
    | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) sorry))
Tactic: rcases (decode n : Option α) with - | a
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
none :
  r (f p)
    (f
      (match (motive := Option α → α) Option.none with
      | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
⊢ r (f p)
    (f
      (match (motive := Option α → α) decode n with
      | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
have some : ∀ (a : α),
  r (f p)
    (f
      (match (motive := Option α → α) some a with
      | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) sorry
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) sorry))
Tactic: rcases (decode n : Option α) with - | a
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a) (f (Directed.sequence (r := r) f hf (encode a + 1)))
have simp : r (f a)
  (f (Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf (encode a))) (f x) ∧ r (f a) (f x)) sorry))
Tactic: simp only [Directed.sequence, encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
⊢ Eq (α := Option (Quotient s))
    ((fun (n : ℕ) ↦ (Quotient.mk'' <$> decode n : Option (Quotient s)))
      ((fun (q : Quotient s) ↦ encode q.rep) (Quot.mk (⇑s : α → α → Prop) l)))
    (some (Quot.mk (⇑s : α → α → Prop) l))
have mk : Eq (α := Option (Quotient s))
  (Option.map Quotient.mk'' (decode (encode (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l)))))
  (some (Quot.mk (⇑s : α → α → Prop) l))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
⊢ Eq (α := Option (Quotient s))
    (Option.map Quotient.mk'' (decode (encode (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l)))))
    (some (Quot.mk (⇑s : α → α → Prop) l))
have mk : Eq (α := Option (Quotient s)) (Option.map Quotient.mk'' (some (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l))))
  (some (Quot.mk (⇑s : α → α → Prop) l))
Tactic: rw [encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
inst_1 : CompleteLattice α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, f b) (⨆ (b : β), f b)
have rw : Eq.{u_1 + 1} (α := α) (⨆ (j : β), ⨆ (i : ℕ), ⨆ (_ : j ∈ decode₂ β i), f j) (⨆ (b : β), f b)
Tactic: rw [iSup_comm]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ C (⋃ b_1 ∈ some b, f b_1)
have h : ⋃ b_1 ∈ some b, f b_1 = f b
Tactic: convert! H1 b
-- Lean 4 proof step from Mathlib.Logic.Encodable.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (i : ℕ) ↦ ⋃ b ∈ decode₂ β i, f b) i j
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) ((fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) i) x →
    x ∉ (fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) j
Tactic: refine disjoint_left.mpr fun x => ?_
-- Lean 4 proof step from Mathlib.Logic.Encodable.Lattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
⊢ Membership.mem (γ := Set α) ((fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) i) x →
    x ∉ (fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) j
have suffices : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
Tactic: suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
-- 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_10
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
⊢ (fun (x : β none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦ ((f none, fun (a : α) ↦ f (some a)) : β none × ((a : α) → β (some a)))) f) a =
    f a
have none : Eq (α := β none)
  ((fun (x : β none × ((a : α) → β (some a))) (a : Option α) ↦
      Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
    ((fun (f : (a : Option α) → β a) ↦ ((f none, fun (a : α) ↦ f (some a)) : β none × ((a : α) → β (some a)))) f) none)
  (f none)
Tactic: cases a
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_10
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
none :
  Eq (α := β Option.none)
    ((fun (x : β Option.none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦
          ((f Option.none, fun (a : α) ↦ f (some a)) : β Option.none × ((a : α) → β (some a))))
        f)
      Option.none)
    (f Option.none)
⊢ (fun (x : β Option.none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦
          ((f Option.none, fun (a : α) ↦ f (some a)) : β Option.none × ((a : α) → β (some a))))
        f)
      a =
    f a
have some : ∀ (val : α),
  Eq (α := β (some val))
    ((fun (x : β Option.none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦
          ((f Option.none, fun (a : α) ↦ f (some a)) : β Option.none × ((a : α) → β (some a))))
        f)
      (some val))
    (f (some val))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)
have pos : ∀ (h : p a),
  Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
pos :
  ∀ (h : p a),
    Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
      (if h : p a then
          (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
        else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
        ε)
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)
have neg : ∀ (h : ¬p a),
  Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
⊢ subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε
have H : ∀ (x : ε),
  Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
x : ε
⊢ Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)
have pos : ∀ (h : p x),
  Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)
Tactic: by_cases h : p x
-- Lean 4 proof step from Mathlib.Logic.Equiv.Basic (goal)
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
x : ε
pos :
  ∀ (h : p x),
    Eq (α := ε)
      ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
      ((Equiv.refl ε : (a : ε) → ε) x : ε)
⊢ Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)
have neg : ∀ (h : ¬p x),
  Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)
Tactic: by_cases h : p x
-- 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 : α
⊢ (↑((fun (x : { a : α // ¬p a } → β) ↦
              (Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀)
                  (fun (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 : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }))
            ((fun (x : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }) (a : { a : α // ¬p a }) ↦
                (↑x : α → β) (↑a : α))
              (Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀) x hx))) :
        α → β)
      a =
    (↑(Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀) x hx) : α → β) a
have dsimp : (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x a) = x a
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_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
⊢ (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x a) = x a
have pos : ∀ (h : p a), x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
Tactic: split_ifs