awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c : C
m : M
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[R] m) : 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))
        (c ⊗ₜ[R] m) :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
have h : Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[A] Submodule.Quotient.mk (1 ⊗ₜ[R] m))
  (((cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule) :
        C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) :
      (a : C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (c ⊗ₜ[B] (fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (1 ⊗ₜ[R] m)))
Tactic: simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
-- 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
z : C ⊗[R] M
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) z : 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))
        z :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
have h : Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) 0)
  (((↑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))
    0)
Tactic: induction z using TensorProduct.induction_on with
    | zero => simp [fAC, fBC, e]
    | tmul c m =>
      simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
      simp [fAB, baseChangeMkQ]
    | add x y hx hy =>
      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *
      rw [hx, hy]
Cleared hypotheses: z
-- 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
z : C ⊗[R] M
h :
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) 0)
    (((↑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))
      0)
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) z : 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))
        z :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
have h₁ : ∀ (c : C) (m : M),
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[R] m) : 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))
        (c ⊗ₜ[R] m) :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
Tactic: induction z using TensorProduct.induction_on with
    | zero => simp [fAC, fBC, e]
    | tmul c m =>
      simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
      simp [fAB, baseChangeMkQ]
    | add x y hx hy =>
      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *
      rw [hx, hy]
Cleared hypotheses: z
-- 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
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
Tactic: have hcomp : fAC = e.toLinearMap.comp fBC := by
    apply LinearMap.ext
    intro z
    induction z using TensorProduct.induction_on with
    | zero => simp [fAC, fBC, e]
    | tmul c m =>
      simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
      simp [fAB, baseChangeMkQ]
    | add x y hx hy =>
      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *
      rw [hx, hy]
-- 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
hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have h : x ∈ fAC.ker ↔ x ∈ (map g (map f N)).toSubmodule
Tactic: rw [hfAC_ker_eq, hfBC_ker_eq, hcomp, LinearEquiv.ker_comp]
-- 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
hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
h : x ∈ fAC.ker ↔ x ∈ (map g (map f N)).toSubmodule
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have h₁ : x ∈ fAC.ker ↔ x ∈ fBC.ker
Tactic: rw [hfAC_ker_eq, hfBC_ker_eq, hcomp, LinearEquiv.ker_comp]
-- 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
hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
h : x ∈ fAC.ker ↔ x ∈ (map g (map f N)).toSubmodule
h₁ : x ∈ fAC.ker ↔ x ∈ fBC.ker
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have h₂ : x ∈ ((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC).ker ↔ x ∈ fBC.ker
Tactic: rw [hfAC_ker_eq, hfBC_ker_eq, hcomp, LinearEquiv.ker_comp]
-- 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
hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
h : x ∈ fAC.ker ↔ x ∈ (map g (map f N)).toSubmodule
h₁ : x ∈ fAC.ker ↔ x ∈ fBC.ker
h₂ : x ∈ ((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC).ker ↔ x ∈ fBC.ker
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
have h₃ : x ∈ fBC.ker ↔ x ∈ fBC.ker
Tactic: rw [hfAC_ker_eq, hfBC_ker_eq, hcomp, LinearEquiv.ker_comp]
-- 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_1 : Type w
inst_3 : CommRing A_1
inst_4 : Algebra R A_1
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A_1 →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat.{w, u} R
⊢ ↾map (CommAlgCat.Hom.hom (𝟙 A)) = 𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))
have w : ∀ (N : G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))),
  Eq (α := G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (𝟙 A))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
Tactic: ext N : 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_1 : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g_1 : B →ₐ[R] C
X Y Z : CommAlgCat.{w, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w)) ⟶
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    (↾map (CommAlgCat.Hom.hom (f ≫ g))) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g))
have w : ∀ (N : G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w))),
  Eq (α := G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (f ≫ g))) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
Tactic: ext N : 1
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
x : R
⊢ HSMul.hSMul (β := V⟦Γ⟧) x 0 = 0
have coeff : ∀ (x_1 : Γ), (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = coeff 0 x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
⊢ ¬(r • x).orderTop < x.orderTop
have pos : ∀ (hrx : r • x = 0), ¬(r • x).orderTop < x.orderTop
Tactic: by_cases hrx : r • x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
pos : ∀ (hrx : r • x = 0), ¬(r • x).orderTop < x.orderTop
⊢ ¬(r • x).orderTop < x.orderTop
have neg : ∀ (hrx : ¬r • x = 0), ¬(r • x).orderTop < x.orderTop
Tactic: by_cases hrx : r • x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop
have pos : ¬⊤ < x.orderTop
Tactic: rw [hrx, orderTop_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop
have neg : ¬sorry.min (s := (r • x).support) sorry < sorry.min (s := x.support) sorry
Tactic: simp only [orderTop_of_ne_zero hrx, orderTop_of_ne_zero <| right_ne_zero_of_smul hrx,
      WithTop.coe_lt_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
⊢ ¬(r • x).order < x.order
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := right_ne_zero_of_smul h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬(r • x).order < x.order
have simp_all : ¬sorry.min (s := (r • x).support) sorry < sorry.min (s := x.support) sorry
Tactic: simp_all only [order, dite_false]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
⊢ (truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) (r • x) = HSMul.hSMul (β := V⟦Γ⟧) r ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) x : V⟦Γ⟧)
have coeff : ∀ (x_1 : Γ),
  coeff ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) (r • x)) x_1 =
    (HSMul.hSMul (β := V⟦Γ⟧) r ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) x : V⟦Γ⟧)).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
⊢ (single a : (a : R) → R⟦Γ⟧) (r + s) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
have coeff : coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
  (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
⊢ (single a : (a : R) → R⟦Γ⟧) (r + s) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)
have coeff : coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
  (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
      ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
Tactic: classical
  ext : 1; exact Pi.single_add (f := fun _ => R) a r s
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x + y).map f = HAdd.hAdd (α := S⟦Γ⟧) (x.map f) (y.map f)
have coeff : ∀ (x_1 : Γ), coeff ((x + y).map f) x_1 = (HAdd.hAdd (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a))
have h : (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) = x.support
Tactic: convert! x.isPWO_support