Theorem: PreHFSet.eq_or_mem_of_mem_insert (Hfzfa.lean)

State before:
atoms : Type u_1
x y z : PreHFSet atoms
a : atoms
⊢ x ∈ insert y (atom a) → isAtom (atom a) = false ∧ (x ≈ y ∨ x ∈ atom a)
Tactic:
simp [insert, isAtom, Membership.mem, Mem]
State after:
no goals

State before:
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
⊢ x ∈ insert y (lst b) → isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
rintro ⟨i, hi⟩
State after:
case intro
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi : x ≈ Fin.cons y b i
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)

State before:
case intro
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi : x ≈ Fin.cons y b i
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
induction' i using Fin.cases with i
State after:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)

case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)

State before:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
refine ⟨rfl, Or.inl ?_⟩
State after:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ x ≈ y

State before:
case intro.H0
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i
hi : x ≈ Fin.cons y b 0
⊢ x ≈ y
Tactic:
simpa using hi
State after:
no goals

State before:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ isAtom (lst b) = false ∧ (x ≈ y ∨ x ∈ lst b)
Tactic:
refine ⟨rfl, Or.inr ⟨i, ?_⟩⟩
State after:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ x ≈ b i

State before:
case intro.Hs
atoms : Type u_1
x y z : PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
i✝ : Fin (n✝ + 1)
hi✝ : x ≈ Fin.cons y b i✝
i : Fin n✝
hi : x ≈ Fin.cons y b (Fin.succ i)
⊢ x ≈ b i
Tactic:
simpa using hi
State after:
no goals