awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
S : Type u_4
inst_5 : CommSemiring S
inst_6 : Module S A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower S A A
inst_9 : CompatibleSMul A A R S
a : A
⊢ Eq.{u_2 + 1} (α := A →ₗ[R] A)
    ((↑R :
        {S : Type u_4} →
          {M M₂ : Type u_2} →
            [inst : Semiring R] →
              [inst_10 : Semiring S] →
                [inst_11 : AddCommMonoid M] →
                  [inst_12 : AddCommMonoid M₂] →
                    [inst_13 : Module R M] →
                      [inst_14 : Module R M₂] →
                        [inst_15 : Module S M] →
                          [inst_16 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) ((mul S A : (a : A) → A →ₗ[S] A) a))
    ((mul R A : (a : A) → A →ₗ[R] A) a)
have h : ∀ (x : A),
  Eq (α := A)
    (((↑R :
              {S : Type u_4} →
                {M M₂ : Type u_2} →
                  [inst : Semiring R] →
                    [inst_10 : Semiring S] →
                      [inst_11 : AddCommMonoid M] →
                        [inst_12 : AddCommMonoid M₂] →
                          [inst_13 : Module R M] →
                            [inst_14 : Module R M₂] →
                              [inst_15 : Module S M] →
                                [inst_16 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) ((mul S A : (a : A) → A →ₗ[S] A) a) :
          (a : A) → A)
        x :
      A)
    ((((mul R A : (a : A) → A →ₗ[R] A) a : A →ₗ[R] A) : (a : A) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ Eq (α := R ⊗[R] M →ₗ[R] M) (lift (lsmul R M ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) r))
    ((lsmul R M : (a : R) → M →ₗ[R] M) r ∘ₗ lift (lsmul R M))
have H : ∀ (x : R) (y : M),
  Eq.{u_4 + 1} (α := M) ((lift (lsmul R M ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) r) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] y) : M)
    (((lsmul R M : (a : R) → M →ₗ[R] M) r ∘ₗ lift (lsmul R M) : (a : R ⊗[R] M) → M) (x ⊗ₜ[R] y) : M)
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
a b : A
⊢ Commute (S := A →ₗ[R] A) (mulLeft R a) (mulRight R b)
have h : ∀ (c : A),
  Eq (α := A) ((HMul.hMul (α := A →ₗ[R] A) (mulLeft R a) (mulRight R b) : (a : A) → A) c : A)
    ((HMul.hMul (α := A →ₗ[R] A) (mulRight R b) (mulLeft R a) : (a : A) → A) c : A)
Tactic: ext c
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n : ℕ
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulLeft R a) 0 = mulLeft R (HPow.hPow (β := ℕ) a 0)
have rw : Eq (α := A →ₗ[R] A) 1 (mulLeft R (HPow.hPow (β := ℕ) a 0))
Tactic: rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulLeft R (HPow.hPow (β := ℕ) a 0))
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulLeft R a) 0 = mulLeft R (HPow.hPow (β := ℕ) a 0)
have rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulLeft R 1)
Tactic: rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulLeft R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulLeft R 1)
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulLeft R a) 0 = mulLeft R (HPow.hPow (β := ℕ) a 0)
have rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
Tactic: rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulLeft R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulLeft R 1)
rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulLeft R a) 0 = mulLeft R (HPow.hPow (β := ℕ) a 0)
have rw₃ : Eq.{u_2 + 1} (α := A →ₗ[R] A) id id
Tactic: rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))
have rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
Tactic: rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))
have rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n * a)
Tactic: rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n * a)
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))
have rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
Tactic: rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n * a)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))
have rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
Tactic: rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n * a)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n * mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) n ∘ₗ mulLeft R a = mulLeft R (a ^ n) ∘ₗ mulLeft R a
⊢ HPow.hPow (α := A →ₗ[R] A) (mulLeft R a) (n + 1) = mulLeft R (a ^ (n + 1))
have rw₄ : Eq (α := A →ₗ[R] A) (mulLeft R (a ^ n) ∘ₗ mulLeft R a) (mulLeft R (a ^ n) ∘ₗ mulLeft R a)
Tactic: rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n : ℕ
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulRight R a) 0 = mulRight R (HPow.hPow (β := ℕ) a 0)
have rw : Eq (α := A →ₗ[R] A) 1 (mulRight R (HPow.hPow (β := ℕ) a 0))
Tactic: rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulRight R (HPow.hPow (β := ℕ) a 0))
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulRight R a) 0 = mulRight R (HPow.hPow (β := ℕ) a 0)
have rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulRight R 1)
Tactic: rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulRight R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulRight R 1)
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulRight R a) 0 = mulRight R (HPow.hPow (β := ℕ) a 0)
have rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
Tactic: rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n : ℕ
rw : Eq (α := A →ₗ[R] A) 1 (mulRight R (HPow.hPow (β := ℕ) a 0))
rw₁ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 (mulRight R 1)
rw₂ : Eq.{u_2 + 1} (α := A →ₗ[R] A) 1 id
⊢ HPow.hPow (α := A →ₗ[R] A) (β := ℕ) (mulRight R a) 0 = mulRight R (HPow.hPow (β := ℕ) a 0)
have rw₃ : Eq.{u_2 + 1} (α := A →ₗ[R] A) id id
Tactic: rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))
have rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
Tactic: rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))
have rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a * a ^ n)
Tactic: rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a * a ^ n)
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))
have rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
Tactic: rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a * a ^ n)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))
have rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
Tactic: rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
n_1 n : ℕ
rw : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ (n + 1))
rw₁ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a * a ^ n)
rw₂ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n * mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
rw₃ : HPow.hPow (α := A →ₗ[R] A) (mulRight R a) n ∘ₗ mulRight R a = mulRight R (a ^ n) ∘ₗ mulRight R a
⊢ HPow.hPow (α := A →ₗ[R] A) (mulRight R a) (n + 1) = mulRight R (a ^ (n + 1))
have rw₄ : Eq (α := A →ₗ[R] A) (mulRight R (a ^ n) ∘ₗ mulRight R a) (mulRight R (a ^ n) ∘ₗ mulRight R a)
Tactic: rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
⊢ IsUnit (M := End R A) ((Algebra.lmul R A : (a : A) → End R A) x : End R A) ↔ IsUnit x
have rw : IsUnit x ↔ Function.Bijective (α := A) (β := A) (⇑((Algebra.lmul R A : (a : A) → End R A) x : End R A) : (a : A) → A)
Tactic: rw [Module.End.isUnit_iff, Iff.comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := R →ₗ[R] A) (toSpanSingleton R A 1) (Algebra.linearMap R A)
have h : Eq.{u_2 + 1} (α := A) ((toSpanSingleton R A 1 : (a : R) → A) 1 : A) ((Algebra.linearMap R A : (a : R) → A) 1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Bilinear (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalCommSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
⊢ Eq (α := A →ₗ[R] A →ₗ[R] A) (flip (mul R A)) (mul R A)
have h : ∀ (x x_1 : A),
  Eq (α := A) ((((flip (mul R A) : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)
    ((((mul R A : (a : A) → A →ₗ[R] A) x : A →ₗ[R] A) : (a : A) → A) x_1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X : Type u
Y : AddCommGrpCat
⊢ (free.obj X ⟶ Y) ≃
    (X ⟶
      Functor.obj
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          carrier))
        Y)
have refine : ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier) (free.obj X) Y ≃
  (X →
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y)
Tactic: refine ConcreteCategory.homEquiv.trans (Equiv.trans ?_ TypeCat.homEquiv.symm)
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{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 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                (CC := carrier))
              (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
          (a : X' ⟶ (forget AddCommGrpCat).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 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                  (CC := carrier))
                (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
            (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
          g :
      free.obj X' ⟶ Y)
have hf : ∀ (x : (↑(free.obj X') : Type u)),
  Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (Equiv.trans
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                    (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                (a : X' ⟶ (forget AddCommGrpCat).obj Y) → free.obj X' ⟶ Y)
              (f ≫ g)) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((Hom.hom
            (free.map f ≫
              (Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
                g) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
x : (↑(free.obj X') : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((Hom.hom
            ((Equiv.symm
                  (Equiv.trans
                    (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                    (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                (a : X' ⟶ (forget AddCommGrpCat).obj Y) → free.obj X' ⟶ Y)
              (f ≫ g)) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((Hom.hom
            (free.map f ≫
              (Equiv.symm
                    (Equiv.trans
                      (ConcreteCategory.homEquiv (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
                      (Equiv.trans (Equiv.symm FreeAbelianGroup.lift) (Equiv.symm TypeCat.homEquiv))) :
                  (a : X ⟶ (forget AddCommGrpCat).obj Y) → free.obj X ⟶ Y)
                g) :
          (a : (↑(free.obj X') : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
have hf : Eq (α := (↑Y : Type u))
  ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
          ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            (of (FreeAbelianGroup X')) Y) :
        (a : FreeAbelianGroup X') → (↑Y : Type u))
      x :
    (↑Y : Type u))
  ((((FreeAbelianGroup.lift : (a : X → ToType Y) → ToHom (of (FreeAbelianGroup X)) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y) :
          ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            (of (FreeAbelianGroup X)) Y) :
        (a : FreeAbelianGroup X) → (↑Y : Type u))
      ((FreeAbelianGroup.map (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X) :
            (a : FreeAbelianGroup X') → FreeAbelianGroup X)
          x :
        FreeAbelianGroup X) :
    (↑Y : Type u))
Tactic: dsimp [ConcreteCategory.homEquiv]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X' X : Type u
Y : AddCommGrpCat
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))
      Y
x : (↑(free.obj X') : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X')) Y) :
          (a : FreeAbelianGroup X') → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((((FreeAbelianGroup.lift : (a : X → ToType Y) → ToHom (of (FreeAbelianGroup X)) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y) :
            ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              (of (FreeAbelianGroup X)) Y) :
          (a : FreeAbelianGroup X) → (↑Y : Type u))
        ((FreeAbelianGroup.map (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X) :
              (a : FreeAbelianGroup X') → FreeAbelianGroup X)
            x :
          FreeAbelianGroup X) :
      (↑Y : Type u))
have hf : Eq (α := (↑Y : Type u))
  ((((FreeAbelianGroup.lift : (a : X' → ToType Y) → ToHom (of (FreeAbelianGroup X')) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X') → ToType Y) :
          ToHom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
            (of (FreeAbelianGroup X')) Y) :
        (a : FreeAbelianGroup X') → (↑Y : Type u))
      x :
    (↑Y : Type u))
  ((((FreeAbelianGroup.lift : (a : X' → (↑Y : Type u)) → FreeAbelianGroup X' →+ (↑Y : Type u))
            (Function.comp (β := X) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : X) → ToType Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X') → X)) :
          FreeAbelianGroup X' →+ (↑Y : Type u)) :
        (a : FreeAbelianGroup X') → (↑Y : Type u))
      x :
    (↑Y : Type u))
Tactic: rw [← FreeAbelianGroup.lift_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
⊢ Mono (free.map f)
have pos : ∀ (hX : IsEmpty X), Mono (free.map f)
Tactic: by_cases! hX : IsEmpty X
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
pos : ∀ (hX : IsEmpty X), Mono (free.map f)
⊢ Mono (free.map f)
have neg : ∀ (hX : Nonempty X), Mono (free.map f)
Tactic: by_cases! hX : IsEmpty X
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
Goal:
X Y : Type u
f : X ⟶ Y
h : Mono f
hX : IsEmpty X
⊢ Mono (free.map f)
have pos : ∀ {Z : AddCommGrpCat.{u}} (g h : Z ⟶ free.obj X), g ≫ free.map f = h ≫ free.map f → g = h
Tactic: constructor
-- 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
⊢ Mono (free.map f)
have 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)
Tactic: have hf : Function.Injective f := by rwa [← mono_iff_injective]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Adjunctions (goal)
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)
⊢ Mono (free.map f)
have neg : ∀ (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)
Tactic: obtain ⟨g, hg⟩ := hf.hasLeftInverse