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

State before:
τ : MLIRTy
t₁ t₂ : Tensor τ
⊢ t₁.shape = t₂.shape → t₁.data = t₂.data → t₁ = t₂
Tactic:
intros h_shape h_data
State after:
τ : MLIRTy
t₁ t₂ : Tensor τ
h_shape : t₁.shape = t₂.shape
h_data : t₁.data = t₂.data
⊢ t₁ = t₂

State before:
τ : MLIRTy
t₁ t₂ : Tensor τ
h_shape : t₁.shape = t₂.shape
h_data : t₁.data = t₂.data
⊢ t₁ = t₂
Tactic:
cases t₁
State after:
case mk
τ : MLIRTy
t₂ : Tensor τ
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape = t₂.shape
h_data : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data = t₂.data
⊢ { shape := shape✝, data := data✝, h_data_size := h_data_size✝ } = t₂

State before:
case mk
τ : MLIRTy
t₂ : Tensor τ
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape = t₂.shape
h_data : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data = t₂.data
⊢ { shape := shape✝, data := data✝, h_data_size := h_data_size✝ } = t₂
Tactic:
cases t₂
State after:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.shape =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape
h_data :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.data =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data
⊢ { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ } =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }

State before:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.shape =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape
h_data :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.data =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data
⊢ { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ } =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }
Tactic:
simp at *
State after:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : shape✝¹ = shape✝
h_data : data✝¹ = data✝
⊢ shape✝¹ = shape✝ ∧ data✝¹ = data✝

State before:
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : shape✝¹ = shape✝
h_data : data✝¹ = data✝
⊢ shape✝¹ = shape✝ ∧ data✝¹ = data✝
Tactic:
trivial
State after:
no goals