Theorem: PreHFSet.insert_equiv_of_equiv (Hfzfa.lean)

State before:
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ insert x (lst a) ≈ insert y (lst b)
Tactic:
constructor
State after:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (i : Fin (n✝¹ + 1)), ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)

case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (j : Fin (n✝ + 1)), ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b j)

State before:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (i : Fin (n✝¹ + 1)), ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
intro i
State after:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin (n✝¹ + 1)
⊢ ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)

State before:
case left
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin (n✝¹ + 1)
⊢ ∃ j, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
induction' i using Fin.cases with i
State after:
case left.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a 0) (Fin.cons y b j)

case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)

State before:
case left.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a 0) (Fin.cons y b j)
Tactic:
exact ⟨0, h⟩
State after:
no goals

State before:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Tactic:
let ⟨j, hj⟩ := h₂ i
State after:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)

State before:
case left.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝¹
j : Fin n✝
hj : Equiv (a i) (b j)
⊢ ∃ j, Equiv (Fin.cons x a (Fin.succ i)) (Fin.cons y b j)
Tactic:
exact ⟨j.succ, hj⟩
State after:
no goals

State before:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∀ (j : Fin (n✝ + 1)), ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b j)
Tactic:
intro i
State after:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin (n✝ + 1)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b i)

State before:
case right
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin (n✝ + 1)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b i)
Tactic:
induction' i using Fin.cases with i
State after:
case right.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b 0)

case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))

State before:
case right.H0
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
⊢ ∃ i, Equiv (Fin.cons x a i) (Fin.cons y b 0)
Tactic:
exact ⟨0, h⟩
State after:
no goals

State before:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Tactic:
let ⟨j, hj⟩ := h₃ i
State after:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))

State before:
case right.Hs
atoms : Type u_1
x y z z' : PreHFSet atoms
h : x ≈ y
h' : z ≈ z'
n✝¹ : ℕ
a : Fin n✝¹ → PreHFSet atoms
n✝ : ℕ
b : Fin n✝ → PreHFSet atoms
h₂ : ∀ (i : Fin n✝¹), ∃ j, Equiv (a i) (b j)
h₃ : ∀ (j : Fin n✝), ∃ i, Equiv (a i) (b j)
i : Fin n✝
j : Fin n✝¹
hj : Equiv (a j) (b i)
⊢ ∃ i_1, Equiv (Fin.cons x a i_1) (Fin.cons y b (Fin.succ i))
Tactic:
exact ⟨j.succ, hj⟩
State after:
no goals