awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.TensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
i j : ι
⊢ ∀ {gi gj : S ⊗[R] A},
    Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 i)) gi →
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 j)) gj →
        Membership.mem (γ := Submodule S (S ⊗[R] A)) (Submodule.baseChange S (𝒜 (i + j))) (gi * gj)
have suffices : LE.le (α := Submodule S (S ⊗[R] A))
  (Submodule.map₂ (M := S ⊗[R] A) (N := S ⊗[R] A)
    (↑(Algebra.lmul S (S ⊗[R] A)) :
      [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
        [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
              (Module.End S (S ⊗[R] A))] →
          S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A))
    (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)))
  (Submodule.baseChange S (𝒜 (i + j)))
Tactic: suffices h : ((𝒜 i).baseChange S).map₂ (Algebra.lmul S (S ⊗[R] A)) ((𝒜 j).baseChange S) ≤
      (𝒜 (i + j)).baseChange S from fun xi xj ↦ (h <| apply_mem_map₂ _ · ·)
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.TensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq ι
inst_4 : AddMonoid ι
inst_5 : Semiring A
inst_6 : Algebra R A
𝒜 : ι → Submodule R A
inst_7 : GradedAlgebra 𝒜
i j : ι
⊢ LE.le (α := Submodule S (S ⊗[R] A))
    (Submodule.map₂ (M := S ⊗[R] A) (N := S ⊗[R] A)
      (↑(Algebra.lmul S (S ⊗[R] A)) :
        [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
          [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                (Module.End S (S ⊗[R] A))] →
            S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A))
      (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)))
    (Submodule.baseChange S (𝒜 (i + j)))
have simp_rw : ∀
  x ∈
    (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1) (𝒜 i)) :
      Set (S ⊗[R] A)),
  ∀
    y ∈
      (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1) (𝒜 j)) :
        Set (S ⊗[R] A)),
    Membership.mem (α := S ⊗[R] A)
      (↑(span S
            (↑(Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R S A : (a : S) → A →ₗ[R] S ⊗[R] A) 1)
                  (𝒜 (i + j))) :
              Set (S ⊗[R] A))) :
        Set (S ⊗[R] A))
      (((((↑(Algebra.lmul S (S ⊗[R] A)) :
                    [inst_8 : FunLike (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (S ⊗[R] A) (Module.End S (S ⊗[R] A))] →
                      [SemilinearMapClass (S ⊗[R] A →ₐ[S] Module.End S (S ⊗[R] A)) (RingHom.id S) (S ⊗[R] A)
                            (Module.End S (S ⊗[R] A))] →
                        S ⊗[R] A →ₗ[S] Module.End S (S ⊗[R] A)) :
                  (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] S ⊗[R] A)
                x :
              S ⊗[R] A →ₗ[S] S ⊗[R] A) :
            (a : S ⊗[R] A) → S ⊗[R] A)
          y :
        S ⊗[R] A)
Tactic: simp_rw [baseChange_eq_span, map₂_span_span, span_le, Set.image2_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.TensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
x : S ⊗[R] A
hx : Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i)) x
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        x :
      B)
have obtain : ∀ (x : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i))
  (hx :
    Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
      (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)),
  Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
      B)
Tactic: obtain ⟨x, rfl⟩ := toBaseChange_surjective' _ _ hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.TensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
x : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
      B)
have zero : ∀
  (hx :
    Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
      (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A)),
  Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A) :
      B)
Tactic: induction x with
        | zero => simp
        | add => simp_all [add_mem]
        | tmul r x => simpa using smul_mem _ _ <| by exact f.map_mem x.2
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
N₁ N₂ : G(k, M; R)
h : N₁.toSubmodule = N₂.toSubmodule
⊢ N₁ = N₂
have mk : ∀ (toSubmodule : Submodule R M) (finite_quotient : Module.Finite.{u, v} R (M ⧸ toSubmodule))
  (projective_quotient : Projective.{u, v} R (M ⧸ toSubmodule))
  (rankAtStalk_eq : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule) p = k)
  (h :
    { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
          rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
      N₂.toSubmodule),
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
      rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
    N₂
Tactic: cases N₁
Cleared hypotheses: N₁, h
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
N₂ : G(k, M; R)
toSubmodule : Submodule R M
finite_quotient : Module.Finite.{u, v} R (M ⧸ toSubmodule)
projective_quotient : Projective.{u, v} R (M ⧸ toSubmodule)
rankAtStalk_eq : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule) p = k
h :
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
    N₂.toSubmodule
⊢ { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
      rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
    N₂
have mk : ∀ (toSubmodule_1 : Submodule R M) (finite_quotient_1 : Module.Finite.{u, v} R (M ⧸ toSubmodule_1))
  (projective_quotient_1 : Projective.{u, v} R (M ⧸ toSubmodule_1))
  (rankAtStalk_eq_1 : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule_1) p = k)
  (h :
    { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
          rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
      { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1,
          projective_quotient := projective_quotient_1, rankAtStalk_eq := rankAtStalk_eq_1 : G(k, M; R) }.toSubmodule),
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
      rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
    { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1, projective_quotient := projective_quotient_1,
      rankAtStalk_eq := rankAtStalk_eq_1 }
Tactic: cases N₂
Cleared hypotheses: N₂, h
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    k
have _ : rankAtStalk
    (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
    p =
  rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p
Tactic: calc
        _ = rankAtStalk (R := B) (B ⊗[A] ((A ⊗[R] M) ⧸ N.toSubmodule)) p := by
          simpa using congrArg (fun g => g p) <| Module.rankAtStalk_eq_of_equiv equiv
        _ = rankAtStalk (R := A) (A ⊗[R] M ⧸ N.toSubmodule)
            (PrimeSpectrum.comap (algebraMap A B) p) := by
          simpa using Module.rankAtStalk_baseChange ..
        _ = k := N.rankAtStalk_eq _
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
_ :
  rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p
⊢ rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    k
have _₁ : rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p =
  rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p)
Tactic: calc
        _ = rankAtStalk (R := B) (B ⊗[A] ((A ⊗[R] M) ⧸ N.toSubmodule)) p := by
          simpa using congrArg (fun g => g p) <| Module.rankAtStalk_eq_of_equiv equiv
        _ = rankAtStalk (R := A) (A ⊗[R] M ⧸ N.toSubmodule)
            (PrimeSpectrum.comap (algebraMap A B) p) := by
          simpa using Module.rankAtStalk_baseChange ..
        _ = k := N.rankAtStalk_eq _
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : CommAlgCat.{u_1, u} R
N : G(k, TensorProduct.{u, u_1, v} R (↑A : Type u_1) M; (↑A : Type u_1))
⊢ map (AlgHom.id R (↑A : Type u_1)) N = N
have h : (map (AlgHom.id R (↑A : Type u_1)) N).toSubmodule = N.toSubmodule
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
⊢ IsScalarTower A B C
have h : Eq (α := A →+* C) (algebraMap A C)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B))
Tactic: apply IsScalarTower.of_algebraMap_eq'
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (hypothesis)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
⊢ map (g.comp f) N = map g (map f N)
have hfAB : Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
  (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
Tactic: have hfAB : Function.Surjective fAB :=
    (LinearMap.baseChange_surjective B (Submodule.mkQ_surjective _)).comp
      (cancelBaseChange R A B B M).symm.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
⊢ map (g.comp f) N = map g (map f N)
have h : ∀ (x : C ⊗[R] M), x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (hypothesis)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
Tactic: have hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker := map_toSubmodule (g.comp f) N
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ (map g (map f N)).toSubmodule = fBC.ker
have rw : LinearMap.ker (M₂ := C ⊗[B] (B ⊗[R] M ⧸ (map f N).toSubmodule)) (baseChangeMkQ C (map f N).toSubmodule) = fBC.ker
Tactic: rw [map_toSubmodule g (map f N), map_toSubmodule f N]
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
rw : LinearMap.ker (M₂ := C ⊗[B] (B ⊗[R] M ⧸ (map f N).toSubmodule)) (baseChangeMkQ C (map f N).toSubmodule) = fBC.ker
⊢ (map g (map f N)).toSubmodule = fBC.ker
have rw₁ : LinearMap.ker (M₂ :=
    C ⊗[B]
      HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
    (baseChangeMkQ C (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule))) =
  fBC.ker
Tactic: rw [map_toSubmodule g (map f N), map_toSubmodule f N]
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (hypothesis)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
Tactic: have hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker := by
    rw [map_toSubmodule g (map f N), map_toSubmodule f N]
-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
⊢ fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
have h : ∀ (x : C ⊗[R] M),
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) x : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC :
          (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        x :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
Tactic: apply LinearMap.ext