-- Module: Mathlib.NumberTheory.Height.MvPolynomial
Goal:
K : Type u_4
inst : Field K
inst_1 : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ
h :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
h₂ :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩)
h₃ :
  ![a, b]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).1 *
      ![c, d]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ),
            (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)).2 =
    Function.comp (α := Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) ![a * c, a * d, b * c, b * d]
      (⇑finProdFinEquiv :
        (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ))
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩)
⊢ ![a, b] i.1 * ![c, d] i.2 =
    (![a * c, a * d, b * c, b * d] ∘
        (⇑finProdFinEquiv :
          (a : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ) → Fin ((Nat.succ 0).succ * (Nat.succ 0).succ)))
      i

Tactic:
fin_cases i