awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ Acc (Shortlex r) l
have intro : l.length < (xa :: xb).length
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < (xa :: xb).length
have intro : l.length < xs.length + 1
Tactic: rw [List.length_cons, ← h2len]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h2len : (x :: xs).length = (xa :: xb).length
h : r x xa
⊢ Acc (Shortlex r) (x :: xs)
have h2len₁ : xs.length = xb.length
Tactic: simp only [List.length_cons, add_left_inj] at h2len
Cleared hypotheses: h2len
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ xs.length < (xa :: xb).length
have rw : xb.length < (xa :: xb).length
Tactic: rw [h2len]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
⊢ Acc (Shortlex r) (x :: xs)
have intro : ∀ (l : List α) (hl : l.length < (x :: xs).length), Acc (Shortlex r) l
Tactic: refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ Acc (Shortlex r) l
have intro : l.length < (xa :: xb).length
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h_1 : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_2 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < (xa :: xb).length
have intro : l.length < xs.length + 1
Tactic: rw [List.length_cons, ← h2len]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
⊢ Acc (Shortlex r) p
have intro : ∀ (lt : Shortlex r [] (xa :: xb)) (h2len : length.{u_1} (α := α) [] = (xa :: xb).length), Acc (Shortlex r) []
Tactic: cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
Cleared hypotheses: p, lt, h2len, h2lex
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
intro : ∀ (lt : Shortlex r [] (xa :: xb)) (h2len : length.{u_1} (α := α) [] = (xa :: xb).length), Acc (Shortlex r) []
⊢ Acc (Shortlex r) p
have intro₁ : ∀ {xs : List α} (lt : Shortlex r (xa :: xs) (xa :: xb)) (h2len : (xa :: xs).length = (xa :: xb).length)
  (h : Lex r xs xb), Acc (Shortlex r) (xa :: xs)
Tactic: cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
Cleared hypotheses: p, lt, h2len, h2lex
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b xb : List α
h_1 : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb →
      ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
p : List α
lt : Shortlex r p (xa :: xb)
h2len : p.length = (xa :: xb).length
h2lex : Lex r p (xa :: xb)
intro : ∀ (lt : Shortlex r [] (xa :: xb)) (h2len : length.{u_1} (α := α) [] = (xa :: xb).length), Acc (Shortlex r) []
intro₁ :
  ∀ {xs : List α} (lt : Shortlex r (xa :: xs) (xa :: xb)) (h2len : (xa :: xs).length = (xa :: xb).length)
    (h : Lex r xs xb), Acc (Shortlex r) (xa :: xs)
⊢ Acc (Shortlex r) p
have intro₂ : ∀ {x : α} {xs : List α} (lt : Shortlex r (x :: xs) (xa :: xb)) (h2len : (x :: xs).length = (xa :: xb).length)
  (h : r x xa), Acc (Shortlex r) (x :: xs)
Tactic: cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
Cleared hypotheses: p, lt, h2len, h2lex
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b : List α
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: b)
have intro : ∀ (xb : List α),
  (∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y) →
    ∀
      (ihb :
        ∀ (y : List α),
          Shortlex r y xb →
            ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y))
      (ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: xb)
Tactic: induction acb with
    | intro xb _ ihb =>
      refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
Cleared hypotheses: acb, ih
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
a : α
b : List α
aca : Acc r a
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (a :: b).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (a :: b)
have intro : ∀ (xa : α),
  (∀ (y : α), r y xa → Acc r y) →
    ∀
      (iha :
        ∀ (y : α),
          r y xa →
            ∀ {b : List α} (acb : Acc (Shortlex r) b)
              (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s), Acc (Shortlex r) (y :: b))
      {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s),
      Acc (Shortlex r) (xa :: b)
Tactic: induction aca generalizing b with
  | intro xa _ iha =>
    induction acb with
    | intro xb _ ihb =>
      refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
Cleared hypotheses: b, aca, acb, ih
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ Acc (Shortlex r) a
have len_a₁ : a = []
Tactic: rw [List.length_eq_zero_iff] at len_a
Cleared hypotheses: len_a
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a
have zero : Acc (Shortlex r) []
Tactic: rw [len_a]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
a : List α
len_a : a.length = n.succ
⊢ Acc (Shortlex r) a
have ind : ∀ (head : α) (tail : List α) (len_a : (head :: tail).length = n.succ), Acc (Shortlex r) (head :: tail)
Tactic: obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a
Cleared hypotheses: a, len_a
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : (head :: tail).length = n.succ
⊢ Acc (Shortlex r) (head :: tail)
have len_a₁ : tail.length = n
Tactic: rw [List.length_cons, add_left_inj] at len_a
Cleared hypotheses: len_a
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)
have ind : ∀ (s : List α), s.length < (head :: tail).length → Acc (Shortlex r) s
Tactic: apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ Acc (Shortlex r) l
have apply : l.length ≤ n
Tactic: apply ih l.length _ _ rfl
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ n
have rw : l.length ≤ tail.length
Tactic: rw [← len_a]
-- Lean 4 proof step from Mathlib.Data.List.Shortlex (goal)
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
⊢ Acc (Shortlex r) a
have induction : ∀ (x : ℕ) (len_a : a.length = x), Acc (Shortlex r) a
Tactic: induction len_a : a.length using Nat.caseStrongRecOn generalizing a with
  | zero =>
    rw [List.length_eq_zero_iff] at len_a
    rw [len_a]
    exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim
  | ind n ih =>
    obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a
    rw [List.length_cons, add_left_inj] at len_a
    apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)
    intro l ll
    apply ih l.length _ _ rfl
    rw [← len_a]
    exact Nat.le_of_lt_succ ll
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys (β := β)
⊢ ∃ (b : β a), Sigma.mk (β := β) a b ∈ l
have this : ∃ (a_1 : Sigma β), a_1 ∈ l ∧ a_1.fst (β := β) = a
Tactic: have := exists_of_mem_map h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ L.flatten.NodupKeys (β := β) ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧ Pairwise Disjoint (map (keys (β := β)) L)
have rw : (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l) ∧
    Pairwise
      (fun (l₁ l₂ : List (Sigma β)) ↦
        ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
      L ↔
  (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧
    Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L
Tactic: rw [nodupKeys_iff_pairwise, pairwise_flatten, pairwise_map]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l) ∧
      Pairwise
        (fun (l₁ l₂ : List (Sigma β)) ↦
          ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
        L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧
      Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L
have refine : Pairwise
    (fun (l₁ l₂ : List (Sigma β)) ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
    L ↔
  Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L
Tactic: refine and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) ?_
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : (dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)
⊢ (dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β)
have pos : a = s.fst (β := β) → ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : (dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)
pos : a = s.fst (β := β) → ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
⊢ (dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β)
have neg : ¬a = s.fst (β := β) → ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ (dlookup (β := β) a l).isSome = true ↔ a ∈ l.keys (β := β)
have nil : Option.isSome.{v} (α := β a) (dlookup (β := β) a []) = true ↔ Membership.mem (γ := List α) (keys (β := β) []) a
Tactic: induction l with
  | nil => simp
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nil : Option.isSome.{v} (α := β a) (dlookup (β := β) a []) = true ↔ Membership.mem (γ := List α) (keys (β := β) []) a
⊢ (dlookup (β := β) a l).isSome = true ↔ a ∈ l.keys (β := β)
have cons : ∀ (s : Sigma β) (tail : List (Sigma β)),
  ((dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)) →
    ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
Tactic: induction l with
  | nil => simp
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
tail_ih : b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail
⊢ b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
have pos : a = s.fst (β := β) → b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
tail_ih : b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail
pos : a = s.fst (β := β) → b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
⊢ b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
have neg : ¬a = s.fst (β := β) → b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ b ∈ dlookup (β := β) a l → Sigma.mk (β := β) a b ∈ l
have nil : Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b →
  Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
Tactic: induction l with
  | nil => grind
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nil :
  Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b →
    Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
⊢ b ∈ dlookup (β := β) a l → Sigma.mk (β := β) a b ∈ l
have cons : ∀ (s : Sigma β) (tail : List (Sigma β)),
  (b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail) →
    b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
Tactic: induction l with
  | nil => grind
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
⊢ b ∈ dlookup (β := β) a l
have obtain : ∀ (b' : β ((Sigma.mk (β := β) a b).fst (β := β)))
  (h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b'), b ∈ dlookup (β := β) a l
Tactic: obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
b' : β ((Sigma.mk (β := β) a b).fst (β := β))
h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b'
⊢ b ∈ dlookup (β := β) a l
have h'₁ : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b
Tactic: cases nd.eq_of_mk_mem h (of_mem_dlookup h')
Cleared hypotheses: b', h'