awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
rw : Ioc m n = Icc (m + 1) n
⊢ Ioc m n = s
have rw₁ : Ioc m n = Ioc m n
Tactic: rw [← hs, Icc_add_one_left_eq_Ioc]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s
have rw : Ioo m n = Icc (m + 1) (n - 1)
Tactic: rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
rw : Ioo m n = Icc (m + 1) (n - 1)
⊢ Ioo m n = s
have rw₁ : Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)
Tactic: rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Iio (n + 1) = s
have rw : Ico ⊥ (n + 1) = s
Tactic: rw [Iio_eq_Ico, Ico_add_one_right_eq_Icc, bot_eq_zero, hs]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
rw : Ico ⊥ (n + 1) = s
⊢ Iio (n + 1) = s
have rw₁ : Icc ⊥ n = s
Tactic: rw [Iio_eq_Ico, Ico_add_one_right_eq_Icc, bot_eq_zero, hs]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
rw : Ico ⊥ (n + 1) = s
rw₁ : Icc ⊥ n = s
rw₂ : Icc 0 n = s
⊢ Iio (n + 1) = s
have rw₃ : s = s
Tactic: rw [Iio_eq_Ico, Ico_add_one_right_eq_Icc, bot_eq_zero, hs]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s
have rw : Icc m n = insert m (Icc (m + 1) n)
Tactic: rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
rw : Icc m n = insert m (Icc (m + 1) n)
⊢ Icc m n = insert m s
have rw₁ : Icc m n = Icc m n
Tactic: rw [← hs, insert_Icc_add_one_left_eq_Icc (by simpa using hmn)]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = s
have rw : Ico m n = Icc m (n - 1)
Tactic: rw [← hs, Icc_sub_one_right_eq_Ico]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
rw : Ico m n = Icc m (n - 1)
⊢ Ico m n = s
have rw₁ : Ico m n = Ico m n
Tactic: rw [← hs, Icc_sub_one_right_eq_Ico]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s
have rw : Ioc m n = Icc (m + 1) n
Tactic: rw [← hs, Icc_add_one_left_eq_Ioc]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
rw : Ioc m n = Icc (m + 1) n
⊢ Ioc m n = s
have rw₁ : Ioc m n = Ioc m n
Tactic: rw [← hs, Icc_add_one_left_eq_Ioc]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s
have rw : Ioo m n = Icc (m + 1) (n - 1)
Tactic: rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]
-- Lean 4 proof step from Mathlib.Tactic.Simproc.FinsetInterval (goal)
Goal:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
rw : Ioo m n = Icc (m + 1) (n - 1)
⊢ Ioo m n = s
have rw₁ : Icc (m + 1) (n - 1) = Icc (m + 1) (n - 1)
Tactic: rw [← hs, ← Icc_add_one_sub_one_eq_Ioo]
-- Lean 4 proof step from Mathlib.Tactic.Translate.Reorder (goal)
Goal:
r : ArgReorder
x : Nat × ArgReorder
h : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r
have mk : ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
  x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
    sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
Tactic: cases r
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Tactic.Translate.Reorder (goal)
Goal:
r : ArgReorder
x : Nat × ArgReorder
h : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r
have mk : ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
  x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
    sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
Tactic: decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Tactic.Translate.Reorder (goal)
Goal:
r : ArgReorder
perm : List String :=
  List.map
    (fun (x : Subtype (Membership.mem r.perm)) ↦
      match (motive := Subtype (Membership.mem r.perm) → String) x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun (x_1 : Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length)))) ↦
              match (motive := Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length))) → String)
                x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length).attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r
have mk : ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
  x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
    sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
Tactic: cases r
Cleared hypotheses: r, perm, h
-- Lean 4 proof step from Mathlib.Tactic.Translate.Reorder (goal)
Goal:
r : ArgReorder
perm : List String :=
  List.map
    (fun (x : Subtype (Membership.mem r.perm)) ↦
      match (motive := Subtype (Membership.mem r.perm) → String) x with
      | ⟨x, h⟩ =>
        " ".intercalate
          (List.map
            (fun (x_1 : Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length)))) ↦
              match (motive := Subtype (Membership.mem (x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length))) → String)
                x_1 with
              | ⟨x_2, h⟩ => ToString.toString (x_2 + 1))
            x.val (p := fun (l : List Nat) ↦ 2 ≤ l.length).attach))
    (List.attach r.perm)
x : Nat × ArgReorder
h : x ∈ r.argReorders
⊢ sizeOf x.snd < sizeOf r
have mk : ∀ (perm : Permutation) (argReorders : Array (Nat × ArgReorder)),
  x ∈ { perm := perm, argReorders := argReorders : ArgReorder }.argReorders →
    sizeOf x.snd < sizeOf { perm := perm, argReorders := argReorders : ArgReorder }
Tactic: decreasing_by
  cases r; grind [→ Array.sizeOf_lt_of_mem]
Cleared hypotheses: r, perm, h
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.getD
      (Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m))
      y =
    (List.dlookup (β := fun (x : α) ↦ β) x m).getD y
have e_opt : Option.map (Sigma.snd (β := fun (x : α) ↦ β))
    (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
  List.dlookup (β := fun (x : α) ↦ β) x m
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
p : (_ : α) × β
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) (p :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (p :: m)
have e_opt : ∀ (fst : α) (snd : β),
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
Tactic: rcases p with ⟨fst, snd⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
have pos : ∀ (heq : fst = x),
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
Tactic: by_cases heq : fst = x
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
pos :
  ∀ (heq : fst = x),
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
          (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
      List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
have neg : ∀ (heq : ¬fst = x),
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
Tactic: by_cases heq : fst = x
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
have neg : Option.map (Sigma.snd (β := fun (x : α) ↦ β))
    (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
      (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
  List.dlookup (β := fun (x : α) ↦ β) x m
Tactic: rw [List.dlookup_cons_ne]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
neg :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x m
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x))
        (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (Sigma.mk (β := fun (x : α) ↦ β) fst snd :: m)
have neg₁ : x ≠ Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd)
Tactic: rw [List.dlookup_cons_ne]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih :
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd)
have neg : Sigma.fst (β := fun (x : α) ↦ β) (Sigma.mk (β := fun (x : α) ↦ β) fst snd) ≠ x
Tactic: symm
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
have e_opt : Eq.{v + 1} (α := Option β)
  (Option.map (α := (_ : α) × β) (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) []) :
    Option β)
  (List.dlookup (β := fun (x : α) ↦ β) x [] : Option β)
Tactic: induction m with
  | nil => simp
  | cons p m ih =>
    rcases p with ⟨fst, snd⟩
    by_cases heq : fst = x
    · simp [heq]
    · rw [List.dlookup_cons_ne]
      · simp [heq, ih]
      · symm
        simp [heq]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
e_opt :
  Eq.{v + 1} (α := Option β)
    (Option.map (α := (_ : α) × β) (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) []) :
      Option β)
    (List.dlookup (β := fun (x : α) ↦ β) x [] : Option β)
⊢ Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
    List.dlookup (β := fun (x : α) ↦ β) x m
have e_opt₁ : ∀ (p : (_ : α) × β) (m : List ((_ : α) × β))
  (ih :
    Option.map (Sigma.snd (β := fun (x : α) ↦ β))
        (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) m) =
      List.dlookup (β := fun (x : α) ↦ β) x m),
  Option.map (Sigma.snd (β := fun (x : α) ↦ β))
      (List.find? (fun (x_1 : (_ : α) × β) ↦ decide (x_1.fst (β := fun (x : α) ↦ β) = x)) (p :: m)) =
    List.dlookup (β := fun (x : α) ↦ β) x (p :: m)
Tactic: induction m with
  | nil => simp
  | cons p m ih =>
    rcases p with ⟨fst, snd⟩
    by_cases heq : fst = x
    · simp [heq]
    · rw [List.dlookup_cons_ne]
      · simp [heq, ih]
      · symm
        simp [heq]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
tf : TotalFunction α β
a : α
⊢ a ∈ tf.zeroDefaultSupp ↔ tf.zeroDefault.apply a ≠ 0
have rcases : ∀ (A : List ((_ : α) × β)) (y : β), a ∈ (withDefault A y).zeroDefaultSupp ↔ (withDefault A y).zeroDefault.apply a ≠ 0
Tactic: rcases tf with ⟨A, y⟩
Cleared hypotheses: tf
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ a ∈ (withDefault A y).zeroDefaultSupp ↔ (withDefault A y).zeroDefault.apply a ≠ 0
have simp : (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
  ¬(withDefault A 0).apply a = 0
Tactic: simp only [zeroDefaultSupp, List.mem_map, List.mem_filter, exists_and_right,
      List.mem_toFinset, exists_eq_right, Sigma.exists, Ne, zeroDefault]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(withDefault A 0).apply a = 0
have rw : (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
  ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
Tactic: rw [apply_eq_dlookup]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
have mp : (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) →
  ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
mp :
  (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) →
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
⊢ (∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true) ↔
    ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
have mpr : ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0 →
  ∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true
Tactic: constructor
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
⊢ ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
have this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
Tactic: have := List.mem_dlookup (List.nodupKeys_dedupKeys A) hval
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
⊢ ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
have mp : ¬(some od).getD 0 = 0
Tactic: rw [(_ : List.dlookup a A = od)]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : Sigma.mk (β := fun (a : α) ↦ β) a od ∈ A.dedupKeys (β := fun (x : α) ↦ β)
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))
mp : ¬(some od).getD 0 = 0
⊢ ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
have rw : List.dlookup (β := fun (x : α) ↦ β) a A = some od
Tactic: rw [(_ : List.dlookup a A = od)]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
⊢ ∃ (x : β), Sigma.mk (β := fun (a : α) ↦ β) a x ∈ A.dedupKeys (β := fun (x : α) ↦ β) ∧ (decide ¬x = 0) = true
have h₁ : Sigma.mk (β := fun (a : α) ↦ β) a ((List.dlookup (β := fun (x : α) ↦ β) a A).getD 0) ∈
    A.dedupKeys (β := fun (x : α) ↦ β) ∧
  (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0) = true
Tactic: use (A.dlookup a).getD (0 : β)
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0
⊢ Sigma.mk (β := fun (a : α) ↦ β) a ((List.dlookup (β := fun (x : α) ↦ β) a A).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a A).getD 0 = 0) = true
have h₁ : ∀ (h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0),
  Sigma.mk (β := fun (a : α) ↦ β) a
        ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0) = true
Tactic: rw [← List.dlookup_dedupKeys] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
⊢ Sigma.mk (β := fun (a : α) ↦ β) a
        ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∈
      A.dedupKeys (β := fun (x : α) ↦ β) ∧
    (decide ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0) = true
have h₁ : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) =
    some ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∧
  decide True = true
Tactic: simp only [h, ← List.mem_dlookup_iff A.nodupKeys_dedupKeys, not_false_iff, Option.mem_def]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
⊢ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) =
      some ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∧
    decide True = true
have h₁ : ∀ (haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = none),
  Eq.{v + 1} (α := Option β) none (some (Option.getD none 0)) ∧ decide True = true
Tactic: cases haA : List.dlookup a A.dedupKeys
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : Zero β
inst_2 : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0 = 0
h₁ :
  ∀ (haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = none),
    Eq.{v + 1} (α := Option β) none (some (Option.getD none 0)) ∧ decide True = true
⊢ List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) =
      some ((List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β))).getD 0) ∧
    decide True = true
have h₂ : ∀ (val : β) (haA : List.dlookup (β := fun (x : α) ↦ β) a (A.dedupKeys (β := fun (x : α) ↦ β)) = some val),
  some val = some ((some val).getD 0) ∧ decide True = true
Tactic: cases haA : List.dlookup a A.dedupKeys
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x
have simp : Option.getD (if h : y = x then some z else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)) x =
  if y = x then z else (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
Tactic: simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]
-- Lean 4 proof step from Mathlib.Testing.Plausible.Functions (goal)
Goal:
α : Type u
inst : DecidableEq α
xs : List (α × α)
x y z : α
⊢ Option.getD (if h : y = x then some z else dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)) x =
    if y = x then z else (dlookup (β := fun (x : α) ↦ α) x (map Prod.toSigma xs)).getD x
have pos : y = x → (some z).getD x = z
Tactic: split_ifs