awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A : (a : R) → A) r₁) ((algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
r : R
⊢ p a ((algebraMap R A : (a : R) → A) r) ha ⋯
have algebraMap : ∀ (x : A) (h : x ∈ s), p x ((algebraMap R A : (a : R) → A) r) sorry sorry
Tactic: induction ha using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both :
  ∀ (r₁ r₂ : R), p ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
r : R
algebraMap : ∀ (x : A) (h : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
⊢ p a ((Algebra.algebraMap R A : (a : R) → A) r) ha ⋯
have algebraMap₁ : ∀ (r_1 : R), p ((Algebra.algebraMap R A : (a : R) → A) r_1) ((Algebra.algebraMap R A : (a : R) → A) r) sorry sorry
Tactic: induction ha using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : Set A
⊢ LE.le (α := Subalgebra R A) (Algebra.adjoin R (s ∪ star s))
    (Subalgebra.centralizer R ((↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A)))
have h : (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)
Tactic: convert! Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : Set A
⊢ (↑(centralizer R s) : Set A) ∪ star (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)
have h : (↑(centralizer R s) : Set A) ∪ (↑(centralizer R s) : Set A) = (↑(Subalgebra.centralizer R (s ∪ star s)) : Set A)
Tactic: rw [StarMemClass.star_coe_eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
⊢ IsMulCommutative.{u_3} ↥(adjoin R s)
have this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
Tactic: have := adjoin_le_centralizer_centralizer R s
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
⊢ IsMulCommutative.{u_3} ↥(adjoin R s)
have refine : ∀ (x : A) (h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) (x_1 : A)
  (h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1), x * x_1 = x_1 * x
Tactic: refine .of_setLike_mul_comm fun _ h₁ _ h₂ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
⊢ x * x_1 = x_1 * x
have hcomm₁ : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
Tactic: have hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a := fun a ha b hb ↦
    Set.union_star_self_comm (fun _ ha _ hb ↦ hcomm _ hb _ ha)
      (fun _ ha _ hb ↦ hcomm_star _ hb _ ha) b hb a ha
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x : A
h₁ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x
x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
⊢ x * x_1 = x_1 * x
have h₃ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
Tactic: apply this at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
h₂ : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x_1
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
⊢ x * x_1 = x_1 * x
have h₃ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
Tactic: apply this at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
⊢ x * x_1 = x_1 * x
have h₃ : x ∈ (s ∪ star s).centralizer.centralizer
Tactic: rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (hypothesis)
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 : Set A
hcomm_1 : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : LE.le (α := StarSubalgebra R A) (adjoin R s) (centralizer R (↑(centralizer R s) : Set A))
x x_1 : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x
h₂ : Membership.mem (γ := StarSubalgebra R A) (centralizer R (↑(centralizer R s) : Set A)) x_1
h₃ : x ∈ (s ∪ star s).centralizer.centralizer
⊢ x * x_1 = x_1 * x
have h₄ : x_1 ∈ (s ∪ star s).centralizer.centralizer
Tactic: rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 ⊤) ⊤
have h : ∀ (x : A), Membership.mem (γ := Subalgebra R A) (toSubalgebra ⊤) x ↔ Membership.mem (γ := Subalgebra R A) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 T : StarSubalgebra R A
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
have h : ∀ (x : A), x ∈ (S ⊓ T).toSubalgebra ↔ x ∈ S.toSubalgebra ⊓ T.toSubalgebra
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 : StarModule R A
inst_6 : Semiring B
inst_7 : Algebra R B
inst_8 : StarRing B
inst_9 : StarModule R B
ι : Sort u_5
inst_10 : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
s : ι → StarSubalgebra R A
⊢ Eq (α := StarSubalgebra R B) (map f (iInf s)) (⨅ (i : ι), map f (s i))
have a : (↑(map f (iInf s)) : Set B) = (↑(⨅ (i : ι), map f (s i)) : Set B)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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
⊢ x ∈ S
have rw : Membership.mem (γ := StarSubalgebra R A) ⊤ x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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
⊢ S = ⊤
have h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := StarSubalgebra R A) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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
have 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 sorry)
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 => ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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 ⋯)
⊢ f = g
have 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)
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 => ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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)
⊢ f = g
have 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)
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 => ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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)
⊢ f = g
have 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)
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 => ?_
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
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)
⊢ f = g
have 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)
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 => ?_