Theorem: Vector.eq_of_fields_eq (MLIR/Dialects/BuiltinModel.lean)

State before:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
⊢ v₁.scale = v₂.scale → v₁.data = v₂.data → v₁ = v₂
Tactic:
intros h_scale h_data
State after:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
h_scale : v₁.scale = v₂.scale
h_data : v₁.data = v₂.data
⊢ v₁ = v₂

State before:
τ fixed : List ℕ
scalable : MLIRTy
v₁ v₂ : Vector τ fixed scalable
h_scale : v₁.scale = v₂.scale
h_data : v₁.data = v₂.data
⊢ v₁ = v₂
Tactic:
cases v₁
State after:
case mk
τ fixed : List ℕ
scalable : MLIRTy
v₂ : Vector τ fixed scalable
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale = v₂.scale
h_data : { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data = v₂.data
⊢ { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ } = v₂

State before:
case mk
τ fixed : List ℕ
scalable : MLIRTy
v₂ : Vector τ fixed scalable
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale = v₂.scale
h_data : { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data = v₂.data
⊢ { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ } = v₂
Tactic:
cases v₂
State after:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.scale =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale
h_data :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.data =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data
⊢ { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ } =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }

State before:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.scale =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale
h_data :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.data =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data
⊢ { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ } =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }
Tactic:
simp at *
State after:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale : scale✝¹ = scale✝
h_data : data✝¹ = data✝
⊢ scale✝¹ = scale✝ ∧ data✝¹ = data✝

State before:
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale : scale✝¹ = scale✝
h_data : data✝¹ = data✝
⊢ scale✝¹ = scale✝ ∧ data✝¹ = data✝
Tactic:
trivial
State after:
no goals