-- Lean 4 proof step from Mathlib.NumberTheory.Height.MvPolynomial (goal)
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, ⋯⟩)
⊢ ![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
have h₃ : ![a, b]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)).1 *
    ![c, d]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ),
          (fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩, (fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i