Theorem: Array.nodup_push (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ Nodup (push as a) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
show (as.push a).data.Nodup ↔ as.Nodup ∧ a ∉ as
State after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (push as a).data ↔ Nodup as ∧ ¬a ∈ as
Tactic:
rewrite [Array.push_data]
State after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ List.Nodup (as.data ++ [a]) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
apply Iff.trans List.pairwise_append
State after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (List.Pairwise (fun x x_1 => x ≠ x_1) as.data ∧
      List.Pairwise (fun x x_1 => x ≠ x_1) [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔
    Nodup as ∧ ¬a ∈ as

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (List.Pairwise (fun x x_1 => x ≠ x_1) as.data ∧
      List.Pairwise (fun x x_1 => x ≠ x_1) [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔
    Nodup as ∧ ¬a ∈ as
Tactic:
show as.Nodup ∧ [a].Nodup ∧ _ ↔ _
State after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ List.Nodup [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔ Nodup as ∧ ¬a ∈ as

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ List.Nodup [a] ∧ ∀ (a_1 : α), a_1 ∈ as.data → ∀ (b : α), b ∈ [a] → a_1 ≠ b) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
simp only [List.nodup_singleton a, true_and, ← mem_iff_mem_data, List.mem_singleton, forall_eq]
State after:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ Nodup as ∧ ¬a ∈ as

State before:
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (Nodup as ∧ ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ Nodup as ∧ ¬a ∈ as
Tactic:
apply and_congr_right'
State after:
case h
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ ¬a ∈ as

State before:
case h
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) ↔ ¬a ∈ as
Tactic:
constructor
State after:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as

case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a

State before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as

case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
. intro h ha; exact h a ha rfl
State after:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a

State before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
. intro ha b hb heq; cases heq; exact ha hb
State after:
no goals

State before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ (∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a) → ¬a ∈ as
Tactic:
intro h ha
State after:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
h : ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a
ha : a ∈ as
⊢ False

State before:
case h.mp
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
h : ∀ (a_1 : α), a_1 ∈ as → a_1 ≠ a
ha : a ∈ as
⊢ False
Tactic:
exact h a ha rfl
State after:
no goals

State before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
Tactic:
intro ha b hb heq
State after:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False

State before:
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False
Tactic:
cases heq
State after:
case h.mpr.refl
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
hb : a ∈ as
⊢ False

State before:
case h.mpr.refl
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
hb : a ∈ as
⊢ False
Tactic:
exact ha hb
State after:
no goals