mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s.toList, ∀ k < ?m.59, x k = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s, ∀ k < ?m.59, x k = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x : CliffordAlgebra Q
⊢ P 0

Tactic:
simpa using

Goal state after:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x : CliffordAlgebra Q
⊢ P 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
r : R
⊢ P (reverse ((Algebra.algebraMap R (CliffordAlgebra Q)) r))

Tactic:
simpa using

Goal state after:
case algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
r : R
⊢ P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
x✝ y✝ : CliffordAlgebra Q
hx : P (reverse x✝)
hy : P (reverse y✝)
⊢ P (reverse (x✝ + y✝))

Tactic:
simpa using

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
x✝ y✝ : CliffordAlgebra Q
hx : P (reverse x✝)
hy : P (reverse y✝)
⊢ P (reverse x✝ + reverse y✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case mul_ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
m✝ : M
x✝ : CliffordAlgebra Q
hx : P (reverse x✝)
⊢ P (reverse (x✝ * (ι Q) m✝))

Tactic:
simpa using

Goal state after:
case mul_ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
m✝ : M
x✝ : CliffordAlgebra Q
hx : P (reverse x✝)
⊢ P ((ι Q) m✝ * reverse x✝)
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (init (update m i (x + y)))) (update m i (x + y) (last n)) =
    (f (init (update m i x))) (update m i x (last n)) + (f (init (update m i y))) (update m i y (last n))

Tactic:
cases i using Fin.lastCases

Goal state after:
case last
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
x y : M (last n)
⊢ (f (init (update m (last n) (x + y)))) (update m (last n) (x + y) (last n)) =
    (f (init (update m (last n) x))) (update m (last n) x (last n)) +
      (f (init (update m (last n) y))) (update m (last n) y (last n))

case cast
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (x + y)))) (update m i✝.castSucc (x + y) (last n)) =
    (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n)) +
      (f (init (update m i✝.castSucc y))) (update m i✝.castSucc y (last n))
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
i : Fin n.succ
c : R
x : M i
⊢ (f (init (update m i (c • x)))) (update m i (c • x) (last n)) = c • (f (init (update m i x))) (update m i x (last n))

Tactic:
cases i using Fin.lastCases

Goal state after:
case last
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
x : M (last n)
⊢ (f (init (update m (last n) (c • x)))) (update m (last n) (c • x) (last n)) =
    c • (f (init (update m (last n) x))) (update m (last n) x (last n))

case cast
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.castSucc
⊢ (f (init (update m i✝.castSucc (c • x)))) (update m i✝.castSucc (c • x) (last n)) =
    c • (f (init (update m i✝.castSucc x))) (update m i✝.castSucc x (last n))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
this : Finset.univ = {0, 1}
⊢ Set.univ = {0, 1}

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
this : Finset.univ = {0, 1}
⊢ Set.univ = {0, 1}
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr.refine_2.refine_1
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i✝ : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
⊢ (B x) ↑(v' i) = 0

Tactic:
exact (v' i).prop _ (Submodule.mem_span_singleton_self x)

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ a ∈ ⟨this.toFinset, ⋯⟩

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ a ∈ s
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ b ∉ ⟨this.toFinset, ⋯⟩

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ b ∉ s
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
this : Fintype α
⊢ Finite ↑(powersetCard α n)

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Finite α
this : Fintype α
⊢ Finite { x // #x = n }
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ a ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

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

Tactic:
simp [algebraMapInv]

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

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

Tactic:
simpa using

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : LeftInverse ⇑(map g) ⇑(map f)
x : M
⊢ g (f x) = x
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
this : HasExt C := ⋯
⊢ Ext.homEquiv₀.symm (𝟙 X) = Ext.homEquiv₀.symm 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasInjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ Ext.mk₀ (𝟙 X) = 0
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:
simpa using

Goal state after:
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.mk₀ (g ≫ φ) = Ext.mk₀ f
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n < i
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 = ⊤
⊢ Submodule.map (⋀[R]^n M).subtype (span R (⇑(ιMulti R n) '' {a | range a ⊆ s})) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
simpa using

Goal state after:
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 ((fun x ↦ (ExteriorAlgebra.ιMulti R n) x) '' {a | range a ⊆ s}) = ⋀[R]^n M
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:
simpa using

Goal state after:
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
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:
simpa using

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
⊢ f v = 0
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case bot
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:
simpa using

Goal state after:
case bot
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
⊢ Subsingleton ↑M ↔ Subsingleton ↑N
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case coe.coe
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 : ℕ
⊢ injectiveDimension M ≤ ↑↑n ↔ injectiveDimension N ≤ ↑↑n

Tactic:
| coe n =>

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

Goal state before:
pp: case coe
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 : ℕ∞
⊢ injectiveDimension M ≤ ↑n ↔ injectiveDimension N ≤ ↑n

Tactic:
| coe n =>

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 ((fun x ↦ (⋀[R]^n M).subtype (ιMulti_family R n v x)) '' univ) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
simpa using

Goal state after:
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 fun x ↦ ExteriorAlgebra.ιMulti_family R n v x) = ⋀[R]^n M
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j j' : J
f : j ⟶ j'
X : Cᵒᵖ
⊢ (((Functor.const J).obj (limitPresheafOfModules F)).map f ≫
          { app := fun X ↦ limit.π (F ⋙ evaluation R X) j', naturality := ⋯ }).app
      X =
    ({ app := fun X ↦ limit.π (F ⋙ evaluation R X) j, naturality := ⋯ } ≫ F.map f).app X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j j' : J
f : j ⟶ j'
X : Cᵒᵖ
⊢ limit.π (F ⋙ evaluation R X) j' = limit.π (F ⋙ evaluation R X) j ≫ (F.map f).app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X✝ Y : J
f : X✝ ⟶ Y
X : Cᵒᵖ
⊢ (F.map f ≫ { app := fun X ↦ colimit.ι (F ⋙ evaluation R X) Y, naturality := ⋯ }).app X =
    ({ app := fun X ↦ colimit.ι (F ⋙ evaluation R X) X✝, naturality := ⋯ } ≫
          ((Functor.const J).obj (colimitPresheafOfModules F)).map f).app
      X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X✝ Y : J
f : X✝ ⟶ Y
X : Cᵒᵖ
⊢ (F.map f).app X ≫ colimit.ι (F ⋙ evaluation R X) Y = colimit.ι (F ⋙ evaluation R X) X✝
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ F.obj Y ◁ β.app Y = F.obj X ◁ β.app X ≫ (tensorObj F G').map f

Tactic:
simp only [← id_tensorHom]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ₘ β.app Y) = (𝟙 (F.obj X) ⊗ₘ β.app X) ≫ (tensorObj F G').map f
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
c : C
⊢ (e.functor.obj (e.inverse.obj c), e.functor.obj (e.inverse.obj c)) ≅ (c, c)

Tactic:
exact Iso.prod (e.counitIso.app c) (e.counitIso.app c)

Goal state after:
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:
simpa using

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)
⊢ Zag X.right c₂