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 : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx : x ∈ HPow.hPow (β := ℕ) M 0
⊢ Membership.mem (γ := Submodule R A) 1 x

Tactic:
rw [pow_zero] at hx

Premises used: pow_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
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
x : A
hx_1 : x ∈ HPow.hPow (β := ℕ) M 0
hx : Membership.mem (γ := Submodule R A) 1 x
zero :
  ∀ (r : R) (hx : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A))
    (hx_2 : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)),
    C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx
⊢ C 0 x hx_1

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp hx

Premises used: Submodule.mem_one, Iff.mp, 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 : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
r : R
hx_1 : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A)
hx : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx_1

Tactic:
algebraMap r
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
r : R
hx_1 : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A)
hx : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx_1

Tactic:
exact algebraMap r
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ (n + 1)
succ : ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
⊢ C (n + 1) x hx

Tactic:
revert hx
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
succ : ∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯
⊢ ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx

Tactic:
simp_rw [pow_succ']

Premises used: pow_succ'
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯

Tactic:
fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Premises used: Submodule.mul_induction_on'
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M * M ^ n), C (n + 1) x ⋯

Tactic:
exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mem_mul : ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
zero : ∀ {x : A} (hx : x ∈ HPow.hPow (β := ℕ) M 0), C 0 x hx
succ : ∀ (n : ℕ) (n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx) {x : A} (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
⊢ C n x hx

Tactic:
induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ']
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mem_mul _ hm _ _ _ (n_ih ih))
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Premises used: pow_zero, Submodule.mem_one, Iff.mp, Submodule.zero, pow_succ', 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 : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx : x ∈ HPow.hPow (β := ℕ) M 0
⊢ Membership.mem (γ := Submodule R A) 1 x

Tactic:
rw [pow_zero] at hx

Premises used: pow_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
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
x : A
hx_1 : x ∈ HPow.hPow (β := ℕ) M 0
hx : Membership.mem (γ := Submodule R A) 1 x
zero :
  ∀ (r : R) (hx : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A))
    (hx_2 : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)),
    C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx
⊢ C 0 x hx_1

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp hx

Premises used: Submodule.mem_one, Iff.mp, 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 : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
r : R
hx_1 : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A)
hx : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx_1

Tactic:
algebraMap r
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
r : R
hx_1 : Membership.mem (α := A) (HPow.hPow (β := ℕ) M 0) ((Algebra.algebraMap R A : (a : R) → A) r : A)
hx : Membership.mem.{v, v} (α := A) (γ := Submodule R A) 1 ((Algebra.algebraMap R A : (a : R) → A) r : A)
⊢ C 0 ((Algebra.algebraMap R A : (a : R) → A) r) hx_1

Tactic:
exact algebraMap r
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ (n + 1)
succ : ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
⊢ C (n + 1) x hx

Tactic:
revert hx
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
succ : ∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯
⊢ ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx

Tactic:
simp_rw [pow_succ]

Premises used: pow_succ
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯

Tactic:
fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Premises used: Submodule.mul_induction_on'
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯

Tactic:
exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx
-- 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
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
x : A
hx : x ∈ M ^ n
zero : ∀ {x : A} (hx : x ∈ HPow.hPow (β := ℕ) M 0), C 0 x hx
succ : ∀ (n : ℕ) (n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx) {x : A} (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
⊢ C n x hx

Tactic:
induction n generalizing x with
  | zero =>
    rw [pow_zero] at hx
    obtain ⟨r, rfl⟩ := mem_one.mp hx
    exact algebraMap r
  | succ n n_ih =>
    revert hx
    simp_rw [pow_succ]
    exact fun hx ↦ Submodule.mul_induction_on' (fun m hm x ih => mul_mem _ _ hm (n_ih _) _ ih)
      (fun x hx y hy Cx Cy => add _ _ _ _ _ Cx Cy) hx

Premises used: pow_succ, pow_zero, Submodule.mem_one, Iff.mp, Submodule.zero, 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 : Submodule R A
C : A → Prop
hr : ∀ (r : R), C ((algebraMap R A : (a : R) → A) r)
hadd : ∀ (x y : A), C x → C y → C (x + y)
hmul : ∀ m ∈ M, ∀ (x : A), C x → C (m * x)
x : A
n : ℕ
hx : x ∈ M ^ n
⊢ C x

Tactic:
Submodule.pow_induction_on_left' M (C := fun _ a _ => C a) hr
    (fun x y _i _hx _hy => hadd x y)
    (fun _m hm _i _x _hx => hmul _ hm _) hx

Premises used: Submodule.pow_induction_on_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
M : Submodule R A
C : A → Prop
hr : ∀ (r : R), C ((algebraMap R A : (a : R) → A) r)
hadd : ∀ (x y : A), C x → C y → C (x + y)
hmul : ∀ (x : A), C x → ∀ m ∈ M, C (x * m)
x : A
n : ℕ
hx : x ∈ M ^ n
⊢ C x

Tactic:
Submodule.pow_induction_on_right' (M := M) (C := fun _ a _ => C a) hr
    (fun x y _i _hx _hy => hadd x y)
    (fun _i _x _hx => hmul _) hx

Premises used: Submodule.pow_induction_on_right'
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Submodule R A →+* Submodule R A) (mapHom (AlgHom.id R A)) (RingHom.id (Submodule R A))

Tactic:
RingHom.ext map_id

Premises used: Submodule.map_id, RingHom.ext
-- 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
p q : Submodule R Aᵐᵒᵖ
⊢ op (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (p + q)) =
    op (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) p) + op (comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) q)

Tactic:
simp [comap_equiv_eq_map_symm, ← op_add]

Premises used: Submodule.comap_equiv_eq_map_symm, MulOpposite.op_add
-- 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
A' : Type u_1
inst_3 : Semiring A'
inst_4 : Algebra R A'
f : A →ₐ[R] A'
n : ℕ
⊢ map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n

Tactic:
map_pow (mapHom f) M n

Premises used: Submodule.mapHom, map_pow, Submodule.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 : Submodule R A
n : ℕ
⊢ comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n

Tactic:
(equivOpposite : Submodule R Aᵐᵒᵖ ≃+* _).symm.map_pow (op M) n

Premises used: Set.Mem, Submodule.equivOpposite, RingEquiv.map_pow, Submodule.comap, MulOpposite.unop, RingEquiv.symm, 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
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n

Tactic:
op_injective <| (equivOpposite : Submodule R Aᵐᵒᵖ ≃+* _).map_pow M n

Premises used: MulOpposite.op_injective, Submodule.equivOpposite, RingEquiv.map_pow
-- 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 :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
rw₁ :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
rw₂ rw₃ :
  comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n =
    comap (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
⊢ map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n

Tactic:
rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]

Premises used: Submodule.map_equiv_eq_comap_symm, Submodule.comap_unop_pow
-- 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 : ℕ
M : Submodule R Aᵐᵒᵖ
rw :
  comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n
rw₁ : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (M ^ n) = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
rw₂ rw₃ : comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n = comap (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) M ^ n
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
    map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) M ^ n

Tactic:
rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]

Premises used: Submodule.comap_equiv_eq_map_symm, Submodule.comap_op_pow
-- 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
⊢ Eq.{v + 1} (α := Submodule R A)
    (OneHom.toFun
      (↑(MonoidHom.comp (↑span.ringHom : SetSemiring A →* Submodule R A) SetSemiring.singletonMonoidHom) :
        OneHom A (Submodule R A))
      0)
    0

Tactic:
simp [SetSemiring.singletonMonoidHom]

Premises used: SetSemiring.singletonMonoidHom
-- 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
⊢ Eq (α := Submodule R A) ((spanSingleton R : (a : A) → Submodule R A) x : Submodule R A) (R ∙ x : Submodule R A)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.singleton, Submodule.span, 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
inst_3 : FaithfulSMul R A
x : A
h : Eq (α := Submodule R A) (R ∙ x) 1
obtain :
  ∀ (r : R) (h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1),
    ∃ (r_1 : Rˣ),
      Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
⊢ ∃ (r : Rˣ), x = (algebraMap R A : (a : R) → A) (↑r : R)

Tactic:
obtain ⟨r, rfl⟩ := mem_one.mp (h ▸ mem_span_singleton_self x)

Premises used: Submodule.mem_one, Iff.mp, 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
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
have :
  ∀ (r' : R) (eq : HSMul.hSMul (β := A) r' ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) 1),
    ∃ (r_1 : Rˣ),
      Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)
⊢ ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)

Tactic:
have ⟨r', eq⟩ := mem_span_singleton.mp (h ▸ algebraMap_mem 1)
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
r' : R
eq : HSMul.hSMul (β := A) r' ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) 1
⊢ r' * r = 1

Tactic:
rw [Algebra.smul_def, ← map_mul, (FaithfulSMul.algebraMap_injective R A).eq_iff] at eq

Premises used: Function.Injective.eq_iff, map_mul, FaithfulSMul.algebraMap_injective, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
r' : R
eq : r' * r = 1
⊢ ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)

Tactic:
⟨.mkOfMulEqOne _ _ (mul_comm _ r ▸ eq), rfl⟩

Premises used: Units.mkOfMulEqOne, Exists.intro, 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
inst_3 : FaithfulSMul R A
r : R
h : Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) r : A))) 1
r' : R
eq : r' * r = 1
⊢ ∃ (r_1 : Rˣ),
    Eq.{v + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) (↑r_1 : R) : A)

Tactic:
exact ⟨.mkOfMulEqOne _ _ (mul_comm _ r ▸ eq), 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
inst_3 : FaithfulSMul R A
r : Rˣ
⊢ Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) (↑r : R) : A))) 1

Tactic:
span_singleton_algebraMap_of_isUnit r.isUnit

Premises used: Submodule.span_singleton_algebraMap_of_isUnit, Units.isUnit
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
r : Rˣ
⊢ Eq (α := Submodule R A) (span R (singleton (α := A) ((algebraMap R A : (a : R) → A) (↑r : R) : A))) 1

Tactic:
exact span_singleton_algebraMap_of_isUnit r.isUnit

Premises used: Submodule.span_singleton_algebraMap_of_isUnit, Units.isUnit
-- Module: Mathlib.Algebra.Algebra.Operations
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
h :
  ∀ (x : A),
    Membership.mem (γ := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R)) x ↔
      Membership.mem (γ := Submonoid A) (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R)) x
⊢ Eq (α := Submonoid A) (MonoidHom.mker (F := A →*₀ Submodule R A) (spanSingleton R))
    (Submonoid.map (F := R →+* A) (algebraMap R A) (IsUnit.submonoid R))

Tactic:
ext