awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
nth_rw :
  LE.le (α := ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) a : ℕ) ((toNat : (a : Cardinal.{u}) → ℕ) (↑n : Cardinal.{u}) : ℕ) ↔
    a ≤ (↑n : Cardinal.{u})
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a ≤ n ↔ a ≤ (↑n : Cardinal.{u})
have nth_rw₁ : a ≤ (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
Tactic: nth_rw 1 [← Cardinal.toNat_natCast.{u} n,
    Cardinal.toNat_le_iff_le_of_lt_aleph0 lt (Cardinal.natCast_lt_aleph0)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.ToNat (goal)
Goal:
a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔ a = (↑n : Cardinal.{u})
have nth_rw : (toNat : (a : Cardinal.{u}) → ℕ) a = n ↔
  Eq.{u + 2} (α := Cardinal.{u}) (↑((toNat : (a : Cardinal.{u}) → ℕ) a) : Cardinal.{u}) (↑n : Cardinal.{u})
Tactic: nth_rw 2 [← Cardinal.cast_toNat_of_lt_aleph0 lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
⊢ UnivLE.{u, v} ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
have simp_rw : (∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
Tactic: simp_rw [univLE_iff, small_iff_lift_mk_lt_univ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
⊢ (∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
have contrapose! : (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
⊢ (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}
have refine_1 : (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) →
  ∀ (α : Type u) (le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α), univ.{v, u + 1} < univ.{u, v + 1}
Tactic: refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
refine_1 :
  (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) →
    ∀ (α : Type u) (le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α), univ.{v, u + 1} < univ.{u, v + 1}
⊢ (∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}
have refine_2 : ∀ (h : univ.{v, u + 1} < univ.{u, v + 1}), ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
Tactic: refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (hypothesis)
Goal:
h : ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}
have le₁ : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
Tactic: rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
h : univ.{v, u + 1} < univ.{u, v + 1}
⊢ ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
have refine_2 : ∀ (w : Cardinal.{u}) (α : Type u)
  (h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)),
  ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
Tactic: obtain ⟨⟨α⟩, h⟩ := lt_univ'.mp h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
⊢ ∃ (α : Type u), univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
have h₁ : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
Tactic: use α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
h_1 : univ.{v, u + 1} < univ.{u, v + 1}
w : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
have h₁ : univ.{v, u + 1} ≤ lift.{max (v + 1) (u + 1), u} #α
Tactic: rw [univ_umax.{v, u}, ← lift_le.{u + 1}, lift_univ, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
have rw : univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
Tactic: rw [univLE_iff_cardinal_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.UnivLE (goal)
Goal:
⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}
have simp_rw : univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
Tactic: simp_rw [univLE_iff_cardinal_le]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T : Set (List A) | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
w : Set (List A)
left : t ∈ S
⊢ x ∈ sSup S
have right : x ∈ t
Tactic: use t, ht, hS ht hx
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : x ++ y ∈ T
⊢ x ∈ T
have nil : ∀ {x : List A} (h : x ++ [] ∈ T), x ∈ T
Tactic: induction y generalizing x with
  | nil => simpa using h
  | cons y ys ih => exact T.prop (ih (by simpa))
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : x ++ y ∈ T
nil : ∀ {x : List A} (h : x ++ [] ∈ T), x ∈ T
⊢ x ∈ T
have cons : ∀ (y : A) (ys : List A) (ih : ∀ {x : List A} (h : x ++ ys ∈ T), x ∈ T) {x : List A} (h : x ++ y :: ys ∈ T), x ∈ T
Tactic: induction y generalizing x with
  | nil => simpa using h
  | cons y ys ih => exact T.prop (ih (by simpa))
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h' : x <+: y
h : y ∈ T
⊢ x ∈ T
have obtain : ∀ (w : List A) (h : x ++ w ∈ T), x ∈ T
Tactic: obtain ⟨_, rfl⟩ := h'
Cleared hypotheses: y, h', h
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
⊢ T = ⊥
have h₁ : ∀ (x : List A), x ∈ T ↔ Membership.mem (γ := ↥(tree A)) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
S T : ↥(tree A)
x y x_1 : List A
a : A
h : Membership.mem (γ := Set (List A)) ((fun (x_2 : List A) ↦ x ++ x_2) ⁻¹' (↑T : Set (List A))) (x_1 ++ [a])
⊢ (fun (x_2 : List A) ↦ x ++ x_2) x_1 ++ [a] ∈ T
have rwa : x ++ (x_1 ++ [a]) ∈ T
Tactic: rwa [List.append_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ subAt (subAt T x) y = subAt T (x ++ y)
have h : ∀ (x_1 : List A), x_1 ∈ subAt (subAt T x) y ↔ x_1 ∈ subAt T (x ++ y)
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ ∃ z ∈ T, y = x ++ z
have right : y = x ++ List.drop x.length y
Tactic: use y.drop x.length, h2
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ y = x ++ List.drop x.length y
have right : List.take x.length y ++ List.drop x.length y = x ++ List.drop x.length y
Tactic: nth_rw 1 [← List.take_append_drop x.length y]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ (↑(pullSub (subAt T x) x) : Set (List A)) → y ∈ (↑T : Set (List A))
have y₁ : ∀ (h : y ∈ pullSub (subAt T x) x), y ∈ (↑T : Set (List A))
Tactic: (h : y ∈ pullSub _ x)
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
⊢ y ∈ (↑T : Set (List A))
have inl : ∀ (h' : y.length ≤ x.length), y ∈ (↑T : Set (List A))
Tactic: rcases le_total y.length x.length with h' | h'
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
inl : ∀ (h' : y.length ≤ x.length), y ∈ (↑T : Set (List A))
⊢ y ∈ (↑T : Set (List A))
have inr : ∀ (h' : x.length ≤ y.length), y ∈ (↑T : Set (List A))
Tactic: rcases le_total y.length x.length with h' | h'
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (hypothesis)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : y.length ≤ x.length
⊢ y ∈ (↑T : Set (List A))
have h₁ : y <+: x ∧ [] ∈ subAt T x
Tactic: rw [mem_pullSub_short h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (hypothesis)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
h' : x.length ≤ y.length
⊢ y ∈ (↑T : Set (List A))
have h₁ : ∃ z ∈ subAt T x, y = x ++ z
Tactic: rw [mem_pullSub_long h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∃ z ∈ subAt T x, y = x ++ z
h' : x.length ≤ y.length
⊢ y ∈ (↑T : Set (List A))
have inr : ∀ (w : List A) (h : w ∈ subAt T x) (h' : x.length ≤ (x ++ w).length), x ++ w ∈ (↑T : Set (List A))
Tactic: obtain ⟨_, h, rfl⟩ := h
Cleared hypotheses: y, h, h'
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x : List A
⊢ subAt (pullSub T x) x = T
have h : ∀ (y : List A), y ∈ subAt (pullSub T x) x ↔ y ∈ T
Tactic: ext y
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
S T : ↥(tree A)
x : List A
h : pullSub S x ≤ T
⊢ S ≤ subAt T x
have rw : subAt (pullSub S x) x ≤ subAt T x
Tactic: rw [← subAt_pullSub S x]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ pullSub (pullSub T y) x = pullSub T (x ++ y)
have h : ∀ (z : List A), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Tactic: ext z
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have h : ∀ (hl : x.length ≤ z.length), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Tactic: rcases le_total x.length z.length with hl | hl
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
h : ∀ (hl : x.length ≤ z.length), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have h₁ : ∀ (hl : z.length ≤ x.length), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Tactic: rcases le_total x.length z.length with hl | hl
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have pos : ∀ (hp : x <+: z), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Tactic: by_cases hp : x <+: z
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
pos : ∀ (hp : x <+: z), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have neg : ∀ (hp : ¬x <+: z), z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Tactic: by_cases hp : x <+: z
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have pos : ∀ (z : List A) (hl : x.length ≤ (x ++ z).length), x ++ z ∈ pullSub (pullSub T y) x ↔ x ++ z ∈ pullSub T (x ++ y)
Tactic: obtain ⟨z, rfl⟩ := hp
Cleared hypotheses: z, hl, hp
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have neg : z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
neg : z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have neg₁ : z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (hypothesis)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right : List.drop (x ++ y).length z ∈ T
⊢ z ∈ pullSub (pullSub T y) x
have h₁ : List.take x.length z <+: x
Tactic: replace h := by simpa [List.take_take] using h.take x.length
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have neg : ∀ (h : List.take x.length z <+: x), List.drop x.length z ∈ pullSub T y → z ∈ pullSub T (x ++ y)
Tactic: constructor <;> intro ⟨h, _⟩ <;>
        [skip; replace h := by simpa [List.take_take] using h.take x.length]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
neg : ∀ (h : List.take x.length z <+: x), List.drop x.length z ∈ pullSub T y → z ∈ pullSub T (x ++ y)
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have neg₁ : List.drop (x ++ y).length z ∈ T → ∀ (h : List.take x.length z <+: x), z ∈ pullSub (pullSub T y) x
Tactic: constructor <;> intro ⟨h, _⟩ <;>
        [skip; replace h := by simpa [List.take_take] using h.take x.length]
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ (x ++ y).length
have simp : z.length ≤ x.length + y.length
Tactic: simp
-- Lean 4 proof step from Mathlib.SetTheory.Descriptive.Tree (goal)
Goal:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
have h : z <+: x ∧ [] <+: y ∧ [] ∈ T ↔ z <+: x ++ y ∧ [] ∈ T
Tactic: rw [mem_pullSub_short hl, mem_pullSub_short (by simp), mem_pullSub_short (by simp; lia)]
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : List (Lists α)
⊢ (ofList l).toList = l
have nil : Eq.{u_1 + 1} (α := List (Lists α)) (toList (ofList [])) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : List (Lists α)
nil : Eq.{u_1 + 1} (α := List (Lists α)) (toList (ofList [])) []
⊢ (ofList l).toList = l
have cons : ∀ (head : Lists α) (tail : List (Lists α)), (ofList tail).toList = tail → (ofList (head :: tail)).toList = head :: tail
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) l ⋯;
  ofList l'.toList = l'
have atom : ∀ (a : α) (h : true = false),
  let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : false = x) ↦ Lists' α x) (atom a) sorry;
  ofList l'.toList = l'
Tactic: induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl
Cleared hypotheses: h, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
atom :
  ∀ (a : α) (h : true = false),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : false = x) ↦ Lists' α x) (Lists'.atom a) ⋯;
    ofList l'.toList = l'
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) l ⋯;
  ofList l'.toList = l'
have nil : ∀ (h : true = true),
  let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) nil sorry;
  ofList l'.toList = l'
Tactic: induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl
Cleared hypotheses: h, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
atom :
  ∀ (a : α) (h : true = false),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : false = x) ↦ Lists' α x) (Lists'.atom a) ⋯;
    ofList l'.toList = l'
nil :
  ∀ (h : true = true),
    let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) Lists'.nil ⋯;
    ofList l'.toList = l'
⊢ let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) l ⋯;
  ofList l'.toList = l'
have cons' : ∀ {b : Bool} (b_1 : Lists' α b) (a : Lists' α true),
  (∀ (h : true = b),
      let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : b = x) ↦ Lists' α x) b_1 sorry;
      ofList l'.toList = l') →
    ∀
      (IH :
        ∀ (h : true = true),
          let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) a sorry;
          ofList l'.toList = l')
      (h : true = true),
      let l' : Lists' α true := Eq.rec (motive := fun (x : Bool) (h : true = x) ↦ Lists' α x) (b_1.cons' a) sorry;
      ofList l'.toList = l'
Tactic: induction l with
    | atom => cases h
    | nil => simp
    | cons' b a _ IH => simpa [cons] using IH rfl
Cleared hypotheses: h, l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
have refine : ∀ (h : cons a l₁ ⊆ l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
have generalize : ∀ (l₁' : Lists' α true) (h' : cons a l₁ = l₁') (h : l₁' ⊆ l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: generalize h' : Lists'.cons a l₁ = l₁' at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
have nil : ∀ (h' : cons a l₁ = nil), a ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: obtain - | @⟨a', _, _, _, e, m, s⟩ := h
Cleared hypotheses: l₁', h', h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
nil : ∀ (h' : cons a l₁ = Lists'.nil), a ∈ l₂ ∧ l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
have cons : ∀ {a' a'_1 : Lists α} {l : Lists' α true} (e : a' ~ a'_1) (h' : cons a l₁ = cons a' l) (m : a'_1 ∈ l₂.toList)
  (s : l.Subset l₂), a ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: obtain - | @⟨a', _, _, _, e, m, s⟩ := h
Cleared hypotheses: l₁', h', h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
have nil : ∀ (fst : Bool) (snd : Lists' α fst) (h' : cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = nil),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: cases a
Cleared hypotheses: a, h'
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'_1 : Lists α
l : Lists' α true
e : a' ~ a'_1
h' : cons a l₁ = cons a' l
m : a'_1 ∈ l₂.toList
s : l.Subset l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂
have cons : ∀ (fst : Bool) (snd : Lists' α fst) (h' : cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = cons a' l),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: cases a
Cleared hypotheses: a, h'
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' a'_1 : Lists α
l : Lists' α true
e : a' ~ a'_1
m : a'_1 ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
h' : cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ = cons a' l
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
have cons : ∀ (fst_1 : Bool) (snd_1 : Lists' α fst_1) (e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'_1)
  (h' :
    cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
      cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
Tactic: cases a'
Cleared hypotheses: a', e, h'
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
l : Lists' α true
m : a' ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
fst_1 : Bool
snd_1 : Lists' α fst_1
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'
h' :
  cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
    cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
have e₁ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'
Tactic: cases h'
Cleared hypotheses: l, s, fst_1, snd_1, e, h'
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
a' : Lists α
l : Lists' α true
m : a' ∈ l₂.toList
s : l.Subset l₂
fst : Bool
snd : Lists' α fst
fst_1 : Bool
snd_1 : Lists' α fst_1
e : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1 ~ a'
h' :
  cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd) l₁ =
    cons (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst_1 snd_1) l
e₁ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ~ a'
⊢ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) fst snd ∈ l₂ ∧ l₁ ⊆ l₂
have s₁ : l₁.Subset l₂
Tactic: cases h'
Cleared hypotheses: l, s, fst_1, snd_1, e, h'
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head :: tail ⊆ l₂
⊢ ofList (head :: tail) ⊆ ofList l₂
have cons : head ∈ (ofList l₂).toList
Tactic: refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
l₂ : List (Lists α)
head : Lists α
tail : List (Lists α)
l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂
h : head :: tail ⊆ l₂
⊢ head ∈ (ofList l₂).toList
have h₁ : head ∈ l₂ ∧ tail ⊆ l₂
Tactic: simp only [List.cons_subset] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂
have nil : ∀ (h : [] ⊆ l₂), ofList [] ⊆ ofList l₂
Tactic: induction l₁ with
  | nil => exact Subset.nil
  | cons _ _ l₁_ih =>
    refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
    simp only [List.cons_subset] at h; simp [h]
Cleared hypotheses: l₁, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
nil : ∀ (h : [] ⊆ l₂), ofList [] ⊆ ofList l₂
⊢ ofList l₁ ⊆ ofList l₂
have cons : ∀ (head : Lists α) (tail : List (Lists α)) (l₁_ih : ∀ (h : tail ⊆ l₂), ofList tail ⊆ ofList l₂) (h : head :: tail ⊆ l₂),
  ofList (head :: tail) ⊆ ofList l₂
Tactic: induction l₁ with
  | nil => exact Subset.nil
  | cons _ _ l₁_ih =>
    refine Subset.cons (Lists.Equiv.refl _) ?_ (l₁_ih (List.subset_of_cons_subset h))
    simp only [List.cons_subset] at h; simp [h]
Cleared hypotheses: l₁, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : Lists' α true
⊢ l ⊆ l
have rw : ofList l.toList ⊆ ofList l.toList
Tactic: rw [← Lists'.of_toList l]
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil
have rw : ofList l.toList ⊆ nil → ofList l.toList = nil
Tactic: rw [← of_toList l]
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ nil → ofList l.toList = nil
have nil : HasSubset.Subset.{u_1} (α := Lists' α true) (ofList []) nil → Eq.{u_1 + 1} (α := Lists' α true) (ofList []) nil
Tactic: induction toList l