awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
a : comap f (map f S) ≤ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
a₁ : S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ comap f (map f S)
⊢ comap f (map f S) = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ ∃ x_1 ∈ S, Eq.{uB + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) x : B)

Tactic:
rw [mem_comap, mem_map] at hx

Premises used: Subalgebra.mem_map, Subalgebra.mem_comap
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : ∃ x_1 ∈ S, Eq.{uB + 1} (α := B) ((f : (a : A) → B) x_1 : B) ((f : (a : A) → B) x : B)
a :
  ∀ (y : A) (hy : y ∈ S) (hxy : Eq.{uB + 1} (α := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)),
    x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})

Tactic:
obtain ⟨y, hy, hxy⟩ := hx
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Eq.{uB + 1} (α := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)

Tactic:
simp [hxy]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Eq.{uB + 1} (α := B) ((f : (a : A) → B) y : B) ((f : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)

Tactic:
replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)
a :
  Membership.mem (γ := Subalgebra R A) (adjoin R ((↑S : Set A) ∪ Set.preimage (β := B) (⇑f : (a : A) → B) {0}))
    (y + (x - y))
⊢ x ∈ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})

Tactic:
rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]

Premises used: Algebra.adjoin_union, add_sub_cancel, Algebra.adjoin_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R ((↑S : Set A) ∪ Set.preimage (β := B) (⇑f : (a : A) → B) {0}))
    (y + (x - y))

Tactic:
Subalgebra.add_mem _
      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)

Premises used: Set.Mem, Subalgebra.add_mem, Algebra.subset_adjoin, Or.inl, Or.inr
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : Membership.mem (γ := Set A) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) (x - y)
⊢ Membership.mem (γ := Subalgebra R A) (adjoin R ((↑S : Set A) ∪ Set.preimage (β := B) (⇑f : (a : A) → B) {0}))
    (y + (x - y))

Tactic:
exact Subalgebra.add_mem _
      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
a :
  map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) ≤
    map f S
⊢ S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ comap f (map f S)

Tactic:
rw [← map_le, Algebra.map_sup, f.map_adjoin]

Premises used: Algebra.map_sup, AlgHom.map_adjoin, Subalgebra.map_le
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
a :
  map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) =
    map f S
⊢ map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) ≤
    map f S

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
a : Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ⊆ (↑(map f S) : Set B)
⊢ map f S ⊔ adjoin R (Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0})) =
    map f S

Tactic:
rw [sup_eq_left, Algebra.adjoin_le_iff]

Premises used: sup_eq_left, Algebra.adjoin_le_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ⊆ (↑(map f S) : Set B)

Tactic:
(Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)

Premises used: Iff.mpr, Set.singleton_subset_iff, Subalgebra.zero_mem, HasSubset.Subset.trans, Subalgebra.map, Set.image_preimage_subset, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ Set.image.{uA, uB} (α := A) (⇑f : (a : A) → B) (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ⊆ (↑(map f S) : Set B)

Tactic:
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)

Premises used: Iff.mpr, Set.singleton_subset_iff, Subalgebra.zero_mem, HasSubset.Subset.trans, Subalgebra.map, Set.image_preimage_subset, Singleton.singleton, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
⊢ comap f (map f S) = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})

Tactic:
comap_map_eq f S

Premises used: Subalgebra.comap_map_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
h₁ : S = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})
⊢ comap f (map f S) = S

Tactic:
convert! comap_map_eq f S

Premises used: Subalgebra.comap_map_eq
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
h : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
h₁ : adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0}) ≤ S
h₂ h₃ h₄ h₅ : Set.preimage (β := B) (⇑f : (a : A) → B) {0} ⊆ (↑S : Set A)
⊢ S = S ⊔ adjoin R (Set.preimage (β := B) (⇑f : (a : A) → B) {0})

Tactic:
rwa [left_eq_sup, Algebra.adjoin_le_iff]

Premises used: Algebra.adjoin_le_iff, left_eq_sup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : Aᵐᵒᵖ
S : Subalgebra R A
⊢ x ∈ S.op ↔ MulOpposite.unop x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
S : Subalgebra R Aᵐᵒᵖ
⊢ x ∈ S.unop ↔ MulOpposite.op x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.op.unop = S

Tactic:
rfl

Premises used: Subalgebra.unop, Set.Mem, setOf, Set.preimage, MulOpposite.unop, Subsemiring.unop, Submonoid.unop, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R Aᵐᵒᵖ
⊢ S.unop.op = S

Tactic:
rfl

Premises used: Set.Mem, Submonoid.op, MulOpposite, setOf, Subalgebra.op, Set.preimage, Subsemiring.op, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ : Subalgebra R A
S₂ : Subalgebra R Aᵐᵒᵖ
⊢ S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ : Subalgebra R Aᵐᵒᵖ
S₂ : Subalgebra R A
⊢ S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R A
⊢ S₁.op ≤ S₂.op ↔ S₁ ≤ S₂

Tactic:
MulOpposite.op_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, setOf, Set.preimage, MulOpposite.unop, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R Aᵐᵒᵖ
⊢ S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂

Tactic:
MulOpposite.unop_surjective.forall

Premises used: Function.Surjective.forall, Set.Mem, MulOpposite, setOf, Set.preimage, MulOpposite.unop, MulOpposite.unop_surjective, MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := Subalgebra R Aᵐᵒᵖ) (Subalgebra.op ⊥) ⊥

Tactic:
opEquiv.map_bot

Premises used: Subalgebra.opEquiv, Subalgebra.op, OrderIso.map_bot
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := Subalgebra R A) (Subalgebra.unop ⊥) ⊥

Tactic:
opEquiv.symm.map_bot

Premises used: Subalgebra.unop, Subalgebra.opEquiv, OrderIso.symm, OrderIso.map_bot
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := Subalgebra R Aᵐᵒᵖ) (Subalgebra.op ⊤) ⊤

Tactic:
opEquiv.map_top

Premises used: Subalgebra.opEquiv, Subalgebra.op, OrderIso.map_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_3 + 1} (α := Subalgebra R A) (Subalgebra.unop ⊤) ⊤

Tactic:
opEquiv.symm.map_top

Premises used: Subalgebra.unop, Subalgebra.opEquiv, OrderIso.symm, OrderIso.map_top
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R A
⊢ (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op

Tactic:
opEquiv.map_sup _ _

Premises used: Subalgebra.opEquiv, Subalgebra.op, OrderIso.map_sup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R Aᵐᵒᵖ
⊢ (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop

Tactic:
opEquiv.symm.map_sup _ _

Premises used: Subalgebra.unop, Subalgebra.opEquiv, OrderIso.symm, OrderIso.map_sup
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R A
⊢ (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op

Tactic:
opEquiv.map_inf _ _

Premises used: OrderIso.map_inf, Subalgebra.opEquiv, Subalgebra.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S₁ S₂ : Subalgebra R Aᵐᵒᵖ
⊢ (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop

Tactic:
opEquiv.symm.map_inf _ _

Premises used: Subalgebra.unop, OrderIso.map_inf, Subalgebra.opEquiv, OrderIso.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ (sSup S).op = sSup (Subalgebra.unop ⁻¹' S)

Tactic:
opEquiv.map_sSup_eq_sSup_symm_preimage _

Premises used: Subalgebra.unop, Set.Mem, setOf, Subalgebra.opEquiv, OrderIso.map_sSup_eq_sSup_symm_preimage, Subalgebra.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R A)
⊢ (sInf S).op = sInf (Subalgebra.unop ⁻¹' S)

Tactic:
opEquiv.map_sInf_eq_sInf_symm_preimage _

Premises used: Subalgebra.unop, Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, setOf, Subalgebra.opEquiv, Subalgebra.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Set (Subalgebra R Aᵐᵒᵖ)
⊢ (sInf S).unop = sInf (Subalgebra.op ⁻¹' S)

Tactic:
opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

Premises used: Subalgebra.unop, Set.Mem, OrderIso.map_sInf_eq_sInf_symm_preimage, setOf, Subalgebra.opEquiv, Subalgebra.op, OrderIso.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : ι → Subalgebra R A
⊢ (iSup S).op = ⨆ (i : ι), (S i).op

Tactic:
opEquiv.map_iSup _

Premises used: OrderIso.map_iSup, Subalgebra.opEquiv, Subalgebra.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : ι → Subalgebra R Aᵐᵒᵖ
⊢ (iSup S).unop = ⨆ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iSup _

Premises used: Subalgebra.unop, OrderIso.map_iSup, Subalgebra.opEquiv, OrderIso.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : ι → Subalgebra R A
⊢ (iInf S).op = ⨅ (i : ι), (S i).op

Tactic:
opEquiv.map_iInf _

Premises used: Subalgebra.opEquiv, OrderIso.map_iInf, Subalgebra.op
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
ι : Sort u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : ι → Subalgebra R Aᵐᵒᵖ
⊢ (iInf S).unop = ⨅ (i : ι), (S i).unop

Tactic:
opEquiv.symm.map_iInf _

Premises used: Subalgebra.unop, Subalgebra.opEquiv, OrderIso.map_iInf, OrderIso.symm
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
a :
  Eq (α := Subsemiring Aᵐᵒᵖ) (toSubsemiring (Subalgebra.op (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)))
⊢ Eq (α := Subalgebra R Aᵐᵒᵖ) (Subalgebra.op (Algebra.adjoin R s)) (Algebra.adjoin R (MulOpposite.unop ⁻¹' s))

Tactic:
apply toSubsemiring_injective

Premises used: Subalgebra.toSubsemiring_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
a :
  Eq (α := Subsemiring Aᵐᵒᵖ)
    (Subsemiring.closure
      (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪
        MulOpposite.unop ⁻¹' s))
    (Subsemiring.closure
      (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s))
⊢ Eq (α := Subsemiring Aᵐᵒᵖ) (toSubsemiring (Subalgebra.op (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)))

Tactic:
simp_rw [Algebra.adjoin, op_toSubsemiring, Subsemiring.op_closure, Set.preimage_union]

Premises used: Subalgebra.op_toSubsemiring, Algebra.adjoin, Subsemiring.op_closure, Set.preimage_union
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
a :
  ∀ (x : Aᵐᵒᵖ),
    Membership.mem (γ := Set Aᵐᵒᵖ)
        (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x ↔
      Membership.mem (γ := Set Aᵐᵒᵖ) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ)) x
⊢ Eq (α := Subsemiring Aᵐᵒᵖ)
    (Subsemiring.closure
      (MulOpposite.unop ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪
        MulOpposite.unop ⁻¹' s))
    (Subsemiring.closure
      (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s))

Tactic:
congr with x
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : Aᵐᵒᵖ
a :
  ∀ (x_1 : R),
    (algebraMap R A : (a : R) → A) x_1 = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
⊢ (∃ (y : R), (algebraMap R A : (a : R) → A) y = MulOpposite.unop x) ↔
    ∃ (y : R), MulOpposite.op ((algebraMap R A : (a : R) → A) y) = x

Tactic:
congr!
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x_1 : R
a :
  MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = MulOpposite.op (MulOpposite.unop x) ↔
    MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
a₁ a₂ :
  MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x
⊢ (algebraMap R A : (a : R) → A) x_1 = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A : (a : R) → A) x_1) = x

Tactic:
rw [← MulOpposite.op_injective.eq_iff (b := x.unop), MulOpposite.op_unop]

Premises used: MulOpposite.op_injective, MulOpposite.op_unop, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
a :
  Eq (α := Subsemiring A) (toSubsemiring (Subalgebra.unop (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.op ⁻¹' s)))
⊢ Eq (α := Subalgebra R A) (Subalgebra.unop (Algebra.adjoin R s)) (Algebra.adjoin R (MulOpposite.op ⁻¹' s))

Tactic:
apply toSubsemiring_injective

Premises used: Subalgebra.toSubsemiring_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
a :
  Eq (α := Subsemiring A)
    (Subsemiring.closure
      (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪
        MulOpposite.op ⁻¹' s))
    (Subsemiring.closure (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ MulOpposite.op ⁻¹' s))
⊢ Eq (α := Subsemiring A) (toSubsemiring (Subalgebra.unop (Algebra.adjoin R s)))
    (toSubsemiring (Algebra.adjoin R (MulOpposite.op ⁻¹' s)))

Tactic:
simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]

Premises used: Subsemiring.unop_closure, Algebra.adjoin, Set.preimage_union, Subalgebra.unop_toSubsemiring
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
a :
  ∀ (x : A),
    Membership.mem (γ := Set A)
        (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ)) x ↔
      Membership.mem (γ := Set A) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x
⊢ Eq (α := Subsemiring A)
    (Subsemiring.closure
      (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ) ∪
        MulOpposite.op ⁻¹' s))
    (Subsemiring.closure (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A) ∪ MulOpposite.op ⁻¹' s))

Tactic:
congr with x
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set Aᵐᵒᵖ
x : A
⊢ Membership.mem (γ := Set A)
      (MulOpposite.op ⁻¹' Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R Aᵐᵒᵖ) : (a : R) → Aᵐᵒᵖ)) x ↔
    Membership.mem (γ := Set A) (Set.range.{u_3, u_2 + 1} (ι := R) (⇑(algebraMap R A) : (a : R) → A)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
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.op.toSubring = S.toSubring.op

Tactic:
rfl

Premises used: Subring.op, Subsemiring.op, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
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.unop.toSubring = Subring.unop S.toSubring

Tactic:
rfl

Premises used: Subring.unop, Subsemiring.unop, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
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
f : A →ₐ[R] B
⊢ Eq (α := Ideal A) (RingHom.ker f.rangeRestrict) (RingHom.ker f)

Tactic:
Ideal.ext fun _ ↦ Subtype.ext_iff

Premises used: Ideal.ext, Subtype.ext_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Operations
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : Eq.{u_2 + 1} (α := S) (∑ i ∈ ι', l i * s i) 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
H : ∀ (i : ι), ∃ (n : ℕ), s i ^ n • x ∈ S'
this :
  Membership.mem (γ := Submodule (↥S') S)
    ((toSubmodule : (a : Subalgebra (↥S') S) → Submodule (↥S') S) (AlgHom.range (ofId (↥S') S)) : Submodule (↥S') S) x
obtain :
  ∀ (x : ↥S')
    (H :
      ∀ (i : ι),
        ∃ (n : ℕ), HSMul.hSMul (β := S) (s i ^ n) ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S) ∈ S'),
    Membership.mem (α := S) S' ((AlgHom.toRingHom (ofId (↥S') S) : (a : ↥S') → S) x : S)
⊢ x ∈ S'

Tactic:
obtain ⟨x, rfl⟩ := this

Premises used: rfl