awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
⊢ g (x + y) = g x + g y
have rw₁ : g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
  g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
rw₁ :
  g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
    g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
⊢ g (x + y) = g x + g y
have rw₂ : g ((f : (a : A) → B) (g x + g y)) = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
rw₁ :
  g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
    g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₂ : g ((f : (a : A) → B) (g x + g y)) = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
⊢ g (x + y) = g x + g y
have rw₃ : g x + g y = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
rw₁ :
  g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
    g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₂ : g ((f : (a : A) → B) (g x + g y)) = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₃ : g x + g y = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
⊢ g (x + y) = g x + g y
have rw₄ : g x + g y = g x + g ((f : (a : A) → B) (g y))
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (goal)
Goal:
R : Type u
S : Type u₁
T : Type u_1
inst : Monoid R
inst_1 : Monoid S
inst_2 : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst_3 : NonUnitalNonAssocSemiring A
inst_4 : DistribMulAction R A
inst_5 : NonUnitalNonAssocSemiring B
inst_6 : DistribMulAction S B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst_9 : NonUnitalNonAssocSemiring B₁
inst_10 : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse.{u + 1, u₁ + 1} (α := R) (β := S) (⇑φ' : (a : S) → R) (⇑φ : (a : R) → S)
h₁ : Function.LeftInverse g (⇑f : (a : A) → B)
h₂ : Function.RightInverse g (⇑f : (a : A) → B)
x y : B
rw : g (HAdd.hAdd (α := B) ((f : (a : A) → B) (g x) : B) y) = g ((f : (a : A) → B) (g x)) + g y
rw₁ :
  g (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) (g x) : B) ((f : (a : A) → B) (g y) : B)) =
    g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₂ : g ((f : (a : A) → B) (g x + g y)) = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₃ : g x + g y = g ((f : (a : A) → B) (g x)) + g ((f : (a : A) → B) (g y))
rw₄ : g x + g y = g x + g ((f : (a : A) → B) (g y))
⊢ g (x + y) = g x + g y
have rw₅ : g x + g y = g x + g y
Tactic: rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalHom (hypothesis)
Goal:
R_1 : Type u
S_1 : Type u₁
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : Monoid R
inst_1 : Monoid S
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : MulAction R S
inst_5 : DistribMulAction S A
inst_6 : DistribMulAction S B
inst_7 : DistribMulAction R A
inst_8 : DistribMulAction R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
f : A →ₙₐ[S] B
r : R
x : A
⊢ MulHom.toFun (NonUnitalRingHom.toMulHom (↑f : A →ₙ+* B)) (r • x) =
    HSMul.hSMul (α := R) ((MonoidHom.id R : (a : R) → R) r : R)
      (MulHom.toFun (NonUnitalRingHom.toMulHom (↑f : A →ₙ+* B)) x)
have this : (f : (a : A) → B) (HSMul.hSMul (β := S) r 1 • x) =
  HSMul.hSMul (β := B) (HSMul.hSMul (β := S) r 1) ((f : (a : A) → B) x : B)
Tactic: have := map_smul f (r • 1) x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : NonUnitalNonAssocRing A
inst_2 : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
rw : x ∈ S.toNonUnitalSubring ↔ x ∈ T
rw₁ : x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
Tactic: rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : NonUnitalNonAssocSemiring C
inst_4 : Module R A
inst_5 : Module R B
inst_6 : Module R C
S_1 : NonUnitalSubalgebra R A
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
b : B
hb :
  b ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))
⊢ r • b ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))
have rcases : ∀ (a : A) (ha : a ∈ (↑S.toNonUnitalSubsemiring : Set A)),
  HSMul.hSMul (β := B) r (((↑f : A →ₙ+* B) : (a : A) → B) a : B) ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (NonUnitalSubsemiring.toAddSubmonoid
          (NonUnitalSubsemiring.map (F := A →ₙ+* B) (↑f : A →ₙ+* B) S.toNonUnitalSubsemiring)))
Tactic: rcases hb with ⟨a, ha, rfl⟩
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
φ : F
⊢ (↑(NonUnitalAlgHom.range φ) : Set B) = Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)
have h : ∀ (x : B),
  x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
φ : F
x : B
⊢ x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
have h : Membership.mem (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) x ↔
  Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
Tactic: rw [SetLike.mem_coe, mem_range, Set.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
φ : F
x : B
h :
  Membership.mem (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) x ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
⊢ x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
have h₁ : (∃ (x_1 : A), (φ : (a : A) → B) x_1 = x) ↔
  Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
Tactic: rw [SetLike.mem_coe, mem_range, Set.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
φ : F
x : B
h :
  Membership.mem (γ := NonUnitalSubalgebra R B) (NonUnitalAlgHom.range φ) x ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
h₁ :
  (∃ (x_1 : A), (φ : (a : A) → B) x_1 = x) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
⊢ x ∈ (↑(NonUnitalAlgHom.range φ) : Set B) ↔
    Membership.mem (γ := Set B) (Set.range.{w, v + 1} (ι := A) (⇑φ : (a : A) → B)) x
have h₂ : (∃ (x_1 : A), (φ : (a : A) → B) x_1 = x) ↔ ∃ (y : A), (φ : (a : A) → B) y = x
Tactic: rw [SetLike.mem_coe, mem_range, Set.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)
have rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)
have rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)
have rw₂ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)
have rw₃ : HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x + y) : B) ((ψ : (a : A) → B) (x + y) : B)
rw₁ : HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x + y)
rw₂ :
  HAdd.hAdd (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x + y)
have rw₄ : HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
  HAdd.hAdd (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_add, map_add, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 0
have rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) 0 : B) ((ψ : (a : A) → B) 0 : B)
Tactic: rw [Set.mem_setOf_eq, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) 0 : B) ((ψ : (a : A) → B) 0 : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 0
have rw₁ : Eq.{w + 1} (α := B) (0 : B) ((ψ : (a : A) → B) 0 : B)
Tactic: rw [Set.mem_setOf_eq, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) 0 : B) ((ψ : (a : A) → B) 0 : B)
rw₁ : Eq.{w + 1} (α := B) (0 : B) ((ψ : (a : A) → B) 0 : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} 0
have rw₂ : Eq.{w + 1} (α := B) 0 0
Tactic: rw [Set.mem_setOf_eq, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x * y)
have rw : Eq.{w + 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.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 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) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]