mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

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

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 : ℕ
inst✝ : HasInjectiveDimensionLT X n
k : ℕ
⊢ n ≤ k + n

Tactic:
by

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

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
hi : 1 ≤ 0
e : Ext Y X 0
⊢ e = 0

pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext Y X (i + 1)
⊢ e = 0

Tactic:
· simp at hi

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext Y X (i + 1)
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

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

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✝ : HasExt C
h : Injective X
⊢ 1 ≤ 1

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✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)
X✝ Y✝ : C
f : X✝ ⟶ X
g : X✝ ⟶ Y✝
x✝ : Mono g
⊢ ⋯.extClass.comp (Ext.mk₀ f) ⋯ = 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✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)
X✝ Y✝ : C
f : X✝ ⟶ X
g : X✝ ⟶ Y✝
x✝ : Mono g
φ : { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.X₂ ⟶ X
hφ :
  (Ext.mk₀ { X₁ := X✝, X₂ := Y✝, X₃ := cokernel g, f := g, g := cokernel.π g, zero := ⋯ }.f).comp (Ext.homEquiv₀.symm φ)
      ⋯ =
    Ext.mk₀ f
⊢ Ext.homEquiv₀.symm (g ≫ φ) = Ext.homEquiv₀.symm 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
inst✝ : HasExt C
⊢ Injective X ↔ ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)

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
this : HasExt C := HasExt.standard C
x✝ : HasInjectiveDimensionLT X 1
⊢ 1 ≤ 1

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
⊢ Injective X ↔ HasInjectiveDimensionLT X 1

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 Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
⊢ HasInjectiveDimensionLT X n

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
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
⊢ HasInjectiveDimensionLT S.X₂ n

Tactic:
by

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
hi : n + 1 ≤ 0
Y : C
x₃ : Ext Y S.X₁ 0
⊢ x₃ = 0

pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext Y S.X₁ (i + 1)
⊢ x₃ = 0

Tactic:
· simp at hi

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext Y S.X₁ (i + 1)
⊢ x₃ = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.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
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
⊢ HasInjectiveDimensionLT S.X₁ (n + 1)

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)
n : ↑S.X₁
cn : ι →₀ R
hnm : (cn.sum fun a b ↦ (Hom.hom S.f) (b • v a)) = m - m'
hn : (cn.sum fun i a ↦ a • v i) = n
⊢ (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)

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
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext Y S.X₃ i
⊢ n + 1 ≤ 1 + 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
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.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
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
⊢ HasInjectiveDimensionLT S.X₃ n

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
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext Y X i
⊢ e = 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
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + 0
⊢ d = n

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
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
⊢ n + k + 1 = d

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
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd✝ : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
⊢ (Ext.mk₀ { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.g).comp e ⋯ = 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
inst✝¹ : HasExt C
inst✝ : EnoughProjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext Y X n)
⊢ HasInjectiveDimensionLT X n

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 Y : C
e : X ≅ Y
⊢ injectiveDimension X = injectiveDimension Y

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 Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : n ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i}
⊢ n ∈ insert ⊤ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT 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
n : ℕ
h : injectiveDimension X < ↑n
⊢ ⊤ ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT 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
h : HasInjectiveDimensionLT X 0
x✝¹ : ℕ
x✝ : ⊥ < ↑x✝¹
⊢ 0 ≤ 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
h : HasInjectiveDimensionLT X 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
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n + 1 ≤ 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 : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ↑n < ↑(n + 1)

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 : ℕ
⊢ injectiveDimension X < ↑n ↔ HasInjectiveDimensionLT X n

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 : ℕ
⊢ injectiveDimension X ≤ ↑n ↔ HasInjectiveDimensionLE X n

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 : ℕ
⊢ ↑n ≤ injectiveDimension X ↔ ¬HasInjectiveDimensionLT X n

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))
⊢ ⊤ ≤ span R (range u)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}) = ⋀[R]^n M

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
⊢ injectiveDimension X = ⊥ ↔ Limits.IsZero 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
hd : injectiveDimension X = ⊥
⊢ HasInjectiveDimensionLE X 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (range ⇑(ιMulti R n)) = ⊤

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
d : ℕ
hd : injectiveDimension X = ↑↑d
⊢ HasInjectiveDimensionLE X d

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ιMulti R n) '' {a | range a ⊆ s}) = ⊤

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
⊢ injectiveDimension X ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
x y : M
⊢ s.var (update m i (x + y)) = s.var (update m i x) + s.var (update m i y)

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₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⊤ ≤ span R (range (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w)))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
r : R
x : M
⊢ s.var (update m i (r • x)) = r • s.var (update m i x)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : (relations R ι M).Solution N
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ s.var v = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ finrank R ↑S.X₂ = n + p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M [⋀^ι]→ₗ[R] N
⊢ ∀ (r : (relations R ι M).R), (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation r) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
N✝ : Type ?u.42
inst✝¹ : AddCommGroup N✝
inst✝ : Module R N✝
s : (relations R (Fin n) M).Solution N✝
⊢ (relationsSolutionEquiv.symm (ιMulti R n)).postcomp
      (ExteriorAlgebra.liftAlternating (update 0 n (relationsSolutionEquiv s)) ∘ₗ (⋀[R]^n M).subtype) =
    s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
this : Small.{max v v', u} R
n : ℕ
ih : ∀ {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
I : ModuleCat R
injective✝ : Injective I
f : M ⟶ I
mono✝ : Mono f
injf : Function.Injective ⇑(Hom.hom f)
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero (Hom.hom f) (Hom.hom f).range.mkQ ⋯
exactS : S.ShortExact
I' : ModuleCat R := of R (ULift.{v', v} ↑I)
f' : ↑N →ₗ[R] ↑I' := ↑ULift.moduleEquiv.symm ∘ₗ Hom.hom f ∘ₗ ↑e.symm
⊢ Function.Injective ⇑f'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N✝ : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N✝
inst✝² : Module R N✝
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
N : Type ?u.42
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ f = f'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
⊢ (presentation R n M).postcomp f = (presentation R n M).postcomp g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
s : ↑N → ↑M
hs : Function.RightInverse s ⇑(ConcreteCategory.hom p)
⊢ freeDesc (↾fun x ↦ s ((ConcreteCategory.hom f) (freeMk x))) ≫ p = f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
this : Small.{max v v', u} R
n : ℕ
ih : ∀ {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
I : ModuleCat R
injective✝ : Injective I
f : M ⟶ I
mono✝ : Mono f
injf : Function.Injective ⇑(Hom.hom f)
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero (Hom.hom f) (Hom.hom f).range.mkQ ⋯
exactS : S.ShortExact
I' : ModuleCat R := of R (ULift.{v', v} ↑I)
f' : ↑N →ₗ[R] ↑I' := ↑ULift.moduleEquiv.symm ∘ₗ Hom.hom f ∘ₗ ↑e.symm
injf' : Function.Injective ⇑f'
S' : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f' f'.range.mkQ ⋯
exactS' : S'.ShortExact
⊢ Submodule.map (↑ULift.moduleEquiv.symm) (Hom.hom f).range = f'.range

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Epi p
⊢ ∃ f', f' ≫ p = f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ∀ (X : ModuleCat R), isProjective (ModuleCat R) ((forget (ModuleCat R) ⋙ free R).obj X)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
F : ↥(⋀[R]^n M) →ₗ[R] N
m : Fin n → M
⊢ (alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (ιMulti R n)) m

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ alternatingMapLinearEquiv.symm (map n f) = (ιMulti R n).compLinearMap f

Tactic:
by

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

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

Tactic:
by

Goal state after: