awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (hypothesis)
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : Nonempty X
hf :
  Function.Injective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
g : (fun (X : Type u) ↦ X) Y → (fun (X : Type u) ↦ X) X
hg :
  Function.LeftInverse g
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
⊢ Mono (free.map f)
have this : IsSplitMono f
Tactic: have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X' X : Type u
Y : GrpCat
f : X' ⟶ X
g :
  X ⟶ Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
⊢ Eq (α := free.obj X' ⟶ Y)
    ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g) :
      free.obj X' ⟶ Y)
    (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
          g :
      free.obj X' ⟶ Y)
have hf : Eq (α := (↑(free.obj X') : Type u) →* (↑Y : Type u))
  (Hom.hom
    ((Equiv.symm
          (Equiv.trans
            (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier))
            (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
        (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
      (f ≫ g)))
  (Hom.hom
    (free.map f ≫
      (Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
        g))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X' X : Type u
Y : GrpCat
f : X' ⟶ X
g :
  X ⟶ Functor.obj (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) Y
⊢ Eq (α := (↑(free.obj X') : Type u) →* (↑Y : Type u))
    (Hom.hom
      ((Equiv.symm
            (Equiv.trans
              (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier))
              (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (free.map f ≫
        (Equiv.symm
              (Equiv.trans
                (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  carrier))
                (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
          g))
have hf : ∀ (a : X'),
  Eq (α := (↑Y : Type u))
    (((Hom.hom
              ((Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X' ⟶ (forget GrpCat).obj Y) → free.obj X' ⟶ Y)
                (f ≫ g)) :
            (↑(free.obj X') : Type u) →* (↑Y : Type u)) :
          (a : FreeGroup X') → (↑Y : Type u))
        (FreeGroup.of a) :
      (↑Y : Type u))
    ((Hom.hom
            (free.map f ≫
              (Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget GrpCat).obj Y) → free.obj X ⟶ Y)
                g) :
          (a : FreeGroup X') → (↑Y : Type u))
        (FreeGroup.of a) :
      (↑Y : Type u))
Tactic: apply FreeGroup.ext_hom
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X : GrpCat
⊢ CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X)))) =
    𝟙 (CommGrpCat.of (Abelianization (↑X : Type u)))
have hf : CommGrpCat.Hom.hom
    (CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X))))) =
  CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X : GrpCat
⊢ CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑X : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑X : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X))))) =
    CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u))))
have hf : MonoidHom.comp Abelianization.of (Hom.hom (𝟙 X)) =
  (Equiv.symm Abelianization.lift :
      (a : Abelianization (↑X : Type u) →* Abelianization (↑X : Type u)) →
        (↑X : Type u) →* Abelianization (↑X : Type u))
    (CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization (↑X : Type u)))))
Tactic: apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α := CommGrpCat.of (Abelianization (↑X : Type u)) ⟶ CommGrpCat.of (Abelianization (↑Z : Type u)))
    (CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g)))))
    (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom f))))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom g)))))
have hf : Eq.{u + 1} (α :=
  (↑(CommGrpCat.of (Abelianization (↑X : Type u))) : Type u) →*
    (↑(CommGrpCat.of (Abelianization (↑Z : Type u))) : Type u))
  (CommGrpCat.Hom.hom
    (CommGrpCat.ofHom
      ((Abelianization.lift :
          (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
            Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
        (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g))))))
  (CommGrpCat.Hom.hom
    (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom f))))
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom g))))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{u + 1} (α :=
    (↑(CommGrpCat.of (Abelianization (↑X : Type u))) : Type u) →*
      (↑(CommGrpCat.of (Abelianization (↑Z : Type u))) : Type u))
    (CommGrpCat.Hom.hom
      (CommGrpCat.ofHom
        ((Abelianization.lift :
            (a : (↑X : Type u) →* Abelianization (↑Z : Type u)) →
              Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u))
          (MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g))))))
    (CommGrpCat.Hom.hom
      (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom f))))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom g))))))
have hf : MonoidHom.comp Abelianization.of (Hom.hom (f ≫ g)) =
  (Equiv.symm Abelianization.lift :
      (a : Abelianization (↑X : Type u) →* Abelianization (↑Z : Type u)) →
        (↑X : Type u) →* Abelianization (↑Z : Type u))
    (CommGrpCat.Hom.hom
      (CategoryStruct.comp (Y := CommGrpCat.of (Abelianization (↑Y : Type u)))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑X : Type u) →* Abelianization (↑Y : Type u)) →
                Abelianization (↑X : Type u) →* Abelianization (↑Y : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom f))))
        (CommGrpCat.ofHom
          ((Abelianization.lift :
              (a : (↑Y : Type u) →* Abelianization (↑Z : Type u)) →
                Abelianization (↑Y : Type u) →* Abelianization (↑Z : Type u))
            (MonoidHom.comp Abelianization.of (Hom.hom g))))))
Tactic: apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Count (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ countP' p (l₁ * l₂) = countP' p l₁ + countP' p l₂
have dsimp : List.countP (fun (b : α) ↦ decide (p b))
    (HAppend.hAppend (α := List α) (β := List α) ((toList : (a : FreeMonoid α) → List α) l₁ : List α)
      ((toList : (a : FreeMonoid α) → List α) l₂ : List α)) =
  List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₁) +
    List.countP (fun (b : α) ↦ decide (p b)) ((toList : (a : FreeMonoid α) → List α) l₂)
Tactic: dsimp [countP']
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Count (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
⊢ Eq (α := Multiplicative ℕ) ((countP p : (a : FreeMonoid α) → Multiplicative ℕ) (of x) : Multiplicative ℕ)
    (if p x then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
      else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
      Multiplicative ℕ)
have rw : Eq (α := Multiplicative ℕ)
  (if decide (p x) = true then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
    else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
    Multiplicative ℕ)
  (if p x then (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 1
    else (Multiplicative.ofAdd : (a : ℕ) → Multiplicative ℕ) 0 :
    Multiplicative ℕ)
Tactic: rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Count (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
x : α
⊢ Eq (α := ℕ) ((countP p : (a : FreeAddMonoid α) → ℕ) (of x) : ℕ) (if p x then 1 else 0 : ℕ)
have rw : Eq (α := ℕ) (if decide (p x) = true then 1 else 0) (if p x then 1 else 0)
Tactic: rw [countP_apply, toList_of, List.countP_singleton]
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Count (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ Eq (α := ℕ) ((countP fun (x_1 : α) ↦ x_1 = x : (a : FreeAddMonoid α) → ℕ) (of y) : ℕ)
    (Pi.single (M := fun (a : α) ↦ ℕ) x 1 y : ℕ)
have rw : Eq (α := ℕ) (if y = x then 1 else 0 : ℕ) (Pi.single (M := fun (a : α) ↦ ℕ) x 1 y : ℕ)
Tactic: rw [countP_of]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x : M₀
⊢ Commute 0 x
have rw : 0 * x = x * 0
Tactic: rw [commute_iff_eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x : M₀
rw : 0 * x = x * 0
⊢ Commute 0 x
have rw₁ : 0 = x * 0
Tactic: rw [commute_iff_eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x : M₀
rw : 0 * x = x * 0
rw₁ : 0 = x * 0
⊢ Commute 0 x
have rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [commute_iff_eq, zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
⊢ 0 * (x * x_1) = 0 * x * x_1
have rw : 0 = 0 * x * x_1
Tactic: rw [zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = 0 * x * x_1
⊢ 0 * (x * x_1) = 0 * x * x_1
have rw₁ : 0 = 0 * x_1
Tactic: rw [zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = 0 * x * x_1
rw₁ : 0 = 0 * x_1
⊢ 0 * (x * x_1) = 0 * x * x_1
have rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [zero_mul, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
⊢ x * x_1 * 0 = x * (x_1 * 0)
have rw : 0 = x * (x_1 * 0)
Tactic: rw [mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = x * (x_1 * 0)
⊢ x * x_1 * 0 = x * (x_1 * 0)
have rw₁ : 0 = x * 0
Tactic: rw [mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
M₀ : Type u_1
inst : MulZeroClass M₀
x x_1 : M₀
rw : 0 = x * (x_1 * 0)
rw₁ : 0 = x * 0
⊢ x * x_1 * 0 = x * (x_1 * 0)
have rw₂ : Eq.{u_1 + 1} (α := M₀) 0 0
Tactic: rw [mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
⊢ Subset (α := Set G₀ˣ) (center G₀ˣ) (Units.val ⁻¹' center G₀)
have simp_rw : ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * (↑x : G₀) = (↑x : G₀) * g
Tactic: simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * (↑u : G₀) = (↑u : G₀) * a
have inl : 0 * (↑u : G₀) = (↑u : G₀) * 0
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
inl : 0 * (↑u : G₀) = (↑u : G₀) * 0
⊢ a * (↑u : G₀) = (↑u : G₀) * a
have inr : ∀ (ha : a ≠ 0), a * (↑u : G₀) = (↑u : G₀) * a
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * (↑u : G₀) = (↑u : G₀) * 0
have inl : 0 = (↑u : G₀) * 0
Tactic: rw [zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
inl : 0 = (↑u : G₀) * 0
⊢ 0 * (↑u : G₀) = (↑u : G₀) * 0
have inl₁ : Eq.{u_2 + 1} (α := G₀) 0 0
Tactic: rw [zero_mul, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
⊢ a⁻¹ ∈ s.centralizer
have inl : ∀ (ha : 0 ∈ s.centralizer), 0⁻¹ ∈ s.centralizer
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
inl : ∀ (ha : 0 ∈ s.centralizer), 0⁻¹ ∈ s.centralizer
⊢ a⁻¹ ∈ s.centralizer
have inr : ∀ (ha₀ : a ≠ 0), a⁻¹ ∈ s.centralizer
Tactic: obtain rfl | ha₀ := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ c * a⁻¹ = a⁻¹ * c
have inr : c = a⁻¹ * c * a
Tactic: rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
inr : c = a⁻¹ * c * a
⊢ c * a⁻¹ = a⁻¹ * c
have inr₁ : c = a⁻¹ * (c * a)
Tactic: rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
inr : c = a⁻¹ * c * a
inr₁ : c = a⁻¹ * (c * a)
⊢ c * a⁻¹ = a⁻¹ * c
have inr₂ : a * c = c * a
Tactic: rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Center (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
inr : c = a⁻¹ * c * a
inr₁ : c = a⁻¹ * (c * a)
inr₂ : a * c = c * a
⊢ c * a⁻¹ = a⁻¹ * c
have inr₃ : a * c = a * c
Tactic: rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Equiv (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : MulZeroClass α
inst_2 : MulZeroClass β
inst_3 : MulEquivClass F α β
f : F
⊢ (f : (a : α) → β) 0 =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (EquivLike.inv f 0) : β)
have rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (0 * EquivLike.inv f 0) : β)
Tactic: rw [← map_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Equiv (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : EquivLike F α β
inst_1 : MulZeroClass α
inst_2 : MulZeroClass β
inst_3 : MulEquivClass F α β
f : F
rw : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (0 * EquivLike.inv f 0) : β)
⊢ (f : (a : α) → β) 0 =
    HMul.hMul (α := β) (β := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) (EquivLike.inv f 0) : β)
have rw₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) ((f : (a : α) → β) 0 : β)
Tactic: rw [← map_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
⊢ (∀ (X Y : C),
      HasSmallLocalizedShiftedHom (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ (Functor.obj (CochainComplex.singleFunctor C 0) X)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
have simp : (∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) ↔
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
Tactic: simp only [hasSmallLocalizedShiftedHom_iff _ _ Q]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
            (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) ↔
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
            (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
have mp : (∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))) →
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
Tactic: constructor