awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₂ : Eq (α := tsze R' N) ((Algebra.ofId R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)
have rw₃ : Eq (α := tsze R' N) ((algebraMap R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₂ : Eq (α := tsze R' N) ((Algebra.ofId R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
rw₃ : Eq (α := tsze R' N) ((algebraMap R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)
have rw₄ : Eq (α := tsze R' N) (inl r) (inl r)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
have rw : Eq (α := tsze R' N)
  ((((liftEquivOfComm :
              (a :
                  { f : M →ₗ[R'] tsze R' N //
                    ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                tsze R' M →ₐ[R'] tsze R' N)
            (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
              ∀ (x y : M),
                HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                    ((f : (a : M) → tsze R' N) y : tsze R' N) =
                  0)
              (inrHom R' N ∘ₗ f) sorry) :
          tsze R' M →ₐ[R'] tsze R' N) :
        (a : tsze R' M) → tsze R' N)
      (inr x) :
    tsze R' N)
  (inr ((f : (a : M) → N) x) : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
have rw₁ : Eq (α := tsze R' N)
  ((lift (Algebra.ofId R' (tsze R' N))
          (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) sorry) :
            M →ₗ[R'] tsze R' N)
          sorry sorry sorry :
        (a : tsze R' M) → tsze R' N)
      (inr x) :
    tsze R' N)
  (inr ((f : (a : M) → N) x) : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
have rw₂ : Eq (α := tsze R' N)
  (((↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
              ∀ (x y : M),
                HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                    ((f : (a : M) → tsze R' N) y : tsze R' N) =
                  0)
              (inrHom R' N ∘ₗ f) sorry) :
          M →ₗ[R'] tsze R' N) :
        (a : M) → tsze R' N)
      x :
    tsze R' N)
  (inr ((f : (a : M) → N) x) : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₂ :
  Eq (α := tsze R' N)
    (((↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            M →ₗ[R'] tsze R' N) :
          (a : M) → tsze R' N)
        x :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
have rw₃ : Eq (α := tsze R' N) ((inrHom R' N : (a : N) → tsze R' N) ((f : (a : M) → N) x) : tsze R' N)
  (inr ((f : (a : M) → N) x) : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₂ :
  Eq (α := tsze R' N)
    (((↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            M →ₗ[R'] tsze R' N) :
          (a : M) → tsze R' N)
        x :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₃ :
  Eq (α := tsze R' N) ((inrHom R' N : (a : N) → tsze R' N) ((f : (a : M) → N) x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
have rw₄ : Eq (α := tsze R' N) (inr ((f : (a : M) → N) x) : tsze R' N) (inr ((f : (a : M) → N) x) : tsze R' N)
Tactic: rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
⊢ Eq (α := tsze R' M →ₐ[R'] tsze R' M) (map LinearMap.id) (AlgHom.id R' (tsze R' M))
have h : ∀ (m : M),
  Eq (α := tsze R' M) ((map LinearMap.id : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)
    ((AlgHom.id R' (tsze R' M) : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)
Tactic: apply algHom_ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
inst_9 : AddCommMonoid P
inst_10 : Module R' P
inst_11 : Module.{u, u_4} R'ᵐᵒᵖ P
inst_12 : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ Eq (α := tsze R' M →ₐ[R'] tsze R' P) (map (g ∘ₗ f)) (AlgHom.comp (map g) (map f))
have h : ∀ (m : M),
  Eq (α := tsze R' P) ((map (g ∘ₗ f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)
    ((AlgHom.comp (map g) (map f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)
Tactic: apply algHom_ext
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) x ↔ x = inr x.snd
have obtain : ∀ (r : R) (m : M),
  Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) (r, m) ↔
    (r, m) = inr (snd (r, m))
Tactic: obtain ⟨r, m⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) (r, m) ↔
    (r, m) = inr (snd (r, m))
have simp : r = 0 ↔ (r, m) = inr (snd (r, m))
Tactic: simp only [kerIdeal, RingHom.mem_ker, fstHom_apply, fst_mk]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ (r, m) = inr (snd (r, m))
have rw : Eq (α := TrivSqZeroExt R M) (0, m) (inr (snd.{u_1, u_2} (R := R) (0, m)))
Tactic: rw [hr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
⊢ r = 0
have rw : fst (r, m) = 0
Tactic: rw [← fst_mk r m, hrm, fst_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
rw : fst (r, m) = 0
⊢ r = 0
have rw₁ : Eq.{u_1 + 1} (α := R) (fst (inr (snd (r, m)))) 0
Tactic: rw [← fst_mk r m, hrm, fst_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
rw : fst (r, m) = 0
rw₁ : Eq.{u_1 + 1} (α := R) (fst (inr (snd (r, m)))) 0
⊢ r = 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← fst_mk r m, hrm, fst_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
⊢ HPow.hPow (α := Ideal (TrivSqZeroExt R M)) (β := ℕ) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) 2 = ⊥
have simp : ∀ (r : TrivSqZeroExt R M),
  r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (r * s)
Tactic: simp only [pow_two, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (x * y)
have rw : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (inr x.snd * y)
Tactic: rw [hx, hy, mem_bot, inr_mul_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
rw : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (inr x.snd * y)
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (x * y)
have rw₁ : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd))
Tactic: rw [hx, hy, mem_bot, inr_mul_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
rw : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (inr x.snd * y)
rw₁ : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd))
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (x * y)
have rw₂ : HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd) = 0
Tactic: rw [hx, hy, mem_bot, inr_mul_inr]
-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Ideal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
rw : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (inr x.snd * y)
rw₁ : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd))
rw₂ : HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd) = 0
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (x * y)
have rw₃ : Eq (α := TrivSqZeroExt R M) 0 0
Tactic: rw [hx, hy, mem_bot, inr_mul_inr]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
⊢ untrop (a + b) = untrop (if a ≤ b then a else b)
have simp : (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
Tactic: simp only [untrop_add, min_def, untrop_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
have pos : a ≤ b → untrop a = untrop a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
pos : a ≤ b → untrop a = untrop a
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
have neg : ¬a ≤ b → untrop b = untrop b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
⊢ untrop (trop (max (untrop a) (untrop b))) = untrop (if a ≤ b then b else a)
have simp : (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
Tactic: simp only [max_def, untrop_le_iff, untrop_trop]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
have pos : a ≤ b → untrop b = untrop b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
pos : a ≤ b → untrop b = untrop b
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
have neg : ¬a ≤ b → untrop a = untrop a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y
have rw : trop (min (untrop x) (untrop y)) = x ↔ x ≤ y
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.Tropical.Basic (goal)
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
rw : trop (min (untrop x) (untrop y)) = x ↔ x ≤ y
⊢ x + y = x ↔ x ≤ y
have rw₁ : min (untrop x) (untrop y) = untrop x ↔ x ≤ y
Tactic: rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]