mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ sqrt (↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
·

Goal state after:
case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ sqrt (↑n * ⅟↑d) = ↑sn * ⅟↑sd
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ Invertible ↑sd

pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
·

Goal state after:
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ Invertible ↑sd
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
·

Goal state after:
case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ √(↑n * ⅟↑d) = ↑sn * ⅟↑sd
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False

pp: case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
·

Goal state after:
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₁
⊢ False
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False

Tactic:
·

Goal state after:
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬v.satisfies_fmla (f₁.and f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ f₁.and f₂
hn' : ¬v.satisfies c
h : c ∈ f₂
⊢ False
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__x✝¹ : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__x✝ : PLift (a ≤ b)
hab : a ≤ b
h_bn : ¬b < n
hbn_eq : b = n
hba : ¬b = a
⊢ a < n

Tactic:
by lia

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m

pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) = List.dlookup x m
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst

Tactic:
·

Goal state after:
case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ x ≠ ⟨fst, snd⟩.fst
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) → ¬(List.dlookup a A).getD 0 = 0

pp: case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬(List.dlookup a A).getD 0 = 0 → ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true

Tactic:
·

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) → ¬(List.dlookup a A).getD 0 = 0
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0

pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od

Tactic:
·

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ ¬(some od).getD 0 = 0
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od

Tactic:
·

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬(List.dlookup a A).getD 0 = 0 → ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true

Tactic:
·

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ ¬(List.dlookup a A).getD 0 = 0 → ∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h.none
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
haA : List.dlookup a A.dedupKeys = none
⊢ none = some (none.getD 0) ∧ decide True = true

pp: case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true

Tactic:
·

Goal state after:
case h.none
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
haA : List.dlookup a A.dedupKeys = none
⊢ none = some (none.getD 0) ∧ decide True = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true

Tactic:
·

Goal state after:
case h.some
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
h : ¬(List.dlookup a A.dedupKeys).getD 0 = 0
val✝ : β
haA : List.dlookup a A.dedupKeys = some val✝
⊢ some val✝ = some ((some val✝).getD 0) ∧ decide True = true
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

pp: case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y

Tactic:
·

Goal state after:
case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero.nil
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x' = y ↔ [][0]? = some y

pp: case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
·

Goal state after:
case cons.zero.nil
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x' = y ↔ [][0]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y

Tactic:
·

Goal state after:
case cons.zero.cons
α : Type u
inst✝ : DecidableEq α
y x' : α
xs : List α
h₀ : (x' :: xs).Nodup
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x' → (applyId (xs.zip ys) x' = y ↔ ys[i]? = some y)
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x' = y ↔ (head✝ :: tail✝)[0]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y

Tactic:
·

Goal state after:
case cons.succ
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.nil
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x = y ↔ [][n✝ + 1]? = some y

pp: case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
·

Goal state after:
case cons.succ.nil
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
h₁ : (x' :: xs).length = [].length
⊢ applyId ((x' :: xs).zip []) x = y ↔ [][n✝ + 1]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
·

Goal state after:
case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x

Tactic:
·

Goal state after:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x

Tactic:
·

Goal state after:
case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some.cons.nil
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip [])) = some val
h₂ : [].Nodup
h₁ : (x' :: xs).length = [].length
⊢ val ∈ [] ↔ x ∈ x' :: xs

pp: case some.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip (y :: ys))) = some val
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
·

Goal state after:
case some.cons.nil
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
h₃ : dlookup x (map Prod.toSigma ((x' :: xs).zip [])) = some val
h₂ : [].Nodup
h₁ : (x' :: xs).length = [].length
⊢ val ∈ [] ↔ x ∈ x' :: xs
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

pp: case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys

Tactic:
·

Goal state after:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Tactic:
·

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x