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
ι : 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
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)
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext
-- 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 : ι
h : K i ≤ T
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:
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
ι : 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
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) (Subtype.mk (p := fun (x : A) ↦ x ∈ T) (↑x : A) hx) : 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)
hx : (↑x : A) ∈ T
rw rw₁ : Eq.{u_3 + 1} (α := B) ((f i : (a : ↥(K i)) → B) x : B) ((f i : (a : ↥(K i)) → B) x : B)
⊢ 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_mk]

Premises used: Set.iUnionLift_mk
-- 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 : ↥T
hx : (↑x : A) ∈ K i
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) ⋯ (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)
⊢ 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)

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 : ↥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₁ : ι
hx₁ : (↑(Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) : A) ∈ (↑(K i) : Set A)
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₂ : ι
hx₂ : (↑(Set.inclusion (s := (↑T : Set A)) (t := (↑(iSup K) : Set A)) hT x) : A) ∈ (↑(K i) : 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) ⋯ (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:
rw [Set.iUnionLift_of_mem]

Premises used: Set.iUnionLift_of_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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
⊢ FiniteDimensional F A

Tactic:
haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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 = ⊤

Tactic:
(hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_

Premises used: Membership.mem, Nat.Prime.eq_one_or_self_of_dvd, Subtype, Module.finrank_mul_finrank, Exists.intro, Or.imp, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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 = ⊥
refine_2 : ∀ (h : finrank.{u_1, u_2} F ↥K = finrank F A), K = ⊤
⊢ K = ⊥ ∨ K = ⊤

Tactic:
refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_

Premises used: Membership.mem, Nat.Prime.eq_one_or_self_of_dvd, Subtype, Module.finrank_mul_finrank, Exists.intro, Or.imp, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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
⊢ finrank.{u_1, u_2} F ↥K = 1 → K = ⊥

Tactic:
fun h' => Subalgebra.eq_bot_of_finrank_one h'

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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
⊢ finrank.{u_1, u_2} F ↥K = 1 → K = ⊥

Tactic:
exact fun h' => Subalgebra.eq_bot_of_finrank_one h'

Premises used: Subalgebra.eq_bot_of_finrank_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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
h : finrank.{u_1, u_2} F ↥K = finrank F A
⊢ K = ⊤

Tactic:
Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h)

Premises used: Subalgebra.finrank_toSubmodule, Algebra.toSubmodule_eq_top, Iff.mp, Eq.trans, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
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
h : finrank.{u_1, u_2} F ↥K = finrank F A
⊢ K = ⊤

Tactic:
exact
          Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h)

Premises used: Subalgebra.finrank_toSubmodule, Algebra.toSubmodule_eq_top, Iff.mp, Eq.trans, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ GaloisConnection (β := Subalgebra R A) (adjoin R) SetLike.coe

Tactic:
fun s S =>
  ⟨fun H => le_trans (le_trans Set.subset_union_right Subsemiring.subset_closure) H,
   fun H => show Subsemiring.closure (Set.range (algebraMap R A) ∪ s) ≤ S.toSubsemiring from
      Subsemiring.closure_le.2 <| Set.union_subset S.range_subset H⟩

Premises used: Iff.mpr, Subsemiring.closure_le, Set.subset_union_right, Subsemiring.subset_closure, Set.union_subset, Subalgebra.range_subset, Iff.intro, le_trans, GaloisConnection
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 = adjoin R ((↑S : Set A) ∪ (↑T : Set A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ sSup S = adjoin R (⋃₀ (SetLike.coe '' S))

Tactic:
rfl

Premises used: Set.sUnion, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ (↑⊤ : Set A) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ Membership.mem (γ := Subalgebra R A) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{v + 1} (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) ⊤ : Submodule R A)
    (⊤ : Submodule R A)

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{v + 1} (α := Subsemiring A) (Subalgebra.toSubsemiring.{u, v} (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
⊢ Eq.{u_2 + 1} (α := Subring A) (Subalgebra.toSubring.{u_1, u_2} (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Eq (α := Submodule R A) ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      (⊤ : Submodule R A) ↔
    S = ⊤

Tactic:
Subalgebra.toSubmodule.injective.eq_iff' top_toSubmodule

Premises used: RelEmbedding.injective, Algebra.top_toSubmodule, Function.Injective.eq_iff', Subalgebra.toSubmodule
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.toSubsemiring = ⊤ ↔ S = ⊤

Tactic:
Subalgebra.toSubsemiring_injective.eq_iff' top_toSubsemiring

Premises used: Function.Injective.eq_iff', Algebra.top_toSubsemiring, Subalgebra.toSubsemiring_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.toSubring = ⊤ ↔ S = ⊤

Tactic:
Subalgebra.toSubring_injective.eq_iff' top_toSubring

Premises used: Subalgebra.toSubring_injective, Function.Injective.eq_iff', Algebra.top_toSubring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
⊢ x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left; (this ·)

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
⊢ x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right; (this ·)

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x y : A
hx : x ∈ S
hy : y ∈ T
⊢ x * y ∈ S ⊔ T

Tactic:
(S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)

Premises used: Subalgebra.mul_mem, Algebra.mem_sup_left, Max.max, Algebra.mem_sup_right
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S T : Subalgebra R A
⊢ Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T

Tactic:
(Subalgebra.gc_map_comap f).l_sup

Premises used: Subalgebra.gc_map_comap, GaloisConnection.l_sup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
S T : Subalgebra R A
⊢ Subalgebra.map f (S ⊓ T) = Subalgebra.map f S ⊓ Subalgebra.map f T

Tactic:
SetLike.coe_injective (Set.image_inter hf)

Premises used: Set.image_inter, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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) : Set A) = (↑S : Set A) ∩ (↑T : Set A)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : A
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) (S ⊓ T) : Submodule R A)
    ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S ⊓ (toSubmodule : (a : Subalgebra R A) → Submodule R A) T :
      Submodule R A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
rw : (S ⊔ T).toSubsemiring = Subsemiring.closure ((↑S.toSubsemiring : Set A) ∪ (↑T.toSubsemiring : Set A))
⊢ (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

Tactic:
rw [← S.toSubsemiring.closure_eq, ← T.toSubsemiring.closure_eq, ← Subsemiring.closure_union]

Premises used: Subalgebra.toSubsemiring, Subsemiring.closure_eq, Subsemiring.closure_union
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
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)
⊢ 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)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ (↑S : Set A) ∪ (↑T : Set 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)

Tactic:
rw [Set.union_eq_right]

Premises used: Set.union_eq_right
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : R
⊢ Membership.mem (α := A) ((↑S : Set A) ∪ (↑T : Set A)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
Set.mem_union_left _ (algebraMap_mem S x)

Premises used: algebraMap_mem, Set.mem_union_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x : R
⊢ Membership.mem (α := A) ((↑S : Set A) ∪ (↑T : Set A)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

Premises used: algebraMap_mem, Set.mem_union_left
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ (↑(sInf S) : Set A) = ⋂ s ∈ S, (↑s : Set A)

Tactic:
sInf_image

Premises used: Set.iInter, setOf, sInf_image
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Premises used: Set.mem_iInter₂, SetLike.mem_coe, Algebra.coe_sInf
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ (↑((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (sInf S) : Submodule R A) : Set A) =
    (↑(sInf ((⇑Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) '' S)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ (↑(sInf S).toSubsemiring : Set A) = (↑(sInf (Subalgebra.toSubsemiring '' S)) : Set A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
rw : toSubsemiring '' S = (fun (x : Subalgebra R A) ↦ Subsemiring.closure (↑x : Set A)) '' S
⊢ toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S

Tactic:
rw [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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 : ∀ x ∈ S, x.toSubsemiring = Subsemiring.closure (↑x : Set A)
⊢ toSubsemiring '' S = (fun (x : Subalgebra R A) ↦ Subsemiring.closure (↑x : Set A)) '' S

Tactic:
congr! with x
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
x : Subalgebra R A
h : x ∈ S
⊢ x.toSubsemiring = Subsemiring.closure (↑x : Set A)

Tactic:
x.toSubsemiring.closure_eq.symm

Premises used: Subalgebra.toSubsemiring, Subsemiring.closure_eq, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
x : Subalgebra R A
h : x ∈ S
⊢ x.toSubsemiring = Subsemiring.closure (↑x : Set A)

Tactic:
exact x.toSubsemiring.closure_eq.symm

Premises used: Subalgebra.toSubsemiring, Subsemiring.closure_eq, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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

Tactic:
have h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubsemiring.closure_eq.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
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)))
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]

Premises used: Algebra.sSup_def, Subsemiring.closure_sUnion, sSup_image, Algebra.adjoin_toSubsemiring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (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)))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
e_s : Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ⊆ ⋃₀ (SetLike.coe '' S)
⊢ Set.range.{v, u + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
rw [Set.union_eq_right]

Premises used: Set.union_eq_right
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
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
x : R
e_s :
  ∀ (y : Subalgebra R A) (hy : y ∈ S),
    Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)
⊢ Membership.mem (α := A) (⋃₀ (SetLike.coe '' S)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
obtain ⟨y, hy⟩ := hS