awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
h₁ : ∀ (x : A), x ∈ S ↔ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x
⊢ S = ⊤

Tactic:
ext x
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

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

Premises used: NonUnitalAlgebra.mem_top, Iff.intro
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ Membership.mem (γ := NonUnitalSubalgebra R A) ⊤ x

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
⊢ Eq (α := NonUnitalSubalgebra R A)
    (NonUnitalAlgHom.range (F := A →ₙₐ[R] A) (A := A) (NonUnitalAlgHom.id R A) : NonUnitalSubalgebra R A)
    (⊤ : NonUnitalSubalgebra R A)

Tactic:
SetLike.coe_injective Set.range_id

Premises used: SetLike.coe_injective, Set.range_id
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
f : A →ₙₐ[R] B
⊢ Eq.{w + 1} (α := NonUnitalSubalgebra R B) (NonUnitalSubalgebra.map f (⊤ : NonUnitalSubalgebra R A))
    (NonUnitalAlgHom.range f)

Tactic:
SetLike.coe_injective Set.image_univ

Premises used: Set.image_univ, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
f : A →ₙₐ[R] B
⊢ (↑(NonUnitalSubalgebra.map f (⊥ : NonUnitalSubalgebra R A)) : Set B) = (↑⊥ : Set B)

Tactic:
simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]

Premises used: NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
f : A →ₙₐ[R] B
⊢ Eq (α := NonUnitalSubalgebra R A) (NonUnitalSubalgebra.comap (B := B) f ⊤ : NonUnitalSubalgebra R A)
    (⊤ : NonUnitalSubalgebra R A)

Tactic:
eq_top_iff.2 fun _ => mem_top

Premises used: Iff.mpr, NonUnitalAlgebra.eq_top_iff, NonUnitalAlgebra.mem_top
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R B B
inst_6 : SMulCommClass R B B
f : A →ₙₐ[R] B
⊢ Eq.{w + 1} (α := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range f) ⊤ ↔
    Function.Surjective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
NonUnitalAlgebra.eq_top_iff

Premises used: Set.Mem, setOf, NonUnitalAlgebra.eq_top_iff, Set.range, Function.Surjective
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ NonUnitalAlgHom.range (F := ↥S →ₙₐ[R] A) (A := ↥S) (NonUnitalSubalgebraClass.subtype S) = S

Tactic:
ext <| Set.ext_iff.1 <|
    (NonUnitalAlgHom.coe_range <| NonUnitalSubalgebraClass.subtype S).trans Subtype.range_val

Premises used: NonUnitalSubalgebraClass.subtype, Subtype.range_val, NonUnitalAlgHom.coe_range, NonUnitalSubalgebra.ext, Iff.mp, Set.ext_iff, Eq.trans
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B_1 : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : Subsingleton A
B C : NonUnitalSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

Premises used: ZeroMemClass.zero_mem, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
S₁ : NonUnitalSubalgebra R B
⊢ (↑(S.prod S₁) : Set (A × B)) = (↑S : Set A) ×ˢ (↑S₁ : Set B)

Tactic:
rfl

Premises used: setOf, Set.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
S₁ : NonUnitalSubalgebra R B
⊢ (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule

Tactic:
rfl

Premises used: Submodule.prod, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
S : NonUnitalSubalgebra R A
S₁ : NonUnitalSubalgebra R B
x : A × B
⊢ x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

Tactic:
Set.mem_prod

Premises used: Set.Mem, setOf, Set.prod, Set.mem_prod
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
S T : NonUnitalSubalgebra R A
S₁ T₁ : NonUnitalSubalgebra R B
⊢ S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

Tactic:
Set.prod_mono

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, Set.prod_mono
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
h :
  ∀ (x : A × B),
    Membership.mem (γ := NonUnitalSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
      Membership.mem (γ := NonUnitalSubalgebra R (A × B)) ⊤ x
⊢ Eq (α := NonUnitalSubalgebra R (A × B)) (prod ⊤ ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
x : A × B
⊢ Membership.mem (γ := NonUnitalSubalgebra R (A × B)) (prod ⊤ ⊤) x ↔
    Membership.mem (γ := NonUnitalSubalgebra R (A × B)) ⊤ x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : IsScalarTower R B B
inst_8 : SMulCommClass R B B
S T : NonUnitalSubalgebra R A
S₁ T₁ : NonUnitalSubalgebra R B
⊢ S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

Tactic:
SetLike.coe_injective Set.prod_inter_prod

Premises used: SetLike.coe_injective, Set.prod_inter_prod
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S ≤ T
⊢ Function.Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

Tactic:
fun _ _ => Subtype.ext ∘ Subtype.mk.inj

Premises used: Function.comp, Subtype.mk.inj, Function.Injective, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
⊢ inclusion ⋯ = NonUnitalAlgHom.id R ↥S

Tactic:
rfl

Premises used: NonUnitalSubalgebra.inclusion, NonUnitalAlgHom.id, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S ≤ T
x : A
hx : x ∈ S
⊢ (inclusion h : (a : ↥S) → ↥T) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) x hx) = Subtype.mk (p := fun (x : A) ↦ x ∈ T) x ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S ≤ T
x : ↥T
m : (↑x : A) ∈ S
⊢ (inclusion h : (a : ↥S) → ↥T) (Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑x : A) m) = x

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T U : NonUnitalSubalgebra R A
hst : S ≤ T
htu : T ≤ U
x : ↥S
⊢ Eq (α := ↥U) ((inclusion htu : (a : ↥T) → ↥U) ((inclusion hst : (a : ↥S) → ↥T) x) : ↥U)
    ((inclusion ⋯ : (a : ↥S) → ↥U) x : ↥U)

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S ≤ T
s : ↥S
⊢ (↑((inclusion h : (a : ↥S) → ↥T) s) : A) = (↑s : A)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : Subsingleton.{v + 1} (NonUnitalSubalgebra R A)
⊢ Subsingleton (A →ₙₐ[R] B)

Tactic:
⟨fun f g =>
    NonUnitalAlgHom.ext fun a =>
      have : a ∈ (⊥ : NonUnitalSubalgebra R A) :=
        Subsingleton.elim (⊤ : NonUnitalSubalgebra R A) ⊥ ▸ mem_top
      (mem_bot.mp this).symm ▸ (map_zero f).trans (map_zero g).symm⟩

Premises used: Eq.rec, map_zero, Bot.bot, NonUnitalAlgebra.mem_top, Subsingleton.intro, Iff.mp, Subsingleton.elim, Top.top, NonUnitalAlgebra.mem_bot, Eq.symm, Eq.trans, NonUnitalAlgHom.ext
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_1
inst_5 : Nonempty ι
S : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) S
⊢ (↑(iSup S) : Set A) = ⋃ (i : ι), (↑(S i) : Set A)

Tactic:
let K : NonUnitalSubalgebra R A :=
    { __ := NonUnitalSubsemiring.copy _ _ (NonUnitalSubsemiring.coe_iSup_of_directed dir).symm
      smul_mem' := fun r _x hx ↦
        let ⟨i, hi⟩ := Set.mem_iUnion.1 hx
        Set.mem_iUnion.2 ⟨i, (S i).smul_mem' r hi⟩ }
  have : iSup S = K := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
  this.symm ▸ rfl

Premises used: Iff.mpr, Set.iUnion_subset, _private.0.NonUnitalSubalgebra.coe_iSup_of_directed.match_1, iSup, NonUnitalSubsemiring.coe_iSup_of_directed, Set.mem_iUnion, AddSubsemigroup.carrier, Membership.mem, NonUnitalSubsemiring.copy, Eq.rec, le_iSup, AddSubmonoid.toAddSubsemigroup, NonUnitalSubalgebra.smul_mem', le_antisymm, NonUnitalSubsemiring.toAddSubmonoid, SetLike.coe, NonUnitalSubalgebra.toNonUnitalSubsemiring, NonUnitalSubalgebra.mk, Exists.intro, Iff.mp, iSup_le, HSMul.hSMul, Eq.symm, Set.iUnion, rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
inst_5 : Nonempty ι
S : ι → NonUnitalSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{v} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), (S i).toNonUnitalSubsemiring)

Tactic:
have := NonUnitalSubsemiring.isMulCommutative_iSup dir
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
ι : Sort u_2
inst_5 : Nonempty ι
S : ι → NonUnitalSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{v} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) S
this : IsMulCommutative.{v} ↥(⨆ (i : ι), (S i).toNonUnitalSubsemiring)
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    NonUnitalSubsemiring.coe_iSup_of_directed dir]

Premises used: NonUnitalSubsemiring.coe_iSup_of_directed, NonUnitalSubalgebra.coe_iSup_of_directed, SetLike.mem_coe, isMulCommutative_iff
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S_1 : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι_1 : Sort u_1
ι : Type u_2
inst_7 : Nonempty ι
inst_8 : Preorder ι
inst_9 : IsDirectedOrder ι
S : OrderHom.{u_2, v} ι (NonUnitalSubalgebra R A)
hS : ∀ (i : ι), IsMulCommutative.{v} ↥((S : (a : ι) → NonUnitalSubalgebra R A) i : NonUnitalSubalgebra R A)
⊢ IsMulCommutative.{v} ↥(⨆ (i : ι), (S : (a : ι) → NonUnitalSubalgebra R A) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, NonUnitalSubalgebra.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
subst : NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(iSup K)) B
⊢ NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥T) B

Tactic:
subst hT
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
let :
  ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
    Eq.{w + 1} (α := B)
      ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
      ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))

Tactic:
let ⟨k, hik, hjk⟩ := dir i j
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
simp :
  Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
⊢ Eq.{w + 1} (α := B)
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) i
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x) x hxi))
    ((fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ ((f i : (a : ↥(K i)) → B) x : B)) j
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x) x hxj))

Tactic:
simp only
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
rw :
  Eq.{w + 1} (α := B)
    (((f k).comp (inclusion hik) : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    (((f k).comp (inclusion hjk) : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)
⊢ Eq.{w + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)

Tactic:
rw [hf i k hik, hf j k hjk]
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) i) x
hxj : Membership.mem (γ := Set A) ((fun (i : ι) ↦ (↑(K i) : Set A)) j) x
k : ι
hik : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) (K j) (K k)
⊢ Eq.{w + 1} (α := B)
    (((f k).comp (inclusion hik) : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A)) x hxi) : B)
    (((f k).comp (inclusion hjk) : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K j) : Set A)) x hxj) : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
rw rw₁ : Subset.{v} (α := Set A) (⋃ (i : ι), (↑(K i) : Set A)) (⋃ (i : ι), (↑(K i) : Set A))
⊢ (↑(iSup K) : Set A) ⊆ ⋃ (i : ι), (↑(K i) : Set A)

Tactic:
rw [coe_iSup_of_directed dir]

Premises used: NonUnitalSubalgebra.coe_iSup_of_directed
-- Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
S : NonUnitalSubalgebra R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
ι : Sort u_1
inst_7 : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → NonUnitalAlgHom.{u, u, v, w} (MonoidHom.id R) (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
r : R
dsimp :
  ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (r • x) =
      HSMul.hSMul (β := B) r
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)
⊢ ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
        (↑(iSup K) : Set A) ⋯ (r • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) r : R)
        (Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type v)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
          (↑(iSup K) : Set A) ⋯ x)

Tactic:
dsimp