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
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 : Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' Set.range b')) ⊤
⊢ Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤

Tactic:
rw [Set.range_comp]

Premises used: Set.range_comp
-- 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
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 :
  LE.le (α := Submodule R S) ⊤ (Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p))
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' Set.range b')) ⊤

Tactic:
refine FinrankQuotientMap.span_eq_top p hp.ne_top _ (top_le_iff.mp ?_)

Premises used: Ideal.FinrankQuotientMap.span_eq_top, top_le_iff, Iff.mp, Ideal.IsMaximal.ne_top
-- 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
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''
x : S
refine_2 :
  Membership.mem (γ := Submodule R S) ⊤ x →
    Membership.mem (γ := Submodule R S)
      (Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) x
⊢ Membership.mem (γ := Submodule R S) ⊤ x →
    Membership.mem (γ := Submodule R S)
      (Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) x

Tactic:
_
-- 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
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''
x : S
h : Membership.mem (γ := Submodule R S) ⊤ x
⊢ Membership.mem (α := HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p)) (γ :=
    Submodule.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
    (Submodule.span (R ⧸ p) (Set.range (ι := ι) (⇑b : (a : ι) → S ⧸ map f p)))
    ((Submodule.mkQ (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
      HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p))

Tactic:
have mem_span_b : ((Submodule.mkQ (map (algebraMap R S) p)) x : S ⧸ map (algebraMap R S) p) ∈
          Submodule.span (R ⧸ p) (Set.range b) := b.mem_span _
-- 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
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'
⊢ LinearIndependent.{v, u, v} (ι := ι) (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
    (⇑b : (a : ι) → S ⧸ map f p)

Tactic:
have := b.linearIndependent
-- 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
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'
this :
  LinearIndependent.{v, u, v} (ι := ι) (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
    (⇑b : (a : ι) → S ⧸ map f p)
⊢ LinearIndependent.{v, u, v} (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) 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:
rw [b_eq_b'] at this
-- 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
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'
this :
  LinearIndependent.{v, u, v} (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) 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')
refine_1 : p ≠ ⊤
⊢ Ne (α := Ideal R) (RingHom.ker (F := R →+* R ⧸ p) (algebraMap R (R ⧸ p))) ⊤

Tactic:
rw [Quotient.algebraMap_eq, Ideal.mk_ker]

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.mk_ker
-- 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
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'
this :
  LinearIndependent.{v, u, v} (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) 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')
⊢ p ≠ ⊤

Tactic:
hp.ne_top

Premises used: Ideal.IsMaximal.ne_top
-- 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
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'
this :
  LinearIndependent.{v, u, v} (R ⧸ p) (M := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) 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')
⊢ p ≠ ⊤

Tactic:
exact hp.ne_top

Premises used: Ideal.IsMaximal.ne_top
-- 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
P : Ideal S
x : R
⊢ Eq.{v + 1} (α := S ⧸ P ^ e)
    ((algebraMap (R ⧸ p) (S ⧸ P ^ e) : (a : R ⧸ p) → S ⧸ P ^ e) ((mk p : (a : R) → R ⧸ p) x) : S ⧸ P ^ e)
    ((mk (P ^ e) : (a : S) → S ⧸ P ^ e) ((f : (a : R) → S) x) : S ⧸ P ^ e)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl