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
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''
⊢ Eq (α := Submodule K L) (Submodule.span K (Set.range b'')) ⊤
have refine_2 : Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' Set.range b')) ⊤
Tactic: rw [Set.range_comp]
-- 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''
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' Set.range b')) ⊤
have refine_2 : LE.le (α := Submodule R S) ⊤ (Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p))
Tactic: refine FinrankQuotientMap.span_eq_top p hp.ne_top _ (top_le_iff.mp ?_)
-- 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)))
      ⋯
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 (γ := Submodule R S)
    (Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) x
have mem_span_b : 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 _
-- 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)))
      ⋯
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 K b''
have 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)
Tactic: have := b.linearIndependent
-- 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)))
      ⋯
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 K b''
have 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')
Tactic: rw [b_eq_b'] at this
Cleared hypotheses: this
-- 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'
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')
⊢ LinearIndependent K b''
have refine_1 : Ne (α := Ideal R) (RingHom.ker (F := R →+* R ⧸ p) (algebraMap R (R ⧸ p))) ⊤
Tactic: convert!
      FinrankQuotientMap.linearIndependent_of_nontrivial K _
        ((Algebra.linearMap S L).restrictScalars R) _ ((Submodule.mkQ _).restrictScalars R) this
-- 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'
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')
⊢ Ne (α := Ideal R) (RingHom.ker (F := R →+* R ⧸ p) (algebraMap R (R ⧸ p))) ⊤
have refine_1 : p ≠ ⊤
Tactic: rw [Quotient.algebraMap_eq, Ideal.mk_ker]
-- 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
P : Ideal S
i : ℕ
⊢ Function.Injective (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))) (β :=
    ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (⇑(p.powQuotSuccInclusion P i) :
      (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
have rw : ∀ (m : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))),
  Eq (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      ((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          m :
        ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (0 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))) →
    m = 0
Tactic: rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
-- 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
P : Ideal S
i : ℕ
x : S ⧸ P ^ e
hx : Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x
hx0 :
  Eq (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    ((p.powQuotSuccInclusion P i :
          (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
        (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x) x
          hx) :
      ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (0 : ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
⊢ Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
      Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x) x hx =
    0
have rw : ∀
  (hx0 :
    Eq.{v + 1} (α := S ⧸ P ^ e)
      (↑((p.powQuotSuccInclusion P i :
              (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
            (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
              Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1)))
                x)
              x hx)) :
        S ⧸ P ^ e)
      (↑0 : S ⧸ P ^ e)),
  (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x) x
          hx) :
      S ⧸ P ^ e) =
    (↑0 : S ⧸ P ^ e)
Tactic: rw [Subtype.ext_iff] at hx0 ⊢
Cleared hypotheses: hx0
-- 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
P : Ideal S
i : ℕ
x : S ⧸ P ^ e
hx : Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x
hx0 :
  Eq.{v + 1} (α := S ⧸ P ^ e)
    (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            x hx)) :
      S ⧸ P ^ e)
    (↑0 : S ⧸ P ^ e)
⊢ (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x) x
          hx) :
      S ⧸ P ^ e) =
    (↑0 : S ⧸ P ^ e)
have rwa : ∀
  (hx0 :
    (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x)
            x hx) :
        S ⧸ P ^ e) =
      (↑0 : S ⧸ P ^ e)),
  (↑(Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
          Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ (i + 1))) x) x
          hx) :
      S ⧸ P ^ e) =
    (↑0 : S ⧸ P ^ e)
Tactic: rwa [powQuotSuccInclusion_apply_coe] at hx0
Cleared hypotheses: hx0