awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a
have lift : ∀ (u : Aˣ), 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a
Tactic: lift u to Aˣ using hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a
have rw : 0 ≤ a ∧ IsUnit ((↑u : A) * a * (↑(star u) : A)) ↔ 0 ≤ a ∧ IsUnit a
Tactic: rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a : A
u : Aˣ
rw : 0 ≤ a ∧ IsUnit ((↑u : A) * a * (↑(star u) : A)) ↔ 0 ≤ a ∧ IsUnit a
⊢ 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a
have rw₁ : 0 ≤ a ∧ IsUnit ((↑u : A) * a) ↔ 0 ≤ a ∧ IsUnit a
Tactic: rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
inst : Semiring A
inst_1 : StarRing A
inst_2 : PartialOrder A
inst_3 : StarOrderedRing A
a : A
u : Aˣ
rw : 0 ≤ a ∧ IsUnit ((↑u : A) * a * (↑(star u) : A)) ↔ 0 ≤ a ∧ IsUnit a
rw₁ : 0 ≤ a ∧ IsUnit ((↑u : A) * a) ↔ 0 ≤ a ∧ IsUnit a
⊢ 0 ≤ a ∧ IsUnit ((↑u : A) * a * star (↑u : A)) ↔ 0 ≤ a ∧ IsUnit a
have rw₂ : 0 ≤ a ∧ IsUnit a ↔ 0 ≤ a ∧ IsUnit a
Tactic: rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (hypothesis)
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : Semifield 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
a : A
ha : IsStrictlyPositive a
⊢ IsStrictlyPositive (c • a)
have hunit : IsUnit (c • a)
Tactic: have hunit : IsUnit (c • a) :=
    isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (goal)
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : ZeroLEOneClass A
inst_3 : Semifield 𝕜
inst_4 : PartialOrder 𝕜
inst_5 : Algebra 𝕜 A
inst_6 : PosSMulMono 𝕜 A
c : 𝕜
hc : 0 < c
⊢ IsStrictlyPositive.{u_1} (A := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) c : A)
have rw : IsStrictlyPositive (HSMul.hSMul (β := A) c 1)
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (hypothesis)
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 < x
have h₁ : 0 ≤ x
Tactic: have h₁ : 0 ≤ x := by grind
-- Lean 4 proof step from Mathlib.Algebra.Algebra.StrictPositivity (hypothesis)
Goal:
A : Type u_1
𝕜 : Type u_2
inst : Ring A
inst_1 : PartialOrder A
inst_2 : CommSemiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : Algebra 𝕜 A
inst_5 : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
⊢ 0 < x
have h₂ : x ≠ 0
Tactic: have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R' : Type u'
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
p q : Subalgebra R A
h : Eq.{v + 1} (α := Set A) ((fun (s : Subalgebra R A) ↦ s.carrier) p) ((fun (s : Subalgebra R A) ↦ s.carrier) q)
⊢ p = q
have mk : ∀ (toSubsemiring : Subsemiring A)
  (algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A))
  (h :
    Eq.{v + 1} (α := Set A)
      ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
      ((fun (s : Subalgebra R A) ↦ s.carrier) q)),
  { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R' : Type u'
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
q : Subalgebra R A
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) q)
⊢ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } = q
have mk : ∀ (toSubsemiring_1 : Subsemiring A)
  (algebraMap_mem'_1 :
    ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A))
  (h :
    Eq.{v + 1} (α := Set A)
      ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
      ((fun (s : Subalgebra R A) ↦ s.carrier)
        { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })),
  { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } =
    { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R' : Type u'
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
toSubsemiring : Subsemiring A
algebraMap_mem' : ∀ (r : R), Membership.mem (α := A) toSubsemiring.carrier ((algebraMap R A : (a : R) → A) r : A)
toSubsemiring_1 : Subsemiring A
algebraMap_mem'_1 : ∀ (r : R), Membership.mem (α := A) toSubsemiring_1.carrier ((algebraMap R A : (a : R) → A) r : A)
h :
  Eq.{v + 1} (α := Set A)
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' })
    ((fun (s : Subalgebra R A) ↦ s.carrier) { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 })
⊢ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra R A } =
    { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 }
have mk : toSubsemiring = toSubsemiring_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (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
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toSubsemiring ↔ x ∈ T
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (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
h : S.toSubsemiring = T.toSubsemiring
x : A
rw : x ∈ S.toSubsemiring ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (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
h : S.toSubsemiring = T.toSubsemiring
x : A
rw : x ∈ S.toSubsemiring ↔ x ∈ T
rw₁ : x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toSubring ↔ x ∈ T
Tactic: rw [← mem_toSubring, ← mem_toSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
rw : x ∈ S.toSubring ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toSubring ↔ x ∈ T.toSubring
Tactic: rw [← mem_toSubring, ← mem_toSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
rw : x ∈ S.toSubring ↔ x ∈ T
rw₁ : x ∈ S.toSubring ↔ x ∈ T.toSubring
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toSubring ↔ x ∈ T.toSubring
Tactic: rw [← mem_toSubring, ← mem_toSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R' : Type u'
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
inst_7 : CommSemiring R'
inst_8 : SMul R' R
inst_9 : Algebra R' A
inst_10 : IsScalarTower R' R A
x : R'
⊢ Membership.mem (α := A) S ((algebraMap R' A : (a : R') → A) x : A)
have rw : Membership.mem (α := A) S ((algebraMap R A : (a : R) → A) (HSMul.hSMul (β := R) x 1) : A)
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ←
      Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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
⊢ Membership.mem (α := A) p.carrier ((algebraMap R A : (a : R) → A) r : A)
have rw : HSMul.hSMul (β := A) r 1 ∈ p.carrier
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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
⊢ 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)
have rw : HSMul.hSMul (β := A) r 1 ∈
  { carrier := (↑s : Set A), mul_mem' := hmul, one_mem' := h1, add_mem' := sorry, zero_mem' := sorry : Subsemiring A }.carrier
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)
have rw : Eq.{w + 1} (α := B) ((f : (a : A) → B) (g ((f : (a : A) → B) x')) : B) ((f : (a : A) → B) x' : B)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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)
⊢ (f : (a : A) → B) (g (↑x : B)) = (↑x : B)
have rw₁ : Eq.{w + 1} (α := B) ((f : (a : A) → B) x' : B) ((f : (a : A) → B) x' : B)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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 T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst_5 : SMul X R
inst_6 : SMul X A
inst_7 : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ (↑((x • s) • t) : A) = (↑(x • s • t) : A)
have rw : (↑(HMul.hMul (α := ↥S) ((algebraMap R ↥S : (a : R) → ↥S) (HSMul.hSMul (β := R) x 1) : ↥S) s • t) : A) =
  (↑(HMul.hMul (α := ↥T) ((algebraMap R ↥T : (a : R) → ↥T) (HSMul.hSMul (β := R) x 1) : ↥T) (s • t)) : A)
Tactic: rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc,
      Algebra.smul_def, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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 T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ (↑x : A) = (↑y : A)
have h₁ : (↑x : A) = (↑(HSMul.hSMul (β := ↥T) x 1) : A)
Tactic: convert! Subtype.ext_iff.mp (h 1) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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 T U : Subalgebra R A
h_1 : S ≤ T
this : Module ↥S ↥T := (inclusion h_1).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
h₁ : (↑x : A) = (↑(HSMul.hSMul (β := ↥T) x 1) : A)
⊢ (↑x : A) = (↑y : A)
have h₂ : (↑y : A) = (↑(HSMul.hSMul (β := ↥T) y 1) : A)
Tactic: convert! Subtype.ext_iff.mp (h 1) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl
have h : ∀ (a : ↥S), Eq.{v + 1} (α := A) (↑((S.equivOfEq S sorry : (a : ↥S) → ↥S) a) : A) (↑((AlgEquiv.refl : (a : ↥S) → ↥S) a) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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
⊢ (f.comp S.val).range = map f S
have rw : map f S.val.range = map f S
Tactic: rw [AlgHom.range_comp, range_val]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
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
rw : map f S.val.range = map f S
⊢ (f.comp S.val).range = map f S
have rw₁ : map f S = map f S
Tactic: rw [AlgHom.range_comp, range_val]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring
have rw : RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
  S.toSubsemiring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
    S.toSubsemiring
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring
have rw₁ : RingHom.rangeS (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubsemiring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
    S.toSubsemiring
rw₁ : RingHom.rangeS (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubsemiring
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring
have rw₂ : RingHom.rangeS (↑S.val : ↥S →+* A) = S.toSubsemiring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
    S.toSubsemiring
rw₁ : RingHom.rangeS (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubsemiring
rw₂ : RingHom.rangeS (↑S.val : ↥S →+* A) = S.toSubsemiring
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring
have rw₃ : S.subtype.rangeS = S.toSubsemiring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.rangeS (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) =
    S.toSubsemiring
rw₁ : RingHom.rangeS (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubsemiring
rw₂ : RingHom.rangeS (↑S.val : ↥S →+* A) = S.toSubsemiring
rw₃ : S.subtype.rangeS = S.toSubsemiring
⊢ RingHom.rangeS (R := ↥S) (algebraMap (↥S) A) = S.toSubsemiring
have rw₄ : S.toSubsemiring = S.toSubsemiring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubsemiring_subtype,
    Subsemiring.rangeS_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring
have rw : RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring
have rw₁ : RingHom.range (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₁ : RingHom.range (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubring
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring
have rw₂ : RingHom.range (↑S.val : ↥S →+* A) = S.toSubring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₁ : RingHom.range (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₂ : RingHom.range (↑S.val : ↥S →+* A) = S.toSubring
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring
have rw₃ : S.toSubring.subtype.range = S.toSubring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
S : Subalgebra R A
rw :
  RingHom.range (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₁ : RingHom.range (RingHom.comp (RingHom.id A) (↑S.val : ↥S →+* A)) = S.toSubring
rw₂ : RingHom.range (↑S.val : ↥S →+* A) = S.toSubring
rw₃ : S.toSubring.subtype.range = S.toSubring
⊢ RingHom.range (R := ↥S) (algebraMap (↥S) A) = S.toSubring
have rw₄ : S.toSubring = S.toSubring
Tactic: rw [algebraMap_eq, Algebra.algebraMap_self, RingHom.id_comp, ← toSubring_subtype,
    Subring.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ Eq (α := Subalgebra R A) (centralizer R s.centralizer.centralizer) (centralizer R s)
have a : (↑(centralizer R s.centralizer.centralizer) : Set A) = (↑(centralizer R s) : Set A)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (goal)
Goal:
R : Type u_1
inst : Ring R
S : Subring R
i_1 : ℤ
i : ℕ
ih : Membership.mem (α := R) S.carrier ((algebraMap ℤ R : (a : ℤ) → R) (-(↑i : ℤ)) : R)
⊢ (↑(HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1) : R) ∈ S
have rw : HSub.hSub (α := R) (↑(-(↑i : ℤ)) : R) 1 ∈ S
Tactic: rw [Int.cast_sub, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (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
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)
have rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Basic (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
F : Type u_4
ϕ ψ : F
inst_5 : FunLike F A B
inst_6 : AlgHomClass F R A B
x y : A
hx : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{u_3 + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)}
    (x * y)
have rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]