awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
pos :
  ∀ (h : Module.Finite.{u, v} R ↥A ∧ Module.Finite.{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
have neg : ∀ (h : ¬(Module.Finite.{u, v} R ↥A ∧ Module.Finite.{u, v} R ↥B)),
  finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
Tactic: by_cases h : Module.Finite R A ∧ Module.Finite R B
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have left : Module.Finite.{u, v} R ↥A
Tactic: obtain ⟨_, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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
left : Module.Finite.{u, v} R ↥A
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have right : Module.Finite.{u, v} R ↥B
Tactic: obtain ⟨_, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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)
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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
Tactic: wlog hA : ¬ Module.Finite R A generalizing A B
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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
Tactic: wlog hA : ¬ Module.Finite R A generalizing A B
Cleared hypotheses: inst_4, inst_5, h
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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 ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have this₁ : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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
Tactic: rwa [sup_comm, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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
Tactic: rwa [sup_comm, mul_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have hA₁ : Cardinal.aleph0 ≤ Module.rank R ↥A
Tactic: rw [← rank_lt_aleph0_iff, not_lt] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (hypothesis)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have 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)
Tactic: have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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)
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have rw : finrank.{u, v} R ↥(A ⊔ B) ≤ 0 * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have rw₁ : 0 ≤ 0 * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Dimension (goal)
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
⊢ finrank.{u, v} R ↥(A ⊔ B) ≤ finrank.{u, v} R ↥A * finrank.{u, v} R ↥B
have rw₂ : LE.le (α := ℕ) 0 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
have 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)))
Tactic: rcases fg_def.1 h1 with ⟨p, hp, hp'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
have 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)))
Tactic: rcases fg_def.1 h2 with ⟨q, hq, hq'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)))
have refine_1 : LE.le (α := Submodule R A) (span R (p * q))
  ((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 ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)))
⊢ FG.{u, v} (R := R) (M := A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
have 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)
Tactic: refine fg_def.2 ⟨p * q, hp.mul hq, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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))
⊢ LE.le (α := Submodule R A) (span R (p * q))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R (s ∪ t)))
have 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)
Tactic: rw [span_le, Set.mul_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)
have refine_1 : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) x
Tactic: refine Subalgebra.mul_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) (x * y)
have refine_1₁ : Membership.mem (γ := Subalgebra R A) (adjoin R (s ∪ t)) y
Tactic: refine Subalgebra.mul_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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
have rw : Membership.mem (γ := Submodule R A) (span R p) x
Tactic: rw [← hp']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (goal)
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)
    ((Subalgebra.toSubmodule : (a : Subalgebra (↥(adjoin R s)) A) → Submodule (↥(adjoin R s)) A)
        (adjoin (↥(adjoin R s)) t) :
      Submodule (↥(adjoin R s)) A)
    y
have rw : Membership.mem (γ := Submodule (↥(adjoin R s)) A) (span (↥(adjoin R s)) q) y
Tactic: rw [← hq']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.FG (hypothesis)
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)) y
have this : 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: have : y ∈ Subalgebra.toSubmodule (adjoin (adjoin R s) t) := by
      rw [← hq']
      exact subset_span hy