mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∃ j, c.Rel i j
⊢ IsZero (S.X₃.homology i)

pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)

Tactic:
· obtain ⟨j, hij⟩ := hi
    have := h₂ j hij
    apply (hS.homology_exact₃ i j hij).isZero_X₂
    · simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
        ← HomologicalComplex.homologyMap_comp]
    · simp [← cancel_mono (HomologicalComplex.homologyMap S.f j)]

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_inv_app._auto_1
⊢ m + n = 0

Tactic:
by omega

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ y.app X ≫ x.app X = x.app X ≫ y.app X

Tactic:
exact x.naturality (y.app X)

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: case mp
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
⊢ (∀ (n : V), (∃ a, a • x = n) → (B n) y = 0) → (B x) y = 0

Tactic:
exact fun h ↦ h x ⟨1, one_smul _ _⟩

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp ↑(h.uniq h') = solution'

Tactic:
simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp ↑(h.uniq h') = solution'

Tactic:
by
  simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp ↑(h.uniq h').symm = solution

Tactic:
simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp ↑(h.uniq h').symm = solution

Tactic:
by
  simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h') (solution.var g) = solution'.var g

Tactic:
simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h') (solution.var g) = solution'.var g

Tactic:
by
  simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h').symm (solution'.var g) = solution.var g

Tactic:
simp [uniq]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h').symm (solution'.var g) = solution.var g

Tactic:
by
  simp [uniq]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ ∑ x, b x * (algebraMap R S) (b.toMatrix v x i) = v i

Tactic:
← Algebra.commutes,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ ∑ x, (algebraMap R S) (b.toMatrix v x i) * b x = v i
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: M✝ : Type u_1
inst✝⁶ : MonoidWithZero M✝
inst✝⁵ : Finite M✝
M : Type u_2
inst✝⁴ : MonoidWithZero M
inst✝³ : IsLeftCancelMulZero M
inst✝² : DecidableEq M
inst✝¹ : Fintype M
inst✝ : Nontrivial M
a : M
ha : a ≠ 0
⊢ (a * if h : a = 0 then 0 else bijInv ⋯ 1) = 1

Tactic:
simp only [dif_neg ha]
      exact Fintype.rightInverse_bijInv _ _

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

Goal state before:
pp: case mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
hx : x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
hy : y ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
⊢ x * y ∈ Algebra.adjoin R (Set.range ⇑(ι Q))

Tactic:
exact mul_mem hx hy

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ QuadraticMap.polar (⇑Q) a b • (ι Q) a - (ι Q) b * (algebraMap R (CliffordAlgebra Q)) (Q a) =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
← Algebra.commutes,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ QuadraticMap.polar (⇑Q) a b • (ι Q) a - (algebraMap R (CliffordAlgebra Q)) (Q a) * (ι Q) b =
    (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b c d : R
⊢ a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
      associator a b c * d =
    0

Tactic:
simp only [associator, mul_sub, sub_mul]
  abel1

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ ↑S * ↑S = -1

Tactic:
simp only [S, Int.reduceNeg, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd,
    vecMul_cons, head_cons, zero_smul, tail_cons, neg_smul, one_smul, neg_cons, neg_zero, neg_empty,
    empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply]

Goal state after:
⊢ !![-1, 0; 0, -1] = -1
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂' R

Tactic:
ext M
  simp only [coe_comp, coe_single, Function.comp_apply, toLinearMap₂_apply, Pi.basisFun_repr,
    toLinearMap₂'_apply]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Monoid S
inst✝⁴ : Monoid T
inst✝³ : DistribMulAction S N
inst✝² : DistribMulAction T N
inst✝¹ : SMulCommClass S R N
inst✝ : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
⊢ (a • ⇑Q) (b • x) = (b * b) • (a • ⇑Q) x

Tactic:
by
        rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_comm]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ (-⇑Q) (x + y) = (-⇑Q) x + (-⇑Q) y + ((-B) x) y

Tactic:
by simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
a : R
x : M
⊢ (⇑f * ⇑g) (a • x) = (a * a) • (⇑f * ⇑g) x

Tactic:
rw [Pi.mul_apply, Pi.mul_apply, map_smulₛₗ, RingHom.id_apply, map_smulₛₗ, RingHom.id_apply,
      smul_mul_assoc, mul_smul_comm, ← smul_assoc, smul_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b

Tactic:
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]

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

Goal state before:
pp: case succ.inl
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
hd : finrank K V = d + 1
hB₂ : IsSymm 0
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

pp: case succ.inr
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
hd : finrank K V = d + 1
hB₁ : B ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
· let b := Module.finBasis K V
    rw [hd] at b
    exact ⟨b, fun i j _ => rfl⟩

Goal state after:
case succ.inr
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
hd : finrank K V = d + 1
hB₁ : B ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

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
i' : ZMod 2
x' x y : CliffordAlgebra Q
hx : x ∈ ⨆ i, (ι Q).range ^ ↑i
hy : y ∈ ⨆ i, (ι Q).range ^ ↑i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, hx⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨y, hy⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (x + y) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x + y, ⋯⟩

Tactic:
rw [map_add, ihx, ihy, ← map_add]; rfl

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 : ℕ
⊢ (ι R).range ^ n ≤ Submodule.span R (Set.range ⇑(ιMulti R n))

Tactic:
Submodule.pow_eq_span_pow_set,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Submodule.span R (↑(ι R).range ^ n) ≤ Submodule.span R (Set.range ⇑(ιMulti R 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 : ℕ
⊢ injectiveDimension X ≤ ↑n ↔ HasInjectiveDimensionLE X n

Tactic:
simp [← injectiveDimension_lt_iff, ← ENat.WithBot.lt_add_one_iff]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (⇑(⋀[R]^n M).subtype '' ⇑(ιMulti R n) '' univ) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
Set.image_image

Goal state after:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R ((fun x ↦ (⋀[R]^n M).subtype ((ιMulti R n) x)) '' univ) = Submodule.map (⋀[R]^n M).subtype ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Free

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

Tactic:
apply finrank_eq_of_rank_eq
  rw [free_shortExact_rank_add hS', ← hN, ← hP]
  simp only [Nat.cast_add, finrank_eq_rank]

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 : mk (h m) s = 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
← zero_mk 1,

Goal state after:
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 : mk (h m) s = mk 0 1
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
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 (⇑(⋀[R]^n M).subtype '' ιMulti_family R n v '' univ) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
Set.image_image

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 ((fun x ↦ (⋀[R]^n M).subtype (ιMulti_family R n v x)) '' univ) = Submodule.map (⋀[R]^n M).subtype ⊤
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:
← IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp S f₁.hom f₂.hom

Goal state after:
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 ⇑↑(IsLocalizedModule.linearEquiv S (Hom.hom f₁) (Hom.hom f₂ ∘ₗ Hom.hom f₁))
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
⊢ Λ.chainComplexMap (f ≫ g) = Λ.chainComplexMap f ≫ Λ.chainComplexMap g

Tactic:
ext n
  induction n with
  | zero => simp
  | succ n hn =>
    obtain _ | n := n
    all_goals
      dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

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
⊢ Λ.chainComplexMap (f ≫ g) = Λ.chainComplexMap f ≫ Λ.chainComplexMap g

Tactic:
by
  ext n
  induction n with
  | zero => simp
  | succ n hn =>
    obtain _ | n := n
    all_goals
      dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
⊢ ∃ Z x x, True

Tactic:
by
    obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))
    exact ⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f),
      F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : FinallySmall C
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final

Tactic:
have (C₀ : Type u) [Category.{w} C₀] [IsFiltered C₀] [FinallySmall.{w} C₀] :
      ∃ (D : Type u) (_ : Small.{w} D) (_ : Category.{w} D) (_ : IsFiltered D) (F : D ⥤ C₀),
        F.Final := by
    /- For `D`, we can choose the full subcategory of `C₀` which is the strict image
    of the final functor `fromFinalModel.{w} C₀ : FinalModel.{w} C₀ ⥤ C₀`,
    where `FinalModel.{w} C₀` is a `w`-small category. -/
    let P : ObjectProperty C₀ := ObjectProperty.strictMap ⊤ (fromFinalModel.{w} C₀)
    have hP (X : C₀) : ∃ (Y : C₀) (hY : P Y), Nonempty (X ⟶ Y) := by
      let f : StructuredArrow X (fromFinalModel.{w} C₀) := Classical.arbitrary _
      exact ⟨_, ObjectProperty.strictMap_obj _ _ (X := f.right) (by tauto), ⟨f.hom⟩⟩
    have : IsFiltered P.FullSubcategory :=
      { nonempty := by
          obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
          exact ⟨X, hX⟩
        cocone_objs := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩
          obtain ⟨Z, hZ, ⟨f⟩⟩ := hP (max X Y)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (leftToMax X Y ≫ f),
            ObjectProperty.homMk (rightToMax X Y ≫ f), by tauto⟩
        cocone_maps := by
          rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩ }
    let G : FinalModel.{w} C₀ ⥤ P.FullSubcategory :=
      { obj X := ⟨(fromFinalModel.{w} C₀).obj X, by tauto⟩
        map f := ObjectProperty.homMk ((fromFinalModel.{w} C₀).map f) }
    have : (G ⋙ P.ι).Final := inferInstanceAs (fromFinalModel.{w} C₀).Final
    exact ⟨P.FullSubcategory, small_of_surjective (f := G.obj)
      (by rintro ⟨_, Y, _, rfl⟩; exact ⟨Y, rfl⟩), inferInstance, inferInstance, P.ι,
      Functor.final_of_comp_full_faithful' G P.ι ⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : FinallySmall C
this :
  ∀ (C₀ : Type u) [inst : Category.{w, u} C₀] [IsFiltered C₀] [FinallySmall C₀],
    ∃ D, ∃ (_ : Small.{w, u} D), ∃ x, ∃ (_ : IsFiltered D), ∃ F, F.Final
⊢ ∃ D x, ∃ (_ : IsFiltered D), ∃ F, F.Final
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁

Tactic:
rw [Functor.initial_iff_of_isCofiltered]
  constructor
  · rintro ⟨h, _⟩ j₂
    obtain ⟨j₁, ⟨φ⟩⟩ := h j₂
    exact ⟨j₁,leOfHom φ⟩
  · intro h
    constructor
    · intro j₂
      obtain ⟨j₁, h₁⟩ := h j₂
      exact ⟨j₁, ⟨homOfLE h₁⟩⟩
    · intro _ c _ _
      exact ⟨ c, 𝟙 _, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
⊢ (fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab))
      ((fun φ ↦ freeObjDesc φ) φ) =
    φ

Tactic:
by ext; simp [toPresheaf]

Goal state after: