awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
obtain :
  ∀ (i : ι) (j : ι'),
    (b.smulTower c : (a : ι × ι') → A) (i, j) =
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S) ((c : (a : ι') → A) (i, j).2 : A)
obtain₁ :
  ∀ (i : ι) (j : ι'),
    Eq (α := ι × ι' →₀ R)
      ((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
            ((c : (a : ι') → A) (i, j).2 : A)) :
        ι × ι' →₀ R)
      (single (i, j) 1 : ι × ι' →₀ R)
h :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((repr (b.smulTower c) : (a : A) → ι × ι' →₀ R)
                (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) (i, j).1 : S)
                  ((c : (a : ι') → A) (i, j).2 : A)) :
              ι × ι' →₀ R) :
            (a : ι × ι') → R)
          (i', j') :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₁ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) (i, j).1 : S)
                  (if (i, j).2 = (i', j').2 then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          (i', j').1 :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
h₂ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R)
                (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) (if j = j' then 1 else 0)) :
              ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
pos :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι') (hi : j = j'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 1) : ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
neg neg₁ :
  ∀ (i : ι) (j : ι') (i' : ι) (j' : ι') (hi : ¬j = j'),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) (β := S) ((b : (a : ι) → S) i : S) 0) : ι →₀ R) :
            (a : ι) → R)
          i' :
        R)
      ((single (i, j) 1 : (a : ι × ι') → R) (i', j') : R)
⊢ (b.smulTower c : (a : ι × ι') → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.1 : S) ((c : (a : ι') → A) ij.2 : A)

Tactic:
classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]

Premises used: Finsupp.smul_apply, Module.Basis.apply_eq_iff, Finsupp.single_apply, Module.Basis.smulTower_repr, Module.Basis.repr_self, map_smul
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
rw :
  Eq.{u_1 + 1} (α := R)
    (((b.repr : (a : S) → ι →₀ R)
            ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S)
              (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2) :
          (a : ι) → R)
        (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 :
      R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) ij.1) : ι →₀ R) :
          (a : ι) → R)
        ij.2 :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((((repr (b.smulTower' c) : (a : A) → ι' × ι →₀ R) x : ι' × ι →₀ R) : (a : ι' × ι) → R) ij : R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) ij.1) : ι →₀ R) :
          (a : ι) → R)
        ij.2 :
      R)

Tactic:
rw [smulTower', repr_reindex_apply, smulTower_repr]

Premises used: Module.Basis.smulTower', Module.Basis.smulTower_repr, Module.Basis.repr_reindex_apply
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ Eq.{u_1 + 1} (α := R)
    (((b.repr : (a : S) → ι →₀ R)
            ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S)
              (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2) :
          (a : ι) → R)
        (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 :
      R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) ij.1) : ι →₀ R) :
          (a : ι) → R)
        ij.2 :
      R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
i : ι'
j : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((((repr (b.smulTower' c) : (a : A) → ι' × ι →₀ R) x : ι' × ι →₀ R) : (a : ι' × ι) → R) (i, j) : R)
    ((((b.repr : (a : S) → ι →₀ R) ((((c.repr : (a : A) → ι' →₀ S) x : ι' →₀ S) : (a : ι') → S) i) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)

Tactic:
b.smulTower'_repr c x (i, j)

Premises used: Prod.mk, Module.Basis.smulTower'_repr
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
rw :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A)
      ((b : (a : ι) → S) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 : S)
      ((c : (a : ι') → A) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2 : A) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.2 : S) ((c : (a : ι') → A) ij.1 : A)
⊢ (b.smulTower' c : (a : ι' × ι) → A) ij =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.2 : S) ((c : (a : ι') → A) ij.1 : A)

Tactic:
rw [smulTower', reindex_apply, smulTower_apply]

Premises used: Module.Basis.smulTower', Module.Basis.smulTower_apply, Module.Basis.reindex_apply
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid A
inst_3 : Module R S
inst_4 : Module S A
inst_5 : Module R A
inst_6 : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A)
      ((b : (a : ι) → S) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).1 : S)
      ((c : (a : ι') → A) (((Equiv.prodComm ι ι').symm : (a : ι' × ι) → ι × ι') ij).2 : A) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := A) ((b : (a : ι) → S) ij.2 : S) ((c : (a : ι') → A) ij.1 : A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : Algebra R S
ι : Type u_5
b : Basis ι R S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
have : IsTorsionFree R S := b.isTorsionFree
  FaithfulSMul.algebraMap_injective R S

Premises used: Module.Basis.isTorsionFree, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 f : C →ₐ[A] D
dsimp : AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f
⊢ (fun (fg : (f : B →ₐ[A] D) × (C →ₐ[B] D)) ↦
        let x := fg.fst (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D).toAlgebra;
        (AlgHom.restrictScalars A (fg.snd (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D)) : C →ₐ[A] D))
      ((fun (f : C →ₐ[A] D) ↦
          (Sigma.mk (β := fun (f : B →ₐ[A] D) ↦ C →ₐ[B] D) (AlgHom.restrictDomain B f) (AlgHom.extendScalars B f) :
            (f : B →ₐ[A] D) × (C →ₐ[B] D)))
        f) =
    f

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 f : C →ₐ[A] D
H :
  ∀ (x : C),
    Eq.{u_6 + 1} (α := D) ((AlgHom.restrictScalars A (AlgHom.extendScalars B f) : (a : C) → D) x : D)
      ((f : (a : C) → D) x : D)
⊢ AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f

Tactic:
ext
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 f : C →ₐ[A] D
x : C
⊢ Eq.{u_6 + 1} (α := D) ((AlgHom.restrictScalars A (AlgHom.extendScalars B f) : (a : C) → D) x : D)
    ((f : (a : C) → D) x : D)

Tactic:
rfl
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 : C →ₐ[A] D
f : B → D
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one' : OneHom B D }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom B D }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom B D }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun 0 = 0
map_add' :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
g : C → D
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun 0 = 0
map_add'_1 :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun y
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
h : ∀ (x : B), f x = g ((algebraMap B C : (a : B) → C) x)
⊢ f = fun (x : B) ↦ g ((algebraMap B C : (a : B) → C) x)

Tactic:
ext x
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 : C →ₐ[A] D
f : B → D
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one' : OneHom B D }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom B D }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom B D }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun 0 = 0
map_add' :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
g : C → D
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun 0 = 0
map_add'_1 :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun y
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
x : B
⊢ f x = g ((algebraMap B C : (a : B) → C) x)

Tactic:
(hg x).symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.AlgebraTower
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring A
inst_1 : CommSemiring C
inst_2 : CommSemiring D
inst_3 : Algebra A C
inst_4 : Algebra A D
inst_5 : CommSemiring B
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : IsScalarTower A B C
f_1 : C →ₐ[A] D
f : B → D
map_one' : f 1 = 1
map_mul' :
  ∀ (x y : B),
    { toFun := f, map_one' := map_one' : OneHom B D }.toFun (x * y) =
      { toFun := f, map_one' := map_one' : OneHom B D }.toFun x *
        { toFun := f, map_one' := map_one' : OneHom B D }.toFun y
map_zero' : (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun 0 = 0
map_add' :
  ∀ (x y : B),
    (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun (x + y) =
      (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun x +
        (↑{ toFun := f, map_one' := map_one', map_mul' := map_mul' : B →* D } : OneHom B D).toFun y
commutes' :
  ∀ (r : A),
    (↑(↑{ toFun := f, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    B →+* D } :
                B →* D) :
            OneHom B D).toFun
        ((algebraMap A B : (a : A) → B) r) =
      (algebraMap A D : (a : A) → D) r
g : C → D
map_one'_1 : g 1 = 1
map_mul'_1 :
  ∀ (x y : C),
    { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun (x * y) =
      { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun x *
        { toFun := g, map_one' := map_one'_1 : OneHom C D }.toFun y
map_zero'_1 : (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun 0 = 0
map_add'_1 :
  ∀ (x y : C),
    (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun (x + y) =
      (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun x +
        (↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1 : C →* D } : OneHom C D).toFun y
hg :
  ∀ (r : B),
    (↑(↑{ toFun := g, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 :
                    C →+* D } :
                C →* D) :
            OneHom C D).toFun
        ((algebraMap B C : (a : B) → C) r) =
      (algebraMap B D : (a : B) → D) r
x : B
⊢ f x = g ((algebraMap B C : (a : B) → C) x)

Tactic:
exact (hg x).symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Subsingleton R
x : A
⊢ Transcendental R x

Tactic:
fun ⟨p, h, _⟩ => h <| Subsingleton.elim p 0

Premises used: False, Transcendental, Subsingleton.elim, OfNat.ofNat, Not, _private.0.is_transcendental_of_subsingleton.match_1
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : IsAlgebraic R a
contrapose! : ∀ (h : Subsingleton R), ¬IsAlgebraic R a
⊢ Nontrivial R

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a : A
h : Subsingleton R
⊢ ¬IsAlgebraic R a

Tactic:
apply is_transcendental_of_subsingleton

Premises used: is_transcendental_of_subsingleton
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
alg : Algebra.IsAlgebraic R A
⊢ Nontrivial R

Tactic:
(alg.1 0).nontrivial

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.nontrivial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Subsingleton R
⊢ Algebra.Transcendental R A

Tactic:
⟨⟨0, is_transcendental_of_subsingleton R 0⟩⟩

Premises used: Algebra.Transcendental.mk, is_transcendental_of_subsingleton, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
inst : CommRing R
⊢ Transcendental R (A := R[X]) X

Tactic:
simp [transcendental_iff]

Premises used: transcendental_iff
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
H : IsAlgebraic.{u, v} R (A := A) ((aeval r : (a : R[X]) → A) f : A)
obtain :
  ∀ (p : R[X]) (h1 : p ≠ 0)
    (h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)),
    IsAlgebraic R r
⊢ IsAlgebraic R r

Tactic:
obtain ⟨p, h1, h2⟩ := H
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
h : (p.comp f).coeff (p.natDegree * f.natDegree) = 0
rwa : ∀ (h : p.leadingCoeff * f.leadingCoeff ^ p.natDegree = 0), p = 0
rwa₁ : ∀ (h : p.leadingCoeff = 0), p = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : p = 0), p = 0
⊢ p = 0

Tactic:
rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, pow_mem, Polynomial.coeff_comp_degree_mul_degree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0

Tactic:
have : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0 := fun h ↦ h1 <| by
    rwa [coeff_comp_degree_mul_degree hf,
      mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hf' _),
      leadingCoeff_eq_zero] at h
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
h : p.comp f = 0
⊢ (p.comp f).coeff (p.natDegree * f.natDegree) = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
rwa rwa₁ rwa₂ rwa₃ :
  Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{v + 1} (α := A) ((aeval r : (a : R[X]) → A) (p.comp f) : A) (0 : A)

Tactic:
rwa [aeval_comp]

Premises used: Polynomial.aeval_comp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
p : R[X]
h1 : p ≠ 0
h2 : Eq.{v + 1} (α := A) (((aeval ((aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A)
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
⊢ IsAlgebraic R r

Tactic:
exact ⟨p.comp f, fun h ↦ this (by simp [h]), by rwa [aeval_comp]⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
H : Transcendental R r
f : R[X]
hf : f.natDegree ≠ 0
hf' : Membership.mem (γ := Submonoid R) R⁰ f.leadingCoeff
⊢ Transcendental.{u, v} R (A := A) ((Polynomial.aeval r : (a : R[X]) → A) f : A)

Tactic:
fun h ↦ H (h.of_aeval f hf hf')

Premises used: IsAlgebraic.of_aeval, Transcendental, Not
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
r : A
H : Transcendental R r
f : R[X]
hf : Transcendental R f
rw :
  ∀ (H : ∀ (p : R[X]), Eq.{v + 1} (α := A) ((Polynomial.aeval r : (a : R[X]) → A) p : A) (0 : A) → p = 0) {f : R[X]}
    (hf : ∀ (p : R[X]), Eq (α := R[X]) ((Polynomial.aeval f : (a : R[X]) → R[X]) p : R[X]) (0 : R[X]) → p = 0)
    (p : R[X]),
    Eq.{v + 1} (α := A)
        (((Polynomial.aeval ((Polynomial.aeval r : (a : R[X]) → A) f) : R[X] →ₐ[R] A) : (a : R[X]) → A) p : A) (0 : A) →
      p = 0
⊢ Transcendental.{u, v} R (A := A) ((Polynomial.aeval r : (a : R[X]) → A) f : A)

Tactic:
rw [transcendental_iff] at H hf ⊢

Premises used: transcendental_iff