awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l : Lists' α true
nil :
  HasSubset.Subset.{u_1} (α := Lists' α true) (ofList []) Lists'.nil →
    Eq.{u_1 + 1} (α := Lists' α true) (ofList []) Lists'.nil
⊢ ofList l.toList ⊆ Lists'.nil → ofList l.toList = Lists'.nil
have cons : ∀ (head : Lists α) (tail : List (Lists α)),
  (ofList tail ⊆ Lists'.nil → ofList tail = Lists'.nil) →
    ofList (head :: tail) ⊆ Lists'.nil → ofList (head :: tail) = Lists'.nil
Tactic: induction toList l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
b : Bool
a0 : Lists' α b
l0 l₂ : Lists' α true
s : a0.cons' l0 ⊆ l₂
h : a ∈ (a0.cons' l0).toList
⊢ a ∈ l₂
have cons : ∀ {a_1 a' : Lists α} (e : a_1 ~ a') (h : a ∈ (a_1.snd (β := fun (b : Bool) ↦ Lists' α b).cons' l0).toList)
  (m : a' ∈ l₂.toList) (s : l0.Subset l₂), a ∈ l₂
Tactic: obtain - | ⟨e, m, s⟩ := s
Cleared hypotheses: b, a0, s, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
h : a ∈ (a_1.snd (β := fun (b : Bool) ↦ Lists' α b).cons' l0).toList
m : a' ∈ l₂.toList
s : l0.Subset l₂
⊢ a ∈ l₂
have h₁ : a = a_1 ∨ a ∈ l0.toList
Tactic: simp only [toList, Sigma.eta, List.mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
m : a' ∈ l₂.toList
s : l0.Subset l₂
h : a = a_1 ∨ a ∈ l0.toList
⊢ a ∈ l₂
have cons : ∀ (e : a ~ a'), a ∈ l₂
Tactic: rcases h with (rfl | h)
Cleared hypotheses: a_1, e, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : Lists α
l0 l₂ : Lists' α true
a_1 a' : Lists α
e : a_1 ~ a'
m : a' ∈ l₂.toList
s : l0.Subset l₂
h : a = a_1 ∨ a ∈ l0.toList
cons : ∀ (e : a ~ a'), a ∈ l₂
⊢ a ∈ l₂
have cons₁ : ∀ (h : a ∈ l0.toList), a ∈ l₂
Tactic: rcases h with (rfl | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂
⊢ l₁ ⊆ l₂
have ofList : ∀ (l₁ : List (Lists α)) (H : ∀ (a : Lists α), a ∈ (ofList l₁).toList → a ∈ l₂), ofList l₁ ⊆ l₂
Tactic: induction l₁ using recOfList with | _ l₁
Cleared hypotheses: l₁, H
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (ofList t).toList → a ∈ l₂), ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ (ofList (h :: t)).toList → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
have t_ih₁ : ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂
Tactic: simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
Cleared hypotheses: t_ih, H
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (ofList t).toList → a ∈ l₂), ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ (ofList (h :: t)).toList → a ∈ l₂
t_ih₁ : ∀ (H : ∀ (a : Lists α), a ∈ t → a ∈ l₂), ofList t ⊆ l₂
⊢ ofList (h :: t) ⊆ l₂
have H₁ : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
Tactic: simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
Cleared hypotheses: t_ih, H
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₂ : Lists' α true
l₁ : List (Lists α)
H : ∀ (a : Lists α), a ∈ (ofList l₁).toList → a ∈ l₂
⊢ ofList l₁ ⊆ l₂
have ofList : ∀ (H : ∀ (a : Lists α), Membership.mem (γ := List (Lists α)) (toList (ofList [])) a → a ∈ l₂), ofList [] ⊆ l₂
Tactic: induction l₁ with
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩
Cleared hypotheses: l₁, H
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₂ : Lists' α true
l₁ : List (Lists α)
H : ∀ (a : Lists α), a ∈ (Lists'.ofList l₁).toList → a ∈ l₂
ofList :
  ∀ (H : ∀ (a : Lists α), Membership.mem (γ := List (Lists α)) (toList (Lists'.ofList [])) a → a ∈ l₂),
    Lists'.ofList [] ⊆ l₂
⊢ Lists'.ofList l₁ ⊆ l₂
have ofList₁ : ∀ (h : Lists α) (t : List (Lists α))
  (t_ih : ∀ (H : ∀ (a : Lists α), a ∈ (Lists'.ofList t).toList → a ∈ l₂), Lists'.ofList t ⊆ l₂)
  (H : ∀ (a : Lists α), a ∈ (Lists'.ofList (h :: t)).toList → a ∈ l₂), Lists'.ofList (h :: t) ⊆ l₂
Tactic: induction l₁ with
    | nil => exact Subset.nil
    | cons h t t_ih =>
      simp only [to_ofList, ofList, toList_cons, List.mem_cons, forall_eq_or_imp] at *
      exact cons_subset.2 ⟨H.1, t_ih H.2⟩
Cleared hypotheses: l₁, H
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)
have suffices : {b : Bool} →
  (l : Lists' α b) →
    PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
      (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
      | true, l => D l
      | false, x => PUnit)
Tactic: suffices ∀ {b} (l : Lists' α b),
      PProd (C ⟨_, l⟩)
        (match b, l with
        | true, l => D l
        | false, _ => PUnit)
    by exact ⟨fun ⟨b, l⟩ => (this _).1, fun l => (this l).2⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b b_1 : Bool
a : Lists' α b_1
l : Lists' α true
IH₁ :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b_1 a))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b_1, a with
    | true, l => D l
    | false, x => PUnit)
IH :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, l with
    | true, l => D l
    | false, x => PUnit)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
    | true, l => D l
    | false, x => PUnit)
have cons' : (this : D (a.cons' l)) →
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
    | true, l => D l
    | false, x => PUnit)
Tactic: have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
    | true, l => D l
    | false, x => PUnit)
have atom : (a : α) →
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) false, Lists'.atom a with
    | true, l => D l
    | false, x => PUnit)
Tactic: induction l with
  | atom => exact ⟨C0 _, ⟨⟩⟩
  | nil => exact ⟨C1 _ D0, D0⟩
  | cons' a l IH₁ IH =>
    have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
    exact ⟨C1 _ this, this⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (Lists.atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
atom :
  (a : α) →
    PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)))
      (match (motive := (b : Bool) → Lists' α b → Sort u_3) false, Lists'.atom a with
      | true, l => D l
      | false, x => PUnit)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
    | true, l => D l
    | false, x => PUnit)
have nil : PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true Lists'.nil))
  (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, Lists'.nil with
  | true, l => D l
  | false, x => PUnit)
Tactic: induction l with
  | atom => exact ⟨C0 _, ⟨⟩⟩
  | nil => exact ⟨C1 _ D0, D0⟩
  | cons' a l IH₁ IH =>
    have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
    exact ⟨C1 _ this, this⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (Lists.atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
atom :
  (a : α) →
    PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) false (Lists'.atom a)))
      (match (motive := (b : Bool) → Lists' α b → Sort u_3) false, Lists'.atom a with
      | true, l => D l
      | false, x => PUnit)
nil :
  PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true Lists'.nil))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, Lists'.nil with
    | true, l => D l
    | false, x => PUnit)
⊢ PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b l))
    (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, l with
    | true, l => D l
    | false, x => PUnit)
have cons' : {b : Bool} →
  (a : Lists' α b) →
    (l : Lists' α true) →
      (IH₁ :
          PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) b a))
            (match (motive := (b : Bool) → Lists' α b → Sort u_3) b, a with
            | true, l => D l
            | false, x => PUnit)) →
        (IH :
            PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l))
              (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, l with
              | true, l => D l
              | false, x => PUnit)) →
          PProd.{u_2, u_3} (C (Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true (a.cons' l)))
            (match (motive := (b : Bool) → Lists' α b → Sort u_3) true, a.cons' l with
            | true, l => D l
            | false, x => PUnit)
Tactic: induction l with
  | atom => exact ⟨C0 _, ⟨⟩⟩
  | nil => exact ⟨C1 _ D0, D0⟩
  | cons' a l IH₁ IH =>
    have : D (Lists'.cons' a l) := D1 ⟨_, _⟩ _ IH₁.1 IH.2
    exact ⟨C1 _ this, this⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
have refine : ∀ (h : of' l₁ ~ of' l₂), l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
Tactic: refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
have refl : l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
refl : l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
have antisymm : ∀ (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁), l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l
have refl : atom a = atom a
Tactic: cases h
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
have refl : l₁ ~ l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
refl : l₁ ~ l₁
⊢ l₂ ~ l₁
have antisymm : ∀ {l₁ l₂ : Lists' α true} (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁
have refl : l₁ ~ l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h <;> [rfl; exact Equiv.antisymm h₂ h₁]
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
refl : l₁ ~ l₁
⊢ l₂ ~ l₁
have antisymm : ∀ {l₁ l₂ : Lists' α true} (h₁ : l₁.Subset l₂) (h₂ : l₂.Subset l₁),
  Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₁
Tactic: obtain - | ⟨h₁, h₂⟩ := h <;> [rfl; exact Equiv.antisymm h₂ h₁]
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
have suffices : (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
Tactic: suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
have C0 : ∀ (a : α), trans (atom a)
Tactic: apply inductionMut
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
C0 : ∀ (a : α), trans (atom a)
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
have C1 : ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)
Tactic: apply inductionMut
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
C0 : ∀ (a : α), trans (atom a)
C1 : ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
have D0 : ∀ (l' : Lists α), Membership.mem (γ := List (Lists α)) (Lists'.toList Lists'.nil) l' → trans l'
Tactic: apply inductionMut
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
C0 : ∀ (a : α), trans (atom a)
C1 : ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)
D0 : ∀ (l' : Lists α), Membership.mem (γ := List (Lists α)) (Lists'.toList Lists'.nil) l' → trans l'
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
have D1 : ∀ (a : Lists α) (l : Lists' α true),
  trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Tactic: apply inductionMut
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
h₂ : l₂ ~ l₃
⊢ atom a ~ l₃
have C0 : ∀ (h₂ : atom a ~ l₃), atom a ~ l₃
Tactic: rwa [← equiv_atom.1 h₁] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
⊢ of' l₁ ~ l₃
have C1 : ∀ (h₁ : of' l₁ ~ of' l₁) (h₂ : of' l₁ ~ l₃), of' l₁ ~ l₃
Tactic: obtain - | l₂ := id h₁
Cleared hypotheses: l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
h₂ : l₂ ~ l₃
C1 : ∀ (h₁ : of' l₁ ~ of' l₁) (h₂ : of' l₁ ~ l₃), of' l₁ ~ l₃
⊢ of' l₁ ~ l₃
have C1₁ : ∀ {l₂ : Lists' α true} (l₂_1 : l₁.Subset l₂),
  l₂.Subset l₁ →
    ∀ (h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂)
      (h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂ ~ l₃), of' l₁ ~ l₃
Tactic: obtain - | l₂ := id h₁
Cleared hypotheses: l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ l₃
⊢ of' l₁ ~ l₃
have C1 : ∀ (h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1),
  of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
Tactic: obtain - | l₃ := id h₂
Cleared hypotheses: l₃, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ l₃
C1 :
  ∀
    (h₂ :
      Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1),
    of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
⊢ of' l₁ ~ l₃
have C1₁ : ∀ {l₂ : Lists' α true} (l₃ : l₂_1.Subset l₂),
  l₂.Subset l₂_1 →
    ∀
      (h₂ :
        Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂),
      of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂
Tactic: obtain - | l₃ := id h₂
Cleared hypotheses: l₃, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
have hl₁ : l₁ ⊆ l₂_1
Tactic: obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
have hr₁ : l₂_1 ⊆ l₁
Tactic: obtain ⟨hl₁, hr₁⟩ := Equiv.antisymm_iff.1 h₁
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
have hl₂ : l₂_1 ⊆ l₂_2
Tactic: obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (hypothesis)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
have hr₂ : l₂_2 ⊆ l₂_1
Tactic: obtain ⟨hl₂, hr₂⟩ := Equiv.antisymm_iff.1 h₂
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
⊢ of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
have C1 : l₁ ⊆ l₂_2 ∧ l₂_2 ⊆ l₁
Tactic: apply Equiv.antisymm_iff.2
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
⊢ l₁ ⊆ l₂_2 ∧ l₂_2 ⊆ l₁
have C1 : l₁ ⊆ l₂_2
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
C1 : l₁ ⊆ l₂_2
⊢ l₁ ⊆ l₂_2 ∧ l₂_2 ⊆ l₁
have C1₁ : l₂_2 ⊆ l₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Lists (goal)
Goal:
α : Type u_1
trans : (l₁ : Lists α) → Prop := fun (l₁ : Lists α) ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂_1 : Lists' α true
l₂ : l₁.Subset l₂_1
h : l₂_1.Subset l₁
h₁ : of' l₁ ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1
l₂_2 : Lists' α true
l₃ : l₂_1.Subset l₂_2
h_1 : l₂_2.Subset l₂_1
h₂ : Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_1 ~ Sigma.mk (β := fun (b : Bool) ↦ Lists' α b) true l₂_2
hl₁ : l₁ ⊆ l₂_1
hr₁ : l₂_1 ⊆ l₁
hl₂ : l₂_1 ⊆ l₂_2
hr₂ : l₂_2 ⊆ l₂_1
⊢ l₁ ⊆ l₂_2
have C1 : ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂_2
Tactic: apply Lists'.subset_def.2