awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
h : Submodule.FG.{u, v} (R := R) (M := A) ⊤
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
⊢ (↑s : Set A) ⊆
    (↑((toSubmodule : (a : Subalgebra R A) → Submodule R A) (Algebra.adjoin R (↑s : Set A)) : Submodule R A) : Set A)

Tactic:
exact Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
obtain : ∀ (s : Set A) (hs : s.Finite ∧ Algebra.adjoin R s = S), (S.prod T).FG
⊢ (S.prod T).FG

Tactic:
obtain ⟨s, hs⟩ := fg_def.1 hS

Premises used: Subalgebra.fg_def, Iff.mp
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
obtain : ∀ (t : Set B) (ht : t.Finite ∧ Algebra.adjoin R t = T), (S.prod T).FG
⊢ (S.prod T).FG

Tactic:
obtain ⟨t, ht⟩ := fg_def.1 hT

Premises used: Subalgebra.fg_def, Iff.mp
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
rw : FG (Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t))
⊢ (S.prod T).FG

Tactic:
rw [← hs.2, ← ht.2]

Premises used: And.right
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ FG (Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t))

Tactic:
fg_def.2 ⟨LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}),
    Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
      (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
    Algebra.adjoin_inl_union_inr_eq_prod R s t⟩

Premises used: Iff.mpr, Set.Finite.union, LinearMap.inl, Subalgebra.fg_def, Set.Finite.image, Algebra.adjoin_inl_union_inr_eq_prod, And.left, And.intro, Exists.intro, Set.image, Union.union, Singleton.singleton, OfNat.ofNat, LinearMap.inr, DFunLike.coe, Set.finite_singleton
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ FG (Subalgebra.prod (Algebra.adjoin R s) (Algebra.adjoin R t))

Tactic:
exact fg_def.2 ⟨LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}),
    Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
      (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
    Algebra.adjoin_inl_union_inr_eq_prod R s t⟩

Premises used: Iff.mpr, Set.Finite.union, LinearMap.inl, Subalgebra.fg_def, Set.Finite.image, Algebra.adjoin_inl_union_inr_eq_prod, And.left, And.intro, Exists.intro, Set.image, Union.union, Singleton.singleton, OfNat.ofNat, LinearMap.inr, DFunLike.coe, Set.finite_singleton
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs : S.FG
let : ∀ (s : Finset A) (hs : Algebra.adjoin R (↑s : Set A) = S), (Subalgebra.map f S).FG
⊢ (Subalgebra.map f S).FG

Tactic:
let ⟨s, hs⟩ := hs
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
rw : Algebra.adjoin R ((⇑f : (a : A) → B) '' (↑s : Set A)) = Subalgebra.map f S
rw₁ : Subalgebra.map f (Algebra.adjoin R (↑s : Set A)) = Subalgebra.map f S
rw₂ rw₃ : Subalgebra.map f S = Subalgebra.map f S
⊢ Algebra.adjoin R (↑(Finset.image (⇑f : (a : A) → B) s) : Set B) = Subalgebra.map f S

Tactic:
rw [Finset.coe_image, Algebra.adjoin_image, hs]

Premises used: Finset.coe_image, Algebra.adjoin_image
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
⊢ (Subalgebra.map f S).FG

Tactic:
exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs_1 : S.FG
s : Finset A
hs : Algebra.adjoin R (↑s : Set A) = S
⊢ (Subalgebra.map f S).FG

Tactic:
classical
  exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
rw : (↑s : Set B) ⊆ Set.range.{w, v + 1} (ι := A) (⇑f : (a : A) → B)
⊢ map f (Algebra.adjoin R (↑(s.preimage (⇑f : (a : A) → B) ⋯) : Set A)) = map f S

Tactic:
rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]

Premises used: Finset.coe_preimage, Algebra.adjoin_image, Set.image_preimage_eq_of_subset
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
rw : map f S ≤ map f ⊤
⊢ (↑s : Set B) ⊆ Set.range.{w, v + 1} (ι := A) (⇑f : (a : A) → B)

Tactic:
rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]

Premises used: AlgHom.coe_range, Algebra.adjoin_le_iff, Algebra.map_top
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
⊢ map f S ≤ map f ⊤

Tactic:
map_mono le_top

Premises used: Subalgebra.map_mono, le_top
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hs_1 : (map f S).FG
s : Finset B
hs : Algebra.adjoin R (↑s : Set B) = map f S
⊢ map f S ≤ map f ⊤

Tactic:
exact map_mono le_top

Premises used: Subalgebra.map_mono, le_top
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : FG.{u, v} (R := R) (A := ↥S) ⊤
rw : (map S.val ⊤).FG
⊢ S.FG

Tactic:
rw [← S.range_val, ← Algebra.map_top]

Premises used: Subalgebra.range_val, Algebra.map_top
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : FG.{u, v} (R := R) (A := ↥S) ⊤
⊢ (map S.val ⊤).FG

Tactic:
FG.map _ h

Premises used: Subalgebra.FG.map
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : FG.{u, v} (R := R) (A := ↥S) ⊤
⊢ (map S.val ⊤).FG

Tactic:
exact FG.map _ h

Premises used: Subalgebra.FG.map
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h rw : S.FG
⊢ (map S.val ⊤).FG

Tactic:
rw [Algebra.map_top, range_val]

Premises used: Subalgebra.range_val, Algebra.map_top
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.FG

Tactic:
h
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
h : S.FG
⊢ S.FG

Tactic:
exact h
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
⊢ P S

Tactic:
obtain ⟨t, rfl⟩ := S.fg_of_noetherian

Premises used: Subalgebra.fg_of_noetherian, rfl
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t : Finset A
⊢ P (Algebra.adjoin R (↑t : Set A))

Tactic:
Finset.induction_on t ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t : Finset A
refine_1 : P (Algebra.adjoin R (↑∅ : Set A))
refine_2 :
  ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R (↑s : Set A)) → P (Algebra.adjoin R (↑(insert a s) : Set A))
⊢ P (Algebra.adjoin R (↑t : Set A))

Tactic:
refine Finset.induction_on t ?_ ?_
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t : Finset A
⊢ P (Algebra.adjoin R (↑∅ : Set A))

Tactic:
simpa using base
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t_1 : Finset A
x : A
t : Finset A
refine_2 : x ∉ t → P (Algebra.adjoin R (↑t : Set A)) → P (Algebra.adjoin R (↑(insert x t) : Set A))
⊢ x ∉ t → P (Algebra.adjoin R (↑t : Set A)) → P (Algebra.adjoin R (↑(insert x t) : Set A))

Tactic:
_
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t_1 : Finset A
x : A
t : Finset A
h_1 : x ∉ t
h : P (Algebra.adjoin R (↑t : Set A))
refine_2 : P (Algebra.adjoin R (insert x (↑t : Set A)))
⊢ P (Algebra.adjoin R (↑(insert x t) : Set A))

Tactic:
rw [Finset.coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
t_1 : Finset A
x : A
t : Finset A
h_1 : x ∉ t
h : P (Algebra.adjoin R (↑t : Set A))
⊢ P (Algebra.adjoin R (insert x (↑t : Set A)))

Tactic:
simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h

Premises used: Algebra.adjoin_insert_adjoin
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x (↑S : Set A)))
S : Subalgebra R A
obtain : ∀ (t : Finset A), P (Algebra.adjoin R (↑t : Set A))
refine_1 : ∀ (t : Finset A), P (Algebra.adjoin R (↑∅ : Set A))
refine_2 refine_2₁ refine_2₂ :
  ∀ (t : Finset A) (x : A) (t : Finset A),
    x ∉ t → ∀ (h : P (Algebra.adjoin R (↑t : Set A))), P (Algebra.adjoin R (↑(insert x t) : Set A))
refine_2₃ :
  ∀ (t : Finset A) (x : A) (t : Finset A),
    x ∉ t → ∀ (h : P (Algebra.adjoin R (↑t : Set A))), P (Algebra.adjoin R (insert x (↑t : Set A)))
⊢ P S

Tactic:
classical
  obtain ⟨t, rfl⟩ := S.fg_of_noetherian
  refine Finset.induction_on t ?_ ?_
  · simpa using base
  intro x t _ h
  rw [Finset.coe_insert]
  simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h

Premises used: Subalgebra.fg_of_noetherian, Algebra.adjoin_insert_adjoin, Finset.coe_insert, rfl
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
rw : Algebra.adjoin R s ⊔ Algebra.adjoin R s' = S ⊔ S'
rw₁ : S ⊔ Algebra.adjoin R s' = S ⊔ S'
rw₂ rw₃ : S ⊔ S' = S ⊔ S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'

Tactic:
rw [Algebra.adjoin_union, hs.2, hs'.2]

Premises used: Algebra.adjoin_union, And.right
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
inst_5 : IsNoetherianRing A
⊢ IsNoetherianRing.{w} ↥f.range

Tactic:
_root_.isNoetherianRing_range f.toRingHom

Premises used: Set.Mem, isNoetherianRing_range, Subring.copy, AlgHom.toRingHom, RingHom.range, Subsemiring.copy, RingHom.rangeS
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
HS : S.FG
inst_3 : IsNoetherianRing R
⊢ IsNoetherianRing.{v} ↥S

Tactic:
let ⟨t, ht⟩ := HS
  ht ▸ (Algebra.adjoin_eq_range R (↑t : Set A)).symm ▸ AlgHom.isNoetherianRing_range _

Premises used: MvPolynomial.aeval, Membership.mem, Eq.rec, Subtype, IsNoetherianRing, _private.0.isNoetherianRing_of_fg.match_1, SetLike.coe, Algebra.adjoin_eq_range, AlgHom.isNoetherianRing_range, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
inst : CommRing R
s : Set R
hs : s.Finite
⊢ IsNoetherianRing.{u} ↥(Subring.closure s)

Tactic:
show IsNoetherianRing (subalgebraOfSubring (Subring.closure s)) from
    Algebra.adjoin_int s ▸ isNoetherianRing_of_fg (Subalgebra.fg_def.2 ⟨s, hs, rfl⟩)

Premises used: Iff.mpr, Set.Mem, setOf, Eq.rec, Subalgebra.fg_def, Subring.mk', And.intro, Exists.intro, isNoetherianRing_of_fg, Algebra.adjoin_int, rfl, Subring.closure
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
obtain :
  ∀ (S : Finset (A × B)) (hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2),
    ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x

Tactic:
obtain ⟨S, hS⟩ := TensorProduct.exists_finset x

Premises used: TensorProduct.exists_finset
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x

Tactic:
⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩

Premises used: Algebra.adjoin, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
refine_2 :
  Membership.mem (γ := Subalgebra A (A ⊗[R] B))
    (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x

Tactic:
refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))

Tactic:
Subalgebra.fg_adjoin_finset _

Premises used: Subalgebra.fg_adjoin_finset
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))

Tactic:
exact Subalgebra.fg_adjoin_finset _

Premises used: Subalgebra.fg_adjoin_finset
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Membership.mem (γ := Subalgebra A (A ⊗[R] B))
    (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x

Tactic:
hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)

Premises used: Algebra.subset_adjoin, Eq.rec, Subalgebra.sum_mem, Prod.fst, Subalgebra.tmul_mem_baseChange, Finset.mem_image_of_mem, Eq.symm, Prod.snd
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Membership.mem (γ := Subalgebra A (A ⊗[R] B))
    (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x

Tactic:
exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)
-- Module: Mathlib.RingTheory.Adjoin.FGBaseChange
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
refine_1 : Subalgebra.FG (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))
refine_2 refine_2₁ :
  Membership.mem (γ := Subalgebra A (A ⊗[R] B))
    (Subalgebra.baseChange A (Algebra.adjoin R (↑(Finset.image (fun (j : A × B) ↦ j.2) S) : Set B))) x
⊢ ∃ (C : Subalgebra R B), C.FG ∧ Membership.mem (γ := Subalgebra A (A ⊗[R] B)) (Subalgebra.baseChange A C) x

Tactic:
classical
  refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
  · exact Subalgebra.fg_adjoin_finset _
  · exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)

Premises used: Subalgebra.fg_adjoin_finset
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F x)) (β := ↥F[x])
    (⇑(Minpoly.toAdjoin F x) : (a : AdjoinRoot (minpoly F x)) → ↥F[x])

Tactic:
⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩

Premises used: Iff.mpr, AdjoinRoot.Minpoly.toAdjoin.surjective, injective_iff_map_eq_zero, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
refine :
  ∀ (P₁ : AdjoinRoot (minpoly F x))
    (hP₁ :
      Eq.{u_2 + 1} (α := ↥F[x])
        (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
              (a : AdjoinRoot (minpoly F x)) → ↥F[x])
            P₁ :
          ↥F[x])
        (0 : ↥F[x])),
    P₁ = 0
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly F x)) (β := ↥F[x])
    (⇑(Minpoly.toAdjoin F x) : (a : AdjoinRoot (minpoly F x)) → ↥F[x])

Tactic:
refine ⟨(injective_iff_map_eq_zero _).2 fun P₁ hP₁ ↦ ?_, Minpoly.toAdjoin.surjective F x⟩
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P₁ : AdjoinRoot (minpoly F x)
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        P₁ :
      ↥F[x])
    (0 : ↥F[x])
obtain :
  ∀ (P : F[X])
    (hP₁ :
      Eq.{u_2 + 1} (α := ↥F[x])
        (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
              (a : AdjoinRoot (minpoly F x)) → ↥F[x])
            ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
          ↥F[x])
        (0 : ↥F[x])),
    Eq (α := AdjoinRoot (minpoly F x))
      ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P : AdjoinRoot (minpoly F x))
      (0 : AdjoinRoot (minpoly F x))
⊢ P₁ = 0

Tactic:
obtain ⟨P, rfl⟩ := mk_surjective P₁

Premises used: AdjoinRoot.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P : F[X]
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
      ↥F[x])
    (0 : ↥F[x])
⊢ Eq (α := AdjoinRoot (minpoly F x))
    ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P : AdjoinRoot (minpoly F x))
    (0 : AdjoinRoot (minpoly F x))

Tactic:
AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)

Premises used: Iff.mpr, AdjoinRoot.mk_eq_zero, minpoly.dvd
-- Module: Mathlib.RingTheory.Adjoin.Field
Goal:
F : Type u_1
inst : Field F
R : Type u_2
inst_1 : CommRing R
inst_2 : Algebra F R
x : R
P : F[X]
hP₁ :
  Eq.{u_2 + 1} (α := ↥F[x])
    (((Minpoly.toAdjoin F x : AlgHom.{u_1, u_1, u_2} F (AdjoinRoot (minpoly F x)) ↥F[x]) :
          (a : AdjoinRoot (minpoly F x)) → ↥F[x])
        ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P) :
      ↥F[x])
    (0 : ↥F[x])
refine : Eq.{u_2 + 1} (α := R) ((aeval x : (a : F[X]) → R) P : R) (0 : R)
⊢ Eq (α := AdjoinRoot (minpoly F x))
    ((AdjoinRoot.mk (minpoly F x) : (a : F[X]) → AdjoinRoot (minpoly F x)) P : AdjoinRoot (minpoly F x))
    (0 : AdjoinRoot (minpoly F x))

Tactic:
refine AdjoinRoot.mk_eq_zero.mpr (minpoly.dvd F x ?_)

Premises used: Iff.mpr, AdjoinRoot.mk_eq_zero, minpoly.dvd