awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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) :=
  ⋯
⊢ ∀ (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
have 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) sorry (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) sorry 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) sorry y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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) :=
  ⋯
⊢ ∀ (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
have hopi : ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
  Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry (x * y) =
    HMul.hMul (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry x)
      (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry y)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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)
⊢ ∀ (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
have 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)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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) :=
  ⋯
⊢ ∀ (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
have 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) sorry (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) sorry 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) sorry y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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) :=
  ⋯
⊢ ∀ (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
have hopi : ∀ (i : ι) (x y : (↑(↑(K i) : Set A) : Type u_2)),
  Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry (x + y) =
    HAdd.hAdd (α := ↥(iSup K)) (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry x)
      (Set.inclusion (s := (↑(K i) : Set A)) (t := (↑(iSup K) : Set A)) sorry y)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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)
⊢ ∀ (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
have 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)
Tactic: apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· + ·))
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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
⊢ 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)
have dsimp : Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
    (↑(iSup K) : Set A) sorry (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(iSup K) : Set A)) (↑x : A) sorry) =
  (f i : (a : ↥(K i)) → B) x
Tactic: dsimp [iSupLift, inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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
⊢ 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
have h₁ : (↑(K i) : Set A) ⊆ (↑(iSup K) : Set A)
Tactic: rw [Set.iUnionLift_inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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 : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i
have H : ∀ (x : ↥(K i)),
  Eq.{u_3 + 1} (α := B) (((iSupLift K dir f hf T hT).comp (inclusion h) : (a : ↥(K i)) → B) x : B)
    ((f i : (a : ↥(K i)) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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)
hx : (↑x : A) ∈ T
⊢ Eq.{u_3 + 1} (α := B)
    ((iSupLift K dir f hf T hT : (a : ↥T) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ T) (↑x : A) hx) : B)
    ((f i : (a : ↥(K i)) → B) x : B)
have dsimp : Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
    (↑(iSup K) : Set A) sorry (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(iSup K) : Set A)) (↑x : A) sorry) =
  (f i : (a : ↥(K i)) → B) x
Tactic: dsimp [iSupLift, inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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)
hx : (↑x : A) ∈ T
⊢ 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
have rw : Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) x : B)
Tactic: rw [Set.iUnionLift_mk]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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 : ↥T
hx : (↑x : A) ∈ K i
⊢ Eq.{u_3 + 1} (α := B) ((iSupLift K dir f hf T hT : (a : ↥T) → B) x : B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
have dsimp : Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) sorry
    (↑(iSup K) : Set A) sorry (Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) =
  (f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx)
Tactic: dsimp [iSupLift, inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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 : ↥T
hx : (↑x : A) ∈ K i
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
      (↑(iSup K) : Set A) ⋯ (Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) =
    (f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx)
have rw : Eq.{u_3 + 1} (α := B)
  ((f i : (a : ↥(K i)) → B)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A))
        (↑(Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) : A) hx) :
    B)
  ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
Tactic: rw [Set.iUnionLift_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Directed (goal)
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 : ↥T
hx : (↑x : A) ∈ K i
rw :
  Eq.{u_3 + 1} (α := B)
    ((f i : (a : ↥(K i)) → B)
        (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑(K i) : Set A))
          (↑(Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) : A) hx) :
      B)
    ((f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx) : B)
i₁ : ι
⊢ Set.iUnionLift (fun (i : ι) ↦ (↑(K i) : Set A)) (fun (i : ι) (x : ↥(K i)) ↦ (f i : (a : ↥(K i)) → B) x) ⋯
      (↑(iSup K) : Set A) ⋯ (Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) =
    (f i : (a : ↥(K i)) → B) (Subtype.mk (p := fun (x : A) ↦ x ∈ K i) (↑x : A) hx)
have hx₁ : (↑(Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) : A) ∈ (↑(K i) : Set A)
Tactic: rw [Set.iUnionLift_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder (hypothesis)
Goal:
F : Type u_1
A : Type u_2
inst : Field F
inst_1 : Ring A
inst_2 : IsDomain A
inst_3 : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
⊢ K = ⊥ ∨ K = ⊤
have this : FiniteDimensional F A
Tactic: haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder (goal)
Goal:
F : Type u_1
A : Type u_2
inst : Field F
inst_1 : Ring A
inst_2 : IsDomain A
inst_3 : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this_1 : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ K = ⊥ ∨ K = ⊤
have refine_1 : finrank.{u_1, u_2} F ↥K = 1 → K = ⊥
Tactic: refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder (goal)
Goal:
F : Type u_1
A : Type u_2
inst : Field F
inst_1 : Ring A
inst_2 : IsDomain A
inst_3 : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this_1 : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
refine_1 : finrank.{u_1, u_2} F ↥K = 1 → K = ⊥
⊢ K = ⊥ ∨ K = ⊤
have refine_2 : ∀ (h : finrank.{u_1, u_2} F ↥K = finrank F A), K = ⊤
Tactic: refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
⊢ (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring
have rw : (S ⊔ T).toSubsemiring = Subsemiring.closure ((↑S.toSubsemiring : Set A) ∪ (↑T.toSubsemiring : Set A))
Tactic: rw [← S.toSubsemiring.closure_eq, ← T.toSubsemiring.closure_eq, ← Subsemiring.closure_union]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
⊢ Eq (α := Subsemiring A)
    (Subsemiring.closure
      (Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ((↑S : Set A) ∪ (↑T : Set A))))
    (Subsemiring.closure ((↑S : Set A) ∪ (↑T : Set A)))
have e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ((↑S : Set A) ∪ (↑T : Set A)) =
  (↑S : Set A) ∪ (↑T : Set A)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
⊢ Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ((↑S : Set A) ∪ (↑T : Set A)) =
    (↑S : Set A) ∪ (↑T : Set A)
have e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ (↑S : Set A) ∪ (↑T : Set A)
Tactic: rw [Set.union_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
have rw : toSubsemiring '' S = (fun (x : Subalgebra R A) ↦ Subsemiring.closure (↑x : Set A)) '' S
Tactic: rw [Set.image_image]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = (fun (x : Subalgebra R A) ↦ Subsemiring.closure (↑x : Set A)) '' S
have h : ∀ x ∈ S, x.toSubsemiring = Subsemiring.closure (↑x : Set A)
Tactic: congr! with x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)
have h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
Tactic: have h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubsemiring.closure_eq.symm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)
have rw : Eq (α := Subsemiring A)
  (Subsemiring.closure (Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S)))
  (Subsemiring.closure (⋃₀ (SetLike.coe '' S)))
Tactic: rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Lattice (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
⊢ Eq (α := Subsemiring A)
    (Subsemiring.closure (Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S)))
    (Subsemiring.closure (⋃₀ (SetLike.coe '' S)))
have e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
Tactic: congr 1