awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
a :
  ∀ (hd : R)
    (HL :
      Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
          ((algebraMap R A : (a : R) → A) hd : A) ∧
        ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
      z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
a₁ :
  ∀ (hs : hd ∈ s),
    ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r

Tactic:
rcases HL.1 with (⟨hd, rfl⟩ | hs)

Premises used: And.left, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
    z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)

Tactic:
⟨hd * z, r, hr, ?_⟩

Premises used: HMul.hMul, Exists.intro
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a : (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1),
    z_1 • r_1 = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)

Tactic:
refine ⟨hd * z, r, hr, ?_⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hd : R
HL :
  Membership.mem (α := A) (Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s)
      ((algebraMap R A : (a : R) → A) hd : A) ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
a :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)
a₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) (hd * z) : A) r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
a₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) hd : A) ((algebraMap R A : (a : R) → A) z : A) * r =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
a₃ a₄ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) z : A) r)
⊢ (hd * z) • r = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) hd : A) (z • r)

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]

Premises used: Algebra.algebraMap, mul_assoc, Algebra.smul_def, RingHom.map_mul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r

Tactic:
⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr,
          (mul_smul_comm _ _ _).symm⟩

Premises used: HMul.hMul, Submonoid.mul_mem, Exists.intro, mul_smul_comm, Eq.symm, Submonoid.subset_closure
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hd : A
tl : List A
ih :
  ∀ (HL : ∀ y ∈ tl, y ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s),
    ∃ (z : R) (r : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r), z • r = tl.prod
HL :
  hd ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s ∧
    ∀ x ∈ tl, x ∈ Set.range.{uA, uR + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ s
z : R
r : A
hr : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ (z_1 : R) (r_1 : A) (_ : Membership.mem (γ := Submonoid A) (Submonoid.closure s) r_1), z_1 • r_1 = hd * z • r

Tactic:
exact
        ⟨z, hd * r, Submonoid.mul_mem _ (Submonoid.subset_closure hs) hr,
          (mul_smul_comm _ _ _).symm⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Submodule R A) (span R (↑(Submonoid.closure s) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))

Tactic:
span_le.2 ?_

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
a :
  (↑(Submonoid.closure s) : Set A) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A) : Set A)
⊢ LE.le (α := Submodule R A) (span R (↑(Submonoid.closure s) : Set A))
    ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))

Tactic:
refine span_le.2 ?_

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Submonoid A) (Submonoid.closure s) (toSubmonoid (Subalgebra.toSubsemiring (adjoin R s)))

Tactic:
Submonoid.closure_le.2 subset_adjoin

Premises used: Iff.mpr, Algebra.subset_adjoin, Submonoid.closure_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Submonoid A) (Submonoid.closure s) (toSubmonoid (Subalgebra.toSubsemiring (adjoin R s)))

Tactic:
exact Submonoid.closure_le.2 subset_adjoin

Premises used: Iff.mpr, Algebra.subset_adjoin, Submonoid.closure_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Submodule R A) (span R s) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s))

Tactic:
span_le.mpr subset_adjoin

Premises used: Iff.mpr, Algebra.subset_adjoin, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
t : Submodule R A
rw : span R (↑(Submonoid.closure s) : Set A) ≤ t ↔ (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
rw₁ rw₂ : (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A) ↔ (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) ≤ t ↔
    (↑(Submonoid.closure s) : Set A) ⊆ (↑t : Set A)

Tactic:
rw [adjoin_eq_span, span_le]

Premises used: Algebra.adjoin_eq_span, Submodule.span_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hs : (↑(Submonoid.closure s) : Set A) ⊆ (↑(span R s) : Set A)
⊢ Eq (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (adjoin R s) : Submodule R A)
    (span R s : Submodule R A)

Tactic:
le_antisymm ((adjoin_toSubmodule_le R).mpr hs) (span_le_adjoin R s)

Premises used: Iff.mpr, Algebra.span_le_adjoin, Algebra.adjoin_toSubmodule_le, le_antisymm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(span R s) : Set A)) (adjoin R s)

Tactic:
le_antisymm (adjoin_le (span_le_adjoin _ _)) (adjoin_mono Submodule.subset_span)

Premises used: Algebra.span_le_adjoin, le_antisymm, Algebra.adjoin_mono, Algebra.adjoin_le, Submodule.subset_span
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
s : Set A
t : Subalgebra R B
⊢ adjoin R ((⇑f : (a : A) → B) '' s) ≤ t ↔ Subalgebra.map f (adjoin R s) ≤ t

Tactic:
simp [Subalgebra.map_le, adjoin_le_iff]

Premises used: Subalgebra.map_le, Algebra.adjoin_le_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : A
t : Subalgebra R A
⊢ adjoin R (insert x (↑(adjoin R s) : Set A)) ≤ t ↔ adjoin R (insert x s) ≤ t

Tactic:
simp [adjoin_le_iff, Set.insert_subset_iff]

Premises used: Set.insert_subset_iff, Algebra.adjoin_le_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
a : A
ha : a ∈ s
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) a : B)

Tactic:
subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩

Premises used: Algebra.subset_adjoin, Set.subset_union_left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
a : A
ha : a ∈ s
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) a : B)

Tactic:
exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)

Tactic:
have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
⊢ Membership.mem (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    (HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B))

Tactic:
Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r

Premises used: Algebra.adjoin, Subalgebra.smul_mem, Set.image, Union.union, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
h : (f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)

Tactic:
convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r

Premises used: Algebra.adjoin, Subalgebra.smul_mem, Set.image, Union.union, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
h : (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)
⊢ (f : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)

Tactic:
rw [algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
⊢ (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)

Tactic:
f.map_smul _ _

Premises used: LinearMap.map_smul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
r : R
this :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) 1 : B)
⊢ (f : (a : A) → B) (HSMul.hSMul (β := A) r 1) = HSMul.hSMul (β := B) r ((f : (a : A) → B) 1 : B)

Tactic:
exact f.map_smul _ _

Premises used: LinearMap.map_smul
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) y : B)
hz :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) z : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) (y + z) : B)

Tactic:
simpa [hy, hz] using Subalgebra.add_mem _ hy hz

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
y z : A
hx : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hy_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) z
hy :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) y : B)
hz :
  Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) z : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) (y * z) : B)

Tactic:
simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf :
  ∀ (a₁ a₂ : A),
    (f : (a : A) → B) (a₁ * a₂) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a₁ : B) ((f : (a : A) → B) a₂ : B)
h : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
mem :
  ∀ (a : A) (ha : a ∈ s),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) a : B)
algebraMap :
  ∀ (r : R),
    Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
      ((f : (a : A) → B) ((Algebra.algebraMap R A : (a : R) → A) r : A) : B)
add :
  ∀ (y z : A),
    Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
      Membership.mem (γ := Subalgebra R A) (adjoin R s) z →
        ∀
          (hy :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) y : B))
          (hz :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) z : B)),
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) (y + z) : B)
mul :
  ∀ (y z : A),
    Membership.mem (γ := Subalgebra R A) (adjoin R s) y →
      Membership.mem (γ := Subalgebra R A) (adjoin R s) z →
        ∀
          (hy :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) y : B))
          (hz :
            Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
              ((f : (a : A) → B) z : B)),
          Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
            ((f : (a : A) → B) (y * z) : B)
⊢ Membership.mem.{uB, uB} (α := B) (γ := Subalgebra R B) (adjoin R ((⇑f : (a : A) → B) '' (s ∪ {1})))
    ((f : (a : A) → B) x : B)

Tactic:
induction h using adjoin_induction with
  | mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
  | algebraMap r =>
    have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _
  | add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
  | mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

Premises used: Algebra.algebraMap, Submodule.mul, Algebra.algebraMap_eq_smul_one, LinearMap.map_smul, Submodule.add
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ LE.le (α := Subalgebra R A) (adjoin R s) (Subalgebra.centralizer R (↑(Subalgebra.centralizer R s) : Set A))

Tactic:
adjoin_le Set.subset_centralizer_centralizer

Premises used: Set.subset_centralizer_centralizer, Algebra.adjoin_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
⊢ IsMulCommutative.{uA} ↥(adjoin R s)

Tactic:
have := adjoin_le_centralizer_centralizer R s
  .of_setLike_mul_comm fun _ h₁ _ h₂ ↦
    Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂)

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, Algebra.adjoin, IsMulCommutative.of_setLike_mul_comm, Set.centralizer_centralizer_comm_of_comm, Algebra.adjoin_le_centralizer_centralizer
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : Algebra R B
inst_8 : IsScalarTower R S A
s t : Set A
x : A
⊢ ∀ (x_1 : A), Membership.mem (γ := Set A) {x} x_1 → ∀ (y : A), Membership.mem (γ := Set A) {x} y → x_1 * y = y * x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
S_1 : Type uS
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S_1
inst_5 : Algebra R A
inst_6 : Algebra S_1 A
inst_7 : Algebra R B
inst_8 : IsScalarTower R S_1 A
s_1 t : Set A
S : Type u_1
inst_9 : SetLike S A
inst_10 : MulMemClass S A
s : S
inst_11 : IsMulCommutative.{uA} ↥s
⊢ IsMulCommutative.{uA} ↥(adjoin R (↑s : Set A))

Tactic:
isMulCommutative_adjoin R fun _ h₁ _ h₂ => setLike_mul_comm h₁ h₂

Premises used: setLike_mul_comm, Algebra.isMulCommutative_adjoin