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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ (singleObjXSelf (ComplexShape.up ℤ) i I).inv =
    𝟙 (((singleFunctor C i).obj I).X i)

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ 𝟙 (((singleFunctor C i).obj I).X i) = 𝟙 (((singleFunctor C i).obj I).X i)
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ y, ∑ x, (w x • A x y) • v y = 0
⊢ w = 0

Tactic:
simp_rw [← Finset.sum_smul] at hw

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
⊢ w = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
⊢ ∀ i ∈ s, ∃ d, f i = d ^ n

Tactic:
classical
    intro i hi
    rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
    refine
      exists_eq_pow_of_mul_eq_pow_of_coprime
        (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
    rw [hij] at hj
    exact (s.notMem_erase _) hj

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
i✝ j✝ : ι
⊢ (b.map f).toMatrix v i✝ j✝ = b.toMatrix (⇑f.symm ∘ v) i✝ j✝

Tactic:
simp only [toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
M N : Matrix n n A
h : N.Nondegenerate
⊢ (M * N).Nondegenerate ↔ M.Nondegenerate

Tactic:
simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_right h

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ (toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) i j = f i j

Tactic:
simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_single]

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
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = v x✝¹ * ∑ x, M x✝¹ x * w x

Tactic:
rw [Finset.mul_sum]

Goal state after:
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
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = ∑ i, v x✝¹ * (M x✝¹ i * w i)
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
M : Matrix n m N₂
i✝¹ : n
i✝ : m
⊢ (((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M ∘ₗ LinearMap.single R (fun i ↦ R) i✝¹) 1 ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1 =
    (((toLinearMap₂' R) M ∘ₗ LinearMap.single R (fun i ↦ R) i✝¹) 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1

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

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
i j : ι
r : R
x : A i
y : A j
⊢ { toFun := fun b ↦ GradedMonoid.GMul.mul (r • x) b, map_add' := ⋯, map_smul' := ⋯ } y =
    ((RingHom.id R) r • { toFun := fun b ↦ GradedMonoid.GMul.mul x b, map_add' := ⋯, map_smul' := ⋯ }) y

Tactic:
injection smul_assoc r (GradedMonoid.mk _ x) (GradedMonoid.mk _ y)

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

Goal state before:
pp: case e'_1.e'_3
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * P * A₂ = ↑v * y

Tactic:
rw [mul_assoc, mul_assoc, ← mul_assoc J]

Goal state after:
case e'_1.e'_3
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * (J * P * A₂) = ↑v * y
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r fun i₁ x₁ ↦ if i₁ + i = n then ↑x₁ * ↑r' else 0) = 0

Tactic:
rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_left i x).trans_eq H)

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

Goal state before:
pp: 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'
⊢ ∀ (c : K), ∀ x_1 ∈ Submodule.orthogonalBilin B (K ∙ x), c • x + x_1 = 0 → c = 0

Tactic:
rintro c y hy hc
        rw [add_eq_zero_iff_neg_eq] at hc
        rw [← hc, Submodule.neg_mem_iff] at hy
        have := (isCompl_span_singleton_orthogonal hx).disjoint
        rw [Submodule.disjoint_def] at this
        have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
        exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _

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

Goal state before:
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
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' ⋯ ⋯
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
refine ⟨b, ?_⟩

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
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' ⋯ ⋯
⊢ IsOrthoᵢ B ⇑b
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
⊢ motive x hx

Tactic:
apply Submodule.iSup_induction' (motive := motive) _ _ (range_ι_pow 0 (Submodule.zero_mem _)) add

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
⊢ ∀ (i : { n_1 // ↑n_1 = n }) (x : CliffordAlgebra Q) (hx : x ∈ (ι Q).range ^ ↑i), motive x ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.add
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive ((x + y) * b) ⋯

Tactic:
| add x y n hx hy ihx ihy =>

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
Set.nontrivial_coe_sort,

Goal state after:
case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ (powersetCard α n).Nontrivial
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 : M
⊢ ιInv ((ι R) x) = x

Tactic:
by
  simp [ιInv]

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
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ (f ∘ₗ ιInv) x = y

Tactic:
← ιInv_comp_map,

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
h : Function.Surjective ⇑(map f)
y : N
x : ExteriorAlgebra R M
hx : (map f) x = (ι R) y
⊢ (ιInv ∘ₗ (map f).toLinearMap) x = y
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✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (Prod.mkHom f₁ (𝟙 x.2)) ≫
      G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ colimMap ((curry.obj G).map f₁) ≫ colimit.ι (curry.obj G ⋙ colim) y.1

Tactic:
simp [ι_colimMap_assoc, curry_obj_map_app, reassoc_of% this]

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₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
x✝¹ : Cᵒᵖ
x✝ : F₁.obj x✝¹
⊢ (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)).app
            x✝¹)).toFun
      x✝

Tactic:
simp [freeHomEquiv, toPresheaf]

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)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit G ≅ limit (uncurry.obj (curry.obj G))

Tactic:
apply HasLimit.isoOfNatIso i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ { l // l ≫ (Fork.ofι f w).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = l }

Tactic:
by
    refine ⟨↾fun i => ?_, ?_, ?_⟩
    · apply Classical.choose (t (s.ι i) _)
      apply congr_hom s.condition i
    · ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).1
    · intro m hm
      ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).2 _ (congr_hom hm i)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Exists.choose ⋯ = s.ι.app j

Tactic:
intro s f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f
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
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : D
g : Z ⟶ F.obj X
hg : map F (ofArrows Y f) g
⊢ ofArrows (fun i ↦ F.obj (Y i)) (fun i ↦ F.map (f i)) g

Tactic:
obtain ⟨hu⟩ := hg

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
ι : Type u_1
Y✝¹ : ι → C
f : (i : ι) → Y✝¹ i ⟶ X
Y : D
Y✝ : C
u✝ : Y✝ ⟶ X
hu : ofArrows Y✝¹ f u✝
⊢ ofArrows (fun i ↦ F.obj (Y✝¹ i)) (fun i ↦ F.map (f i)) (F.map u✝)
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
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map (pullback.lift g₁ g₂ comm).op))
      ((ConcreteCategory.hom (P.map (pullback.fst f₁ f₂).op)) (x f₁ hf₁)) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
t hf₁ hf₂,

Goal state after:
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
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map (pullback.lift g₁ g₂ comm).op))
      ((ConcreteCategory.hom (P.map (pullback.snd f₁ f₂).op)) (x f₂ hf₂)) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ (pullback e.hom (ofArrows Z f)).arrows (a ≫ f i ≫ e.inv)

Tactic:
exact ⟨_, a, _, ⟨i⟩, by simp⟩

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 Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
⊢ f = g

Tactic:
by
    ext Y y
    simpa [Subtype.ext_iff] using congr_hom (NatTrans.congr_app h Y) y

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
let e : S ⟶ ⊤ := homOfLE (OrderTop.le_top _)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P X) (op ⊤))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ {x | ∃ y, (ConcreteCategory.hom (p.app i)) y = x}
⊢ ∃ y, (ConcreteCategory.hom ((toRange p).app i)) y = ⟨x, hx⟩

Tactic:
obtain ⟨y, rfl⟩ := hx

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
i : C
y : F'.obj i
⊢ ∃ y_1, (ConcreteCategory.hom ((toRange p).app i)) y_1 = ⟨(ConcreteCategory.hom (p.app i)) y, ⋯⟩
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
⊢ ∀ {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y),
    (J.diagram P X ⋙ F).map f ≫
        ((isLimitOfPreserves F (limit.isLimit ((unop Y).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop Y).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop Y)).symm).hom =
      ((isLimitOfPreserves F (limit.isLimit ((unop X_1).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop X_1).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop X_1)).symm).hom ≫
        (J.diagram (P ⋙ F) X).map f

Tactic:
intro A B f
      dsimp
      ext g
      simp [← F.map_comp]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImage f ≫ imageι f).hom = f.hom

Tactic:
simp [Subfunctor.toRangeSheafify]

Goal state after: