internlm/Lean-Github huggingface dataset:
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ i = j
Tactic:
exfalso
Proof state after:
case h
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ False
Theorem: Array.nodup_append
Proof state before:
case h
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : i < size as
hj' : ¬j < size as
hij : as[i] = bs[j - size as]
⊢ False
Tactic:
exact hdisj _ _ _ _ hij
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
have hi'' : i ≥ as.size := Nat.le_of_not_lt hi'
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
have : i - as.size < bs.size :=
  Nat.sub_lt_left_of_lt_add hi'' (size_append _ _ ▸ hi)
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
⊢ (as ++ bs)[i] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hi')]
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
if hj' : j < as.size then
  rewrite [getElem_append_left as bs hj']
  intro hij; exfalso
  exact hdisj _ _ _ _ hij.symm
else
  have hj'' : j ≥ as.size := Nat.le_of_not_lt hj'
  have : j - as.size < bs.size :=
    Nat.sub_lt_left_of_lt_add hj'' (size_append _ _ ▸ hj)
  rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
  intro h
  have := hbs.get_inj (i-as.size) (j-as.size) ‹_› ‹_› h
  conv at this =>
    rewrite [Nat.sub_eq_iff_eq_add hi'']
    rewrite [Nat.sub_add_cancel hj'']
  exact this
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_left as bs hj']
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
⊢ bs[i - size as] = as[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
⊢ bs[i - size as] = as[j] → i = j
Tactic:
intro hij
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ i = j
Tactic:
exfalso
Proof state after:
case h
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ False
Theorem: Array.nodup_append
Proof state before:
case h
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : j < size as
hij : bs[i - size as] = as[j]
⊢ False
Tactic:
exact hdisj _ _ _ _ hij.symm
Proof state after:
no goals
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : ¬j < size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
have hj'' : j ≥ as.size := Nat.le_of_not_lt hj'
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
have : j - as.size < bs.size :=
  Nat.sub_lt_left_of_lt_add hj'' (size_append _ _ ▸ hj)
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = (as ++ bs)[j] → i = j
Tactic:
rewrite [getElem_append_right as bs (Nat.le_of_not_lt hj')]
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = bs[j - size as] → i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
⊢ bs[i - size as] = bs[j - size as] → i = j
Tactic:
intro h
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
⊢ i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
⊢ i = j
Tactic:
have := hbs.get_inj (i-as.size) (j-as.size) ‹_› ‹_› h
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝¹ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i - size as = j - size as
⊢ i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝¹ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i - size as = j - size as
⊢ i = j
Tactic:
conv at this =>
  rewrite [Nat.sub_eq_iff_eq_add hi'']
  rewrite [Nat.sub_add_cancel hj'']
Proof state after:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝¹ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i = j
⊢ i = j
Theorem: Array.nodup_append
Proof state before:
α : Type u
as bs : Array α
has : Nodup as
hbs : Nodup bs
hdisj : ∀ (i j : Nat) (hi : i < size as) (hj : j < size bs), as[i] ≠ bs[j]
i j : Nat
hi : i < size (as ++ bs)
hj : j < size (as ++ bs)
hi' : ¬i < size as
hi'' : i ≥ size as
this✝¹ : i - size as < size bs
hj' : ¬j < size as
hj'' : j ≥ size as
this✝ : j - size as < size bs
h : bs[i - size as] = bs[j - size as]
this : i = j
⊢ i = j
Tactic:
exact this
Proof state after:
no goals
Theorem: Array.nodup_map
Proof state before:
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : (map f as)[i] = (map f as)[j]
⊢ i = j
Tactic:
conv at h =>
  simp only [Array.getElem_map]
Proof state after:
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ i = j
Theorem: Array.nodup_map
Proof state before:
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ i = j
Tactic:
apply has.get_inj
Proof state after:
case a
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ as[i] = as[j]

case hi
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ i < size as

case hj
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ j < size as
Theorem: Array.nodup_map
Proof state before:
case a
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ as[i] = as[j]

case hi
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ i < size as

case hj
α : Type u
β : Type v
f : α → β
as : Array α
has : Nodup as
hf : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
i j : Nat
hi : i < size (map f as)
hj : j < size (map f as)
h : f as[i] = f as[j]
⊢ j < size as
Tactic:
apply hf _ _ h
Proof state after:
no goals
Theorem: Array.nodup_swap
Proof state before:
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ Nodup (swap as i j)
Tactic:
apply nodup_of_get_inj
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ ∀ (i_1 j_1 : Nat) (hi : i_1 < size (swap as i j)) (hj : j_1 < size (swap as i j)),
    (swap as i j)[i_1] = (swap as i j)[j_1] → i_1 = j_1
Theorem: Array.nodup_swap
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
⊢ ∀ (i_1 j_1 : Nat) (hi : i_1 < size (swap as i j)) (hj : j_1 < size (swap as i j)),
    (swap as i j)[i_1] = (swap as i j)[j_1] → i_1 = j_1
Tactic:
intro k l hk hl has
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ k = l
Theorem: Array.nodup_swap
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ k = l
Tactic:
apply h.get_inj k l (as.size_swap i j ▸ hk) (as.size_swap i j ▸ hl)
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has : (swap as i j)[k] = (swap as i j)[l]
⊢ as[k] = as[l]
Tactic:
simp only [getElem_swap] at has
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk : k < size (swap as i j)
hl : l < size (swap as i j)
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
⊢ as[k] = as[l]
Tactic:
rewrite [as.size_swap i j] at hk hl
Proof state after:
case h
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k l : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
hl✝ : l < size (swap as i j)
hl : l < size as
has :
  (if j.val = k then as[i.val] else if i.val = k then as[j.val] else as[k]) =
    if j.val = l then as[i.val] else if i.val = l then as[j.val] else as[l]
⊢ as[k] = as[l]
Theorem: Array.nodup_swap
Proof state before:
case h.t.e.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[i.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : j.val < size (swap as i j)
hk : j.val < size as
hik : ¬i.val = j.val
⊢ as[j.val] = as[l]

case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]

case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
. exfalso; exact hil <| h.get_inj _ _ _ _ has
Proof state after:
case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]

case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Theorem: Array.nodup_swap
Proof state before:
case h.e.t.e.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
l : Nat
hl✝ : l < size (swap as i j)
hl : l < size as
has : as[j.val] = as[l]
hil : ¬i.val = l
hjl : ¬j.val = l
hk✝ : i.val < size (swap as i j)
hk : i.val < size as
hjk : ¬j.val = i.val
⊢ as[i.val] = as[l]

case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
. exfalso; exact hjl <| h.get_inj _ _ _ _ has
Proof state after:
case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Theorem: Array.nodup_swap
Proof state before:
case h.e.e.t.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]
Tactic:
. simp only [hil]
Proof state after:
case h.e.e.t.e.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[i.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : j.val < size (swap as i j)
hl : j.val < size as
hil : ¬i.val = j.val
⊢ as[i.val] = as[j.val]

case h.e.e.e.t.refl
α : Type u
as : Array α
i j : Fin (size as)
h : Nodup as
k : Nat
hk✝ : k < size (swap as i j)
hk : k < size as
has : as[k] = as[j.val]
hik : ¬i.val = k
hjk : ¬j.val = k
hl✝ : i.val < size (swap as i j)
hl : i.val < size as
hjl : ¬j.val = i.val
⊢ as[j.val] = as[i.val]