mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : M →ₗ[R] A),
    (∀ (m : M), a m * a m = 0) ↔
      ∀ (m : M), ((Equiv.refl (M →ₗ[R] A)) a) m * ((Equiv.refl (M →ₗ[R] A)) a) m = (algebraMap R A) (0 m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : M
⊢ 0 x✝ * 0 x✝ = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
⊢ algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ ιInv ((ι R) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Disjoint (ι R).range 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
ι : Type u_5
⊢ Module R (M [⋀^ι]→ₗ[R] N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
i : Fin n
⊢ (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
F : MultilinearMap R (fun x ↦ M) (ExteriorAlgebra R M) :=
  (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun x ↦ ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ F f = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (liftAlternating f) ((ι R) m) = (f 1) ![m]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : Fin 0 → M
⊢ (ιMulti R 0) v = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n.succ → M
⊢ (ιMulti R n.succ) v = (ι R) (v 0) * (ιMulti R n) (Matrix.vecTail v)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
m : M
⊢ (ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R ((ι R) m)).compAlternatingMap (ιMulti R n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ (liftAlternating f) ((ι R) m * x) = (liftAlternating fun i ↦ (f i.succ).curryLeft m) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating f) 1 = (f 0) 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ (ιMulti R m) a * (ιMulti R n) b = (ιMulti R (m + n)) (Fin.append a b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
⊢ (liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Set.range ⇑(ιMulti R n) ⊆ ↑(⋀[R]^n M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
n : ℕ
N : ModuleCat R
φ : M.AlternatingMap N n
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (desc φ)) (mk x) = φ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
n : ℕ
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (map f n)) (mk x) = mk (⇑(ConcreteCategory.hom f) ∘ x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Submodule.span R (Set.range ⇑(ιMulti R n)) = ⋀[R]^n M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) ((ιMulti R n) v) = (f n) v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) = g ∘ₗ liftAlternating f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t =
    Equiv.Perm.sign (permOfDisjoint h) • ιMulti_family R (m + n) v (disjUnion h)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ (map f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ liftAlternating (ιMulti R) = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j k : J
f : j ⟶ k
x : ↑(F.obj j)
⊢ (hom (F.map (𝟙 ⟨k, (hom (F.map f)) x⟩.fst))) ⟨k, (hom (F.map f)) x⟩.snd = (hom (F.map f)) ⟨j, x⟩.snd

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
F : ExteriorAlgebra R M →ₗ[R] N
⊢ F ∘ₗ liftAlternating (ιMulti R) = F

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁸ : CommRing R
M : Type u2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsCentralScalar R M
inst✝¹ : Module Rᵐᵒᵖ N
inst✝ : IsCentralScalar R N
f : M →ₗ[R] N
⊢ toTrivSqZeroExt.comp (map f) = (TrivSqZeroExt.map f).comp toTrivSqZeroExt

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × ↑(F.obj j)
h : Types.FilteredColimit.Rel (F ⋙ forget (ModuleCat R)) x y
⊢ colimitSMulAux F r x = colimitSMulAux F r y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x : ↑(M F)
⊢ ↑(M F)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j : J
⊢ 0 = M.mk F ⟨j, 0⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ LinearIndependent R u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x y : (j : J) × ↑(F.obj j)
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
⊢ M.mk F x + M.mk F y = M.mk F ⟨k, (hom (F.map f)) x.snd + (hom (F.map g)) y.snd⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j : J
x y : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ + M.mk F ⟨j, y⟩ = M.mk F ⟨j, x + y⟩

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : ↑(M F)
⊢ (r * s) • x = r • s • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x : ↑(M F)
⊢ 1 • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
⊢ r • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x : ↑(M F)
⊢ 0 • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ LeftInverse ⇑(map g) ⇑(map f) ↔ LeftInverse ⇑g ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩
  obtain ⟨x, hx⟩ := h (ι R y)
  existsi ιInv x
  rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]
  simp [hx, ιInv]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective ⇑(map f) ↔ Function.Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ toExterior ((ι R) m) = (ExteriorAlgebra.ι R) m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : ↑(M F)
⊢ r • (x + y) = r • x + r • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : ↑(M F)
⊢ (r + s) • x = r • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
j : J
⊢ ∀ (m : R) (x : ↑(F.1 j)),
    (↑(AddCommGrpCat.Hom.hom
              ((AddCommGrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)).ι.app j))).toFun
        (m • x) =
      (RingHom.id R) m •
        (↑(AddCommGrpCat.Hom.hom
                ((AddCommGrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)).ι.app
                  j))).toFun
          x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ coconeMorphism F x✝ = coconeMorphism F x✝¹ ≫ ((Functor.const J).obj (colimit F)).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
⊢ m - m' ∈ (Hom.hom S.f).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
h : IsColimit (AddCommGrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)) :=
  AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
f : ↑(colimit F) →+ ↑t.pt := AddCommGrpCat.Hom.hom (h.desc ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone t))
hf : ∀ {j : J} (x : ↑(F.obj j)), f (M.mk F ⟨j, x⟩) = (hom (t.ι.app j)) x
r : R
x : ↑(M F)
⊢ (↑f).toFun (r • x) = (RingHom.id R) r • (↑f).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
x✝ : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = colimitDesc F t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : HasInjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext Y X i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext Y X i
⊢ e₁ = e₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext Y X i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
⊢ HasInjectiveDimensionLT X 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c • (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ 0 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
⊢ IsZero X

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ↟(Hom.hom f).range.subtype = Limits.image.ι f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext Y X i
⊢ n ≤ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
⊢ HasInjectiveDimensionLT X m

Tactic:
by

Goal state after: