awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Operations
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'
apply :
  Eq.{u_1 + 1} (α := 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))
    (range 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))
⊢ ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N) =
    map₂ (LinearMap.mul R A') (map f.toLinearMap M) (map f.toLinearMap N)

Tactic:
apply congr_arg sSup

Premises used: congr_arg, SupSet.sSup
-- Module: Mathlib.Algebra.Algebra.Operations
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'
h :
  ∀ (S : Submodule R 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 ↔
      Membership.mem (γ := Set (Submodule R A'))
        (range 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))
        S
⊢ Eq.{u_1 + 1} (α := 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))
    (range 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))

Tactic:
ext S
-- Module: Mathlib.Algebra.Algebra.Operations
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'
h :
  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 →
    Membership.mem (γ := Set (Submodule R A'))
      (range 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))
      S
h₁ :
  Membership.mem (γ := Set (Submodule R A'))
      (range 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))
      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
⊢ 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 ↔
    Membership.mem (γ := Set (Submodule R A'))
      (range 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))
      S

Tactic:
constructor
-- Module: Mathlib.Algebra.Algebra.Operations
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
h :
  (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)) ⋯) =
    S
⊢ Membership.mem (γ := Set (Submodule R A'))
    (range 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))
    S

Tactic:
use ⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ (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)) ⋯) =
    S

Tactic:
Eq.trans ?_ hy

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Algebra.Operations
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
h :
  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)
⊢ (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)) ⋯) =
    S

Tactic:
refine Eq.trans ?_ hy

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Algebra.Operations
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
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)) ⋯))
        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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Algebra.Operations
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
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)) ⋯))
      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:
simp
-- Module: Mathlib.Algebra.Algebra.Operations
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
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
⊢ 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

Premises used: Submodule.mem_map, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Algebra.Operations
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')
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
⊢ 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:
use ⟨y', hy'⟩
-- Module: Mathlib.Algebra.Algebra.Operations
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

Tactic:
Eq.trans ?_ hy

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Algebra.Operations
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')
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)
⊢ (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:
refine Eq.trans ?_ hy

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Algebra.Operations
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')
⊢ (f : (a : A) → A') y' = (↑y : A')

Tactic:
rw [f.toLinearMap_apply] at fy_eq

Premises used: AlgHom.toLinearMap_apply
-- Module: Mathlib.Algebra.Algebra.Operations
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')
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
⊢ 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:
ext
-- Module: Mathlib.Algebra.Algebra.Operations
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')
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:
simp [fy_eq]
-- Module: Mathlib.Algebra.Algebra.Operations
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
a₁ :
  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ᵐᵒᵖ) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Algebra.Operations
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 :
  M * N ≤
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (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

Tactic:
simp_rw [map_le_iff_le_comap]

Premises used: Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Algebra.Operations
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)

Tactic:
mul_le.2 fun m hm n hn => ?_

Premises used: Iff.mpr, Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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 :
  ∀ (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)
⊢ 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 => ?_

Premises used: Iff.mpr, Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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
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ᵐᵒᵖ)
⊢ m * n ∈
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
      (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M)

Tactic:
rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]

Premises used: Submodule.mem_comap, Submodule.map_equiv_eq_comap_symm
-- Module: Mathlib.Algebra.Algebra.Operations
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
a :
  op n * op m ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M
⊢ 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:
change op n * op m ∈ _

Premises used: MulOpposite.op
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ op n * op m ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M

Tactic:
mul_mem_mul hn hm

Premises used: Submodule.mul_mem_mul, Set.Mem
-- Module: Mathlib.Algebra.Algebra.Operations
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
⊢ op n * op m ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M

Tactic:
exact mul_mem_mul hn hm

Premises used: Submodule.mul_mem_mul
-- Module: Mathlib.Algebra.Algebra.Operations
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)

Tactic:
mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)

Premises used: Iff.mpr, Set.Mem, MulOpposite.rec', Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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 :
  ∀ (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)
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ≤
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)

Tactic:
refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)

Premises used: Iff.mpr, MulOpposite.rec', Submodule.mul_le
-- Module: Mathlib.Algebra.Algebra.Operations
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
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)
⊢ op m * op n ∈ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N)

Tactic:
rw [Submodule.mem_map_equiv] at hm hn ⊢

Premises used: Submodule.mem_map_equiv
-- Module: Mathlib.Algebra.Algebra.Operations
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 : 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:
mul_mem_mul hn hm

Premises used: Submodule.mul_mem_mul, Set.Mem, MulOpposite.unop
-- Module: Mathlib.Algebra.Algebra.Operations
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 : 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:
exact mul_mem_mul hn hm

Premises used: Submodule.mul_mem_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M N : Submodule R A
simp_rw :
  map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M
⊢ 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

Tactic:
simp_rw [← map_equiv_eq_comap_symm, map_op_mul]

Premises used: Submodule.map_equiv_eq_comap_symm, Submodule.map_op_mul