awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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
⊢ a • S • T = S • a • T
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)
⊢ a • S • T = S • a • T
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have rw₆ : HSMul.hSMul (β := Submodule R A) a (span R ((↑S : Set A) * (↑T : Set A))) = span R ((↑S : Set A) * a • (↑T : Set A))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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))
⊢ a • S • T = S • a • T
have rw₇ : Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R ((↑S : Set A) * a • (↑T : Set A)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
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)))
⊢ a • S • T = S • a • T
have rw₈ : Eq (α := Submodule R A) (span R (a • ((↑S : Set A) * (↑T : Set A)))) (span R (a • ((↑S : Set A) * (↑T : Set A))))
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]
-- 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
⊢ ∃ (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 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
Tactic: obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx
-- 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
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
have 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
Tactic: obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h
-- 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
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'
⊢ ∃ (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 : Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
Tactic: use T, T', hS, hS'
-- 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
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)
have assumption_mod_cast : U ≤ T * T'
Tactic: assumption_mod_cast
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (hypothesis)
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'
⊢ Membership.mem (γ := Submodule R A) (span R ((↑T : Set A) * (↑T' : Set A))) x
have h' : (↑U : Set A) ⊆ (↑T : Set A) * (↑T' : Set A)
Tactic: have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
-- 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
⊢ ∃ (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 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
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_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
have 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
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_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
⊢ ∃ (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'),
  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_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
⊢ ∃ (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)),
  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