mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : Fin n → M
⊢ (map n f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

Tactic:
by

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

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
have exactS' := ModuleCat.shortComplex_shortExact S'
      f'.hom.exact_map_mkQ_range injf' (Submodule.mkQ_surjective _)

Goal state after:
case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
⊢ ⇑(map n f) ∘ ιMulti_family R n v = ιMulti_family R n (⇑f ∘ v)

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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : ↑(powersetCard I n)
⊢ (map n f) (ιMulti_family R n v s) = ιMulti_family R n (⇑f ∘ v) s

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
⊢ map n LinearMap.id = LinearMap.id

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'
f : M →ₗ[R] N
g : N →ₗ[R] N'
⊢ map n (g ∘ₗ f) = map n g ∘ₗ map n 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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this : Module.Injective R' ↑I'
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 :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (of R ↑I)

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
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n g) ((map n f) x✝) = x✝

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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
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 :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
⊢ 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
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Surjective ⇑(map 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
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
this : (ExteriorAlgebra.ιMulti R n) (v ∘ α) = 0
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
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 :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
exactS : S.ShortExact
⊢ Submodule.map (↑eI) f.range = (Hom.hom f').range

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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
this : ∃ σ, (ExteriorAlgebra.ιMulti R n) ((v ∘ α) ∘ ⇑σ) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

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
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
⊢ injectiveDimension M = injectiveDimension 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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f✝ : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
X₀✝ X₁✝ : C
f : X₁✝ ⟶ X₀✝
⊢ ι.map (ι.preimage (Λ.π.app (kernel (ι.map f)) ≫ kernel.ι (ι.map f)) ≫ f) = ι.map 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ ι.map ((Λ.chainComplex X).d 1 0) =
    ι.map (Λ.chainComplexXOneIso X).hom ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫ kernel.ι (Λ.π.app X) ≫ ι.map (Λ.chainComplexXZeroIso X).inv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (Λ.chainComplex X).X (n + 2) ≅ Λ.F.obj (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))) ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) (mk m s) = 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M : ModuleCat R
S : Submonoid R
⊢ IsLocalizedModule S (M.localizedModuleMkLinearMap S)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = 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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) = ⋀[R]^n M

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat R
f : X ⟶ Y
g : Y ⟶ Z
⊢ localizedModuleMap S (f ≫ g) = localizedModuleMap S f ≫ localizedModuleMap S g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
T : ShortComplex (ModuleCat R)
h : T.Exact
⊢ (T.map (localizedModuleFunctor S)).Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteColimits (localizedModuleFunctor S)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ Function.Bijective ⇑(Hom.hom f₂)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ IsIso 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
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (range v) = ⊤
⊢ Submodule.span R (range (ιMulti_family R n v)) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
⊢ span R (range f) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).ExactAt (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ ι.map
      (((Λ.chainComplexXOneIso X).hom ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ (Λ.chainComplexXOneIso Y).inv) ≫
        (Λ.chainComplex Y).d 1 0) =
    ι.map ((Λ.chainComplex X).d 1 0 ≫ (Λ.chainComplexXZeroIso X).hom ≫ Λ.F.map f ≫ (Λ.chainComplexXZeroIso Y).inv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n) ≫ ι.map p.fst = ι.map p.snd.fst ≫ ι.map ((Λ.chainComplex Y).d (n + 1) n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
p :
  (f : (Λ.chainComplex X).X n ⟶ (Λ.chainComplex Y).X n) ×'
    (f' : (Λ.chainComplex X).X (n + 1) ⟶ (Λ.chainComplex Y).X (n + 1)) ×'
      f' ≫ (Λ.chainComplex Y).d (n + 1) n = (Λ.chainComplex X).d (n + 1) n ≫ f
⊢ ι.map
      (((Λ.chainComplexXIso X n).hom ≫
          Λ.F.map
              (kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n)) (ι.map ((Λ.chainComplex Y).d (n + 1) n))
                (ι.map p.snd.fst) (ι.map p.fst) ⋯) ≫
            (Λ.chainComplexXIso Y n).inv) ≫
        (Λ.chainComplex Y).d (n + 2) (n + 1)) =
    ι.map ((Λ.chainComplex X).d (n + 2) (n + 1) ≫ p.snd.fst)

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
I : Type u_4
inst✝ : LinearOrder I
v : I → M
⊢ (map n (span R (range v)).subtype).range = span R (range (ιMulti_family R n v))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n) ≫ ι.map ((Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1)) ≫ ι.map ((Λ.chainComplex Y).d (n + 1) 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'
r : R
⊢ Fin 0 → M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y : A
f : X ⟶ Y
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ (Λ.chainComplexMap f).f (n + 2) =
    (Λ.chainComplexXIso X n).hom ≫
      Λ.F.map
          (kernel.map (ι.map ((Λ.chainComplex X).d (n + 1) n)) (ι.map ((Λ.chainComplex Y).d (n + 1) n))
            (ι.map ((Λ.chainComplexMap f).f (n + 1))) (ι.map ((Λ.chainComplexMap f).f n)) ⋯) ≫
        (Λ.chainComplexXIso Y n).inv

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'
⊢ ∀ (x y : R),
    ((x + y) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
      (x • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) +
        y • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim

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'
⊢ ∀ (m x : R),
    ((m • x) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
      (RingHom.id R) m • x • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim

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'
⊢ alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) ∘ₗ
      { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } =
    LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
⊢ Λ.chainComplexMap (𝟙 X) = 𝟙 (Λ.chainComplex 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'
⊢ { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) =
    LinearMap.id

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
⊢ (zeroEquiv R M) ((ιMulti R 0) f) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
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
⊢ ↑(zeroEquiv R N) ∘ₗ map 0 f = ↑(zeroEquiv R M)

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'
m : M
⊢ (fun x ↦ m) = update (fun x ↦ 0) 0 m

Tactic:
by

Goal state after: