awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemisimpleModule R M
s : Set (Submodule R M)
hs : sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_1_iff_2 : Module.Finite R M ↔ IsNoetherian R M
tfae_2_to_5 :
  ∀ (a : IsNoetherian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_3_to_5 :
  ∀ (a : IsArtinian R M),
    ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m
tfae_5_to_4 :
  ∀ (a : ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m),
    IsNoetherian R M ∧ IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
tfae_4_to_3 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M,
      ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule.{u_1, u_2} R ↥m].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsSemisimpleModule R M
inst_6 : Module.Finite R M
⊢ IsArtinian R M

Tactic:
(IsSemisimpleModule.finite_tfae.out 0 2).mp ‹_›

Premises used: IsSemisimpleModule.finite_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsFiniteLength R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw :
  ∀ (H : IsNoetherian R N ∧ IsArtinian R N)
    (hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)), IsNoetherian R M ∧ IsArtinian R M
⊢ IsFiniteLength R M

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsNoetherian R N ∧ IsArtinian R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsNoetherian R N

Tactic:
cases H
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsNoetherian R N ∧ IsArtinian R N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R N
⊢ IsArtinian R N

Tactic:
cases H
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R N
right : IsArtinian R N
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
⟨isNoetherian_of_injective f hf, isArtinian_of_injective f hf⟩

Premises used: isNoetherian_of_injective, isArtinian_of_injective, And.intro
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R N
right : IsArtinian R N
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
exact ⟨isNoetherian_of_injective f hf, isArtinian_of_injective f hf⟩
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsFiniteLength R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw :
  ∀ (H : IsNoetherian R M ∧ IsArtinian R M)
    (hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)),
    IsNoetherian R N ∧ IsArtinian R N
⊢ IsFiniteLength R N

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsNoetherian R M ∧ IsArtinian R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ IsNoetherian R M

Tactic:
cases H
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
H : IsNoetherian R M ∧ IsArtinian R M
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R M
⊢ IsArtinian R M

Tactic:
cases H
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R M
right : IsArtinian R M
⊢ IsNoetherian R N ∧ IsArtinian R N

Tactic:
⟨isNoetherian_of_surjective f (LinearMap.range_eq_top.mpr hf),
    isArtinian_of_surjective _ f hf⟩

Premises used: Iff.mpr, isNoetherian_of_surjective, LinearMap.range_eq_top, And.intro, isArtinian_of_surjective
-- Module: Mathlib.RingTheory.FiniteLength
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
left : IsNoetherian R M
right : IsArtinian R M
⊢ IsNoetherian R N ∧ IsArtinian R N

Tactic:
exact ⟨isNoetherian_of_surjective f (LinearMap.range_eq_top.mpr hf),
    isArtinian_of_surjective _ f hf⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
    (hf :
      Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)),
    FiniteType R A
⊢ FiniteType R A

Tactic:
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)

Premises used: Algebra.FinitePresentation.out
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
apply :
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ FiniteType R A

Tactic:
apply FiniteType.iff_quotient_mvPolynomial''.2

Premises used: Iff.mpr, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)

Tactic:
⟨n, f, hf.1⟩

Premises used: And.left, Exists.intro
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)

Tactic:
exact ⟨n, f, hf.1⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
⊢ FiniteType R A ↔ FinitePresentation R A

Tactic:
⟨fun h => ?_, fun hfp => Algebra.FiniteType.of_finitePresentation⟩

Premises used: Algebra.FiniteType.of_finitePresentation, Iff.intro
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
refine : ∀ (h : FiniteType R A), FinitePresentation R A
⊢ FiniteType R A ↔ FinitePresentation R A

Tactic:
refine ⟨fun h => ?_, fun hfp => Algebra.FiniteType.of_finitePresentation⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
    (hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)),
    FinitePresentation R A
⊢ FinitePresentation R A

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h

Premises used: Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ FinitePresentation R A

Tactic:
⟨n, f, hf, ?_⟩

Premises used: Algebra.FinitePresentation.mk, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
refine : Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R A

Tactic:
refine ⟨n, f, hf, ?_⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
(inferInstance : IsNoetherianRing (MvPolynomial (Fin n) R)).noetherian
    (RingHom.ker f.toRingHom)

Premises used: IsNoetherian.noetherian, Submodule.FG, Ideal.FG, AlgHom.toRingHom, RingHom.ker
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
exact (inferInstance : IsNoetherianRing (MvPolynomial (Fin n) R)).noetherian
    (RingHom.ker f.toRingHom)

Premises used: IsNoetherian.noetherian, AlgHom.toRingHom, RingHom.ker
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
    (hf :
      Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)),
    FinitePresentation R B
⊢ FinitePresentation R B

Tactic:
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)

Premises used: Algebra.FinitePresentation.out
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h :
  Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
      (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B) ∧
    Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
⊢ FinitePresentation R B

Tactic:
use n, AlgHom.comp (↑e) f

Premises used: AlgHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h :
  Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B)
h₁ : Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
      (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B) ∧
    Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)

Tactic:
constructor
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h :
  Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (Function.comp.{w₁ + 1, w₂ + 1, w₃ + 1} (β := A) (⇑(↑e : A →ₐ[R] B) : (a : A) → B)
      (⇑f : (a : MvPolynomial (Fin n) R) → A))
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B)

Tactic:
rw [AlgHom.coe_comp]

Premises used: AlgHom.coe_comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (Function.comp.{w₁ + 1, w₂ + 1, w₃ + 1} (β := A) (⇑(↑e : A →ₐ[R] B) : (a : A) → B)
      (⇑f : (a : MvPolynomial (Fin n) R) → A))

Tactic:
Function.Surjective.comp e.surjective hf.1

Premises used: And.left, Function.Surjective.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (Function.comp.{w₁ + 1, w₂ + 1, w₃ + 1} (β := A) (⇑(↑e : A →ₐ[R] B) : (a : A) → B)
      (⇑f : (a : MvPolynomial (Fin n) R) → A))

Tactic:
exact Function.Surjective.comp e.surjective hf.1

Premises used: And.left, Function.Surjective.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
this :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
rw : Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
this :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
this :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
exact hf.2

Premises used: And.right
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)

Tactic:
suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom by
    rw [this]
    exact hf.2
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom

Tactic:
have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
⊢ (↑e.toRingEquiv : A →+* B) = (↑e : A →ₐ[R] B).toRingHom

Tactic:
have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
h1 : (↑e.toRingEquiv : A →+* B) = (↑e : A →ₐ[R] B).toRingHom
rw : (↑e : A →ₐ[R] B).comp f.toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
rw₁ rw₂ : (↑e : A →ₐ[R] B).comp f.toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom

Tactic:
rw [h, h1]
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom

Tactic:
have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
    f.toRingHom := by
    have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
    have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
    rw [h, h1]
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
h₁ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom) ⊥)
    (RingHom.ker f.toRingHom)
h₂ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (Ideal.comap (F := A →+* B) (↑e.toRingEquiv : A →+* B) ⊥)) (RingHom.ker f.toRingHom)
h₃ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (RingHom.ker (F := A →+* B) (↑e.toRingEquiv : A →+* B))) (RingHom.ker f.toRingHom)
h₄ : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap f.toRingHom ⊥) (RingHom.ker f.toRingHom)
h₅ h₆ : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap f.toRingHom ⊥) (Ideal.comap f.toRingHom ⊥)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)

Tactic:
rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_eq_comap_bot, AlgEquiv.toRingEquiv, RingHom.ker_coe_equiv, Ideal.comap_comap