awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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
⊢ ∃ (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
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s t : Submodule R A
⊢ s * t = span R ((↑s : Set A) * (↑t : Set A))
have rw : map₂ (LinearMap.mul R A) s t = span R ((↑s : Set A) * (↑t : Set A))
Tactic: rw [mul_eq_map₂]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P Q : Submodule R A
x : A
hx : x ∈ P * Q
⊢ Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
have rwa : ∀ (hx : x ∈ span R (↑P : Set A) * Q), 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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
⊢ Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
have 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
Tactic: rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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
⊢ Membership.mem (γ := Submodule R A) (span R ((↑P : Set A) * (↑Q : Set A))) x
have 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
Tactic: rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x
have simp_rw : x ∈ map₂ (LinearMap.mul R A) (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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P : Submodule R A
x y : A
simp_rw : x ∈ map₂ (LinearMap.mul R A) (R ∙ y) P ↔ ∃ z ∈ P, y * z = x
⊢ x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x
have 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
Tactic: simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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
⊢ x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x
have 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
Tactic: simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x
have simp_rw : x ∈ map₂ (LinearMap.mul R A) 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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
P : Submodule R A
x y : A
simp_rw : x ∈ map₂ (LinearMap.mul R A) P (R ∙ y) ↔ ∃ z ∈ P, z * y = x
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x
have 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
Tactic: simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x
have 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
Tactic: simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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
⊢ x ∈ P * (R ∙ y) ↔ ∃ z ∈ P, z * y = x
have 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
Tactic: simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map_flip, mem_map, LinearMap.flip_apply,
    LinearMap.mul_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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
⊢ y ∈ x • p ↔ x⁻¹ * y ∈ p
have mp : y ∈ x • p → x⁻¹ * y ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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
⊢ y ∈ x • p ↔ x⁻¹ * y ∈ p
have mpr : x⁻¹ * y ∈ p → y ∈ x • p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ HPow.hPow (α := Submodule R A) (β := ℕ) (span R s) 0 = span R (HPow.hPow (β := ℕ) s 0)
have rw : Eq (α := Submodule R A) 1 (span R (HPow.hPow (β := ℕ) s 0))
Tactic: rw [pow_zero, pow_zero, one_eq_span_one_set]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
rw : Eq (α := Submodule R A) 1 (span R (HPow.hPow (β := ℕ) s 0))
⊢ HPow.hPow (α := Submodule R A) (β := ℕ) (span R s) 0 = span R (HPow.hPow (β := ℕ) s 0)
have rw₁ : Eq.{v + 1} (α := Submodule R A) 1 (span R 1)
Tactic: rw [pow_zero, pow_zero, one_eq_span_one_set]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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)
⊢ HPow.hPow (α := Submodule R A) (β := ℕ) (span R s) 0 = span R (HPow.hPow (β := ℕ) s 0)
have rw₂ : Eq.{v + 1} (α := Submodule R A) (span R 1) (span R 1)
Tactic: rw [pow_zero, pow_zero, one_eq_span_one_set]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
n : ℕ
⊢ HPow.hPow (α := Submodule R A) (span R s) (n + 1) = span R (s ^ (n + 1))
have rw : HPow.hPow (α := Submodule R A) (span R s) n * span R s = span R (s ^ (n + 1))
Tactic: rw [pow_succ, pow_succ, span_pow s n, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
n : ℕ
rw : HPow.hPow (α := Submodule R A) (span R s) n * span R s = span R (s ^ (n + 1))
⊢ HPow.hPow (α := Submodule R A) (span R s) (n + 1) = span R (s ^ (n + 1))
have rw₁ : HPow.hPow (α := Submodule R A) (span R s) n * span R s = span R (s ^ n * s)
Tactic: rw [pow_succ, pow_succ, span_pow s n, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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)
⊢ HPow.hPow (α := Submodule R A) (span R s) (n + 1) = span R (s ^ (n + 1))
have rw₂ : HMul.hMul (α := Submodule R A) (span R (s ^ n)) (span R s) = span R (s ^ n * s)
Tactic: rw [pow_succ, pow_succ, span_pow s n, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
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)
⊢ HPow.hPow (α := Submodule R A) (span R s) (n + 1) = span R (s ^ (n + 1))
have rw₃ : Eq (α := Submodule R A) (span R (s ^ n * s)) (span R (s ^ n * s))
Tactic: rw [pow_succ, pow_succ, span_pow s n, span_mul_span]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
n : ℕ
⊢ M ^ n = span R ((↑M : Set A) ^ n)
have rw : M ^ n = HPow.hPow (α := Submodule R A) (span R (↑M : Set A)) n
Tactic: rw [← span_pow, span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : Submodule R A
n : ℕ
rw : M ^ n = HPow.hPow (α := Submodule R A) (span R (↑M : Set A)) n
⊢ M ^ n = span R ((↑M : Set A) ^ n)
have rw₁ : M ^ n = M ^ n
Tactic: rw [← span_pow, span_eq]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
N P : Submodule R A
h : N * P = 1
| ⊤
have rw : ⊤ * N * P
Tactic: rw [← mul_one ⊤, ← h, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
N P : Submodule R A
h : N * P = 1
⊢ ⊤ ≤ ⊤ * P
have conv_lhs : ⊤ * N * P ≤ ⊤ * P
Tactic: conv_lhs => rw [← mul_one ⊤, ← h, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C 0 x hx
have hx₁ : Membership.mem (γ := Submodule R A) 1 x
Tactic: rw [pow_zero] at hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C 0 x hx_1
have 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
Tactic: obtain ⟨r, rfl⟩ := mem_one.mp hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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)
⊢ C (n + 1) x hx
have succ : ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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)), C (n + 1) x hx
have succ : ∀ (hx : x ∈ M * M ^ n), C (n + 1) x sorry
Tactic: simp_rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C n x hx
have zero : ∀ {x : A} (hx : x ∈ HPow.hPow (β := ℕ) M 0), C 0 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
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C n x hx
have 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
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
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C 0 x hx
have hx₁ : Membership.mem (γ := Submodule R A) 1 x
Tactic: rw [pow_zero] at hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C 0 x hx_1
have 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
Tactic: obtain ⟨r, rfl⟩ := mem_one.mp hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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)
⊢ C (n + 1) x hx
have succ : ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx
Tactic: revert hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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)), C (n + 1) x hx
have succ : ∀ (hx : x ∈ M ^ n * M), C (n + 1) x sorry
Tactic: simp_rw [pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C n x hx
have zero : ∀ {x : A} (hx : x ∈ HPow.hPow (β := ℕ) M 0), C 0 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
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
M : 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
⊢ C n x hx
have 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
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
Cleared hypotheses: n, x, hx