awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
Goal:
I : Type u
inst : DecidableEq I
i_1 : 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 : {i : I} → AlgHom.{v, w, w'} R (A i) B
maps : FreeProduct R A →ₐ[R] B
i : I
a : A i
⊢ Eq.{w' + 1} (α := B)
    (((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := FreeTensorAlgebra R A) (rel R A))
                  ((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))
                    ((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i) maps))
                  (RingQuot.mkAlgHom R (rel R A))) ∘ₗ
              TensorAlgebra.ι R) ∘ₗ
            DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
    ((((maps ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)

Tactic:
aesop (add simp [ι, ι'])

Premises used: LinearAlgebra.FreeProduct.ι', LinearAlgebra.FreeProduct.ι
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
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)
⊢ 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

Tactic:
ext a
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
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:
simp [lift_apply, ι]

Premises used: LinearAlgebra.FreeProduct.lift_apply, LinearAlgebra.FreeProduct.ι
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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)
rw₁ rw₂ : Eq.{w' + 1} (α := B) ((algebraMap R B : (a : R) → B) r : 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)

Tactic:
rw [lift_apply, AlgHom.commutes]

Premises used: AlgHom.commutes, LinearAlgebra.FreeProduct.lift_apply
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
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)
⊢ f = (lift R A : (a : {i : I} → A i →ₐ[R] B) → FreeProduct R A →ₐ[R] B) fun {i : I} ↦ maps

Tactic:
ext i a
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
⊢ ∀ (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

Premises used: AlgHom.ext_iff
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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 ∘ₐ ι R A i : (a : A i) → B) a : B) ((maps : (a : A i) → B) a : B)

Tactic:
specialize h i a
-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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 : Eq.{w' + 1} (α := B) ((f ∘ₐ ι R A i : (a : A i) → B) a : B) ((maps : (a : A i) → B) a : 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)

Tactic:
simp [h.symm, ι]

Premises used: LinearAlgebra.FreeProduct.ι, Eq.symm
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
neg : ∀ (hV : Nontrivial V), ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T

Tactic:
by_cases! hV : Subsingleton V

Premises used: Subsingleton
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
⊢ Nontrivial W

Tactic:
nontriviality W
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
h : Nontrivial W
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T

Tactic:
simpa using congr(f $(Subsingleton.allEq 0 1))
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
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
⊢ ∃ (T : V ≃ₗ[K] W), f = conjAlgEquiv K T

Tactic:
simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← comp_assoc, eq_comp_toLinearMap_symm]

Premises used: LinearEquiv.conjAlgEquiv_apply, LinearMap.comp_assoc, AlgEquiv.ext_iff, LinearEquiv.eq_comp_toLinearMap_symm
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
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
⊢ ∃ (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)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
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
⊢ ∃ (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

Premises used: Module.Projective.exists_dual_ne_zero
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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)
rw : ¬∀ (x : V), Eq (α := V) ((smulRight v u : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)
⊢ ∃ (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)

Tactic:
rw [← not_forall, ← LinearMap.ext_iff, EmbeddingLike.map_eq_zero_iff, LinearMap.ext_iff]

Premises used: LinearMap.ext_iff, Classical.not_forall, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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)
⊢ ¬∀ (x : V), Eq (α := V) ((smulRight v u : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)

Tactic:
not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩

Premises used: Iff.mpr, Ne.isUnit, Iff.not, IsUnit.smul_eq_zero, Exists.intro, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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)
⊢ ¬∀ (x : V), Eq (α := V) ((smulRight v u : (a : V) → V) x : V) ((0 : (a : V) → V) x : V)

Tactic:
exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩

Premises used: Iff.mpr, Exists.intro, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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)
neg :
  ∀ (z : W)
    (hz :
      ¬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)),
    ∃ (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
⊢ ∃ (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 ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : End K W) z := by
    rw [← not_forall, ← LinearMap.ext_iff, EmbeddingLike.map_eq_zero_iff, LinearMap.ext_iff]
    exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
⊢ ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)

Tactic:
have hT x : T x = f (smulRight v x) z := rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
A : End K V
x : V
simp :
  Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v ((A : (a : V) → V) x)) : End K W) : (a : W) → W) z : W)
    ((((f : (a : End K V) → End K W) (A * smulRight v x) : End K W) : (a : W) → W) z : W)
⊢ Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
    ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)

Tactic:
simp only [hT, ← End.mul_apply, ← map_mul]

Premises used: map_mul, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
A : End K V
x : V
e_a : smulRight v ((A : (a : V) → V) x) = A * smulRight v x
⊢ Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v ((A : (a : V) → V) x)) : End K W) : (a : W) → W) z : W)
    ((((f : (a : End K V) → End K W) (A * smulRight v x) : End K W) : (a : W) → W) z : W)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
A : End K V
x : V
e_a :
  ∀ (x_1 : V),
    Eq (α := V) (((smulRight v ((A : (a : V) → V) x) : V →ₗ[K] V) : (a : V) → V) x_1 : V)
      ((A * smulRight v x : (a : V) → V) x_1 : V)
⊢ smulRight v ((A : (a : V) → V) x) = A * smulRight v x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
A : End K V
x x_1 : V
⊢ Eq (α := V) (((smulRight v ((A : (a : V) → V) x) : V →ₗ[K] V) : (a : V) → V) x_1 : V)
    ((A * smulRight v x : (a : V) → V) x_1 : V)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
⊢ ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)

Tactic:
have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← End.mul_apply, ← map_mul]
    congr; ext; simp
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv
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
hz :
  ¬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)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
w : W
obtain :
  ∀ (d : Dual K W)
    (hd :
      Eq.{u_1 + 1} (α := K)
        ((d : (a : W) → K) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W) : K)
        (1 : K)),
    ∃ (a : V), (T : (a : V) → W) a = w
⊢ ∃ (a : V), (T : (a : V) → W) a = w

Tactic:
obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz

Premises used: Module.Projective.exists_dual_eq_one