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ᵐᵒᵖ
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
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
rw₆ : map LinearMap.id (M * N) = map LinearMap.id M * map LinearMap.id N
rw₇ : M * N = map LinearMap.id M * map LinearMap.id N
rw₈ : M * N = M * map LinearMap.id N
rw₉ rw₁₀ : M * N = M * 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)

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]

Premises used: Submodule.map_id, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, Submodule.map_comp, LinearEquiv.comp_coe, Submodule.map_op_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 (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) N *
      map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M
⊢ comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
    comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) N * comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M

Tactic:
simp_rw [comap_equiv_eq_map_symm, map_unop_mul]

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.map_unop_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : IsScalarTower α A A
a : α
S T : Submodule R A
rw :
  HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A)) • T =
    a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T
rw₁ :
  HSMul.hSMul (β := Submodule R A) (HSMul.hSMul (β := Submodule R A) a (span R (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₂ :
  HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₃ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₄ :
  HMul.hMul (α := Submodule R A) (span R (a • (↑S : Set A))) (span R (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₅ :
  span R (a • (↑S : Set A) * (↑T : Set A)) =
    a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A))
rw₆ :
  span R (a • (↑S : Set A) * (↑T : Set A)) = HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A)))
rw₇ : Eq (α := Submodule R A) (span R (a • (↑S : Set A) * (↑T : Set A))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
rw₈ rw₉ :
  Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
⊢ (a • S) • T = a • S • T

Tactic:
rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, smul_mul_assoc]

Premises used: Submodule.span_mul_span, smul_mul_assoc, Submodule.span_eq, Submodule.smul_span, smul_eq_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S_1 T_1 : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : SMulCommClass α A A
a : α
S T : Submodule R A
rw :
  a • HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) T =
    HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) (a • T)
rw₁ :
  a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A)) =
    HSMul.hSMul (α := Submodule R A) (span R (↑S : Set A)) (HSMul.hSMul (β := Submodule R A) a (span R (↑T : Set A)))
rw₂ :
  a • HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A)) =
    HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (a • (↑T : Set A)))
rw₃ :
  a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A)) =
    HSMul.hSMul (α := Submodule R A) (β := Submodule R A) (span R (↑S : Set A)) (span R (a • (↑T : Set A)))
rw₄ :
  a • HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (↑T : Set A)) =
    HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (a • (↑T : Set A)))
rw₅ :
  HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A))) =
    HMul.hMul (α := Submodule R A) (span R (↑S : Set A)) (span R (a • (↑T : Set A)))
rw₆ :
  HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A))) = span R ((↑S : Set A) * a • (↑T : Set A))
rw₇ : Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R ((↑S : Set A) * a • (↑T : Set A)))
rw₈ rw₉ :
  Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
⊢ a • S • T = S • a • T

Tactic:
rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, mul_smul_comm]

Premises used: Submodule.span_mul_span, Submodule.span_eq, mul_smul_comm, Submodule.smul_span, smul_eq_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
ι : Sort uι
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst_3 : Monoid α
inst_4 : DistribMulAction α A
inst_5 : SMulCommClass α R A
inst_6 : SMulCommClass A α A
⊢ SMulCommClass.{v, u_1, v} (Submodule R A) α (Submodule R A)

Tactic:
have := SMulCommClass.symm A α A; .symm ..

Premises used: Submodule, SMulCommClass.symm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
obtain :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x),
    ∃ (T : Finset A) (T' : Finset A),
      (↑T : Set A) ⊆ S ∧
        (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
⊢ ∃ (T : Finset A) (T' : Finset A),
    (↑T : Set A) ⊆ S ∧
      (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx

Premises used: Submodule.mem_span_finite_of_mem_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
obtain :
  ∀ (T T' : Finset A) (hS : (↑T : Set A) ⊆ S) (hS' : (↑T' : Set A) ⊆ S') (h : U ⊆ T * T'),
    ∃ (T : Finset A) (T' : Finset A),
      (↑T : Set A) ⊆ S ∧
        (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
⊢ ∃ (T : Finset A) (T' : Finset A),
    (↑T : Set A) ⊆ S ∧
      (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h

Premises used: Finset.subset_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h_1 : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
T T' : Finset A
hS : (↑T : Set A) ⊆ S
hS' : (↑T' : Set A) ⊆ S'
h : U ⊆ T * T'
right : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
⊢ ∃ (T : Finset A) (T' : Finset A),
    (↑T : Set A) ⊆ S ∧
      (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
use T, T', hS, hS'
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h_1 : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
T T' : Finset A
hS : (↑T : Set A) ⊆ S
hS' : (↑T' : Set A) ⊆ S'
h : U ⊆ T * T'
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : U ≤ T * T'
⊢ (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)

Tactic:
assumption_mod_cast
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h_1 : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
T T' : Finset A
hS : (↑T : Set A) ⊆ S
hS' : (↑T' : Set A) ⊆ S'
h : U ⊆ T * T'
⊢ (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)

Tactic:
have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h_1 : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
T T' : Finset A
hS : (↑T : Set A) ⊆ S
hS' : (↑T' : Set A) ⊆ S'
h : U ⊆ T * T'
h' : (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)
⊢ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
have h'' := span_mono h' hU
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
U : Finset A
h_1 : (↑U : Set A) ⊆ S * S'
hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x
T T' : Finset A
hS : (↑T : Set A) ⊆ S
hS' : (↑T' : Set A) ⊆ S'
h : U ⊆ T * T'
h' : (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)
h'' : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
⊢ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
assumption
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid A
inst_2 : Mul A
inst_3 : Module R A
S S' : Set A
x : A
hx : Membership.mem (γ := Submodule R A) (span R (S * S')) x
obtain :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x),
    ∃ (T : Finset A) (T' : Finset A),
      (↑T : Set A) ⊆ S ∧
        (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
obtain₁ :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x)
    (T T' : Finset A) (hS : (↑T : Set A) ⊆ S) (hS' : (↑T' : Set A) ⊆ S') (h : U ⊆ T * T'),
    ∃ (T : Finset A) (T' : Finset A),
      (↑T : Set A) ⊆ S ∧
        (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
right :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x)
    (T T' : Finset A) (hS : (↑T : Set A) ⊆ S) (hS' : (↑T' : Set A) ⊆ S') (h : U ⊆ T * T'),
    Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
right₁ :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x)
    (T T' : Finset A) (hS : (↑T : Set A) ⊆ S) (hS' : (↑T' : Set A) ⊆ S') (h : U ⊆ T * T')
    (h' : (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)),
    Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
right₂ :
  ∀ (U : Finset A) (h : (↑U : Set A) ⊆ S * S') (hU : Membership.mem (γ := Submodule R A) (span R (↑U : Set A)) x)
    (T T' : Finset A) (hS : (↑T : Set A) ⊆ S) (hS' : (↑T' : Set A) ⊆ S') (h : U ⊆ T * T')
    (h' : (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A))
    (h'' : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x),
    Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
⊢ ∃ (T : Finset A) (T' : Finset A),
    (↑T : Set A) ⊆ S ∧
      (↑T' : Set A) ⊆ S' ∧ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x

Tactic:
classical
  obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx
  obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h
  use T, T', hS, hS'
  have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
  have h'' := span_mono h' hU
  assumption

Premises used: Submodule.mem_span_finite_of_mem_span
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Submodule R A
rw : map₂ (LinearMap.mul R A) s t = span R ((↑s : Set A) * (↑t : Set A))
⊢ s * t = span R ((↑s : Set A) * (↑t : Set A))

Tactic:
rw [mul_eq_map₂]

Premises used: Submodule.mul_eq_map₂
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R ((↑s : Set A) * (↑t : Set A))

Tactic:
map₂_eq_span_image2 _ s t

Premises used: Submodule.map₂_eq_span_image2
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Submodule R A
⊢ map₂ (LinearMap.mul R A) s t = span R ((↑s : Set A) * (↑t : Set A))

Tactic:
exact map₂_eq_span_image2 _ s t

Premises used: Submodule.map₂_eq_span_image2
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P Q : Submodule R A
x : A
hx : x ∈ P * Q
rwa : ∀ (hx : x ∈ span R (↑P : Set A) * Q), Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
rwa₁ :
  ∀ (hx : x ∈ HMul.hMul (α := Submodule R A) (span R (↑P : Set A)) (span R (↑Q : Set A))),
    Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hx : Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x),
    Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
⊢ Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x

Tactic:
rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx

Premises used: Submodule.span_mul_span, Submodule.span_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
P : Submodule R A
x y : A
simp_rw : x ∈ map₂ (LinearMap.mul R A) (R ∙ y) P ↔ ∃ z ∈ P, y * z = x
simp_rw₁ :
  Membership.mem (γ := Submodule R A) (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) y) P) x ↔
    ∃ z ∈ P, y * z = x
simp_rw₂ :
  (∃ y_1 ∈ P, (((LinearMap.mul R A : (a : A) → A →ₗ[R] A) y : A →ₗ[R] A) : (a : A) → A) y_1 = x) ↔ ∃ z ∈ P, y * z = x
⊢ x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x

Tactic:
simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]

Premises used: LinearMap.mul_apply_apply, Submodule.mem_map, Submodule.map₂_span_singleton_eq_map, Submodule.mul_eq_map₂
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P : Submodule R A
x y : A
simp_rw : x ∈ map₂ (LinearMap.mul R A) P (R ∙ y) ↔ ∃ z ∈ P, z * y = x
simp_rw₁ :
  Membership.mem (γ := Submodule R A)
      (map (σ₁₂ := RingHom.id R) ((LinearMap.flip (LinearMap.mul R A) : (a : A) → A →ₗ[R] A) y) P) x ↔
    ∃ z ∈ P, z * y = x
simp_rw₂ :
  (∃ y_1 ∈ P, (((LinearMap.flip (LinearMap.mul R A) : (a : A) → A →ₗ[R] A) y : A →ₗ[R] A) : (a : A) → A) y_1 = x) ↔
    ∃ z ∈ P, z * y = x
simp_rw₃ :
  (∃ y_1 ∈ P, (((LinearMap.mul R A : (a : A) → A →ₗ[R] A) y_1 : A →ₗ[R] A) : (a : A) → A) y = x) ↔ ∃ z ∈ P, z * y = x
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x

Tactic:
simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]

Premises used: LinearMap.mul_apply_apply, Submodule.mem_map, LinearMap.flip_apply, Submodule.map₂_span_singleton_eq_map_flip, Submodule.mul_eq_map₂
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
p : Submodule R A
⊢ (R ∙ x) * p = x • p

Tactic:
ext fun _ ↦ mem_span_singleton_mul

Premises used: Submodule.mem_span_singleton_mul, Submodule.ext
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : DivisionSemiring S
inst_2 : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
mp : y ∈ x • p → x⁻¹ * y ∈ p
mpr : x⁻¹ * y ∈ p → y ∈ x • p
⊢ y ∈ x • p ↔ x⁻¹ * y ∈ p

Tactic:
constructor
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : DivisionSemiring S
inst_2 : Algebra R S
x : S
p : Submodule R S
hx : x ≠ 0
a : S
ha : a ∈ p
⊢ HMul.hMul (β := S) x⁻¹ ((DistribSMul.toLinearMap R S x : (a : S) → S) a : S) ∈ p

Tactic:
simpa [inv_mul_cancel_left₀ hx]

Premises used: inv_mul_cancel_left₀
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : DivisionSemiring S
inst_2 : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
h : x⁻¹ * y ∈ p
⊢ (DistribSMul.toLinearMap R S x : (a : S) → S) (x⁻¹ * y) = y

Tactic:
simp [mul_inv_cancel_left₀ hx]

Premises used: mul_inv_cancel_left₀
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : DivisionSemiring S
inst_2 : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ≠ 0
⊢ x⁻¹ * y ∈ p → y ∈ x • p

Tactic:
exact fun h ↦ ⟨_, h, by simp [mul_inv_cancel_left₀ hx]⟩
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Ring S
inst_2 : Algebra R S
x : S
p : Submodule R S
y : S
hx : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) x
⊢ x * y ∈ x • p ↔ y ∈ p

Tactic:
simp [mem_smul_pointwise_iff_exists, mul_cancel_left_mem_nonZeroDivisors hx]

Premises used: mul_cancel_left_mem_nonZeroDivisors, Submodule.mem_smul_pointwise_iff_exists
-- 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
x y : R
⊢ (x * y) • (M * N) = x • M * y • N

Tactic:
mul_smul_mul_comm x y M N

Premises used: mul_smul_mul_comm
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
rw : Eq (α := Submodule R A) 1 (span R (HPow.hPow (β := ℕ) s 0))
rw₁ : Eq.{v + 1} (α := Submodule R A) 1 (span R 1)
rw₂ rw₃ : Eq.{v + 1} (α := Submodule R A) (span R 1) (span R 1)
⊢ HPow.hPow (α := Submodule R A) (β := ℕ) (span R s) 0 = span R (HPow.hPow (β := ℕ) s 0)

Tactic:
rw [pow_zero, pow_zero, one_eq_span_one_set]

Premises used: pow_zero, Submodule.one_eq_span_one_set
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
n : ℕ
rw : HPow.hPow (α := Submodule R A) (span R s) n * span R s = span R (s ^ (n + 1))
rw₁ : HPow.hPow (α := Submodule R A) (span R s) n * span R s = span R (s ^ n * s)
rw₂ : HMul.hMul (α := Submodule R A) (span R (s ^ n)) (span R s) = span R (s ^ n * s)
rw₃ rw₄ : Eq (α := Submodule R A) (span R (s ^ n * s)) (span R (s ^ n * s))
⊢ HPow.hPow (α := Submodule R A) (span R s) (n + 1) = span R (s ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

Premises used: pow_succ, Submodule.span_mul_span
-- 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 : Submodule R A
n : ℕ
rw : M ^ n = HPow.hPow (α := Submodule R A) (span R (↑M : Set A)) n
rw₁ rw₂ : M ^ n = M ^ n
⊢ M ^ n = span R ((↑M : Set A) ^ n)

Tactic:
rw [← span_pow, span_eq]

Premises used: Submodule.span_pow, Submodule.span_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
N P : Submodule R A
h : N * P = 1
rw : ⊤ * N * P
| ⊤

Tactic:
rw [← mul_one ⊤, ← h, ← mul_assoc]

Premises used: mul_assoc, mul_one, Top.top
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
N P : Submodule R A
h : N * P = 1
conv_lhs : ⊤ * N * P ≤ ⊤ * P
⊢ ⊤ ≤ ⊤ * P

Tactic:
conv_lhs => rw [← mul_one ⊤, ← h, ← mul_assoc]

Premises used: mul_assoc, mul_one, Top.top
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ * N * P ≤ ⊤ * P

Tactic:
smul_mono_left le_top

Premises used: Set.Mem, le_top, Submodule.smul_mono_left
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ * N * P ≤ ⊤ * P

Tactic:
exact smul_mono_left le_top

Premises used: le_top, Submodule.smul_mono_left