awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower A B M
h : ¬IsFiniteLength B M
this : ¬IsFiniteLength A M
h₁ : length B M = ⊤
⊢ length A M = ⊤

Tactic:
rw [← length_ne_top_iff, not_ne_iff] at h this

Premises used: not_ne_iff, Module.length_ne_top_iff
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
⊢ length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using Module.length_pos

Premises used: Module.length_pos, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
⊢ length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0

Tactic:
have ne : length (ResidueField A) (ResidueField B) ≠ 0 := by
      simpa [pos_iff_ne_zero] using Module.length_pos
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Module B M
inst_9 : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
ne : length.{u_1, u_2} (ResidueField A) (ResidueField B) ≠ 0
neg : length A M = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
neg₁ : ⊤ = ⊤ * length.{u_1, u_2} (ResidueField A) (ResidueField B)
neg₂ neg₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ length A M = length B M * length.{u_1, u_2} (ResidueField A) (ResidueField B)

Tactic:
rw [h, this, ENat.top_mul ne]

Premises used: ENat.top_mul
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
pos :
  ∀ (h : IsFiniteLength A M),
    length B (B ⊗[A] M) =
      length A M *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
neg :
  ∀ (h : ¬IsFiniteLength A M),
    length B (B ⊗[A] M) =
      length A M *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
by_cases h : IsFiniteLength A M

Premises used: IsFiniteLength
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
pos :
  ∀ (s : CompositionSeries (Submodule A M))
    (hs_bot :
      RelSeries.head (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊥)
    (hs_top :
      RelSeries.last (r :=
          {x : Submodule A M × Submodule A M |
            match (motive := Submodule A M × Submodule A M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
          s =
        ⊤),
    length B (B ⊗[A] M) =
      length A M *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h

Premises used: isFiniteLength_iff_exists_compositionSeries, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
pos :
  length B (B ⊗[A] M) =
    (↑(s.length (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
        ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
rw [← length_compositionSeries s hs_bot hs_top]

Premises used: Module.length_compositionSeries
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
pos :
  ∀
    (k :
      Fin
        (s.length (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}) +
          1)),
    length B
        ↥(Submodule.baseChange B
            (s.toFun (r :=
              {x : Submodule A M × Submodule A M |
                match (motive := Submodule A M × Submodule A M → Prop) x with
                | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
              k)) =
      (↑(↑k : ℕ) : ℕ∞) *
        length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B (B ⊗[A] M) =
    (↑(s.length (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
        ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
suffices ∀ k, length B ((s k).baseChange B) =
        k * length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top, baseChange_top, length_top]
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
pos :
  length B ↥⊥ =
    (↑(↑0 : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            0)) =
    (↑(↑0 : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
rw [← RelSeries.head, hs_bot, baseChange_bot]

Premises used: Submodule.baseChange_bot, RelSeries.head
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ length B ↥⊥ =
    (↑(↑0 : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength A M
s : CompositionSeries (Submodule A M)
hs_bot :
  RelSeries.head (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs_top :
  RelSeries.last (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
i :
  Fin
    (s.length (r :=
      {x : Submodule A M × Submodule A M |
        match (motive := Submodule A M × Submodule A M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y}))
hi :
  length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            i.castSucc)) =
    (↑(↑i.castSucc : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
⊢ length B
      ↥(Submodule.baseChange B
          (s.toFun (r :=
            {x : Submodule A M × Submodule A M |
              match (motive := Submodule A M × Submodule A M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
            i.succ)) =
    (↑(↑i.succ : ℕ) : ℕ∞) *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
simpa [hi, add_one_mul] using (s.step i).length_baseChange B

Premises used: CovBy.length_baseChange, add_one_mul, RelSeries.step
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
contrapose! : ∀ (h : IsFiniteLength B (B ⊗[A] M)), IsFiniteLength A M
⊢ ¬IsFiniteLength B (B ⊗[A] M)

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsFiniteLength B (B ⊗[A] M)
rw : ∀ (h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)), IsNoetherian A M ∧ IsArtinian A M
⊢ IsFiniteLength A M

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)
⊢ FaithfullyFlat A B

Tactic:
have : FaithfullyFlat A B := FaithfullyFlat.of_flat_of_isLocalHom
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)
this : FaithfullyFlat A B
⊢ IsNoetherian A M ∧ IsArtinian A M

Tactic:
h.imp IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
        IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat

Premises used: And.imp, Submodule.IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat, Submodule.IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : IsNoetherian B (B ⊗[A] M) ∧ IsArtinian B (B ⊗[A] M)
this : FaithfullyFlat A B
⊢ IsNoetherian A M ∧ IsArtinian A M

Tactic:
exact h.imp IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
        IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat

Premises used: And.imp, Submodule.IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat, Submodule.IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
⊢ ¬IsFiniteLength B (B ⊗[A] M)

Tactic:
have : ¬ IsFiniteLength B (B ⊗[A] M) := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      have : FaithfullyFlat A B := FaithfullyFlat.of_flat_of_isLocalHom
      exact h.imp IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
        IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
this : ¬IsFiniteLength B (B ⊗[A] M)
⊢ length A M = ⊤

Tactic:
rw [← length_ne_top_iff, not_ne_iff] at h this

Premises used: not_ne_iff, Module.length_ne_top_iff
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : ¬IsFiniteLength A M
this : ¬IsFiniteLength B (B ⊗[A] M)
h₁ : length A M = ⊤
⊢ length B (B ⊗[A] M) = ⊤

Tactic:
rw [← length_ne_top_iff, not_ne_iff] at h this

Premises used: not_ne_iff, Module.length_ne_top_iff
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0

Tactic:
simpa [← pos_iff_ne_zero, length_pos_iff] using (map_maximalIdeal_lt_top (algebraMap A B)).ne

Premises used: Algebra.algebraMap, Module.length_pos_iff, pos_iff_ne_zero, IsLocalRing.map_maximalIdeal_lt_top, LT.lt.ne
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0

Tactic:
have ne : length B (B ⧸ (maximalIdeal A).map (algebraMap A B)) ≠ 0 := by
      simpa [← pos_iff_ne_zero, length_pos_iff] using (map_maximalIdeal_lt_top (algebraMap A B)).ne
-- Module: Mathlib.RingTheory.LocalRing.Length
Goal:
A : Type u_1
B : Type u_2
M : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsLocalRing A
inst_3 : IsLocalRing B
inst_4 : Algebra A B
inst_5 : IsLocalHom (R := A) (S := B) (F := A →+* B) (algebraMap A B)
inst_6 : AddCommGroup M
inst_7 : Module A M
inst_8 : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
ne : length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A))) ≠ 0
neg :
  length B (B ⊗[A] M) =
    ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
neg₁ :
  ⊤ = ⊤ * length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))
neg₂ neg₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ length B (B ⊗[A] M) =
    length A M *
      length B (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (maximalIdeal A)))

Tactic:
rw [h, this, ENat.top_mul ne]

Premises used: ENat.top_mul
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : Nontrivial S
f : R →+* S
s : Subring R
inst_4 : IsLocalRing.{u_1} ↥s
⊢ IsLocalRing.{u_2} ↥(Subring.map f s)

Tactic:
.of_surjective' (f.restrict s _ (fun _ ↦ Set.mem_image_of_mem f))
    (fun ⟨_, a, ha, e⟩ ↦ ⟨⟨a, ha⟩, Subtype.ext e⟩)

Premises used: Subring.map, Exists, Subtype.mk, RingHom.restrict, _private.0.instIsLocalRingSubtypeMemSubringMapOfNontrivial.match_1, Set.mem_image_of_mem, Exists.intro, IsLocalRing.of_surjective', Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : IsLocalRing R
⊢ IsLocalRing.{u_1} ↥⊤

Tactic:
Subring.topEquiv.symm.isLocalRing

Premises used: RingEquiv.isLocalRing
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
inst : CommRing R
a : Subring R
isLocalRing : IsLocalRing.{u_1} ↥a
isLocalRing_1 : IsLocalRing.{u_1} ↥{ toSubring := a, isLocalRing := isLocalRing : LocalSubring R }.toSubring
⊢ { toSubring := a, isLocalRing := isLocalRing : LocalSubring R } =
    { toSubring := { toSubring := a, isLocalRing := isLocalRing }.toSubring, isLocalRing := isLocalRing_1 }

Tactic:
rfl
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : IsLocalRing R
inst_4 : Nontrivial S
f : R →+* S
h :
  ∀ (x : S),
    x ∈ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) ↔
      x ∈ (↑(map f { toSubring := ⊤, isLocalRing := ⋯ : LocalSubring R }).toSubring : Set S)
⊢ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) =
    (↑(map f { toSubring := ⊤, isLocalRing := ⋯ : LocalSubring R }).toSubring : Set S)

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : IsLocalRing R
inst_4 : Nontrivial S
f : R →+* S
x : S
⊢ x ∈ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) ↔
    x ∈ (↑(map f { toSubring := ⊤, isLocalRing := ⋯ : LocalSubring R }).toSubring : Set S)

Tactic:
congr(x ∈ $(Set.image_univ.symm))

Premises used: Set.image_univ, congrArg, Membership.mem, id, Eq.symm, iff_of_eq
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
inst_3 : IsLocalRing R
inst_4 : Nontrivial S
f : R →+* S
x : S
⊢ x ∈ (↑(RingHom.range.{u_1, u_2} (R := R) f) : Set S) ↔
    x ∈ (↑(map f { toSubring := ⊤, isLocalRing := ⋯ : LocalSubring R }).toSubring : Set S)

Tactic:
exact congr(x ∈ $(Set.image_univ.symm))

Premises used: Set.image_univ, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
inst : CommRing R
A B : LocalSubring R
⊢ A ≤ B ↔ ∃ (h : A.toSubring ≤ B.toSubring), IsLocalHom (R := ↥A.toSubring) (S := ↥B.toSubring) (Subring.inclusion h)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.LocalRing.LocalSubring
Goal:
R : Type u_1
inst : CommRing R
⊢ Monotone.{u_1, u_1} (α := LocalSubring R) toSubring

Tactic:
fun _ _ e ↦ e.1

Premises used: Monotone