Theorem: Array.data_injective (One.lean)

State before:
α : Type u_1
⊢ Function.Injective data
Tactic:
unfold Function.Injective
State after:
α : Type u_1
⊢ ∀ ⦃a₁ a₂ : Array α⦄, a₁.data = a₂.data → a₁ = a₂

State before:
α : Type u_1
⊢ ∀ ⦃a₁ a₂ : Array α⦄, a₁.data = a₂.data → a₁ = a₂
Tactic:
intro a₁ a₂ h
State after:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ a₁ = a₂

State before:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ a₁ = a₂
Tactic:
rw [← Array.toArray_data a₁, ← Array.toArray_data a₂]
State after:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ List.toArray a₁.data = List.toArray a₂.data

State before:
α : Type u_1
a₁ a₂ : Array α
h : a₁.data = a₂.data
⊢ List.toArray a₁.data = List.toArray a₂.data
Tactic:
congr
State after:
no goals