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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
obtain :
  ∀ (a' : Fin n → R),
    (∀ (i : Fin n), a' i ∈ p) →
      ∀ (quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')),
        HSMul.hSMul (β := S ⧸ M) A.det (Submodule.Quotient.mk x') = 0
⊢ HSMul.hSMul (β := S ⧸ M) A.det (Submodule.Quotient.mk x') = 0

Tactic:
obtain ⟨a', _, quot_x_eq⟩ := exists_sum (Submodule.Quotient.mk x')

Premises used: Submodule.Quotient.mk
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
rw : Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, A.det • a' x • a x) 0
⊢ HSMul.hSMul (β := S ⧸ M) A.det (Submodule.Quotient.mk x') = 0

Tactic:
rw [← quot_x_eq, Finset.smul_sum]

Premises used: Finset.smul_sum
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
lhs : ∑ x : Fin n, A.det • a' x • a x
| Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, A.det • a' x • a x) 0

Tactic:
lhs
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
congr : Finset.univ
f : fun (x : Fin n) ↦ A.det • a' x • a x
| ∑ x : Fin n, A.det • a' x • a x

Tactic:
congr
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
| Finset.univ

Tactic:
next => skip
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
x : Fin n
f : 0
| A.det • a' x • a x

Tactic:
rw [smul_comm A.det, d_smul, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm, 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
f : ∀ (x : Fin n), 0
| Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, A.det • a' x • a x) 0

Tactic:
lhs; congr; next => skip
      intro x; rw [smul_comm A.det, d_smul, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm, 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
conv : Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, 0) 0
⊢ Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, A.det • a' x • a x) 0

Tactic:
conv =>
      lhs; congr; next => skip
      intro x; rw [smul_comm A.det, d_smul, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm, 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
⊢ Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finset.sum_const_zero
-- 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
x' : S
hx :
  Membership.mem (γ := Submodule S S) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) (A.det • x')
a' : Fin n → R
left : ∀ (i : Fin n), a' i ∈ p
quot_x_eq : Eq (α := S ⧸ M) (∑ i : Fin n, a' i • a i) (Submodule.Quotient.mk x')
⊢ Eq.{v + 1} (α := S ⧸ M) (∑ x : Fin n, 0) 0

Tactic:
exact Finset.sum_const_zero

Premises used: Finset.sum_const_zero
-- 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
⊢ Submodule.restrictScalars R (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) ≤ M

Tactic:
have span_d : (Submodule.span S ({algebraMap R S A.det} : Set S)).restrictScalars R ≤ M := by
    intro x hx
    rw [Submodule.restrictScalars_mem] at hx
    obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hx
    rw [smul_eq_mul, mul_comm, ← Algebra.smul_def] at hx ⊢
    rw [← Submodule.Quotient.mk_eq_zero, Submodule.Quotient.mk_smul]
    obtain ⟨a', _, quot_x_eq⟩ := exists_sum (Submodule.Quotient.mk x')
    rw [← quot_x_eq, Finset.smul_sum]
    conv =>
      lhs; congr; next => skip
      intro x; rw [smul_comm A.det, d_smul, smul_zero]
    exact Finset.sum_const_zero
-- 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
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤

Tactic:
top_le_iff.mp
      (calc
        ⊤ = (Ideal.span {algebraMap R L A.det}).restrictScalars K := ?_
        _ ≤ Submodule.span K (algebraMap S L '' b) := ?_)

Premises used: Trans.trans, top_le_iff, Iff.mp