mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case a
ι : 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₂ := ⋯
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
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ (cn.sum fun a b ↦ b • u (Sum.inl a)) ∈ span R (range u)

pp: case a
ι : 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₂ := ⋯
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
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ m' ∈ span R (range u)

Tactic:
·

Goal state after:
case a
ι : 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₂ := ⋯
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
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ (cn.sum fun a b ↦ b • u (Sum.inl a)) ∈ span R (range u)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_1
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 = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ ⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f ∈ {a | range a ⊆ s}

pp: case a.refine_2
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 = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (ExteriorAlgebra.ιMulti R n) (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) = (List.ofFn fun i ↦ ↑(f i)).prod

Tactic:
·

Goal state after:
case a.refine_1
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 = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ ⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f ∈ {a | range a ⊆ s}
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case a
ι : 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₂ := ⋯
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
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ m' ∈ span R (range u)

Tactic:
·

Goal state after:
case a
ι : 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₂ := ⋯
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
hn' : (cn.sum fun a b ↦ b • (ConcreteCategory.hom S.f) (v a)) = cn.sum fun a b ↦ b • u (Sum.inl a)
⊢ m' ∈ span R (range u)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_2
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 = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (ExteriorAlgebra.ιMulti R n) (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) = (List.ofFn fun i ↦ ↑(f i)).prod

Tactic:
·

Goal state after:
case a.refine_2
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 = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (ExteriorAlgebra.ιMulti R n) (⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) = (List.ofFn fun i ↦ ↑(f i)).prod
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
⊢ HasInjectiveDimensionLT X n

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
⊢ HasInjectiveDimensionLT X n
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑n
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasInjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑0

pp: case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑(n + 1)

Tactic:
·

Goal state after:
case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasInjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑(n + 1)

Tactic:
·

Goal state after:
case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}, a < ↑(n + 1)
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case refine_1
ι : 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
⊢ Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inl =
    ⇑(ConcreteCategory.hom S.f) ∘ v

pp: case refine_2
ι : 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
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inl =
    ⇑(ConcreteCategory.hom S.f) ∘ v
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case refine_2
ι : 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
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))

Tactic:
·

Goal state after:
case refine_2
ι : 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
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case add
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
m : ι → M
i : ι
x y : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.add m i x y)) = 0

pp: case smul
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
m : ι → M
i : ι
r : R
x : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.smul m i r x)) = 0

pp: case alt
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
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.alt v i j hm hij)) = 0

Tactic:
·

Goal state after:
case add
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
m : ι → M
i : ι
x y : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.add m i x y)) = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case smul
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
m : ι → M
i : ι
r : R
x : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.smul m i r x)) = 0

pp: case alt
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
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.alt v i j hm hij)) = 0

Tactic:
·

Goal state after:
case smul
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
m : ι → M
i : ι
r : R
x : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.smul m i r x)) = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case alt
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
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.alt v i j hm hij)) = 0

Tactic:
·

Goal state after:
case alt
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
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.alt v i j hm hij)) = 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case neg
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 α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

pp: case pos
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 α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
·

Goal state after:
case neg
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 α
⊢ (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
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

pp: case a
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) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
·

Goal state after:
case a
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
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
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) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
·

Goal state after:
case a
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) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq : (RingCat.Hom.hom (R.map f ≫ α.app Y)) r = (RingCat.Hom.hom (α.app X ≫ R'.map f)) r
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x

Tactic:
dsimp at eq

Goal state after:
C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq :
  (RingCat.Hom.hom (α.app Y)) ((RingCat.Hom.hom (R.map f)) r) =
    (RingCat.Hom.hom (R'.map f)) ((RingCat.Hom.hom (α.app X)) r)
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case refine_1
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).1 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).1

pp: case refine_2
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).2 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).2

Tactic:
·

Goal state after:
case refine_1
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).1 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).1
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case refine_1
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).1 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).1

Tactic:
change h₁.homEquiv ((f ≫ g) ≫ fst X Y) = F.map f.op (h₁.homEquiv (g ≫ fst X Y))

Goal state after:
case refine_1
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ h₁.homEquiv ((f ≫ g) ≫ fst X Y) = (ConcreteCategory.hom (F.map f.op)) (h₁.homEquiv (g ≫ fst X Y))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case refine_2
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).2 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).2

Tactic:
·

Goal state after:
case refine_2
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).2 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).2
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: case h.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [c₁, X.right, c₂]

pp: case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
·

Goal state after:
case h.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [c₁, X.right, c₂]
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: case h.left.hr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ Zag c₁ X.right

pp: case h.left.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [X.right, c₂]

Tactic:
·

Goal state after:
case h.left.hr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ Zag c₁ X.right
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: case h.left.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [X.right, c₂]

Tactic:
·

Goal state after:
case h.left.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [X.right, c₂]
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
·

Goal state after:
case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂