awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Eq.{v + 1} (α := A) (↑1 : A) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ (↑(-x) : A) = -(↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S : Subalgebra R A
x y : ↥S
⊢ (↑(x - y) : A) = (↑x : A) - (↑y : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
inst_3 : SMul R' R
inst_4 : SMul R' A
inst_5 : IsScalarTower R' R A
r : R'
x : ↥S
⊢ (↑(r • x) : A) = r • (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
inst_3 : CommSemiring R'
inst_4 : SMul R' R
inst_5 : Algebra R' A
inst_6 : IsScalarTower R' R A
r : R'
⊢ Eq.{v + 1} (α := A) ((↑((algebraMap R' ↥S : (a : R') → ↥S) r) : A) : A) ((algebraMap R' A : (a : R') → A) r : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
n : ℕ
⊢ (↑(x ^ n) : A) = (↑x : A) ^ n

Tactic:
SubmonoidClass.coe_pow x n

Premises used: SubmonoidClass.coe_pow
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ (↑x : A) = 0 ↔ x = 0

Tactic:
ZeroMemClass.coe_eq_zero

Premises used: ZeroMemClass.coe_eq_zero
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ (↑x : A) = 1 ↔ x = 1

Tactic:
OneMemClass.coe_eq_one

Premises used: OneMemClass.coe_eq_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ Eq (α := (a : ↥S) → A) (⇑S.val : (a : ↥S) → A) (Subtype.val (p := fun (x : A) ↦ x ∈ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : ↥S
⊢ (S.val : (a : ↥S) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.subtype = (↑S.val : ↥S →+* A)

Tactic:
rfl

Premises used: Subsemiring.subtype, Set.Mem, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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.subtype = (↑S.val : ↥S →+* A)

Tactic:
rfl

Premises used: Set.Mem, MonoidHomClass.toMonoidHom, Subring.subtype, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
S₁ S₂ : Subalgebra R A
f : A →ₐ[R] B
⊢ S₁ ≤ S₂ → map f S₁ ≤ map f S₂

Tactic:
Set.image_mono

Premises used: Set.Mem, Set.image_mono, setOf, Set.Subset, Set.image
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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)
⊢ Function.Injective (map f)

Tactic:
fun _S₁ _S₂ ih =>
  ext <| Set.ext_iff.1 <| Set.image_injective.2 hf <| Set.ext <| SetLike.ext_iff.mp ih

Premises used: Iff.mpr, Set.ext, Set.image_injective, SetLike.ext_iff, Iff.mp, Subalgebra.ext, Set.ext_iff, Function.Injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ map (AlgHom.id R A) S = S

Tactic:
SetLike.coe_injective <| Set.image_id _

Premises used: SetLike.coe_injective, Set.image_id
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
S : Subalgebra R A
g : B →ₐ[R] C
f : A →ₐ[R] B
⊢ map g (map f S) = map (g.comp f) S

Tactic:
SetLike.coe_injective <| Set.image_image _ _ _

Premises used: Set.image_image, SetLike.coe_injective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
S : Subalgebra R A
f : A →ₐ[R] B
y : B
⊢ y ∈ map f S ↔ ∃ x ∈ S, (f : (a : A) → B) x = y

Tactic:
Subsemiring.mem_map

Premises used: Set.Mem, Subsemiring.mem_map
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
S : Subalgebra R A
f : A →ₐ[R] B
⊢ (toSubmodule : (a : Subalgebra R B) → Submodule R B) (map f S) =
    Submodule.map f.toLinearMap ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S)

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
S : Subalgebra R A
f : A →ₐ[R] B
U : Subalgebra R B
⊢ map f S ≤ U ↔ S ≤ comap f U

Tactic:
Set.image_subset_iff

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.image, Set.image_subset_iff
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
⊢ GaloisConnection (map f) (comap f)

Tactic:
fun _S _U => map_le

Premises used: Subalgebra.map_le, GaloisConnection
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
S : Subalgebra R B
f : A →ₐ[R] B
x : A
⊢ x ∈ comap f S ↔ Membership.mem (α := B) S ((f : (a : A) → B) x : B)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R_1 : Type u
A_1 : Type v
B : Type w
C : Type w'
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : Semiring B
inst_4 : Algebra R_1 B
inst_5 : Semiring C
inst_6 : Algebra R_1 C
S_1 : Subalgebra R_1 A_1
R : Type u_1
A : Type u_2
inst_7 : CommSemiring R
inst_8 : Semiring A
inst_9 : NoZeroDivisors A
inst_10 : Algebra R A
S : Subalgebra R A
⊢ NoZeroDivisors.{u_2} ↥S

Tactic:
inferInstanceAs (NoZeroDivisors S.toSubsemiring)

Premises used: _private.0.Subalgebra.noZeroDivisors._proof_1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R' : Type u'
R_1 : Type u
A_1 : Type v
B : Type w
C : Type w'
inst : CommSemiring R_1
inst_1 : Semiring A_1
inst_2 : Algebra R_1 A_1
inst_3 : Semiring B
inst_4 : Algebra R_1 B
inst_5 : Semiring C
inst_6 : Algebra R_1 C
S_1 : Subalgebra R_1 A_1
R : Type u_1
A : Type u_2
inst_7 : CommRing R
inst_8 : Ring A
inst_9 : IsDomain A
inst_10 : Algebra R A
S : Subalgebra R A
⊢ IsDomain.{u_2} ↥S

Tactic:
inferInstanceAs (IsDomain S.toSubring)

Premises used: _private.0.Subalgebra.isDomain._proof_1
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ Eq.{u_3 + 1} (α := A) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) 1) ⋯) : A) : A)
    ((↑1 : A) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x x_1 : R
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) (x * x_1)) ⋯) : A) =
    (↑(HMul.hMul (α := ↥s) (β := ↥s) (Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) x) ⋯ : ↥s)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) x_1) ⋯ : ↥s)) :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ Eq.{u_3 + 1} (α := A) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) 0) ⋯) : A) : A)
    ((↑0 : A) : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x x_1 : R
⊢ (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) (x + x_1)) ⋯) : A) =
    (↑(HAdd.hAdd (α := ↥s) (β := ↥s) (Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) x) ⋯ : ↥s)
          (Subtype.mk (p := fun (x : A) ↦ x ∈ s) ((algebraMap R A : (a : R) → A) x_1) ⋯ : ↥s)) :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
r : R
⊢ Eq.{u_3 + 1} (α := A) ((↑((algebraMap R ↥s : (a : R) → ↥s) r) : A) : A) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : SetLike S A
inst_4 : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ Eq (α := (a : ↥s) → A) (⇑(val s) : (a : ↥s) → A) (Subtype.val (p := fun (x : A) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p_1 p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
r : R
rw : HSMul.hSMul (β := A) r 1 ∈ p.carrier
⊢ Membership.mem (α := A) p.carrier ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p_1 p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
r : R
⊢ HSMul.hSMul (β := A) r 1 ∈ p.carrier

Tactic:
p.smul_mem _ h_one

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p_1 p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
r : R
⊢ HSMul.hSMul (β := A) r 1 ∈ p.carrier

Tactic:
exact p.smul_mem _ h_one

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
x : A
⊢ x ∈ p.toSubalgebra h_one h_mul ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
rw :
  HSMul.hSMul (β := A) r 1 ∈
    { carrier := (↑s : Set A), mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ : Subsemiring A }.carrier
⊢ Membership.mem (α := A)
    { carrier := (↑s : Set A), mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ : Subsemiring A }.carrier
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ HSMul.hSMul (β := A) r 1 ∈
    { carrier := (↑s : Set A), mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ : Subsemiring A }.carrier

Tactic:
apply s.smul_mem _ h1

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
⊢ s.toSubalgebra h1 hmul =
    { carrier := (↑s : Set A), mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Tactic:
rfl

Premises used: Submodule.toSubalgebra, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : Submodule R A
h_one : 1 ∈ p
h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p
⊢ (Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) (p.toSubalgebra h_one h_mul) = p

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ toSubalgebra ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) S) ⋯ ⋯ = S

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
φ : A →ₐ[R] B
y : B
⊢ y ∈ φ.range ↔ ∃ (x : A), (φ : (a : A) → B) x = y

Tactic:
RingHom.mem_rangeS

Premises used: Set.Mem, RingHom.mem_rangeS
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
φ : A →ₐ[R] B
x : A
⊢ Membership.mem (α := B) φ.range ((φ : (a : A) → B) x : B)

Tactic:
φ.mem_range.2 ⟨x, rfl⟩

Premises used: Iff.mpr, AlgHom.mem_range, Exists.intro, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ (g.comp f).range = Subalgebra.map g f.range

Tactic:
SetLike.coe_injective (Set.range_comp g f)

Premises used: Set.range_comp, SetLike.coe_injective, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : Semiring C
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ (g.comp f).range ≤ g.range

Tactic:
SetLike.coe_mono (Set.range_comp_subset_range f g)

Premises used: Set.range_comp_subset_range, Set.Subset, DFunLike.coe, SetLike.coe_mono
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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 : Subalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ S.val.comp (f.codRestrict S hf) = f

Tactic:
AlgHom.ext fun _ => rfl

Premises used: AlgHom.ext, rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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 : Subalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
x : A
⊢ Eq.{w + 1} (α := B) ((↑((f.codRestrict S hf : (a : A) → ↥S) x) : B) : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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 : Subalgebra R B
hf : ∀ (x : A), Membership.mem (α := B) S ((f : (a : A) → B) x : B)
⊢ Function.Injective.{v + 1, w + 1} (α := A) (β := ↥S) (⇑(f.codRestrict S hf) : (a : A) → ↥S) ↔
    Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
⟨fun H _x _y hxy => H <| Subtype.ext hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy :)⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
φ : A →ₐ[R] B
⊢ φ.range.val.comp φ.rangeRestrict = φ

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
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
⊢ Function.Surjective.{v + 1, w + 1} (α := A) (β := ↥f.range) (⇑f.rangeRestrict : (a : A) → ↥f.range)

Tactic:
fun ⟨_y, hy⟩ =>
    let ⟨x, hx⟩ := hy
    ⟨x, SetCoe.ext hx⟩

Premises used: SetCoe.ext, AlgHom.rangeRestrict, Exists, Subtype.mk, _private.0.AlgHom.rangeRestrict_surjective.match_2, Exists.intro, _private.0.AlgHom.rangeRestrict_surjective.match_1, Eq, DFunLike.coe, Function.Surjective
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
g : B → A
f : A →ₐ[R] B
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥f.range
x' : A
hx' : (f : (a : A) → B) x' = (↑x : B)
rw : Eq.{w + 1} (α := B) ((f : (a : A) → B) (g ((f : (a : A) → B) x')) : B) ((f : (a : A) → B) x' : B)
rw₁ rw₂ : Eq.{w + 1} (α := B) ((f : (a : A) → B) x' : B) ((f : (a : A) → B) x' : B)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)

Tactic:
rw [← hx', h x']
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
g : B → A
f : A →ₐ[R] B
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : A
⊢ Eq.{w + 1} (α := B) ((↑((ofLeftInverse h : (a : A) → ↥f.range) x) : B) : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
g : B → A
f : A →ₐ[R] B
h : Function.LeftInverse g (⇑f : (a : A) → B)
x : ↥f.range
⊢ ((ofLeftInverse h).symm : (a : ↥f.range) → A) x = g (↑x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x : A
⊢ Eq.{w + 1} (α := B) ((↑((ofInjective f hf : (a : A) → ↥f.range) x) : B) : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
a :
  (↑(Equiv.toFun (RingEquiv.toEquiv (e.toRingEquiv.subsemiringMap S.toSubsemiring))
          ((algebraMap R ↥S : (a : R) → ↥S) r)) :
      B) =
    (↑((algebraMap R ↥(Subalgebra.map (↑e : A →ₐ[R] B) S) : (a : R) → ↥(Subalgebra.map (↑e : A →ₐ[R] B) S)) r) : B)
⊢ Eq (α := ↥(Subalgebra.map (↑e : A →ₐ[R] B) S))
    (Equiv.toFun (RingEquiv.toEquiv (e.toRingEquiv.subsemiringMap S.toSubsemiring))
      ((algebraMap R ↥S : (a : R) → ↥S) r))
    ((algebraMap R ↥(Subalgebra.map (↑e : A →ₐ[R] B) S) : (a : R) → ↥(Subalgebra.map (↑e : A →ₐ[R] B) S)) r)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (↑(Equiv.toFun (RingEquiv.toEquiv (e.toRingEquiv.subsemiringMap S.toSubsemiring))
          ((algebraMap R ↥S : (a : R) → ↥S) r)) :
      B) =
    (↑((algebraMap R ↥(Subalgebra.map (↑e : A →ₐ[R] B) S) : (a : R) → ↥(Subalgebra.map (↑e : A →ₐ[R] B) S)) r) : B)

Tactic:
e.commutes r

Premises used: AlgEquiv.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (↑(Equiv.toFun (RingEquiv.toEquiv (e.toRingEquiv.subsemiringMap S.toSubsemiring))
          ((algebraMap R ↥S : (a : R) → ↥S) r)) :
      B) =
    (↑((algebraMap R ↥(Subalgebra.map (↑e : A →ₐ[R] B) S) : (a : R) → ↥(Subalgebra.map (↑e : A →ₐ[R] B) S)) r) : B)

Tactic:
exact e.commutes r

Premises used: AlgEquiv.commutes
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
B_1 : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B_1
inst_4 : Algebra R B_1
S T U : Subalgebra R A
inst_5 : Subsingleton A
B C : Subalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

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

Premises used: ZeroMemClass.zero_mem, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.val.range = S

Tactic:
ext <| Set.ext_iff.1 <| S.val.coe_range.trans Subtype.range_val

Premises used: AlgHom.coe_range, Subalgebra.val, Subtype.range_val, Iff.mp, Subalgebra.ext, Set.ext_iff, Eq.trans
-- Module: Mathlib.Algebra.Algebra.Subalgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S ≤ T
⊢ Function.Injective (α := ↥S) (β := ↥T) (⇑(inclusion h) : (a : ↥S) → ↥T)

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

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

Tactic:
AlgHom.ext fun _x => Subtype.ext rfl

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

Tactic:
rfl

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

Tactic:
Subtype.ext rfl

Premises used: rfl, Subtype.ext