-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Discriminant.Defs (goal)
Goal:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst : Field K
inst_1 : DecidableEq ι
inst_2 : DecidableEq ι'
inst_3 : Fintype ι
inst_4 : Fintype ι'
inst_5 : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b' : (a : ι') → K) i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K) i j)
rw :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr (ι := ι') ℚ (B := K)
      (Matrix.vecMul (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
        (Matrix.map ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)) (⇑(algebraMap ℚ K) : (a : ℚ) → K)))
rw₁ :
  discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₂ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑(b.reindex (b.indexEquiv b')) : (a : ι') → K)
rw₃ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_3} (ι := ι') ℚ (B := K)
        (Function.comp.{u_3 + 1, u_2 + 1, u_1 + 1} (β := ι) (⇑b : (a : ι) → K) (⇑(b.indexEquiv b').symm : (a : ι') → ι))
rw₄ rw₅ rw₆ :
  1 * discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2 *
      discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K)
e_a : 1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
⊢ discr.{0, u_1, u_2} (ι := ι) ℚ (B := K) (⇑b : (a : ι) → K) =
    discr.{0, u_1, u_3} (ι := ι') ℚ (B := K) (⇑b' : (a : ι') → K)
have e_a₁ : ∀ (hint : IsIntegral ℤ (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K)))),
  1 = HPow.hPow (β := ℕ) (Matrix.det ((b.reindex (b.indexEquiv b')).toMatrix (⇑b' : (a : ι') → K))) 2
Tactic: classical
  rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
  congr
  have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
  obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
  have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
  rw [← map_one (algebraMap ℤ ℚ), ← hr]
  rcases Int.isUnit_iff.1 hunit with hp | hm
  · simp [hp]
  · simp [hm]