mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map φ.hom₃.unop).op ≫
      ((shiftFunctor C 1).map T₂.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁ ≫ φ.hom₁

Tactic:
← opShiftFunctorEquivalence_unitIso_inv_naturality,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : Triangle Cᵒᵖ
φ : T₁ ⟶ T₂
⊢ ((shiftFunctor C 1).map φ.hom₃.unop).op ≫
      ((shiftFunctor C 1).map T₂.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁ =
    ((shiftFunctor C 1).map T₁.mor₃.unop).op ≫
      ((shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map φ.hom₁).unop).op ≫
        (opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ (Submodule.span A (Set.range relations.relation)).mkQ (relations.relation r) = 0

Tactic:
rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.relation r ∈ Submodule.span A (Set.range relations.relation)
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
e : M ≃ₗ[A] N
this : (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient
⊢ Function.Bijective (⇑e ∘ ⇑solution.fromQuotient)

Tactic:
exact Function.Bijective.comp e.bijective h.bijective

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.IsPresentationCore
N : Type w''
x✝¹ : AddCommGroup N
x✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
x : M
this : (solution.postcomp f).postcomp ↑ULift.moduleEquiv.symm = (solution.postcomp f').postcomp ↑ULift.moduleEquiv.symm
⊢ f x = f' x

Tactic:
simp only [← postcomp_comp] at this

Goal state after:
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.IsPresentationCore
N : Type w''
x✝¹ : AddCommGroup N
x✝ : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
x : M
this : solution.postcomp (↑ULift.moduleEquiv.symm ∘ₗ f) = solution.postcomp (↑ULift.moduleEquiv.symm ∘ₗ f')
⊢ f x = f' x
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) ↑(range (orderOf x))

Tactic:
simpa using pow_injOn_Iio_orderOf

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

Goal state before:
pp: case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (M.map ⇑(algebraMap A K) *ᵥ ⇑(algebraMap A K) ∘ fun i ↦ f (v i) ⋯) i =
    ((algebraMap A K).mapMatrix M *ᵥ (algebraMap A K) b • v) i

Tactic:
mulVec,

Goal state after:
case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((fun j ↦ M.map (⇑(algebraMap A K)) i j) ⬝ᵥ ⇑(algebraMap A K) ∘ fun i ↦ f (v i) ⋯) =
    (fun j ↦ (algebraMap A K).mapMatrix M i j) ⬝ᵥ (algebraMap A K) b • v
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₁ ((↑f.symm).toFun m) = Q₂ m

Tactic:
rw [← f.map_app]

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₂ (f ((↑f.symm).toFun m)) = Q₂ m
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 : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
h2 : IsUnit 2
f : M →ₗ[R] A
x : M
h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)
⊢ 2 * (f x * f x) = 2 * (algebraMap R A) (Q x)

Tactic:
rw [two_mul, two_mul, h x x, QuadraticMap.polar_self, two_smul, map_add]

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

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (diag2n hij c hc)

Tactic:
change P (diag2 c hc)

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ P (diag2 c hc)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
this : SMulWithZero (A 0) (⨁ (i : ι), A i) := SMulWithZero.compHom (⨁ (i : ι), A i) ↑(of A 0)
⊢ SMulWithZero (A 0) (A i)

Tactic:
exact Function.Injective.smulWithZero (of A i).toZeroHom DFinsupp.single_injective
    (of_zero_smul A)

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

Goal state before:
pp: M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
⊢ x = 0

Tactic:
have : Q x = 0 := le_antisymm h (hQ.nonneg x)

Goal state after:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
this : Q x = 0
⊢ x = 0
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

Tactic:
let b := Module.finBasis K V

Goal state after:
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
b : Basis (Fin (finrank K V)) K V := finBasis K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) w✝ * x) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

Tactic:
rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]

Goal state after:
case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) (1 + ↑i)) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩
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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
⊢ ∀ (val : ℕ) (property : ∃ k, val = 2 * k + n.val) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ val), motive x ⋯

Tactic:
rintro n' ⟨k, rfl⟩ xv

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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
⊢ Surjective (ofFinEmb n β)

Tactic:
intro ⟨s, hs⟩

Goal state after:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ ∃ a, ofFinEmb n β a = ⟨s, hs⟩
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 ↦ x) fun x ↦ y) = (f fun x_1 ↦ x) fun x ↦ y

Tactic:
curryFinFinset_symm_apply

Goal state after:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((f fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i ↦
      s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) =
    (f fun x_1 ↦ x) fun x ↦ y
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
⊢ Subsingleton (Ext Y X i)

Tactic:
by
    have : Subsingleton (Ext Y X i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
    let := HasExt.standard C
    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
⊢ injectiveDimension X < ↑⊥ ↔ injectiveDimension X < 0

Tactic:
bot_eq_zero',

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ injectiveDimension X < ↑0 ↔ injectiveDimension X < 0
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
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(finrank R ↑S.X₁ + finrank R ↑S.X₃)

Tactic:
simp only [Nat.cast_add, finrank_eq_rank]

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

Goal state before:
pp: case zero
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
⊢ Module.Injective R ↑M ↔ Module.Injective R' ↑N

Tactic:
exact ⟨fun _ ↦ Module.Injective.of_ringEquiv eR e,
      fun _ ↦ Module.Injective.of_ringEquiv eR.symm e.symm⟩

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

Goal state before:
pp: case e'_5
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
e_3✝ :
  (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).X₁ =
    ι.obj ((Λ.chainComplex X).X (n + 2))
e_4✝ :
  kernel (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).g =
    (𝟭 A).obj (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))
⊢ (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).f =
    (ι.map (Λ.chainComplexXIso X n).hom ≫ Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))) ≫
      kernel.ι (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).g

Tactic:
simp [map_chainComplex_d]

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

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

Tactic:
simp [map_chainComplex_d]

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✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
exact ⟨op c, ⟨f.op⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
Q' : (j : J) → IsLimit (Q.obj j) := fun j ↦ limit.isLimit ((curry.obj G).obj j)
c' : Cone G
f : c'.pt ⟶ (coneOfHasLimitCurryCompLim G).pt
h : ∀ (j : J × K), f ≫ (coneOfHasLimitCurryCompLim G).π.app j = c'.π.app j
⊢ f = limit.lift (curry.obj G ⋙ lim) (coneOfConeCurry G Q' c')

Tactic:
dsimp [coneOfHasLimitCurryCompLim] at f h ⊢

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
Q' : (j : J) → IsLimit (Q.obj j) := fun j ↦ limit.isLimit ((curry.obj G).obj j)
c' : Cone G
f : c'.pt ⟶ limit (curry.obj G ⋙ lim)
h : ∀ (j : J × K), f ≫ limit.π (curry.obj G ⋙ lim) j.1 ≫ limit.π ((curry.obj G).obj j.1) j.2 = c'.π.app j
⊢ f = limit.lift (curry.obj G ⋙ lim) (coneOfConeCurry G Q' c')
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
⊢ { obj := fun U ↦ F.obj U ⊔ G.obj U, map := ⋯ }.obj U ⊆ H.obj U

Tactic:
rintro x (h | h)
    · exact h₁ _ h
    · exact h₂ _ h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
i : X ⟶ Y
inst✝ : IsIso i
S : Sieve Y
⊢ Sieve.pullback i S ∈ J X ↔ S ∈ J Y

Tactic:
refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
  convert! J.pullback_stable (inv i) H
  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ∈ J.coverings X

Tactic:
refine J.comp_mem_coverings (Y := fun (i : ι) (j : κ (g i) ⟨i⟩) ↦ W _ _ j)
      (g := fun i j ↦ p _ _ j) _ hR fun i ↦ ?_

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
i : ι
⊢ (ofArrows (fun j ↦ W (g i) ⋯ j) fun j ↦ p (g i) ⋯ j) ∈ J.coverings (Z i)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝¹ : Y ⟶ X
S R✝ : Sieve X
f : Y ⟶ X
R : Sieve Y
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : ∃ g, g ≫ f = f✝ ∧ R.arrows g
h : Z✝ ⟶ Y✝
j : Y✝ ⟶ Y
k : j ≫ f = f✝
z : R.arrows j
⊢ (h ≫ j) ≫ f = h ≫ f✝

Tactic:
by simp [k]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve (F.obj X)
⊢ generate (Presieve.functorPullback F R) ≤ functorPullback F (generate R)

Tactic:
by
  rw [generate_le_iff]
  intro Z g hg
  exact le_generate _ _ _ hg

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ x₁.IsAmalgamation (e.symm t₂)

Tactic:
simpa only [this] using ht₂

Goal state after: