mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
j : ℤ
ι : (singleFunctor C (j + 1)).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE (j + 1)
inst✝ : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I).inv ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I).hom ≫ α
⊢ L.d j (j + 1) ≫ Injective.factorThru (𝟙 I) α = 0

Tactic:
apply (L.isZero_of_isStrictlyGE (j + 1) j (by simp)).eq_of_src

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x✝ : ↑(AddCommGrpCat.of (Ext S.X₃ Y n))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → (B n) y = 0) ↔ (B x) y = 0

Tactic:
constructor

Goal state after:
case mp
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → (B n) y = 0) → (B x) y = 0

case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (B x) y = 0 → ∀ (n : V), (∃ a, a • x = n) → (B n) y = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.precomp Y h) = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₂ Y n₀))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.precomp Y h)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
⊢ π = Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)

Tactic:
ext

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
r : relations.R
a✝ : relations.G
⊢ (π ∘ₗ Finsupp.lsingle a✝) 1 = ((Finsupp.linearCombination A fun g ↦ π (Finsupp.single g 1)) ∘ₗ Finsupp.lsingle a✝) 1
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
⊢ (ofπ π hπ).π = π

Tactic:
ext

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
π : (relations.G →₀ A) →ₗ[A] M
hπ : ∀ (r : relations.R), π (relations.relation r) = 0
a✝ : relations.G
⊢ ((ofπ π hπ).π ∘ₗ Finsupp.lsingle a✝) 1 = (π ∘ₗ Finsupp.lsingle a✝) 1
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient ↔ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
constructor

Goal state after:
case mp
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient → solution.π.ker = Submodule.span A (Set.range relations.relation)

case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation) → Function.Injective ⇑solution.fromQuotient
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
constructor

Goal state after:
case left
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤

case right
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ℕ) v)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
e : Basis ι R M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ j✝ : ι
⊢ e.toMatrix v i✝ j✝ = (LinearMap.toMatrix e e) ((e.constr ℕ) v) i✝ j✝
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ AddCommGrpCat.ofHom (hS.extClass.precomp Y h) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
x✝ : ↑(AddCommGrpCat.of (Ext S.X₁ Y n₀))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (hS.extClass.precomp Y h) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯)))
      x✝ =
    (AddCommGrpCat.Hom.hom 0) x✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
⊢ b.toMatrix (x • w) = (Algebra.leftMulMatrix b) x * b.toMatrix w

Tactic:
ext

Goal state after:
ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ b.toMatrix (x • w) i✝ j✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
⊢ (algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) = b.toMatrix fun i ↦ ↑(v i)

Tactic:
ext

Goal state after:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝¹¹ : CommRing R₂
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : Module R₂ M₂
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
S : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Nontrivial S
inst✝⁴ : Algebra R₂ S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R₂ S M₂
inst✝¹ : IsDomain R₂
inst✝ : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range ⇑b))
i✝ j✝ : ι
⊢ (algebraMap R₂ S).mapMatrix ((restrictScalars R₂ b).toMatrix v) i✝ j✝ = b.toMatrix (fun i ↦ ↑(v i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) _root_.id

Tactic:
ext

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (b.toMatrix v).submatrix (⇑e.symm) _root_.id i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
⊢ (b.map f).toMatrix v = b.toMatrix (⇑f.symm ∘ v)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
i✝ j✝ : ι
⊢ (b.map f).toMatrix v i✝ j✝ = b.toMatrix (⇑f.symm ∘ v) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_9
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
b : Basis ι R M
c : Basis κ R N
f : M →ₗ[R] N
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite κ
⊢ (LinearMap.toMatrix b c) f = c.toMatrix (⇑f ∘ ⇑b)

Tactic:
ext

Goal state after:
ι : Type u_1
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_9
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
b : Basis ι R M
c : Basis κ R N
f : M →ₗ[R] N
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Finite κ
i✝ : κ
j✝ : ι
⊢ (LinearMap.toMatrix b c) f i✝ j✝ = c.toMatrix (⇑f ∘ ⇑b) i✝ j✝
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
            X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                  X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.precomp Y hn₁), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
exact this x₁ hx₁

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℤ
⊢ (zpowGroupHom k).ker = rootsOfUnity k.natAbs M

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℤ
x✝ : Mˣ
⊢ x✝ ∈ (zpowGroupHom k).ker ↔ x✝ ∈ rootsOfUnity k.natAbs M
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m n : ℕ
⊢ rootsOfUnity m M ⊓ rootsOfUnity n M = rootsOfUnity (m.gcd n) M

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
m n : ℕ
x✝ : Mˣ
⊢ x✝ ∈ rootsOfUnity m M ⊓ rootsOfUnity n M ↔ x✝ ∈ rootsOfUnity (m.gcd n) M
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ (_root_.restrictRootsOfUnity σ.symm n) ((_root_.restrictRootsOfUnity σ n) ξ) = ξ

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑↑((_root_.restrictRootsOfUnity σ.symm n) ((_root_.restrictRootsOfUnity σ n) ξ)) = ↑↑ξ
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ (_root_.restrictRootsOfUnity σ n) ((_root_.restrictRootsOfUnity σ.symm n) ξ) = ξ

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : CommMonoid R
inst✝¹ : CommMonoid S
inst✝ : FunLike F R S
σ : R ≃* S
n : ℕ
ξ : ↥(rootsOfUnity n S)
⊢ ↑↑((_root_.restrictRootsOfUnity σ n) ((_root_.restrictRootsOfUnity σ.symm n) ξ)) = ↑↑ξ
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
constructor

Goal state after:
case mp
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) → M.det = 0

case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ M.det = 0 → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

Tactic:
constructor

Goal state after:
case mp
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0

case mpr
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
⊢ (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
⊢ det ((scalar n) u) = u ^ Fintype.card n

Tactic:
ext

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
u : Rˣ
⊢ ↑(det ((scalar n) u)) = ↑(u ^ Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ det ((map f) g) = (Units.map ↑f) (det g)

Tactic:
ext

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ ↑(det ((map f) g)) = ↑((Units.map ↑f) (det g))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
⊢ (map f) ((scalar n) u) = (scalar n) ((Units.map ↑f) u)

Tactic:
ext

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
u : Rˣ
i✝ j✝ : n
⊢ ↑((map f) ((scalar n) u)) i✝ j✝ = ↑((scalar n) ((Units.map ↑f) u)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝⁸ : DecidableEq n
inst✝⁷ : Fintype n
R : Type v
inst✝⁶ : CommRing R
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
g : SpecialLinearGroup n R
⊢ (GeneralLinearGroup.map (algebraMap S T)) ((mapGL S) g) = (mapGL T) g

Tactic:
ext

Goal state after:
n : Type u
inst✝⁸ : DecidableEq n
inst✝⁷ : Fintype n
R : Type v
inst✝⁶ : CommRing R
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
g : SpecialLinearGroup n R
i✝ j✝ : n
⊢ ↑((GeneralLinearGroup.map (algebraMap S T)) ((mapGL S) g)) i✝ j✝ = ↑((mapGL T) g) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ rootsOfUnity.mkOfPowEq ((↑↑A * ↑↑B) i i) ⋯ = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯ * rootsOfUnity.mkOfPowEq (↑↑B i i) ⋯

Tactic:
ext

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
A B : ↥(center (SpecialLinearGroup n R))
⊢ ↑↑(rootsOfUnity.mkOfPowEq ((↑↑A * ↑↑B) i i) ⋯) =
    ↑↑(rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯ * rootsOfUnity.mkOfPowEq (↑↑B i i) ⋯)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩

Tactic:
ext

Goal state after:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i✝ j✝ : Fin 2
⊢ ↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
⊢ transvection hij 0 = 1

Tactic:
ext

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
i✝ j✝ : ι
⊢ ↑(transvection hij 0) i✝ j✝ = ↑1 i✝ j✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
⊢ mul.comp (mulLeft 0) = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ mul.comp (mulLeft (x + y)) = mul.comp (mulLeft x) + mul.comp (mulLeft y)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft (x + y))) x✝¹) x✝ = ((mul.comp (mulLeft x) + mul.comp (mulLeft y)) x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
⊢ mul.compr₂ (mulLeft 0) = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ mul.compr₂ (mulLeft (x + y)) = mul.compr₂ (mulLeft x) + mul.compr₂ (mulLeft y)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft (x + y))) x✝¹) x✝ = ((mul.compr₂ (mulLeft x) + mul.compr₂ (mulLeft y)) x✝¹) x✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ diag2n hij c hc = diag2 c⁻¹ ⋯

Tactic:
ext

Goal state after:
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ ↑(diag2n hij c hc) i✝ j✝ = ↑(diag2 c⁻¹ ⋯) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
ext i j
  fin_cases i <;> fin_cases j <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ B = B' → (toMatrix₂' R) B = (toMatrix₂' R) B'

case mpr
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
⊢ (toMatrix₂' R) B = (toMatrix₂' R) B' → B = B'