awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw : HPow.hPow (α := R ⧸ p) (-1) (Fintype.card (Fin n)) * Matrix.det (n := Fin n) 1 = HPow.hPow (α := R ⧸ p) (-1) n
rw₁ : HPow.hPow (α := R ⧸ p) (-1) n * Matrix.det (n := Fin n) 1 = HPow.hPow (α := R ⧸ p) (-1) n
rw₂ : HPow.hPow (α := R ⧸ p) (-1) n * 1 = HPow.hPow (α := R ⧸ p) (-1) n
rw₃ rw₄ : HPow.hPow (α := R ⧸ p) (-1) n = HPow.hPow (α := R ⧸ p) (-1) n
⊢ Matrix.det (n := Fin n) (-1) = HPow.hPow (α := R ⧸ p) (-1) n

Tactic:
rw [Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]

Premises used: Fintype.card_fin, Matrix.det_neg, Matrix.det_one, mul_one
-- 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)
⊢ HPow.hPow (α := R ⧸ p) (-1) n ≠ 0

Tactic:
IsUnit.ne_zero (isUnit_one.neg.pow _)

Premises used: IsUnit.pow, isUnit_one, IsUnit.ne_zero, IsUnit.neg
-- 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)
⊢ 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))

Tactic:
congr_arg Matrix.det (Matrix.ext fun i j => ?_)

Premises used: congr_arg, Matrix.ext, Matrix.det
-- 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 :
  ∀ (i j : 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))
        i j =
      HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p)
⊢ 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))

Tactic:
refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)

Premises used: congr_arg, Matrix.ext, Matrix.det
-- 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)
i j : Fin n
refine_1 :
  HSub.hSub (α := Matrix (Fin n) (Fin n) (R ⧸ p)) (β := Matrix (Fin n) (Fin n) (R ⧸ p))
      (Matrix.map (α := R) ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A')
        (⇑(Quotient.mk p) : (a : R) → R ⧸ p))
      1 i j =
    HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p)
⊢ (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))
      i j =
    HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p)

Tactic:
rw [map_sub, RingHom.mapMatrix_apply, map_one]

Premises used: RingHom.mapMatrix_apply, map_sub, map_one
-- 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)
i j : Fin n
⊢ HSub.hSub (α := Matrix (Fin n) (Fin n) (R ⧸ p)) (β := Matrix (Fin n) (Fin n) (R ⧸ p))
      (Matrix.map (α := R) ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A')
        (⇑(Quotient.mk p) : (a : R) → R ⧸ p))
      1 i j =
    HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p)

Tactic:
simp
-- 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)
⊢ 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))

Tactic:
congr_arg Matrix.det (Matrix.ext fun i j => ?_)

Premises used: congr_arg, Matrix.ext, Matrix.det
-- 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 :
  ∀ (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) = (-1) i j
⊢ 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))

Tactic:
refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)

Premises used: congr_arg, Matrix.ext, Matrix.det
-- 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)
i j : Fin n
refine_1 : HSub.hSub (α := R ⧸ p) 0 (1 i j) = (-1) i j
refine_1₁ : Eq.{u + 1} (α := R ⧸ p) (-1 i j) ((-1) i j)
refine_1₂ refine_1₃ : Eq.{u + 1} (α := R ⧸ p) (-1 i j) (-1 i j)
⊢ HSub.hSub (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p) = (-1) i j

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub, Matrix.neg_apply]

Premises used: Iff.mpr, Matrix.neg_apply, Ideal.Quotient.eq_zero_iff_mem, zero_sub
-- 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
x : L
hx :
  Membership.mem (γ := Submodule K L)
    (Submodule.restrictScalars K (span (singleton (α := L) ((algebraMap R L : (a : R) → L) A.det : L)))) x
⊢ Membership.mem (γ := Submodule L L)
    (span (singleton (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) A.det : S) : L))) x

Tactic:
rw [Submodule.restrictScalars_mem, IsScalarTower.algebraMap_apply R S L] at hx

Premises used: Submodule.restrictScalars_mem, IsScalarTower.algebraMap_apply