-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : (i : Fin n) → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R :=
  HSub.hSub (α := Matrix (Fin n) (Fin n) R) (β := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A' : Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), Eq.{v + 1} (α := S ⧸ M) (∑ j : Fin n, A i j • a j) 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) ≤ M
this : Nontrivial.{u} (R ⧸ p)
refine_1 :
  Eq.{u + 1} (α := R ⧸ p)
    (Matrix.det (n := Fin n)
      ((RingHom.mapMatrix (Quotient.mk p) : (a : Matrix (Fin n) (Fin n) R) → Matrix (Fin n) (Fin n) (R ⧸ p))
        (HSub.hSub (α := Matrix (Fin n) (Fin n) R) (β := Matrix (Fin n) (Fin n) R)
          ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A' : Matrix (Fin n) (Fin n) R)
          (1 : Matrix (Fin n) (Fin n) R))))
    (Matrix.det (n := Fin n) fun (i j : Fin n) ↦
      HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p))
refine_1₁ :
  Eq.{u + 1} (α := R ⧸ p)
    (Matrix.det (n := Fin n) fun (i j : Fin n) ↦
      HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p))
    (Matrix.det (n := Fin n) (-1))
⊢ Ne (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) A.det : R ⧸ p) (0 : R ⧸ p)

Tactic:
calc
      Ideal.Quotient.mk p A.det = Matrix.det ((Ideal.Quotient.mk p).mapMatrix A) := by
        rw [RingHom.map_det]
      _ = Matrix.det ((Ideal.Quotient.mk p).mapMatrix (Matrix.of A' - 1)) := rfl
      _ = Matrix.det fun i j =>
          (Ideal.Quotient.mk p) (A' i j) - (1 : Matrix (Fin n) (Fin n) (R ⧸ p)) i j := ?_
      _ = Matrix.det (-1 : Matrix (Fin n) (Fin n) (R ⧸ p)) := ?_
      _ = (-1 : R ⧸ p) ^ n := by rw [Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
      _ ≠ 0 := IsUnit.ne_zero (isUnit_one.neg.pow _)

Premises used: Ideal.Quotient.mk, Matrix.of, HSub.hSub, IsUnit.pow, isUnit_one, RingHom.mapMatrix, IsUnit.ne_zero, IsUnit.neg, OfNat.ofNat, DFunLike.coe, Matrix.det, Neg.neg, rfl