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

State before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
⊢ t₁.toTensor.shape = t₂.toTensor.shape → t₁.toTensor.data = t₂.toTensor.data → t₁ = t₂
Tactic:
intros h_shape h_data
State after:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁ = t₂

State before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁ = t₂
Tactic:
suffices t₁.toTensor = t₂.toTensor by
  cases t₁; cases t₂; simp at *; trivial
State after:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁.toTensor = t₂.toTensor

State before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁.toTensor = t₂.toTensor
Tactic:
apply Tensor.eq_of_fields_eq <;> trivial
State after:
no goals

State before:
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
this : t₁.toTensor = t₂.toTensor
⊢ t₁ = t₂
Tactic:
cases t₁
State after:
case mk
τ : DimList
D : MLIRTy
t₂ : RankedTensor τ D
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape = t₂.toTensor.shape
h_data : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data = t₂.toTensor.data
this : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor = t₂.toTensor
⊢ { toTensor := toTensor✝, h_refines := h_refines✝ } = t₂

State before:
case mk
τ : DimList
D : MLIRTy
t₂ : RankedTensor τ D
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape = t₂.toTensor.shape
h_data : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data = t₂.toTensor.data
this : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor = t₂.toTensor
⊢ { toTensor := toTensor✝, h_refines := h_refines✝ } = t₂
Tactic:
cases t₂
State after:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.shape =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape
h_data :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.data =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data
this :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor
⊢ { toTensor := toTensor✝¹, h_refines := h_refines✝¹ } = { toTensor := toTensor✝, h_refines := h_refines✝ }

State before:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.shape =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape
h_data :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.data =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data
this :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor
⊢ { toTensor := toTensor✝¹, h_refines := h_refines✝¹ } = { toTensor := toTensor✝, h_refines := h_refines✝ }
Tactic:
simp at *
State after:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : toTensor✝¹.shape = toTensor✝.shape
h_data : toTensor✝¹.data = toTensor✝.data
this : toTensor✝¹ = toTensor✝
⊢ toTensor✝¹ = toTensor✝

State before:
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : toTensor✝¹.shape = toTensor✝.shape
h_data : toTensor✝¹.data = toTensor✝.data
this : toTensor✝¹ = toTensor✝
⊢ toTensor✝¹ = toTensor✝
Tactic:
trivial
State after:
no goals