awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ (↑(toSubalgebra (⨅ (i : ι), S i)) : Set A) = (↑(⨅ (i : ι), (S i).toSubalgebra) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
⊢ Eq.{u_3 + 1} (α := Subalgebra R A) (toSubalgebra ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) ⊥ x ↔
    Membership.mem (γ := Set A) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
⊢ (↑⊥ : Set A) = Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)

Tactic:
rfl

Premises used: setOf, Set.range, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
rw : Membership.mem (γ := StarSubalgebra R A) ⊤ x
⊢ x ∈ S

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) ⊤ x

Tactic:
mem_top

Premises used: StarSubalgebra.mem_top
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : S = ⊤
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) ⊤ x

Tactic:
exact mem_top

Premises used: StarSubalgebra.mem_top
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := StarSubalgebra R A) ⊤ x
⊢ S = ⊤

Tactic:
ext x
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := StarSubalgebra R A) ⊤ x

Tactic:
⟨fun _ => mem_top, fun _ => h x⟩

Premises used: StarSubalgebra.mem_top, Iff.intro
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := StarSubalgebra R A) ⊤ x

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext f g fun a =>
    adjoin_induction_subtype (p := fun y => f y = g y) a (fun x hx => ?_) (fun r => ?_)
    (fun x y hx hy => ?_) (fun x y hx hy => ?_) fun x hx => ?_

Premises used: DFunLike.ext, StarAlgebra.adjoin_induction_subtype
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
refine_1 :
  ∀ (a : ↥(adjoin R s)) (x : A) (hx : x ∈ s),
    (fun (y : ↥(adjoin R s)) ↦
        Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) x ⋯)
refine_2 :
  ∀ (a : ↥(adjoin R s)) (r : R),
    (fun (y : ↥(adjoin R s)) ↦
        Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
      ((algebraMap R ↥(adjoin R s) : (a : R) → ↥(adjoin R s)) r)
refine_3 :
  ∀ (a x y : ↥(adjoin R s))
    (hx :
      (fun (y : ↥(adjoin R s)) ↦
          Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
        x)
    (hy :
      (fun (y : ↥(adjoin R s)) ↦
          Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
        y),
    (fun (y : ↥(adjoin R s)) ↦
        Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
      (x + y)
refine_4 :
  ∀ (a x y : ↥(adjoin R s))
    (hx :
      (fun (y : ↥(adjoin R s)) ↦
          Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
        x)
    (hy :
      (fun (y : ↥(adjoin R s)) ↦
          Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
        y),
    (fun (y : ↥(adjoin R s)) ↦
        Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
      (x * y)
refine_5 :
  ∀ (a x : ↥(adjoin R s))
    (hx :
      (fun (y : ↥(adjoin R s)) ↦
          Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
        x),
    (fun (y : ↥(adjoin R s)) ↦
        Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
      (star x)
⊢ f = g

Tactic:
refine DFunLike.ext f g fun a =>
    adjoin_induction_subtype (p := fun y => f y = g y) a (fun x hx => ?_) (fun r => ?_)
    (fun x y hx hy => ?_) (fun x y hx hy => ?_) fun x hx => ?_

Premises used: DFunLike.ext, StarAlgebra.adjoin_induction_subtype
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a : ↥(adjoin R s)
x : A
hx : x ∈ s
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) x ⋯)

Tactic:
h ⟨x, subset_adjoin R s hx⟩ hx

Premises used: StarAlgebra.subset_adjoin, Subtype.mk
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a : ↥(adjoin R s)
x : A
hx : x ∈ s
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) x ⋯)

Tactic:
exact h ⟨x, subset_adjoin R s hx⟩ hx

Premises used: StarAlgebra.subset_adjoin, Subtype.mk
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a : ↥(adjoin R s)
r : R
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    ((algebraMap R ↥(adjoin R s) : (a : R) → ↥(adjoin R s)) r)

Tactic:
simp only [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a x y : ↥(adjoin R s)
hx :
  (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    x
hy :
  (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    y
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    (x + y)

Tactic:
simp only [map_add, map_add, hx, hy]

Premises used: map_add
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a x y : ↥(adjoin R s)
hx :
  (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    x
hy :
  (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    y
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    (x * y)

Tactic:
simp only [map_mul, map_mul, hx, hy]

Premises used: map_mul
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
s : Set A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R s)) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R s)) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R s)) B
f g : F
h :
  ∀ (x : ↥(adjoin R s)),
    (↑x : A) ∈ s → Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) x : B) ((g : (a : ↥(adjoin R s)) → B) x : B)
a x : ↥(adjoin R s)
hx :
  (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    x
⊢ (fun (y : ↥(adjoin R s)) ↦
      Eq.{u_4 + 1} (α := B) ((f : (a : ↥(adjoin R s)) → B) y : B) ((g : (a : ↥(adjoin R s)) → B) y : B))
    (star x)

Tactic:
simp only [map_star, hx]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
a : A
inst_9 : FunLike.{u_1 + 1, u_3 + 1, u_4 + 1} F (↥(adjoin R {a})) B
inst_10 : AlgHomClass.{u_1, u_2, u_3, u_4} F R (↥(adjoin R {a})) B
inst_11 : StarHomClass.{u_1, u_3, u_4} F (↥(adjoin R {a})) B
f g : F
h :
  Eq.{u_4 + 1} (α := B)
    ((f : (a : ↥(adjoin R {a})) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) a ⋯) :
      B)
    ((g : (a : ↥(adjoin R {a})) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) a ⋯) :
      B)
⊢ f = g

Tactic:
ext_adjoin fun x hx =>
    (show x = ⟨a, self_mem_adjoin_singleton R a⟩ from
          Subtype.ext <| Set.mem_singleton_iff.mp hx).symm ▸
      h

Premises used: StarAlgHom.ext_adjoin
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
f g : F
a : A
ha : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ star a ∈
    Subsemigroup.carrier
      (Submonoid.toSubsemigroup
        (Subsemiring.toSubmonoid
          (Subalgebra.toSubsemiring (AlgHom.equalizer (F := A →ₐ[R] B) (↑f : A →ₐ[R] B) (↑g : A →ₐ[R] B)))))

Tactic:
simpa only [← map_star] using congrArg star ha

Premises used: congrArg, StarHomClass.map_star, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
f g : F
x : A
⊢ Membership.mem (γ := StarSubalgebra R A) (equalizer f g) x ↔
    Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
f g : F
s : Set A
h : Set.EqOn.{u_3, u_4} (β := B) (⇑f : (a : A) → B) (⇑g : (a : A) → B) s
⊢ LE.le (α := StarSubalgebra R A) (adjoin R s) (equalizer f g)

Tactic:
adjoin_le h

Premises used: StarAlgebra.adjoin_le
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
s : Set A
h : Eq (α := StarSubalgebra R A) (adjoin R s) ⊤
f g : F
hs : Set.EqOn.{u_3, u_4} (β := B) (⇑f : (a : A) → B) (⇑g : (a : A) → B) s
⊢ f = g

Tactic:
DFunLike.ext f g fun _x => StarAlgHom.adjoin_le_equalizer f g hs <| h.symm ▸ trivial

Premises used: DFunLike.ext, StarAlgHom.adjoin_le_equalizer
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : StarModule R B
f : A →⋆ₐ[R] B
s : Set A
⊢ Eq (α := StarSubalgebra R B) (map f (adjoin R s)) (adjoin R ((⇑f : (a : A) → B) '' s))

Tactic:
GaloisConnection.l_comm_of_u_comm Set.image_preimage (gc_map_comap f) StarAlgebra.gc
    StarAlgebra.gc fun _ => rfl

Premises used: GaloisConnection.l_comm_of_u_comm, StarSubalgebra.gc_map_comap, Set.image_preimage, StarAlgebra.gc, rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
f g : F
inst_12 : StarModule R B
φ : A →⋆ₐ[R] B
b : A
⊢ Membership.mem (α := B) (↑φ : A →ₐ[R] B).range.carrier (star (((↑φ : A →ₐ[R] B).toRingHom : (a : A) → B) b) : B)

Tactic:
⟨star b, map_star φ b⟩

Premises used: Set.Mem, setOf, StarHomClass.map_star, Exists.intro, Set.range, Star.star
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : FunLike F A B
inst_10 : AlgHomClass F R A B
inst_11 : StarHomClass F A B
f g : F
inst_12 : StarModule R B
φ : A →⋆ₐ[R] B
b : A
⊢ Membership.mem (α := B) (↑φ : A →ₐ[R] B).range.carrier (star (((↑φ : A →ₐ[R] B).toRingHom : (a : A) → B) b) : B)

Tactic:
exact ⟨star b, map_star φ b⟩
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ((↑φ : A →ₐ[R] B).toRingHom : (a : A) → B) a = x
⊢ a ∈ (↑(Subalgebra.toSubsemiring.{u_2, u_3} (R := R) (toSubalgebra ⊤)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ((↑φ : A →ₐ[R] B).toRingHom : (a : A) → B) a = x
⊢ Membership.mem (γ := StarSubalgebra R B) (map φ ⊤) x

Tactic:
exact ⟨a, by simp, ha⟩
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ((↑(↑φ : A →ₐ[R] B) : A →+* B) : (a : A) → B) a = x
⊢ Membership.mem (γ := StarSubalgebra R B) φ.range x

Tactic:
⟨a, ha⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R A
inst_9 : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : ((↑(↑φ : A →ₐ[R] B) : A →+* B) : (a : A) → B) a = x
⊢ Membership.mem (γ := StarSubalgebra R B) φ.range x

Tactic:
exact ⟨a, ha⟩
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R B
f : A →⋆ₐ[R] B
S : StarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
x : A
⊢ Eq.{u_4 + 1} (α := B) ((↑((f.codRestrict S hf : (a : A) → ↥S) x) : B) : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R B
f : A →⋆ₐ[R] B
S : StarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ S.subtype.comp (f.codRestrict S hf) = f

Tactic:
StarAlgHom.ext <| coe_codRestrict _ S hf

Premises used: StarAlgHom.coe_codRestrict, StarAlgHom.ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : Semiring B
inst_6 : Algebra R B
inst_7 : StarRing B
inst_8 : StarModule R B
f : A →⋆ₐ[R] B
S : StarSubalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := ↥S) (⇑(f.codRestrict S hf) : (a : A) → ↥S) ↔
    Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : Star A
inst_12 : Star B
⊢ Function.Injective (α := A →⋆ₐ[S] B) (β := A →⋆ₐ[R] B) (restrictScalars R)

Tactic:
fun f g h => StarAlgHom.ext fun x =>
    show f.restrictScalars R x = g.restrictScalars R x from DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun, Function.Injective, StarAlgHom.ext
-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : Algebra S B
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : Star A
inst_12 : Star B
⊢ Function.Injective (α := A ≃⋆ₐ[S] B) (β := A ≃⋆ₐ[R] B) (restrictScalars R)

Tactic:
fun f g h => StarAlgEquiv.ext fun x =>
    show f.restrictScalars R x = g.restrictScalars R x from DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun, Function.Injective, StarAlgEquiv.ext