Theorem: Array.nodup_iff_nodup_data (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
inst✝ : DecidableEq α
x : Array α
⊢ Nodup x ↔ List.Nodup x.data
Tactic:
induction x using cons_induction with
| empty => simp only [nodup_empty, true_iff]; exact .nil
| cons a x IH =>
  simp only [nodup_cons, data_cons]
  dsimp [List.Nodup]; rewrite [List.pairwise_cons, IH]
  apply and_congr_left'
  simp only [← mem_iff_mem_data]
  constructor
  . intro h _ ha hcntr; cases hcntr
    exact h ha
  . intro h ha
    exact h a ha rfl
State after:
no goals

State before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ Nodup #[] ↔ List.Nodup #[].data
Tactic:
simp only [nodup_empty, true_iff]
State after:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ List.Nodup #[].data

State before:
case empty
α : Type u
inst✝ : DecidableEq α
⊢ List.Nodup #[].data
Tactic:
exact .nil
State after:
no goals

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ Nodup (cons a x) ↔ List.Nodup (cons a x).data
Tactic:
simp only [nodup_cons, data_cons]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Nodup (a :: x.data)

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Nodup (a :: x.data)
Tactic:
dsimp [List.Nodup]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Pairwise (fun x x_1 => ¬x = x_1) (a :: x.data)

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ Nodup x ↔ List.Pairwise (fun x x_1 => ¬x = x_1) (a :: x.data)
Tactic:
rewrite [List.pairwise_cons, IH]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ List.Nodup x.data ↔ (∀ (a' : α), a' ∈ x.data → ¬a = a') ∧ List.Pairwise (fun x x_1 => ¬x = x_1) x.data

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ∧ List.Nodup x.data ↔ (∀ (a' : α), a' ∈ x.data → ¬a = a') ∧ List.Pairwise (fun x x_1 => ¬x = x_1) x.data
Tactic:
apply and_congr_left'
State after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x.data → ¬a = a'

State before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x.data → ¬a = a'
Tactic:
simp only [← mem_iff_mem_data]
State after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x → ¬a = a'

State before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x ↔ ∀ (a' : α), a' ∈ x → ¬a = a'
Tactic:
constructor
State after:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'

case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x

State before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'

case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
. intro h _ ha hcntr; cases hcntr
  exact h ha
State after:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x

State before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
. intro h ha
  exact h a ha rfl
State after:
no goals

State before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ ¬a ∈ x → ∀ (a' : α), a' ∈ x → ¬a = a'
Tactic:
intro h _ ha hcntr
State after:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
a'✝ : α
ha : a'✝ ∈ x
hcntr : a = a'✝
⊢ False

State before:
case cons.h.mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
a'✝ : α
ha : a'✝ ∈ x
hcntr : a = a'✝
⊢ False
Tactic:
cases hcntr
State after:
case cons.h.mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
ha : a ∈ x
⊢ False

State before:
case cons.h.mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ¬a ∈ x
ha : a ∈ x
⊢ False
Tactic:
exact h ha
State after:
no goals

State before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
⊢ (∀ (a' : α), a' ∈ x → ¬a = a') → ¬a ∈ x
Tactic:
intro h ha
State after:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ∀ (a' : α), a' ∈ x → ¬a = a'
ha : a ∈ x
⊢ False

State before:
case cons.h.mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
IH : Nodup x ↔ List.Nodup x.data
h : ∀ (a' : α), a' ∈ x → ¬a = a'
ha : a ∈ x
⊢ False
Tactic:
exact h a ha rfl
State after:
no goals