awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
left : Module.Finite.{u, v} R ↥A
right : Module.Finite.{u, v} R ↥B
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
simpa only [map_mul] using Cardinal.toNat_le_toNat (A.rank_sup_le_of_free B)
      (Cardinal.mul_lt_aleph0 (rank_lt_aleph0 R A) (rank_lt_aleph0 R B))

Premises used: Membership.mem, Subtype, Cardinal.toNat_le_toNat, map_mul, Subalgebra.rank_sup_le_of_free, Cardinal.mul_lt_aleph0, Module.rank_lt_aleph0
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
neg :
  ∀
    (this :
      ∀ (A B : Subalgebra R S) [Free.{u, v} R ↥A] [Free.{u, v} R ↥B]
        (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)) (hA : ¬Module.Finite.{u, v} R ↥A),
        finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B)
    (hA : ¬¬Module.Finite.{u, v} R ↥A), finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
wlog :
  ∀ (A B : Subalgebra R S) [Free.{u, v} R ↥A] [Free.{u, v} R ↥B]
    (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)) (hA : ¬Module.Finite.{u, v} R ↥A),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
wlog hA : ¬ Module.Finite R A generalizing A B

Premises used: Membership.mem, Subtype, Module.Finite
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
this :
  ∀ (A B : Subalgebra R S) [Free.{u, v} R ↥A] [Free.{u, v} R ↥B]
    (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)) (hA : ¬Module.Finite.{u, v} R ↥A),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
hA : ¬¬Module.Finite.{u, v} R ↥A
⊢ finrank.{u, v} R ↥(B ⊔ A) ≤ finrank.{u, v} R ↥B * finrank.{u, v} R ↥A

Tactic:
have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA))
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
this_1 :
  ∀ (A B : Subalgebra R S) [Free.{u, v} R ↥A] [Free.{u, v} R ↥B]
    (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)) (hA : ¬Module.Finite.{u, v} R ↥A),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
hA : ¬¬Module.Finite.{u, v} R ↥A
this : finrank.{u, v} R ↥(B ⊔ A) ≤ finrank.{u, v} R ↥B * finrank.{u, v} R ↥A
neg :
  ∀ (this : finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥B * finrank.{u, v} R ↥A),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
neg₁ neg₂ neg₃ neg₄ :
  ∀ (this : finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B),
    finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
rwa [sup_comm, mul_comm] at this

Premises used: sup_comm, mul_comm
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A_1 B_1 A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
hA : ¬Module.Finite.{u, v} R ↥A
⊢ Cardinal.aleph0 ≤ Module.rank R ↥A

Tactic:
rw [← rank_lt_aleph0_iff, not_lt] at hA

Premises used: Module.rank_lt_aleph0_iff, not_lt
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A_1 B_1 A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
⊢ LE.le (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)
    ((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A_1 B_1 A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
⊢ Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≤
    Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)

Tactic:
have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp
-- Module: Mathlib.RingTheory.Adjoin.Dimension
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : StrongRankCondition R
inst_2 : CommRing S
inst_3 : Algebra R S
A_1 B_1 A B : Subalgebra R S
inst_4 : Free.{u, v} R ↥A
inst_5 : Free.{u, v} R ↥B
h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this :
  Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≤
    Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊔ B) : Submodule R S)
rw : finrank.{u, v} R ↥(A ⊔ B) ≤ 0 * finrank.{u, v} R ↥B
rw₁ : 0 ≤ 0 * finrank.{u, v} R ↥B
rw₂ rw₃ : LE.le (α := ℕ) 0 0
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B

Tactic:
rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,
    show finrank R ↥(A ⊔ B) = 0 from Cardinal.toNat_apply_of_aleph0_le (hA.trans this), zero_mul]

Premises used: Cardinal.toNat_apply_of_aleph0_le, MulZeroClass.zero_mul, LE.le.trans
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
rcases :
  ∀ (p : Set A) (hp : p.Finite)
    (hp' :
      Eq (α := Submodule R A) (span R p)
        ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))),
    FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))

Tactic:
rcases fg_def.1 h1 with ⟨p, hp, hp'⟩

Premises used: Submodule.fg_def, Iff.mp
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
rcases :
  ∀ (q : Set A) (hq : q.Finite)
    (hq' :
      Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
        ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
          (adjoin (↥(adjoin R s)) t))),
    FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))

Tactic:
rcases fg_def.1 h2 with ⟨q, hq, hq'⟩

Premises used: Submodule.fg_def, Iff.mp
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))

Tactic:
fg_def.2 ⟨p * q, hp.mul hq, le_antisymm ?_ ?_⟩

Premises used: Iff.mpr, HMul.hMul, Set.Finite.mul, Submodule.fg_def, le_antisymm, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
refine_1 :
  LE.le (α := Submodule R A) (span R (p * q))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
refine_2 :
  LE.le (α := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)) : Submodule R A)
    (span R (p * q) : Submodule R A)
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))

Tactic:
refine fg_def.2 ⟨p * q, hp.mul hq, le_antisymm ?_ ?_⟩

Premises used: Iff.mpr, HMul.hMul, Set.Finite.mul, Submodule.fg_def, le_antisymm, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
refine_1 :
  ∀ x ∈ p,
    ∀ y ∈ q,
      x * y ∈
        (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)) : Submodule R A) : Set A)
⊢ LE.le (α := Submodule R A) (span R (p * q))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))

Tactic:
rw [span_le, Set.mul_subset_iff]

Premises used: Set.mul_subset_iff, Submodule.span_le
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) (x * y)

Tactic:
Subalgebra.mul_mem _ ?_ ?_

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
refine_1 : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) x
refine_1₁ : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) y
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) (x * y)

Tactic:
refine Subalgebra.mul_mem _ ?_ ?_

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
rw : Membership.mem (γ := Submodule R A) (span R p) x
⊢ Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) x

Tactic:
rw [← hp']
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule R A) (span R p) x

Tactic:
subset_span hx

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule R A) (span R p) x

Tactic:
exact subset_span hx

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) x

Tactic:
have : x ∈ Subalgebra.toSubmodule (adjoin R s) := by
        rw [← hp']
        exact subset_span hx
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) x
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) x

Tactic:
adjoin_mono Set.subset_union_left this

Premises used: Set.subset_union_left, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
this :
  Membership.mem (γ := Submodule R A)
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) x
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) x

Tactic:
exact adjoin_mono Set.subset_union_left this

Premises used: Set.subset_union_left, Algebra.adjoin_mono
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
rw : Membership.mem (γ := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q) y
⊢ Membership.mem (γ := Submodule (↥(adjoin R s)) A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    y

Tactic:
rw [← hq']
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q) y

Tactic:
subset_span hy

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Adjoin.FG
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
s t : Set A
h1 : FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
h2 :
  FG.{v, v} (R := ↥(adjoin R s)) (M := A)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
p : Set A
hp : p.Finite
hp' : Eq (α := Submodule R A) (span R p) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))
q : Set A
hq : q.Finite
hq' :
  Eq (α := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
      (adjoin (↥(adjoin R s)) t))
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ Membership.mem (γ := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q) y

Tactic:
exact subset_span hy

Premises used: Submodule.subset_span