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

Goal state before:
pp: case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
·

Goal state after:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case inr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
this :
  ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ)
    (f : Fin n → M) (x y : Fin n), f x = f y → x ≠ y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
h : ¬x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

pp: R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
·

Goal state after:
case inr
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
this :
  ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℕ)
    (f : Fin n → M) (x y : Fin n), f x = f y → x ≠ y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
h : ¬x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_1
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'
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

pp: case refine_2
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'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N), (?refine_1 m) ((?refine_1 m) x) = 0 m • x

Tactic:
·

Goal state after:
case refine_1
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'
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

pp: case neg
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
·

Goal state after:
case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_2
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'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    ((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m)
        (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) x) =
      0 m • x

Tactic:
·

Goal state after:
case refine_2
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'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    ((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m)
        (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) x) =
      0 m • x
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case neg
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
·

Goal state after:
case neg
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case h
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) (Fin.castAdd n j) =
    Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) (Fin.natAdd m k)

pp: case hij
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.castAdd n j ≠ Fin.natAdd m k

Tactic:
·

Goal state after:
case h
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) (Fin.castAdd n j) =
    Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) (Fin.natAdd m k)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case hij
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.castAdd n j ≠ Fin.natAdd m k

Tactic:
·

Goal state after:
case hij
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.castAdd n j ≠ Fin.natAdd m k
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case pos
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
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

pp: case neg
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
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

Tactic:
·

Goal state after:
case pos
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
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case neg
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
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))

Tactic:
·

Goal state after:
case neg
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
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) i =
    v
      ↑(e
          (e.symm
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
              (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (finSumFinEquiv.symm i)))))
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:
ext v
  rw [LinearMap.comp_apply]
  induction v using CliffordAlgebra.left_induction generalizing f with
  | algebraMap =>
    rw [liftAlternating_algebraMap, liftAlternating_algebraMap, map_smul,
      LinearMap.compAlternatingMap_apply]
  | add _ _ hx hy => rw [map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx =>
    rw [liftAlternating_ι_mul, liftAlternating_ι_mul, ← hx]
    simp_rw [AlternatingMap.curryLeft_compAlternatingMap]

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
⊢ (Hom.hom S.f).ker = ⊥

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 v

Tactic:
·

Goal state after:
ι : 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
⊢ (Hom.hom S.f).ker = ⊥
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Mono F'.m

pp: case a
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'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((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:
·

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Mono F'.m
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ Mono F'.m

pp: case a
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'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((RingHom.id R) c •
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))

Tactic:
·

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ Mono F'.m
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
this✝ : Subsingleton (Ext Y X i)
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext Y X i)

Tactic:
exact Ext.chgUniv.{max u v, w}.symm.subsingleton

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 lia

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 ≤ n + k

Tactic:
by lia

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 lia

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:
·

Goal state after:
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
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
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:
·

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: 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:
·

Goal state after:
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
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
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:
·

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 lia

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 lia

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
⊢ x₁ = 0

Tactic:
obtain ⟨x₂, rfl⟩ := Ext.covariant_sequence_exact₃ _ hS x₁ (add_comm _ _)
    (Ext.eq_zero_of_hasInjectiveDimensionLT _ (n + 1) (by lia))

Goal state after:
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
⊢ x₂.comp (Ext.mk₀ S.g) ⋯ = 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 ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ n ≤ i

Tactic:
by lia

Goal state after:
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
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}) ≤ ⋀[R]^n M

pp: case a
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 = ⊤
⊢ ⋀[R]^n M ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})

Tactic:
·

Goal state after:
case a
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
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
s : Set M
hs : span R s = ⊤
⊢ ⋀[R]^n M ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})

Tactic:
·

Goal state after:
case a
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 = ⊤
⊢ ⋀[R]^n M ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})