awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥M
hy :
  (fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      y =
    S
⊢ Eq.{u_1 + 1} (α := Submodule R A')
    ((fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      (Subtype.mk (p := fun (x : A') ↦ x ∈ map f.toLinearMap M) ((f : (a : A) → A') (↑y : A)) ⋯))
    ((fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      y)
have h : ∀ (x : A'),
  Membership.mem (γ := Submodule R A')
      ((fun (s : ↥(map f.toLinearMap M)) ↦
          (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
            Submodule R A'))
        (Subtype.mk (p := fun (x : A') ↦ x ∈ map f.toLinearMap M) ((f : (a : A) → A') (↑y : A)) sorry))
      x ↔
    Membership.mem (γ := Submodule R A')
      ((fun (i : ↥M) ↦
          map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
        y)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy :
  (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y =
    S
⊢ Membership.mem (γ := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    S
have h : ∀ (y' : A) (hy' : y' ∈ M) (fy_eq : (f.toLinearMap : (a : A) → A') y' = (↑y : A')),
  Membership.mem (γ := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    S
Tactic: obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy :
  (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y =
    S
y' : A
hy' : y' ∈ M
fy_eq : (f.toLinearMap : (a : A) → A') y' = (↑y : A')
⊢ Membership.mem (γ := Set (Submodule R A'))
    (range fun (i : ↥M) ↦
      map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    S
have h : (fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy') =
  S
Tactic: use ⟨y', hy'⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy :
  (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y =
    S
y' : A
hy' : y' ∈ M
fy_eq : (f.toLinearMap : (a : A) → A') y' = (↑y : A')
⊢ (fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy') =
    S
have h : Eq.{u_1 + 1} (α := Submodule R A')
  ((fun (i : ↥M) ↦ map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
    (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy'))
  ((fun (s : ↥(map f.toLinearMap M)) ↦
      (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
        Submodule R A'))
    y)
Tactic: refine Eq.trans ?_ hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy :
  (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y =
    S
y' : A
hy' : y' ∈ M
fy_eq : (f.toLinearMap : (a : A) → A') y' = (↑y : A')
⊢ Eq.{u_1 + 1} (α := Submodule R A')
    ((fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy'))
    ((fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y)
have fy_eq₁ : (f : (a : A) → A') y' = (↑y : A')
Tactic: rw [f.toLinearMap_apply] at fy_eq
Cleared hypotheses: fy_eq
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : ↥(map f.toLinearMap M)
hy :
  (fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y =
    S
y' : A
hy' : y' ∈ M
fy_eq : (f : (a : A) → A') y' = (↑y : A')
⊢ Eq.{u_1 + 1} (α := Submodule R A')
    ((fun (i : ↥M) ↦
        map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
      (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy'))
    ((fun (s : ↥(map f.toLinearMap M)) ↦
        (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
          Submodule R A'))
      y)
have h : ∀ (x : A'),
  Membership.mem (γ := Submodule R A')
      ((fun (i : ↥M) ↦
          map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N))
        (Subtype.mk (p := fun (x : A) ↦ x ∈ M) y' hy'))
      x ↔
    Membership.mem (γ := Submodule R A')
      ((fun (s : ↥(map f.toLinearMap M)) ↦
          (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A' : (a : A') → A' →ₗ[R] A') (↑s : A')) (map f.toLinearMap N) :
            Submodule R A'))
        y)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
have a : map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) ≤
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
a :
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) ≤
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
have a₁ : map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ≤
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) ≤
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
have a : M * N ≤
  comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
    (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M)
Tactic: simp_rw [map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ M * N ≤
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M)
have a : ∀ (m : A) (hm : m ∈ M) (n : A) (hn : n ∈ N),
  m * n ∈
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M)
Tactic: refine mul_le.2 fun m hm n hn => ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M)
have a : Membership.mem (α := Aᵐᵒᵖ)
  (comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
  (((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ) (m * n) : Aᵐᵒᵖ)
Tactic: rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ Membership.mem (α := Aᵐᵒᵖ)
    (comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
    (((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ) (m * n) : Aᵐᵒᵖ)
have a : op n * op m ∈
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M
Tactic: change op n * op m ∈ _
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ≤
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)
have a : ∀ (m : A) (hm : op m ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N) (n : A)
  (hn : op n ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M), op m * op n ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)
Tactic: refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
m : A
hm : op m ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)
have a : ∀ (hm : Membership.mem (α := A) N ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) (op m) : A)) (n : A)
  (hn : Membership.mem (α := A) M ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) (op n) : A)),
  Membership.mem (α := A) (M * N) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) (op m * op n) : A)
Tactic: rw [Submodule.mem_map_equiv] at hm hn ⊢
Cleared hypotheses: hm, n, hn
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
⊢ comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M
have simp_rw : map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
Tactic: simp_rw [← map_equiv_eq_comap_symm, map_op_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw : map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
    (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₁ : map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₂ : map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₃ : map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₄ : map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective.{v + 1, v + 1} (α := A) (β := Aᵐᵒᵖ) (⇑(↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) : (a : A) → Aᵐᵒᵖ)
rw :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
rw₁ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M) *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₂ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N)
rw₃ :
  map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) (M * N) =
    map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) M *
      map ((↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) N
rw₄ :
  map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M *
      map (↑(LinearEquiv.symm (opLinearEquiv R) ≪≫ₗ opLinearEquiv R) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N)) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M)
have rw₅ : map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) (M * N) =
  map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) M * map (↑(LinearEquiv.refl R Aᵐᵒᵖ) : Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ) N
Tactic: rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]