awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra S A
inst_5 : Algebra R A
inst_6 : IsScalarTower R S A
hRS : Subalgebra.FG.{u_1, u_2} (R := R) (A := S) ⊤
hSA : Subalgebra.FG.{u_2, u_3} (R := S) (A := A) ⊤
rcases :
  ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤),
    Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
⊢ Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
have rcases₁ : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤) (t : Finset A)
  (ht : Eq (α := Subalgebra S A) (adjoin S (↑t : Set A)) ⊤), Subalgebra.FG.{u_1, u_3} (R := R) (A := A) ⊤
Tactic: classical
  rcases hRS with ⟨s, hs⟩
  rcases hSA with ⟨t, ht⟩
  exact ⟨s.image (algebraMap S A) ∪ t, by
    rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
    ⟩
Cleared hypotheses: hRS, hSA
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
hAC : Subalgebra.FG.{w, u_1} (R := A) (A := C) ⊤
hBC : FG.{u₁, u_1} (R := B) (M := C) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have obtain : ∀ (x : Finset C) (hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤),
  ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
Tactic: obtain ⟨x, hx⟩ := hAC
Cleared hypotheses: hAC
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
hBC : FG.{u₁, u_1} (R := B) (M := C) ⊤
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have obtain : ∀ (y : Finset C) (hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤),
  ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
Tactic: obtain ⟨y, hy⟩ := hBC
Cleared hypotheses: hBC
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (hypothesis)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy this : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have this₁ : ∀ (x : C), ∃ (f : C → B), Function.support f ⊆ (↑y : Set C) ∧ ∑ a ∈ y, f a • a = x
Tactic: simp_rw [eq_top_iff', mem_span_finset] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
this : ∀ (x : C), ∃ (f : C → B), Function.support f ⊆ (↑y : Set C) ∧ ∑ a ∈ y, f a • a = x
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have choose : ∀ (f : (x : C) → C → B),
  (∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)) →
    ∀ (hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x), ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
Tactic: choose f _ hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (hypothesis)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have hxy : ∀ xi ∈ x,
  Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
Tactic: have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
have rw : insert 1 (↑y : Set C) * insert 1 (↑y : Set C) ⊆
  (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
Tactic: rw [span_mul_span, span_le, coe_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ HMul.hMul (α := C) 1 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
have inl : 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ 1 * yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
have inl : yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
⊢ yi * 1 ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
have inr : yi ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
yi : C
hyi : yi ∈ (↑y : Set C)
yj : C
hyj : yj ∈ (↑y : Set C)
⊢ yi * yj ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
have inr : ∑ a ∈ y, f (yi * yj) a • a ∈ (↑(span (↥(Algebra.adjoin A (↑s : Set B))) (insert 1 (↑y : Set C))) : Set C)
Tactic: rw [← hf (yi * yj)]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (hypothesis)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have hyy : HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
  span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
Tactic: have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have refine : Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
  (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤
Tactic: refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ Eq (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ⊤
have convert_3 : Eq (α := Submodule A C)
  (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
    (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)))
  (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B))) ⊤)
Tactic: convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy :
  ∀ xi ∈ x,
    Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi
hyy :
  HMul.hMul (α := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) ≤
    span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)
⊢ Eq (α := Submodule A C)
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
      (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)))
    (restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B))) ⊤)
have convert_3 : (↑(Submonoid.closure (↑x : Set C)) : Set C) ⊆
  (↑(restrictScalars.{w, u₁, u_1} A (R := ↥(Algebra.adjoin A (↑s : Set B)))
        (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C))) :
    Set C)
Tactic: rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
A : Type w
B : Type u₁
C : Type u_1
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : Semiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
x : Finset C
hx : Eq (α := Subalgebra A C) (Algebra.adjoin A (↑x : Set C)) ⊤
y : Finset C
hy : Eq (α := Submodule B C) (span B (↑y : Set C)) ⊤
f : (x : C) → C → B
h : ∀ (x : C), Function.support (f x) ⊆ (↑y : Set C)
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
let let₁ let₂ : ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
⊢ ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
have let₃ : let s := image₂ f (x ∪ y * y) y;
∀
  (hxy :
    ∀ xi ∈ x,
      Membership.mem (γ := Submodule.{u₁, u_1} (↥(Algebra.adjoin A (↑s : Set B))) C)
        (span ↥(Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y) : Set C)) xi),
  ∃ (B₀ : Subalgebra A B), B₀.FG ∧ FG.{u₁, u_1} (R := ↥B₀) (M := C) ⊤
Tactic: classical
  let s : Finset B := Finset.image₂ f (x ∪ y * y) y
  have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
  have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
  refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
  convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
  rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
  refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
h : f.degree ≠ 0
⊢ Nontrivial.{u_1} (AdjoinRoot f)
have simp : ∀ (x : R), IsUnit x → ¬(C : (a : R) → R[X]) x = f
Tactic: simp only [AdjoinRoot, Quotient.nontrivial_iff, Ne, span_singleton_eq_top,
    Polynomial.isUnit_iff, not_exists, not_and]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)
have rw : HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
  ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
Tactic: rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
rw :
  HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)
have rw₁ : HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
  ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
Tactic: rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
rw :
  HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₁ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)
have rw₂ : HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
  (mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x))
Tactic: rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
f : R[X]
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
a : S
x : R
rw :
  HSMul.hSMul (β := AdjoinRoot f) a (((mk f).comp C : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₁ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    ((mk f).comp C : (a : R) → AdjoinRoot f) (a • x)
rw₂ :
  HSMul.hSMul (β := AdjoinRoot f) a ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) x) : AdjoinRoot f) =
    (mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x))
⊢ HSMul.hSMul (β := AdjoinRoot f) a ((of f : (a : R) → AdjoinRoot f) x : AdjoinRoot f) =
    (of f : (a : R) → AdjoinRoot f) (a • x)
have rw₃ : Eq (α := AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) (HSMul.hSMul (β := R[X]) a ((C : (a : R) → R[X]) x : R[X])) : AdjoinRoot f)
  ((mk f : (a : R[X]) → AdjoinRoot f) ((C : (a : R) → R[X]) (a • x)) : AdjoinRoot f)
Tactic: rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]