awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
hf :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)))
    (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M)))

Tactic:
have hg : Injective g := lTensor_preserves_injective_linearMap _ (p.injective_inclusionSpan A)
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
hf :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
hg :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)))
    (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M)))
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] ↥(span A (↑p : Set M)))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_3)} →
            {M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (tensorToSpan A p))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f ∘ₗ
      g)

Tactic:
have : p.tensorToSpan A = f.restrictScalars R ∘ₗ g := by ext; simp [tensorToSpan, f, g]
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
a : A
x : ↥p
⊢ (↑((tensorEquivSpan A p : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M))) (a ⊗ₜ[R] x)) : M) = a • (↑x : M)

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, rfl
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
s : Set M
a : A
x : ↥(span R s)
⊢ (↑((tensorSpanEquivSpan R A s : (a : A ⊗[R] ↥(span R s)) → ↥(span A s)) (a ⊗ₜ[R] x)) : M) = a • (↑x : M)

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
inl : Subsingleton R → finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
inr : Nontrivial R → finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p

Tactic:
rcases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
h : Subsingleton R
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p

Tactic:
simp [Algebra.subsingleton R A]

Premises used: Algebra.subsingleton
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
p : Submodule R M
inst_10 : Free.{u_1, u_3} R ↥p
inst_11 : Module.Finite.{u_1, u_3} R ↥p
h : Nontrivial R
ι : Type u_3 := Free.ChooseBasisIndex R ↥p
b₁ : Basis ι R ↥p := Free.chooseBasis R ↥p
b₂ : Basis ι A ↥(span A (↑p : Set M)) :=
  Basis.map (M := TensorProduct.{u_1, u_2, u_3} R A ↥p) (Basis.baseChange A b₁) (tensorEquivSpan A p)
inr : finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = Fintype.card ι
inr₁ inr₂ : Fintype.card ι = Fintype.card ι
⊢ finrank.{u_2, u_3} A ↥(span A (↑p : Set M)) = finrank.{u_1, u_3} R ↥p

Tactic:
rw [finrank_eq_card_basis b₁, finrank_eq_card_basis b₂]

Premises used: Module.finrank_eq_card_basis
-- Module: Mathlib.LinearAlgebra.Span.TensorProduct
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Nontrivial A
inst_3 : Algebra R A
inst_4 : Algebra.IsEpi R A
inst_5 : Flat R A
inst_6 : AddCommGroup M
inst_7 : Module R M
inst_8 : Module A M
inst_9 : IsScalarTower R A M
inst_10 : IsPrincipalIdealRing R
inst_11 : IsDomain R
inst_12 : IsTorsionFree R M
s : Set M
inst_13 : Module.Finite.{u_1, u_3} R ↥(span R s)
rw : finrank.{u_2, u_3} A ↥(span A (↑(span R s) : Set M)) = finrank.{u_1, u_3} R ↥(span R s)
rw₁ rw₂ : finrank.{u_1, u_3} R ↥(span R s) = finrank.{u_1, u_3} R ↥(span R s)
⊢ finrank.{u_2, u_3} A ↥(span A s) = finrank.{u_1, u_3} R ↥(span R s)

Tactic:
rw [← span_span_of_tower R, finrank_span_eq_finrank]

Premises used: Submodule.span_span_of_tower, Submodule.finrank_span_eq_finrank
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
u : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : R) (1 : R)

Tactic:
simp [← LinearEquiv.coe_det, u.prop]

Premises used: Subtype.prop, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
u v : SpecialLinearGroup R V
⊢ u = v ↔
    ∀ (x : V),
      Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
        ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)

Tactic:
simp only [← Subtype.coe_inj, LinearEquiv.ext_iff]

Premises used: Subtype.coe_inj, LinearEquiv.ext_iff
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
u v : SpecialLinearGroup R V
⊢ (∀ (x : V),
      Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
        ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)) →
    u = v

Tactic:
(SpecialLinearGroup.ext_iff u v).mpr

Premises used: Iff.mpr, SpecialLinearGroup.ext_iff
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
a :
  ∀ (x : V),
    Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
      ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
⊢ u = v

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
pos :
  ∀ (hx : x = 0),
    Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
      ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
neg :
  ∀ (hx : ¬x = 0),
    Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
      ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : x = 0
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)

Tactic:
simp [hx]
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
this : ∀ (u : SpecialLinearGroup R V), (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
⊢ ∀ (u : SpecialLinearGroup R V) (x : V), ((↑u : V ≃ₗ[R] V) : (a : V) → V) x = x

Tactic:
simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this

Premises used: LinearMap.id_coe, LinearMap.ext_iff, LinearEquiv.coe_coe, id_eq
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
this : ∀ (u : SpecialLinearGroup R V) (x : V), ((↑u : V ≃ₗ[R] V) : (a : V) → V) x = x
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)

Tactic:
simp [this u, this v]
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
neg : ∀ (u : SpecialLinearGroup R V), (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id
⊢ Eq.{u_2 + 1} (α := V) ((fun (x : V) ↦ (((↑u : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)
    ((fun (x : V) ↦ (((↑v : V ≃ₗ[R] V) : (a : V) → V) x : V)) x)

Tactic:
suffices ∀ (u : SpecialLinearGroup R V), (u : V →ₗ[R] V) = LinearMap.id by
      simp only [LinearMap.ext_iff, LinearEquiv.coe_coe, LinearMap.id_coe, id_eq] at this
      simp [this u, this v]
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x : V
hx : ¬x = 0
u : SpecialLinearGroup R V
neg :
  ∀ (x : V), Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)
⊢ (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) = LinearMap.id

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
⊢ let c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V);
  c = ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)

Tactic:
set c := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm u with hc

Premises used: LinearEquiv.symm, LinearEquiv.smul_id_of_finrank_eq_one, LinearEquiv.toLinearMap, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : c = ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)

Tactic:
rw [LinearEquiv.eq_symm_apply] at hc

Premises used: LinearEquiv.eq_symm_apply
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
this : c = 1
⊢ Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)

Tactic:
simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]

Premises used: LinearEquiv.smul_id_of_finrank_eq_one
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
neg : c = 1
⊢ Eq (α := V) (((↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V) : (a : V) → V) x : V) ((LinearMap.id : (a : V) → V) x : V)

Tactic:
suffices c = 1 by
      simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑u : V ≃ₗ[R] V) : Rˣ) (1 : Rˣ)

Tactic:
have hu := u.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
d1 : Module.finrank R V = 1
u_1 v : SpecialLinearGroup R V
h : Nontrivial R
x_1 : V
hx : ¬x_1 = 0
u : SpecialLinearGroup R V
x : V
c : R := ((LinearEquiv.smul_id_of_finrank_eq_one d1).symm : (a : V →ₗ[R] V) → R) (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1 : (a : R) → V →ₗ[R] V) c = (↑(↑u : V ≃ₗ[R] V) : V →ₗ[R] V)
hu : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑u : V ≃ₗ[R] V) : Rˣ) (1 : Rˣ)
⊢ c = 1

Tactic:
simpa [← Units.val_inj, LinearEquiv.coe_det, ← hc,
      LinearEquiv.smul_id_of_finrank_eq_one, d1] using hu

Premises used: LinearEquiv.smul_id_of_finrank_eq_one, Units.val_inj, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑A : V ≃ₗ[R] V)⁻¹ : Rˣ) (1 : Rˣ)

Tactic:
simp [A.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A B : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) ((↑A : V ≃ₗ[R] V) * (↑B : V ≃ₗ[R] V)) : Rˣ) (1 : Rˣ)

Tactic:
simp [A.prop, B.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A B : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) ((↑A : V ≃ₗ[R] V) / (↑B : V ≃ₗ[R] V)) : Rˣ) (1 : Rˣ)

Tactic:
simp [A.prop, B.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) 1) 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x : SpecialLinearGroup R V
n : ℕ
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) ((↑x : V ≃ₗ[R] V) ^ n) : Rˣ) (1 : Rˣ)

Tactic:
simp [x.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
x : SpecialLinearGroup R V
n : ℤ
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) ((↑x : V ≃ₗ[R] V) ^ n) : Rˣ) (1 : Rˣ)

Tactic:
simp [x.prop]

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
A : SpecialLinearGroup R V
simp : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (↑(↑A : V ≃ₗ[R] V) : V →ₗ[R] V) : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := Rˣ)
    (((LinearEquiv.det (R := R) (M := Module.Dual R V) : (Module.Dual R V ≃ₗ[R] Module.Dual R V) →* Rˣ) :
          (a : Module.Dual R V ≃ₗ[R] Module.Dual R V) → Rˣ)
        (↑A : V ≃ₗ[R] V).dualMap :
      Rˣ)
    (1 : Rˣ)

Tactic:
simp only [← Units.val_inj, LinearEquiv.coe_det, Units.val_one,
      LinearEquiv.dualMap, LinearMap.det_dualMap]

Premises used: Units.val_inj, LinearMap.det_dualMap, Units.val_one, LinearEquiv.dualMap, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
A : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (↑(↑A : V ≃ₗ[R] V) : V →ₗ[R] V) : R) (1 : R)

Tactic:
simp [← LinearEquiv.coe_det, A.prop]

Premises used: Subtype.prop, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : V ≃ₗ[R] V
h : Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) A : Rˣ) (1 : Rˣ)
⊢ (↑(Subtype.mk (p := fun (u : V ≃ₗ[R] V) ↦
          Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) u : Rˣ) (1 : Rˣ)) A h) :
      V ≃ₗ[R] V) =
    A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A B : SpecialLinearGroup R V
⊢ (↑(A * B) : V ≃ₗ[R] V) = (↑A : V ≃ₗ[R] V) * (↑B : V ≃ₗ[R] V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A B : SpecialLinearGroup R V
⊢ (↑(A / B) : V ≃ₗ[R] V) = (↑A : V ≃ₗ[R] V) / (↑B : V ≃ₗ[R] V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
⊢ (↑A⁻¹ : V ≃ₗ[R] V) = (↑A : V ≃ₗ[R] V)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
⊢ Eq.{u_2 + 1} (α := V ≃ₗ[R] V) (↑1 : V ≃ₗ[R] V) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (↑A : V ≃ₗ[R] V) : Rˣ) (1 : Rˣ)

Tactic:
A.prop

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
m : ℕ
⊢ (↑(A ^ m) : V ≃ₗ[R] V) = (↑A : V ≃ₗ[R] V) ^ m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
m : ℤ
⊢ (↑(A ^ m) : V ≃ₗ[R] V) = (↑A : V ≃ₗ[R] V) ^ m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
inst_3 : Module.Free R V
inst_4 : Module.Finite R V
⊢ (↑Aᵀ : Module.Dual R V ≃ₗ[R] Module.Dual R V) = (↑A : V ≃ₗ[R] V).dualMap

Tactic:
rfl

Premises used: LinearEquiv.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
v : V
⊢ Eq (α := V) ((((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) A : V ≃ₗ[R] V) : (a : V) → V) v : V)
    ((fun (x : V) ↦ (((↑A : V ≃ₗ[R] V) : (a : V) → V) x : V)) v : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.SpecialLinearGroup
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
A : SpecialLinearGroup R V
⊢ (↑((toLinearEquiv : (a : SpecialLinearGroup R V) → V ≃ₗ[R] V) A) : V →ₗ[R] V) = (↑(↑A : V ≃ₗ[R] V) : V →ₗ[R] V)

Tactic:
rfl

Premises used: rfl