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
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''
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
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
rw :
  HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := V) ((algebraMap R K : (a : R) → K) (g' i) : K)
      ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₂ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₃ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    HSMul.hSMul (β := V) (a • g i) (((⇑F : (a : V'') → V) ∘ b) i)
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw₄ : HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
  HSMul.hSMul (β := V) (a * g i) (((⇑F : (a : V'') → V) ∘ b) i)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_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
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''
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
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
i : ι
hi : i ∈ s
rw :
  HSMul.hSMul (β := V) (g' i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := K) (β := V) ((algebraMap R K : (a : R) → K) (g' i) : K)
      ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₂ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₃ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    HSMul.hSMul (β := V) (a • g i) (((⇑F : (a : V'') → V) ∘ b) i)
rw₄ :
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
    HSMul.hSMul (β := V) (a * g i) (((⇑F : (a : V'') → V) ∘ b) i)
⊢ (F : (a : V'') → V) (g' i • b i) = a • HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)
have rw₅ : HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V) =
  HSMul.hSMul (β := V) (a * g i) ((F : (a : V'') → V) (b i) : V)
Tactic: rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_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
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''
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
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
⊢ Eq.{u_4 + 1} (α := V')
    (∑ i ∈ s,
      HSMul.hSMul.{v, u_4, u_4} (α := S) (β := V') ((fun (i : ι) ↦ ((f : (a : R) → S) (g' i) : S)) i)
        (((⇑f' : (a : V'') → V') ∘ b) i))
    0
have eq₁ : Eq.{u_3 + 1} (α := V) ((F : (a : V'') → V) (∑ i ∈ s, g' i • b i) : V) (0 : V)
Tactic: have eq : F (∑ i ∈ s, g' i • b i) = 0 := by
    rw [map_sum, ← smul_zero a, ← eq, Finset.smul_sum]
    refine Finset.sum_congr rfl ?_
    intro i hi
    rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have b_eq_b' : Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
  ((⇑((↑R :
            {S M M₂ : Type v} →
              [inst : Semiring R] →
                [inst_15 : Semiring S] →
                  [inst_16 : AddCommMonoid M] →
                    [inst_17 : AddCommMonoid M₂] →
                      [inst_18 : Module R M] →
                        [inst_19 : Module R M₂] →
                          [inst_20 : Module S M] →
                            [inst_21 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Submodule.mkQ (map (F := R →+* S) f p))) :
      (a : S) → S ⧸ map f p) ∘
    b')
Tactic: have b_eq_b' : ⇑b = (Submodule.mkQ (map (algebraMap R S) p)).restrictScalars R ∘ b' :=
    funext fun i => (Ideal.Quotient.mk_surjective (b i)).choose_spec.symm
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_2 : ∀ (b''_li : LinearIndependent K b''),
  finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
Tactic: have b''_li : LinearIndependent K b'' := ?_
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
refine_2 :
  ∀ (b''_li : LinearIndependent K b''),
    finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_1 : LinearIndependent K b''
Tactic: have b''_li : LinearIndependent K b'' := ?_
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
b''_li : LinearIndependent K b''
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_2 : ∀ (b''_sp : Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤),
  finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
Tactic: have b''_sp : Submodule.span K (Set.range b'') = ⊤ := ?_
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
b''_li : LinearIndependent K b''
refine_2 :
  ∀ (b''_sp : Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤),
    finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_2₁ : Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤
Tactic: have b''_sp : Submodule.span K (Set.range b'') = ⊤ := ?_
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
b''_li : LinearIndependent K b''
b''_sp : Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤
c : Basis ι K L := Basis.mk b''_li ⋯
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_2 : Fintype.card ι = finrank K L
Tactic: rw [finrank_eq_card_basis b, finrank_eq_card_basis c]
-- 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
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
b''_li : LinearIndependent K b''
b''_sp : Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤
c : Basis ι K L := Basis.mk b''_li ⋯
refine_2 : Fintype.card ι = finrank K L
⊢ finrank.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) = finrank K L
have refine_2₁ : Fintype.card ι = Fintype.card ι
Tactic: rw [finrank_eq_card_basis b, finrank_eq_card_basis c]