awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
rwa :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
    (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₁ :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span R s) ⊤) (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₂ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀
      (hs₂ :
        Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
          (span R ((⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t)) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤
have rwa₃ : ∀ (hs₃ : s.Finite),
  let t := Function.surjInv sorry '' s;
  ∀
    (hs₂ :
      Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
        (Submodule.map (σ₁₂ := RingHom.id R) ((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) (span R t)) ⊤)
    (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
    Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
Cleared hypotheses: hs₂, hs₃, t, ht₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
rwa :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
    (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₁ :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span R s) ⊤) (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₂ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀
      (hs₂ :
        Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
          (span R ((⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t)) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₃ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀
      (hs₂ :
        Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
          (Submodule.map (σ₁₂ := RingHom.id R) ((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) (span R t)) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤
have rwa₄ : ∀ (hs₃ : s.Finite),
  let t := Function.surjInv sorry '' s;
  ∀ (hs₂ : Eq (α := Submodule R ↥N) (span R t) ⊤)
    (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
    Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
Cleared hypotheses: hs₂, hs₃, t, ht₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
have ht₂ : Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: have ht₂ : span R t = ⊤ := by
    rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
ht₂ : Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
have grw : s.ncard ≤ s.ncard
Tactic: grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank,
    ← hs₁, Set.ncard_image_le hs₃]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
fg : N.FG
this_1 : Module.{u_1, u_3} 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_3} R 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) := ⋯
⊢ N.spanFinrank =
    Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)
have rw : Module.finrank 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) =
  Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
    (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)
Tactic: rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free]
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
inst_5 : IsStablyFree R M
⊢ IsStablyFree R N
have obtain : ∀ (P : Type u) (hPc : AddCommGroup P) (hPm : Module R P) (hPfin : Module.Finite R P) (hPfree : Free R P),
  Free R (M × P) → IsStablyFree R N
Tactic: obtain ⟨P, hPc, hPm, hPfin, hPfree, _⟩ := IsStablyFree.exist_free_prod R M
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.Basic (goal)
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsStablyFree R M
⊢ Projective R M
have obtain : ∀ (N : Type u) (w : AddCommGroup N) (w_1 : Module R N), Module.Finite R N → Free R N → Free R (M × N) → Projective R M
Tactic: obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
⊢ Free R M
have inl : Subsingleton R → Free R M
Tactic: rcases subsingleton_or_nontrivial R with _ | _
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
inl : Subsingleton R → Free R M
⊢ Free R M
have inr : Nontrivial R → Free R M
Tactic: rcases subsingleton_or_nontrivial R with _ | _
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
⊢ Free R M
have inr : ∀ (N : Type u_1) (w : AddCommGroup N) (w_1 : Module R N), Module.Finite R N → Free R N → Free R (M × N) → Free R M
Tactic: obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
⊢ finrank R (M × N) = n + 1
have h1 : rankAtStalk M 𝔭 = 1
Tactic: have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
h1 : rankAtStalk M 𝔭 = 1
⊢ finrank R (M × N) = n + 1
have heq : rankAtStalk (M × N) 𝔭 =
  HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) 𝔭
Tactic: have heq := congr($(rankAtStalk_prod M N) 𝔭)
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
h1 : rankAtStalk M 𝔭 = 1
heq :
  rankAtStalk (M × N) 𝔭 =
    HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) 𝔭
⊢ finrank R (M × N) = n + 1
have heq₁ : (↑(finrank R (M × N)) : ℕ) = HAdd.hAdd (α := ℕ) 1 (↑(finrank R N) : ℕ)
Tactic: simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Algebra.Module.StablyFree.FreeOfInvertible (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
⊢ Free R M
have hp : finrank R (M × N) = n + 1
Tactic: have hp : Module.finrank R (M × N) = n + 1 := by
    let 𝔭 : PrimeSpectrum R := Nonempty.some inferInstance
    have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
    have heq := congr($(rankAtStalk_prod M N) 𝔭)
    simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq
    grind
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) =
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
have a : map₂ f (span R s) (span R t) ≤
  span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  map₂ f (span R s) (span R t) ≤
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
⊢ map₂ f (span R s) (span R t) =
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
have a₁ : span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t) ≤
  map₂ f (span R s) (span R t)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) ≤
    span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t)
have a : ∀ (m : M),
  Membership.mem (γ := Submodule R M) (span R s) m →
    ∀ (n : N),
      Membership.mem (γ := Submodule R N) (span R t) n →
        Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
Tactic: rw [map₂_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ ∀ (m : M),
    Membership.mem (γ := Submodule R M) (span R s) m →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
have a : ∀ (x : M) (h : x ∈ s) (n : N),
  Membership.mem (γ := Submodule R N) (span R t) n →
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
      ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)
Tactic: apply @span_induction R M _ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  ∀ (x : M) (h : x ∈ s) (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)
⊢ ∀ (m : M),
    Membership.mem (γ := Submodule R M) (span R s) m →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
have a₁ : ∀ (n : N),
  Membership.mem (γ := Submodule R N) (span R t) n →
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
      (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P)
Tactic: apply @span_induction R M _ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a :
  ∀ (x : M) (h : x ∈ s) (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)
a₁ :
  ∀ (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        (((f : (a : M) → N →ₗ[R] P) 0 : (a : N) → P) n : P)
⊢ ∀ (m : M),
    Membership.mem (γ := Submodule R M) (span R s) m →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n : P)
have a₂ : ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
  (hy : Membership.mem (γ := Submodule R M) (span R s) y),
  (∀ (n : N),
      Membership.mem (γ := Submodule R N) (span R t) n →
        Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
          (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
          ((((f : (a : M) → N →ₗ[R] P) x : N →ₗ[R] P) : (a : N) → P) n : P)) →
    (∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) y : N →ₗ[R] P) : (a : N) → P) n : P)) →
      ∀ (n : N),
        Membership.mem (γ := Submodule R N) (span R t) n →
          Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
            (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
            ((((f : (a : M) → N →ₗ[R] P) (x + y) : N →ₗ[R] P) : (a : N) → P) n : P)
Tactic: apply @span_induction R M _ _ _ s
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
⊢ ∀ (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) n : P)
have a₁ : ∀ (x : N) (h : x ∈ t),
  Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
    (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
    ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P)
Tactic: apply @span_induction R N _ _ _ t
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Bilinear (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
a : M
ha : a ∈ s
a₁ :
  ∀ (x : N) (h : x ∈ t),
    Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
      (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
      ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) x : P)
⊢ ∀ (n : N),
    Membership.mem (γ := Submodule R N) (span R t) n →
      Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
        (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
        ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) n : P)
have a₂ : Membership.mem.{u_4, u_4} (α := P) (γ := Submodule R P)
  (span R (image2 (fun (m : M) (n : N) ↦ (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n) s t))
  ((((f : (a : M) → N →ₗ[R] P) a : N →ₗ[R] P) : (a : N) → P) 0 : P)
Tactic: apply @span_induction R N _ _ _ t