awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SMul A B
inst_4 : Module A C
inst_5 : Module B C
inst_6 : IsScalarTower A C C
inst_7 : IsScalarTower B C C
inst_8 : IsScalarTower A B C
I J : Submodule B C
⊢ restrictScalars A (I * J) = HMul.hMul (α := Submodule A C) (restrictScalars A I) (restrictScalars A J)

Tactic:
rfl

Premises used: iInf, Set.Mem, iSup, Set.iInter, Submodule.restrictScalars, setOf, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
ι : Sort uι
s : ι → Submodule R A
t : Submodule R A
⊢ (⨆ (i : ι), s i) * t = ⨆ (i : ι), s i * t

Tactic:
iSup_smul

Premises used: Submodule.iSup_smul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
ι : Sort uι
t : Submodule R A
s : ι → Submodule R A
⊢ t * ⨆ (i : ι), s i = ⨆ (i : ι), t * s i

Tactic:
smul_iSup

Premises used: Submodule.smul_iSup
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
rw : N * (P * ⊤)
| ⊤

Tactic:
rw [← Submodule.one_mul ⊤, ← h, mul_assoc]

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

Tactic:
smul_mono le_rfl le_top

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

Tactic:
exact smul_mono le_rfl le_top

Premises used: le_rfl, Submodule.smul_mono, le_top
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ M ^ n = npowRec n M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ HPow.hPow (β := ℕ) M 0 = 1

Tactic:
rfl

Premises used: LinearMap.range, npowRec, rfl, Submodule.copy
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ M ^ (n + 1) = M ^ n * M

Tactic:
rfl

Premises used: Set.Mem, npowRec, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
m n : ℕ
h : n ≠ 0
⊢ M ^ (m + n) = M ^ m * M ^ n

Tactic:
npowRec_add m n h _ M.one_mul

Premises used: npowRec_add, Set.Mem, Submodule.one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
rw : HPow.hPow (β := ℕ) M 0 * M = M
rw₁ : 1 * M = M
rw₂ rw₃ : M = M
⊢ HPow.hPow (β := ℕ) M 1 = M

Tactic:
rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]

Premises used: Submodule.pow_zero, Submodule.pow_succ, Submodule.one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
rw : M ^ (1 + n) = M * M ^ n
rw₁ : HPow.hPow (β := ℕ) M 1 * M ^ n = M * M ^ n
rw₂ rw₃ : M * M ^ n = M * M ^ n
⊢ M ^ (n + 1) = M * M ^ n

Tactic:
rw [add_comm, M.pow_add h, Submodule.pow_one]

Premises used: Submodule.pow_add, add_comm, Submodule.pow_one
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Submodule R A) ⊥ (n + 1) * ⊥ = ⊥
rw₁ : HMul.hMul (α := Submodule R A) ⊥ ⊥ = ⊥
rw₂ rw₃ : Eq.{v + 1} (α := Submodule R A) ⊥ ⊥
⊢ HPow.hPow (α := Submodule R A) ⊥ (n + 2) = ⊥

Tactic:
rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]

Premises used: Submodule.pow_succ, Nat.succ_ne_zero, Submodule.bot_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
h : Ne (α := ℕ) 0 0
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0

Tactic:
(h rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
h : Ne (α := ℕ) 0 0
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0

Tactic:
exact (h rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
succ : (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid
⊢ (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)

Tactic:
rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]

Premises used: pow_succ, Submodule.pow_succ, Submodule.mul_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
succ₁ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
succ₂ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = M.toAddSubmonoid
succ₃ : (1 * M).toAddSubmonoid = M.toAddSubmonoid
succ₄ succ₅ : M.toAddSubmonoid = M.toAddSubmonoid
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid

Tactic:
rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]

Premises used: Submodule.pow_zero, pow_zero, Submodule.mul_toAddSubmonoid, Submodule.one_mul, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n + 1 ≠ 0), (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
h : n + 1 + 1 ≠ 0
succ succ₁ : M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
⊢ (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid

Tactic:
rw [ih n.succ_ne_zero]

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
succ :
  ∀ (ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0)
    (h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0),
    (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid =
      HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
succ₁ :
  ∀ (n : ℕ) (ih : ∀ (h : n + 1 ≠ 0), (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)) (h : n + 1 + 1 ≠ 0),
    (M ^ (n + 1)).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ (n + 1) * M.toAddSubmonoid
⊢ (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid

Tactic:
cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

Premises used: Submodule.pow_zero, pow_zero, Submodule.mul_toAddSubmonoid, Submodule.one_mul, Submodule.zero, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
zero : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
succ :
  ∀ (n : ℕ) (ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n) (h : n + 1 ≠ 0),
    (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n

Tactic:
induction n with
  | zero => exact (h rfl).elim
  | succ n ih =>
    rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
    cases n with
    | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
    | succ n => rw [ih n.succ_ne_zero]

Premises used: Submodule.pow_zero, pow_succ, False.elim, Submodule.pow_succ, pow_zero, Submodule.mul_toAddSubmonoid, Submodule.one_mul, Submodule.zero, one_mul
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
inl : HPow.hPow (β := ℕ) M.toAddSubmonoid 0 ≤ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid
inr : ∀ (hn : n ≠ 0), M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
obtain rfl | hn := Decidable.eq_or_ne n 0

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ LE.le.{v} (α := AddSubmonoid A) 1 (toAddSubmonoid.{u, v} (R := R) 1)

Tactic:
le_one_toAddSubmonoid

Premises used: Set.Mem, Submodule.le_one_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ LE.le.{v} (α := AddSubmonoid A) 1 (toAddSubmonoid.{u, v} (R := R) 1)

Tactic:
exact le_one_toAddSubmonoid

Premises used: Submodule.le_one_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
(pow_toAddSubmonoid M hn).ge

Premises used: Eq.ge, Submodule.pow_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid

Tactic:
exact (pow_toAddSubmonoid M hn).ge

Premises used: Eq.ge, Submodule.pow_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
⊢ (↑M : Set A) ^ n ⊆ (↑(M ^ n) : Set A)

Tactic:
trans AddSubmonoid.pow_subset_pow (le_pow_toAddSubmonoid M)

Premises used: trans, AddSubmonoid.pow_subset_pow, Submodule.le_pow_toAddSubmonoid
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
x : A
hx : x ∈ M
n : ℕ
⊢ x ^ n ∈ M ^ n

Tactic:
pow_subset_pow _ <| Set.pow_mem_pow hx

Premises used: Set.pow_mem_pow, Submodule.pow_subset_pow
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SMul A B
inst_4 : Module A C
inst_5 : Module B C
inst_6 : IsScalarTower A C C
inst_7 : IsScalarTower B C C
inst_8 : IsScalarTower A B C
I : Submodule B C
h : Ne (α := ℕ) 1 0
⊢ restrictScalars A (HPow.hPow (β := ℕ) I 1) = HPow.hPow (α := Submodule A C) (β := ℕ) (restrictScalars A I) 1

Tactic:
simp [Submodule.pow_one]

Premises used: Submodule.pow_one
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Semiring A
inst_1 : Semiring B
inst_2 : Semiring C
inst_3 : SMul A B
inst_4 : Module A C
inst_5 : Module B C
inst_6 : IsScalarTower A C C
inst_7 : IsScalarTower B C C
inst_8 : IsScalarTower A B C
I : Submodule B C
n : ℕ
h : n + 2 ≠ 0
⊢ restrictScalars A (I ^ (n + 2)) = HPow.hPow (α := Submodule A C) (restrictScalars A I) (n + 2)

Tactic:
simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

Premises used: Submodule.restrictScalars_mul, Submodule.pow_succ, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
rw : Eq (α := Submodule R A) (R ∙ 1) (LinearMap.range (Algebra.linearMap R A))
rw₁ :
  Eq (α := Submodule R A) (LinearMap.range (LinearMap.toSpanSingleton R A 1)) (LinearMap.range (Algebra.linearMap R A))
rw₂ rw₃ : Eq (α := Submodule R A) (LinearMap.range (Algebra.linearMap R A)) (LinearMap.range (Algebra.linearMap R A))
⊢ Eq (α := Submodule R A) 1 (LinearMap.range (Algebra.linearMap R A))

Tactic:
rw [one_eq_span, LinearMap.span_singleton_eq_range,
    LinearMap.toSpanSingleton_one_eq_algebraLinearMap]

Premises used: LinearMap.toSpanSingleton_one_eq_algebraLinearMap, LinearMap.span_singleton_eq_range, Submodule.one_eq_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
r : R
⊢ Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simp [one_eq_range]

Premises used: Submodule.one_eq_range
-- 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
⊢ Membership.mem (γ := Submodule R A) 1 x ↔ ∃ (y : R), (algebraMap R A : (a : R) → A) y = x

Tactic:
simp [one_eq_range]

Premises used: Submodule.one_eq_range
-- 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
rw : HSMul.hSMul (β := Submodule R A) x (R ∙ 1) = R ∙ x
rw₁ : Eq (α := Submodule R A) (span R (HSMul.hSMul (β := Set A) x {1})) (R ∙ x)
rw₂ : Eq (α := Submodule R A) (R ∙ HSMul.hSMul (β := A) x 1) (R ∙ x)
rw₃ : Eq (α := Submodule R A) (R ∙ x * 1) (R ∙ x)
rw₄ rw₅ : Eq (α := Submodule R A) (R ∙ x) (R ∙ x)
⊢ HSMul.hSMul (β := Submodule R A) x 1 = R ∙ x

Tactic:
rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]

Premises used: Set.smul_set_singleton, Submodule.smul_span, smul_eq_mul, mul_one, Submodule.one_eq_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
r : R
h : IsUnit r
rw : span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))
| 1

Tactic:
rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, Submodule.span_singleton_smul_eq, Submodule.one_eq_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
r : R
h : IsUnit r
conv_rhs : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
conv_rhs₁ :
  Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A)))
    (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A)))
⊢ Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1

Tactic:
conv_rhs => rw [one_eq_span, ← span_singleton_smul_eq h, ← algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, Submodule.span_singleton_smul_eq, Submodule.one_eq_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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
h : ∀ (x : A'), x ∈ map f.toLinearMap 1 ↔ Membership.mem (γ := Submodule R A') 1 x
⊢ map f.toLinearMap 1 = 1

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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
x : A'
⊢ x ∈ map f.toLinearMap 1 ↔ Membership.mem (γ := Submodule R A') 1 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
h :
  ∀ (x : Aᵐᵒᵖ),
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
      Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 x
⊢ Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1

Tactic:
ext x
-- 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ᵐᵒᵖ
h :
  ∀ (X : A),
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) (op X) ↔
      Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 (op X)
⊢ Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 x

Tactic:
induction x
-- 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
⊢ Membership.mem (γ := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) (op X) ↔
    Membership.mem (γ := Submodule R Aᵐᵒᵖ) 1 (op 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
h :
  ∀ (x : A),
    Membership.mem (γ := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
      Membership.mem (γ := Submodule R A) 1 x
⊢ Eq.{v + 1} (α := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1

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
x : A
⊢ Membership.mem (γ := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) x ↔
    Membership.mem (γ := Submodule R A) 1 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
rw : Eq.{v + 1} (α := Submodule R A) (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
rw₁ rw₂ : Eq.{v + 1} (α := Submodule R A) 1 1
⊢ Eq.{v + 1} (α := Submodule R A) (map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1

Tactic:
rw [← comap_equiv_eq_map_symm, comap_op_one]

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.comap_op_one
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
rw : Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) 1) 1
rw₁ rw₂ : Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) 1 1
⊢ Eq.{v + 1} (α := Submodule R Aᵐᵒᵖ) (comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) 1) 1

Tactic:
rw [← map_equiv_eq_comap_symm, map_op_one]

Premises used: Submodule.map_equiv_eq_comap_symm, Submodule.map_op_one
-- 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 = map₂ (LinearMap.mul R A) M N

Tactic:
le_antisymm (mul_le.mpr fun _m hm _n ↦ apply_mem_map₂ _ hm)
    (map₂_le.mpr fun _m hm _n ↦ mul_mem_mul hm)

Premises used: Iff.mpr, Submodule.mul_mem_mul, Submodule.apply_mem_map₂, le_antisymm, Submodule.map₂_le, Submodule.mul_le, LinearMap.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
S T : Set A
rw : Eq (α := Submodule R A) (map₂ (LinearMap.mul R A) (span R S) (span R T)) (span R (S * T))
⊢ HMul.hMul (α := Submodule R A) (span R S) (span R T) = span R (S * T)

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 : Set A
⊢ Eq (α := Submodule R A) (map₂ (LinearMap.mul R A) (span R S) (span R T)) (span R (S * T))

Tactic:
apply map₂_span_span

Premises used: Submodule.map₂_span_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 N : Submodule R A
⊢ M * N = span R ((↑M : Set A) * (↑N : Set A))

Tactic:
simp [← span_mul_span]

Premises used: 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
rw : HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1)
| M * 1

Tactic:
rw [one_eq_span, ← span_eq M]

Premises used: Submodule.span_eq, Submodule.one_eq_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
conv_lhs : HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1) = M
⊢ M * 1 = M

Tactic:
conv_lhs => rw [one_eq_span, ← span_eq M]

Premises used: Submodule.span_eq, Submodule.one_eq_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
rw : span R ((↑M : Set A) * {1}) = M
⊢ HMul.hMul (α := Submodule R A) (span R (↑M : Set A)) (R ∙ 1) = M

Tactic:
rw [span_mul_span]

Premises used: 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
⊢ span R ((↑M : Set A) * {1}) = M

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'
rw :
  map f.toLinearMap (map₂ (LinearMap.mul R A) M N) =
    ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N)
⊢ map f.toLinearMap (M * N) =
    ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N)

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
M N : Submodule R A
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) =
    ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N)

Tactic:
apply map_iSup

Premises used: Submodule.map_iSup
-- 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'
rw :
  ⨆ (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)
⊢ ⨆ (i : ↥M), map f.toLinearMap (map (σ₁₂ := RingHom.id R) ((LinearMap.mul R A : (a : A) → A →ₗ[R] A) (↑i : A)) N) =
    map f.toLinearMap M * map f.toLinearMap N

Tactic:
rw [mul_eq_map₂]

Premises used: Submodule.mul_eq_map₂