awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
fst : ℕ
bS : Basis ι R S
bI : Basis.{0, u_2, u_4} (Fin fst) R ↥(restrictScalars R I)
f : Fin fst ↪ ι
a : Fin fst → R
snf :
  ∀ (i : Fin fst),
    (↑((bI : (a : Fin fst) → ↥(restrictScalars R I)) i) : S) =
      HSMul.hSMul (β := S) (a i) ((bS : (a : ι) → S) ((f : (a : Fin fst) → ι) i : ι) : S)
val : Fintype ι
⊢ finrank.{u_2, u_4} R ↥(restrictScalars R I) = finrank R S
have intro : Fintype.card (Fin fst) = Fintype.card ι
Tactic: rw [Module.finrank_eq_card_basis bS, Module.finrank_eq_card_basis bI]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False
have apply : Eq.{u_4 + 1} (α := ↥I) ((selfBasis b I hI : (a : ι) → ↥I) i : ↥I) (0 : ↥I)
Tactic: apply Basis.ne_zero (Ideal.selfBasis b I hI) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Type u_4
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ Eq.{u_4 + 1} (α := ↥I) ((selfBasis b I hI : (a : ι) → ↥I) i : ↥I) (0 : ↥I)
have refine : Eq.{u_4 + 1} (α := S) ((fun (a : ↥I) ↦ (↑a : S)) ((selfBasis b I hI : (a : ι) → ↥I) i)) ((fun (a : ↥I) ↦ (↑a : S)) 0)
Tactic: refine Subtype.coe_injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
inst_1 : DecidableEq ι
M : ι → Type u_3
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_3} R (M i)
motive : (⨁ (i : ι), M i) → Prop
x : ⨁ (i : ι), M i
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
zero₁ : motive 0
⊢ motive x
have of : ∀ (i : ι) (x : M i), motive ((of M i : (a : M i) → ⨁ (i : ι), M i) x)
Tactic: induction x using DirectSum.induction_on with
  | zero => exact zero
  | of => exact lof _ _
  | add x y hx hy => exact add x y hx hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : A
h_rel : rel x y
⊢ Eq (α := RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B) :
          (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        x :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
    ((AlgHom.comp (mkAlgHom R (rel on (⇑f.symm : (a : B) → A))) (↑f : A →ₐ[R] B) :
          (a : A) → RingQuot (rel on (⇑f.symm : (a : B) → A)))
        y :
      RingQuot (R := B) (rel on (⇑f.symm : (a : B) → A)))
have w : Function.onFun (α := B) rel ((⇑f.symm : (a : B) → A) : (a : B) → A)
  (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) x : B) (((↑(↑f : A →ₐ[R] B) : A →+* B) : (a : A) → B) y : B)
Tactic: apply RingQuot.mkAlgHom_rel
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
A B : Type v
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A ≃ₐ[R] B
rel : A → A → Prop
x y : B
h : (rel on (⇑f.symm : (a : B) → A)) x y
⊢ Eq (α := RingQuot rel)
    ((AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A) : (a : B) → RingQuot rel) x : RingQuot rel)
    ((AlgHom.comp (mkAlgHom R rel) (↑f.symm : B →ₐ[R] A) : (a : B) → RingQuot rel) y : RingQuot rel)
have w : rel (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) x) (((↑(↑f.symm : B →ₐ[R] A) : B →+* A) : (a : B) → A) y)
Tactic: apply RingQuot.mkAlgHom_rel
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
i : I
⊢ Eq (α := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
      FreeProduct R A)
    (1 : FreeProduct R A)
have suffices : Eq (α := FreeProduct R A)
  ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
      (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1) :
    FreeProduct R A)
  ((mkAlgHom R A : (a : FreeTensorAlgebra R A) → FreeProduct R A) 1 : FreeProduct R A)
Tactic: suffices ι' R A (DirectSum.lof R I A i 1) = mkAlgHom R A 1 by simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
a₁ a₂ : A i
⊢ HMul.hMul (α := FreeProduct R A) (β := FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁) :
        FreeProduct R A)
      ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
          (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
        FreeProduct R A) =
    (ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
      (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) (a₁ * a₂))
have h : HMul.hMul (α := FreeProduct R A) (β := FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁) :
      FreeProduct R A)
    ((ι' R A : (a : ⨁ (i : I), A i) → FreeProduct R A)
        (((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂) :
      FreeProduct R A) =
  (RingQuot.mkAlgHom R (rel R A) : (a : TensorAlgebra R (⨁ (i : I), A i)) → RingQuot (rel R A))
    ((tprod R (⨁ (i : I), A i) 2 : (a : (i : Fin 2) → ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
      fun (x : Fin 2) ↦
      match (motive := Fin 2 → ⨁ (i : I), A i) x with
      | 0 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₁
      | 1 => ((lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) a₂)
Tactic: convert! RingQuot.mkAlgHom_rel R <| rel.prod
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps_1 maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
x y : FreeTensorAlgebra R A
r : rel R A x y
⊢ Eq.{w' + 1} (α := B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        x :
      B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        y :
      B)
have id : ∀ {i : I},
  Eq.{w' + 1} (α := B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        ((TensorAlgebra.ι R : (a : ⨁ (i : I), A i) → TensorAlgebra R (⨁ (i : I), A i))
          (((DirectSum.lof R I A i : A i →ₗ[R] ⨁ (i : I), A i) : (a : A i) → ⨁ (i : I), A i) 1)) :
      B)
    ((((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps) :
            TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B) :
          (a : FreeTensorAlgebra R A) → B)
        1 :
      B)
Tactic: cases r with
          | id => simp
          | prod => simp
Cleared hypotheses: x, y, r
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps π : {i : I} → AlgHom.{v, w, w'} R (A i) B
⊢ (fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i)
      ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
          ((liftAlgHom R (s := rel R A) :
                (a :
                    { f : FreeTensorAlgebra R A →ₐ[R] B //
                      ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                        rel R A x y →
                          (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                  RingQuot (rel R A) →ₐ[R] B)
              (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                  rel R A x y →
                    Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                      ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                ((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                  (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                ⋯) :
            RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
        @π) =
    @π
have h : ∀ (i : I) (aᵢ : A i),
  Eq.{w' + 1} (α := B)
    (((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i)
            ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
                ((liftAlgHom R (s := rel R A) :
                      (a :
                          { f : FreeTensorAlgebra R A →ₐ[R] B //
                            ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                              rel R A x y →
                                (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                        RingQuot (rel R A) →ₐ[R] B)
                    (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                      ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                        rel R A x y →
                          Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                            ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                      ((TensorAlgebra.lift R :
                          (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                        (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                      sorry) :
                  RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
              @π)
            i :
          (a : A i) → B)
        aᵢ :
      B)
    ((π : (a : A i) → B) aᵢ : B)
Tactic: ext i aᵢ
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
⊢ AlgHom.comp (B := FreeProduct R A)
      ((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps) (ι R A i) =
    maps
have H : ∀ (a : A i),
  Eq.{w' + 1} (α := B)
    ((AlgHom.comp (B := FreeProduct R A)
            ((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps) (ι R A i) :
          (a : A i) → B)
        a :
      B)
    ((maps : (a : A i) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
r : R
⊢ Eq.{w' + 1} (α := B)
    (((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps : (a : FreeProduct R A) → B)
        ((algebraMap R (FreeProduct R A) : (a : R) → FreeProduct R A) r : FreeProduct R A) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)
have rw : Eq.{w' + 1} (α := B)
  ((((liftAlgHom R (s := rel R A) :
              (a :
                  { f : FreeTensorAlgebra R A →ₐ[R] B //
                    ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                      rel R A x y →
                        (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                RingQuot (rel R A) →ₐ[R] B)
            (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
              ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                rel R A x y →
                  Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                    ((f : (a : FreeTensorAlgebra R A) → B) y : B))
              ((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
              sorry) :
          RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B) :
        (a : FreeProduct R A) → B)
      ((algebraMap R (FreeProduct R A) : (a : R) → FreeProduct R A) r : FreeProduct R A) :
    B)
  ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [lift_apply, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
r : R
rw :
  Eq.{w' + 1} (α := B)
    ((((liftAlgHom R (s := rel R A) :
                (a :
                    { f : FreeTensorAlgebra R A →ₐ[R] B //
                      ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                        rel R A x y →
                          (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                  RingQuot (rel R A) →ₐ[R] B)
              (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                  rel R A x y →
                    Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                      ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                ((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                  (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                ⋯) :
            RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B) :
          (a : FreeProduct R A) → B)
        ((algebraMap R (FreeProduct R A) : (a : R) → FreeProduct R A) r : FreeProduct R A) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)
⊢ Eq.{w' + 1} (α := B)
    (((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps : (a : FreeProduct R A) → B)
        ((algebraMap R (FreeProduct R A) : (a : R) → FreeProduct R A) r : FreeProduct R A) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)
have rw₁ : Eq.{w' + 1} (α := B) ((algebraMap R B : (a : R) → B) r : B) ((algebraMap R B : (a : R) → B) r : B)
Tactic: rw [lift_apply, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
⊢ f = (lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps
have w : ∀ (i : I) (a : A i),
  Eq.{w' + 1} (α := B)
    ((((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i : (a : A i) → B)
        a :
      B)
    (((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := FreeTensorAlgebra R A) (rel R A))
                  ((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps)
                  (RingQuot.mkAlgHom R (rel R A))) ∘ₗ
              TensorAlgebra.ι R) ∘ₗ
            DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
Tactic: ext i a
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
f : FreeProduct R A →ₐ[R] B
h : ∀ (i : I), f ∘ₐ ι R A i = maps
i : I
a : A i
⊢ Eq.{w' + 1} (α := B)
    ((((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i : (a : A i) → B)
        a :
      B)
    (((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := FreeTensorAlgebra R A) (rel R A))
                  ((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps)
                  (RingQuot.mkAlgHom R (rel R A))) ∘ₗ
              TensorAlgebra.ι R) ∘ₗ
            DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
have h₁ : ∀ (i : I) (x : A i), Eq.{w' + 1} (α := B) ((f ∘ₐ ι R A i : (a : A i) → B) x : B) ((maps : (a : A i) → B) x : B)
Tactic: simp_rw [AlgHom.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (hypothesis)
Goal:
I : Type u
inst : DecidableEq I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps : {i : I} → AlgHom.{v, w, w'} R (A i) B
f : FreeProduct R A →ₐ[R] B
i : I
a : A i
h : ∀ (i : I) (x : A i), Eq.{w' + 1} (α := B) ((f ∘ₐ ι R A i : (a : A i) → B) x : B) ((maps : (a : A i) → B) x : B)
⊢ Eq.{w' + 1} (α := B)
    ((((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i : (a : A i) → B)
        a :
      B)
    (((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := FreeTensorAlgebra R A) (rel R A))
                  ((lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps)
                  (RingQuot.mkAlgHom R (rel R A))) ∘ₗ
              TensorAlgebra.ι R) ∘ₗ
            DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
have h₁ : Eq.{w' + 1} (α := B) ((f ∘ₐ ι R A i : (a : A i) → B) a : B) ((maps : (a : A i) → B) a : B)
Tactic: specialize h i a
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
have pos : ∀ (hV : Subsingleton V), ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
Tactic: by_cases! hV : Subsingleton V
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
pos : ∀ (hV : Subsingleton V), ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
have neg : ∀ (hV : Nontrivial V), ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
Tactic: by_cases! hV : Subsingleton V
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Subsingleton V
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
have a : Nontrivial W
Tactic: nontriviality W
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
have neg : ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
Tactic: simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← comp_assoc, eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
⊢ ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
have neg : ∀ (u : V) (hu : u ≠ 0),
  ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
Tactic: obtain ⟨u, hu⟩ := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
⊢ ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
have neg : ∀ (v : Dual K V) (huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)),
  ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
Tactic: obtain ⟨v, huv⟩ := Projective.exists_dual_ne_zero K hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
⊢ ∃ (z : W),
    ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
        ((0 : (a : W) → W) z : W)
have rw : ¬∀ (x : V), Eq (α := V) ((smulRight v u : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)
Tactic: rw [← not_forall, ← LinearMap.ext_iff, EmbeddingLike.map_eq_zero_iff, LinearMap.ext_iff]