mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₃ Y n), X₂ := AddCommGrpCat.of (Ext S.X₂ Y n), X₃ := AddCommGrpCat.of (Ext S.X₁ Y n),
      f := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      zero := ⋯ }.Exact

Tactic:
by
  let := HasDerivedCategory.standard C
  have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₂ _
    (op_distinguished _ hS.singleTriangle_distinguished) n
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)
  all_goals ext; apply singleFunctor_map_comp_hom (C := C)

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

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.toQuotient (relations.relation r) = 0

Tactic:
by
  dsimp only [toQuotient, Quotient]
  rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
  exact Submodule.subset_span (by simp)

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
⊢ solution.IsPresentation ↔ Function.Surjective ⇑solution.π ∧ Function.Injective ⇑solution.fromQuotient

Tactic:
← surjective_fromQuotient_iff_surjective_π,

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
⊢ solution.IsPresentation ↔ Function.Surjective ⇑solution.fromQuotient ∧ Function.Injective ⇑solution.fromQuotient
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
e : Basis ι R M
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ (toMatrix (Pi.basisFun R ι) b) (toLin' A) i j = of (fun i j ↦ (b.repr (A.col j)) i) i j

Tactic:
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k d : ℕ
ζ : Mˣ
h : ζ ∈ rootsOfUnity k M
⊢ ζ ∈ rootsOfUnity (k * d) M

Tactic:
simp_all only [mem_rootsOfUnity, pow_mul, one_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1

Tactic:
rw [← Matrix.map_mul]
  simp only [isUnits_det_units, mul_nonsing_inv, map_zero, map_one, Matrix.map_one]

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

Goal state before:
pp: case mpr
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
⊢ ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
let := Classical.decEq K

Goal state after:
case mpr
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
⊢ ∃ v, v ≠ 0 ∧ M *ᵥ v = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F) ↔ b = 0

Tactic:
by
  refine ⟨fun h ↦ ?_, fun hb ↦ ?_⟩
  · obtain ⟨r, _, hr⟩ := mem_center_iff.1 h
    simpa [transvection_coe, hij] using congr($hr i j).symm
  · simp only [hb, mem_center_iff, scalar_apply, transvection_coe, single_zero,
      add_zero, diagonal_eq_one]
    exact ⟨1, one_pow _, rfl⟩

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 : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ (lift Q).symm f = (lift Q).symm g

Tactic:
rw [lift_symm_apply, lift_symm_apply]

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 : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ ⟨f.toLinearMap ∘ₗ ι Q, ⋯⟩ = ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * (ι Q) a * (ι Q) b = -(x * (ι Q) b * (ι Q) a)

Tactic:
rw [mul_assoc, ι_mul_ι_comm_of_isOrtho h, mul_neg, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ [].dProd fι fA = (map fA []).prod

Tactic:
rw [List.dProd_nil, List.map_nil, List.prod_nil]
    rfl

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

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ •> w x✝¹ •> M x✝³ x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm (w _), ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A i) a ^ (n + 1) = (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
pow_succ,

Goal state after:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A i) a ^ n * (of A i) a = (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
y : Decomposition ℳ
decompose'✝ : M → ⨁ (i : ι), ↥(ℳ i)
left_inv✝ : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
⊢ { decompose' := decompose'✝, left_inv := left_inv✝, right_inv := xr } = y

Tactic:
obtain ⟨_, yl, _⟩ := y

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
decompose'✝¹ : M → ⨁ (i : ι), ↥(ℳ i)
left_inv✝ : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
decompose'✝ : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
right_inv✝ : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
⊢ { decompose' := decompose'✝¹, left_inv := left_inv✝, right_inv := xr } =
    { decompose' := decompose'✝, left_inv := yl, right_inv := right_inv✝ }
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ (of A 0) (a ^ (n + 1)) = (of A 0) a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ (of A 0) (a ^ n * a) = (of A 0) a ^ (n + 1)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ (of A 0) (a ^ n * a) = (of A 0) a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ (of A 0) (a ^ n * a) = (of A 0) a ^ n * (of A 0) a
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (f 0) 0 = (f 0) v

Tactic:
Subsingleton.elim 0 v

Goal state after:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin 0 → M
⊢ (f 0) v = (f 0) v
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e.comp (Ext.mk₀ 0) ⋯ = 0

Tactic:
Ext.mk₀_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext Y X i
⊢ e.comp 0 ⋯ = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case succ
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)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
e : Ext Y X d
hd✝ : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
⊢ e = 0

Tactic:
obtain ⟨x, rfl⟩ := Ext.contravariant_sequence_exact₃ h X e
      (by subst hd; apply Ext.eq_zero_of_projective) ((add_comm _ _).trans hd)

Goal state after:
case succ
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)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d), d = n + k → e = 0
d : ℕ
Y : C
hd✝ : d = n + (k + 1)
p : ProjectivePresentation Y
h : { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.ShortExact
hd : n + k + 1 = d
x : Ext { X₁ := kernel p.f, X₂ := p.p, X₃ := Y, f := kernel.ι p.f, g := p.f, zero := ⋯ }.X₁ X (n + k)
⊢ h.extClass.comp x ⋯ = 0
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:
rw [ExteriorAlgebra.ιMulti_apply]

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
⊢ (List.ofFn fun i ↦ (ExteriorAlgebra.ι R) ((⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) i)).prod =
    (List.ofFn fun i ↦ ↑(f i)).prod
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M [⋀^Fin n]→ₗ[R] N
⊢ (alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n) = f

Tactic:
by
  obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f
  dsimp [alternatingMapLinearEquiv]
  simp only [LinearEquiv.symm_apply_apply]
  rfl

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
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:
· rw [Submodule.span_le, Set.range_subset_iff]
    intro
    rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]
    exact Submodule.coe_mem _

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.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₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
by
      revert hx
      refine induction_on (fun m s hx ↦ ?_) x
      rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]

Goal state after:
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'
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y = (α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)

Tactic:
α.naturality,

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'
X Y : C
f : X ⟶ Y
⊢ α.app X ≫ G.map f ⊗ₘ F'.map f ≫ β.app Y = (α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
let s₁ : C ≌ AsSmall.{max u₁ v₁ u₂ v₂} C := AsSmall.equiv

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
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 C
X : C × C
⊢ ∀ (Y : C), IsCofiltered (CostructuredArrow (Over.forget X.1) Y)

Tactic:
← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
X : C × C
⊢ (Over.forget X.1).Initial
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
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
have n := s.ι.naturality fj

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
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : D.coconePoints.map fj ≫ s.ι.app (j', k').1 = s.ι.app (j, k).1 ≫ ((const J).obj s.pt).map fj
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
⊢ (Presieve.ofArrows (fun p ↦ Y (incl p.fst) (fibincl p.fst p.snd)) fun p ↦
      g (incl p.fst) (fibincl p.fst p.snd) ≫ f (incl p.fst)) ∈
    J.coverings S

Tactic:
· refine IsStableUnderComposition.comp_mem_coverings (f := fun i ↦ f (incl i))
        (g := fun i j ↦ g (incl i) (fibincl i j)) ?_ fun i ↦ ?_
    · convert! hf
      refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_
      exact .mk' (Sum.inl ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)
    · convert! hg (incl i)
      refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_
      match i with
      | .inl i => exact .mk' ⟨⟨_, _⟩, hu⟩ (by cat_disch) (by cat_disch)
      | .inr i => exact .mk' (.inr ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
⊢ x.PullbackCompatible → x.Compatible

Tactic:
intro t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
    have := HasPairwisePullbacks.has_pullbacks hf₁ hf₂
    rw [← pullback.lift_fst _ _ comm, op_comp, Functor.map_comp, comp_apply,
      t hf₁ hf₂, ← comp_apply, ← Functor.map_comp, ← op_comp, pullback.lift_snd]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : D
T : Presieve X
x : FamilyOfElements (F.op ⋙ P) T
Y : C
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F T f
⊢ P.obj (op Y)

Tactic:
obtain ⟨Z, g, h, h₁, _⟩ := getFunctorPushforwardStructure h
  exact P.map h.op (x g h₁)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ FamilyOfElements.pullback f x (f₂ ≫ f₁) ⋯ = (ConcreteCategory.hom (P.map f₂.op)) (FamilyOfElements.pullback f x f₁ hf)

Tactic:
unfold FamilyOfElements.pullback

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
W Z : C
f₁ : W ⟶ Y
f₂ : Z ⟶ W
hf : (Sieve.pullback f S).arrows f₁
⊢ x ((f₂ ≫ f₁) ≫ f) ⋯ = (ConcreteCategory.hom (P.map f₂.op)) (x (f₁ ≫ f) hf)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f ↔ (↑(shrinkFunctorHomEquiv f)).IsAmalgamation (shrinkYonedaEquiv g)

Tactic:
dsimp [Presieve.FamilyOfElements.IsAmalgamation]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f ↔
    ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
      (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
        (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩