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

State before:
α : Type u
inst✝ : DecidableEq α
x : Array α
a : α
⊢ Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
Tactic:
induction x using cons_induction with
| empty =>
  simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
  exact nodup_singleton a
| cons b x IH =>
  simp only [push_cons_eq_cons_push, nodup_cons, mem_push, mem_cons, IH]
  simp only [not_or, and_assoc]
  apply and_congr_right'
  simp only [← and_assoc]; rewrite[and_comm (a:=x.Nodup)]
  apply and_congr_left'; apply and_congr_left'
  exact ⟨Ne.symm, Ne.symm⟩
State after:
no goals

State before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a) ↔ Nodup #[] ∧ ¬a ∈ #[]
Tactic:
simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
State after:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a)

State before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a)
Tactic:
exact nodup_singleton a
State after:
no goals

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ Nodup (push (cons b x) a) ↔ Nodup (cons b x) ∧ ¬a ∈ cons b x
Tactic:
simp only [push_cons_eq_cons_push, nodup_cons, mem_push, mem_cons, IH]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬(b ∈ x ∨ b = a) ∧ Nodup x ∧ ¬a ∈ x ↔ (¬b ∈ x ∧ Nodup x) ∧ ¬(a = b ∨ a ∈ x)

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬(b ∈ x ∨ b = a) ∧ Nodup x ∧ ¬a ∈ x ↔ (¬b ∈ x ∧ Nodup x) ∧ ¬(a = b ∨ a ∈ x)
Tactic:
simp only [not_or, and_assoc]
State after:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b ∈ x ∧ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ ¬b ∈ x ∧ Nodup x ∧ ¬a = b ∧ ¬a ∈ x

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b ∈ x ∧ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ ¬b ∈ x ∧ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Tactic:
apply and_congr_right'
State after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ Nodup x ∧ ¬a = b ∧ ¬a ∈ x

State before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ∧ ¬a ∈ x ↔ Nodup x ∧ ¬a = b ∧ ¬a ∈ x
Tactic:
simp only [← and_assoc]
State after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (Nodup x ∧ ¬a = b) ∧ ¬a ∈ x

State before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (Nodup x ∧ ¬a = b) ∧ ¬a ∈ x
Tactic:
rewrite[and_comm (a:=x.Nodup)]
State after:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (¬a = b ∧ Nodup x) ∧ ¬a ∈ x

State before:
case cons.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ (¬b = a ∧ Nodup x) ∧ ¬a ∈ x ↔ (¬a = b ∧ Nodup x) ∧ ¬a ∈ x
Tactic:
apply and_congr_left'
State after:
case cons.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ↔ ¬a = b ∧ Nodup x

State before:
case cons.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ∧ Nodup x ↔ ¬a = b ∧ Nodup x
Tactic:
apply and_congr_left'
State after:
case cons.h.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ↔ ¬a = b

State before:
case cons.h.h.h
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬b = a ↔ ¬a = b
Tactic:
exact ⟨Ne.symm, Ne.symm⟩
State after:
no goals