awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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))
⊢ Ne (α := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) A.det : R ⧸ p) (0 : R ⧸ p)
have 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))
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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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))
have 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)
Tactic: refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
⊢ (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)
have 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)
Tactic: rw [map_sub, RingHom.mapMatrix_apply, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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))
have 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
Tactic: refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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 (α := R ⧸ p) (β := R ⧸ p) ((Quotient.mk p : (a : R) → R ⧸ p) (A' i j) : R ⧸ p) (1 i j : R ⧸ p) = (-1) i j
have refine_1 : HSub.hSub (α := R ⧸ p) 0 (1 i j) = (-1) i j
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub, Matrix.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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
⊢ 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
have refine_1₁ : Eq.{u + 1} (α := R ⧸ p) (-1 i j) ((-1) i j)
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub, Matrix.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
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)
⊢ 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
have refine_1₂ : Eq.{u + 1} (α := R ⧸ p) (-1 i j) (-1 i j)
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub, Matrix.neg_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (hypothesis)
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 K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) x
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb' : LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)
⊢ LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)
have contrapose : ∀ (hb : ¬LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)),
  ¬LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)
Tactic: contrapose hb' with hb
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ¬LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)
⊢ ¬LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)
have simp : ∀
  (hb :
    ∃ (x : Finset ι) (x_1 : ι → K) (_ :
      Eq.{u_3 + 1} (α := V) (∑ i ∈ x, HSMul.hSMul (β := V) (x_1 i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (x_2 : ι) (_ :
      x_2 ∈ x), ¬x_1 x_2 = 0),
  ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
Tactic: simp only [linearIndependent_iff', not_forall] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb :
  ∃ (x : Finset ι) (x_1 : ι → K) (_ :
    Eq.{u_3 + 1} (α := V) (∑ i ∈ x, HSMul.hSMul (β := V) (x_1 i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
⊢ ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
have obtain : ∀ (s : Finset ι) (g : ι → K)
  (eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (j' : ι)
  (hj's : j' ∈ s) (hj'g : ¬g j' = 0),
  ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
Tactic: obtain ⟨s, g, eq, j', hj's, hj'g⟩ := hb
Cleared hypotheses: hb