awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ (↑(K i) : Set A)
hxj : x ∈ (↑(K j) : Set A)
rcases :
  ∀ (k : ι) (hik : K i ≤ K k) (hjk : K j ≤ K k),
    Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
      ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B)
⊢ Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B)

Tactic:
rcases dir i j with ⟨k, hik, hjk⟩
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ (↑(K i) : Set A)
hxj : x ∈ (↑(K j) : Set A)
k : ι
hik : K i ≤ K k
hjk : K j ≤ K k
⊢ Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B)

Tactic:
simp [hf i k hik, hf j k hjk]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι), Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) ((fun (i : ι) ↦ (1 : ↥(K i))) i) : B) (1 : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
      (↑(iSup K) : Set A) ⋯ 1 =
    1

Tactic:
exact Set.iUnionLift_const _ (fun i : ι => (1 : K i)) (fun _ => rfl) _ (by simp)

Premises used: Set.iUnionLift_const, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
dsimp :
  ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x * y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x *
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x * y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x *
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y

Tactic:
dsimp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
hopi :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x * y) =
      HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)
h :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    (f i : (a : ↥(K i)) → B) (x * y) =
      HMul.hMul (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x * y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x *
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y

Tactic:
apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))

Premises used: Subalgebra.coe_iSup_of_directed, HMul.hMul, Set.iUnionLift_binary
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x * y) =
      HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    (f i : (a : ↥(K i)) → B) (x * y) =
      HMul.hMul (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι), Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) ((fun (i : ι) ↦ (0 : ↥(K i))) i) : B) (0 : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
      (↑(iSup K) : Set A) ⋯ 0 =
    0

Tactic:
exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

Premises used: Set.iUnionLift_const, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
dsimp :
  ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x + y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x +
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x + y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x +
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
          (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y

Tactic:
dsimp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
hopi :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x + y) =
      HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)
h :
  ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    (f i : (a : ↥(K i)) → B) (x + y) =
      HAdd.hAdd (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯ (x + y) =
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ x +
        Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
          (↑(iSup K) : Set A) ⋯ y

Tactic:
apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))

Premises used: Subalgebra.coe_iSup_of_directed, HAdd.hAdd, Set.iUnionLift_binary
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ (x + y) =
      HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ x)
        (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) ⋯ y)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
⊢ ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
    (f i : (a : ↥(K i)) → B) (x + y) =
      HAdd.hAdd (α := B) (β := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) y : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
r : R
⊢ ∀ (i : ι),
    Eq.{u_3 + 1} (α := B)
      ((f i : (a : ↥(K i)) → B) ((fun (i : ι) ↦ ((algebraMap R ↥(K i) : (a : R) → ↥(K i)) r : ↥(K i))) i) : B)
      ((algebraMap R B : (a : R) → B) r : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
r : R
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) compat
      (↑(iSup K) : Set A) ⋯ ((algebraMap R ↥(iSup K) : (a : R) → ↥(iSup K)) r) =
    (algebraMap R B : (a : R) → B) r

Tactic:
exact
          Set.iUnionLift_const _ (fun i : ι => algebraMap R (K i) r) (fun _ => rfl) _ (by simp)

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Set.iUnionLift_const, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ (↑(K i) : Set A)) (hxj : x ∈ (↑(K j) : Set A)),
  Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) x hxi) : B)
    ((f j : (a : ↥(K j)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K j) x hxj) : B) :=
  ⋯
liftSup : AlgHom.{u_1, u_2, u_3} R (↥(iSup K)) B :=
  {
    toFun :=
      Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A))
        (fun (i : ι) (x : (↑((fun (i : ι) ↦ (↑(K i) : Set A)) i) : Type u_2)) ↦ (f i : (a : ↥(K i)) → B) x) compat
        (↑(iSup K) : Set A) ⋯,
    map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ AlgHom.{u_1, u_2, u_3} R (↥T) B

Tactic:
exact liftSup.comp (inclusion hT)

Premises used: Subalgebra.inclusion, AlgHom.comp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
dsimp :
  Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
      (↑(iSup K) : Set A) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(iSup K) : Set A)) (↑x : A) ⋯) =
    (f i : (a : ↥(K i)) → B) x
⊢ Eq.{u_3 + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) ((inclusion h : (a : ↥(K i)) → ↥T) x : ↥T) : B)
    ((f i : (a : ↥(K i)) → B) x : B)

Tactic:
dsimp [iSupLift, inclusion]

Premises used: Subalgebra.iSupLift, Subalgebra.inclusion
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
h₁ : (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
      (↑(iSup K) : Set A) ⋯ (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(iSup K) : Set A)) (↑x : A) ⋯) =
    (f i : (a : ↥(K i)) → B) x

Tactic:
rw [Set.iUnionLift_inclusion]

Premises used: Set.iUnionLift_inclusion
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
SetLike.coe_subset_coe.mpr <| h.trans hT

Premises used: Iff.mpr, SetLike.coe_subset_coe, LE.le.trans
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Directed
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
ι : Type u_4
inst_5 : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun (x1 x2 : Subalgebra R A) ↦ x1 ≤ x2) K
f : (i : ι) → AlgHom.{u_1, u_2, u_3} R (↥(K i)) B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)

Tactic:
exact SetLike.coe_subset_coe.mpr <| h.trans hT

Premises used: Iff.mpr, SetLike.coe_subset_coe, LE.le.trans