mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
⊢ ∃ L L' D,
    ∃ (hD : (diagonal D).det = 1),
      M =
        (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
          (List.map TransvectionStruct.toSpecialLinearGroup L').prod

Tactic:
obtain ⟨L, L', D, hM⟩ := Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M.1

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ∃ L L' D,
    ∃ (hD : (diagonal D).det = 1),
      M =
        (List.map TransvectionStruct.toSpecialLinearGroup L).prod * ⟨diagonal D, hD⟩ *
          (List.map TransvectionStruct.toSpecialLinearGroup L').prod
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
⊢ (ι Q) a * (ι Q) b * (ι Q) a = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ←
    Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub]

Goal state after:
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
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((mulHom A) a) a' =
    DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ((DFinsupp.sumAddHom fun x ↦ (toAddMonoid fun x_1 ↦ ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a) a' =
    DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (decompose ℳ) ((decompose ℳ).symm ((of (fun i ↦ ↥(ℳ i)) i) x)) = (of (fun i ↦ ↥(ℳ i)) i) x

Tactic:
Equiv.apply_symm_apply

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (of (fun i ↦ ↥(ℳ i)) i) x = (of (fun i ↦ ↥(ℳ i)) i) x
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : Semiring A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(((decompose 𝒜) ((decompose 𝒜).symm a)) i) = ↑(a i)

Tactic:
Equiv.apply_symm_apply

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : Semiring A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(a i) = ↑(a i)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(((decompose 𝒜) ((decompose 𝒜).symm a)) i) = ↑(a i)

Tactic:
Equiv.apply_symm_apply

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
a : ⨁ (i : ι), ↥(𝒜 i)
i : ι
⊢ ↑(a i) = ↑(a i)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: 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
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ (foldr' Q f hf n) ((ι Q) m * x) = (f m) (x, (foldr' Q f hf n) x)

Tactic:
by
  dsimp [foldr']
  rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]
  refine congr_arg (f m) (Prod.mk.eta.symm.trans ?_)
  congr 1
  induction x using CliffordAlgebra.left_induction with
  | algebraMap r => simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
  | add x y hx hy => rw [map_add, Prod.fst_add, hx, hy]
  | ι_mul m x hx => rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]

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

Goal state before:
pp: case inr.zero
α : Type u_1
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α 0) = (Nat.card α).choose 0

Tactic:
simp [powersetCard]

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
⊢ Disjoint (ι R).range 1

Tactic:
by
  rw [Submodule.disjoint_def]
  rintro _ ⟨x, hx⟩ h
  obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h
  rw [ι_eq_algebraMap_iff x] at hx
  rw [hx.2, map_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
this : ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
by
    refine LinearMap.compr₂ this ?_
    refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
    exact AlternatingMap.constLinearEquivOfIsEmpty.symm

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
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT X 0

Tactic:
rw [hasInjectiveDimensionLT_iff]

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 : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT X m

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT X 1

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT X n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT S.X₂ n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT S.X₁ (n + 1)

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₁ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
⊢ HasInjectiveDimensionLT S.X₃ n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0
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
s : Set M
hs : span R s = ⊤
⊢ span R (⇑(ExteriorAlgebra.ι R) '' s) ^ n ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})

Tactic:
span_pow,

Goal state after:
case a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
⊢ span R ((⇑(ExteriorAlgebra.ι R) '' s) ^ n) ≤ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s})
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:
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: R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Fin n → M
⊢ ↑(((alternatingMapLinearEquiv (ιMulti R n)).compAlternatingMap (ιMulti R n)) x✝) =
    ↑((LinearMap.id.compAlternatingMap (ιMulti R n)) x✝)

Tactic:
simp only [alternatingMapLinearEquiv_comp_ιMulti, ιMulti_apply_coe,
    LinearMap.compAlternatingMap_apply, LinearMap.id_coe, id_eq]

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
⊢ ι.map (Λ.chainComplexXOneIso X).hom ≫
      ι.map (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)) ≫
        ι.map (Λ.chainComplexXOneIso Y).inv ≫
          ι.map (Λ.chainComplexXOneIso Y).hom ≫
            Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Λ.chainComplexXZeroIso Y).inv =
    ι.map (Λ.chainComplexXOneIso X).hom ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          ι.map (Λ.chainComplexXZeroIso X).inv ≫
            ι.map (Λ.chainComplexXZeroIso X).hom ≫ ι.map (Λ.F.map f) ≫ ι.map (Λ.chainComplexXZeroIso Y).inv

Tactic:
simp only [← ι.map_comp, ← ι.map_comp_assoc]

Goal state after:
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
⊢ ι.map
        ((Λ.chainComplexXOneIso X).hom ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫
            (Λ.chainComplexXOneIso Y).inv ≫ (Λ.chainComplexXOneIso Y).hom) ≫
      Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Λ.chainComplexXZeroIso Y).inv =
    ι.map (Λ.chainComplexXOneIso X).hom ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          ι.map
            ((Λ.chainComplexXZeroIso X).inv ≫
              (Λ.chainComplexXZeroIso X).hom ≫ Λ.F.map f ≫ (Λ.chainComplexXZeroIso Y).inv)
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (StructuredArrow { as := default } F)
d : T
⊢ IsConnected (StructuredArrow { as := d } F)

Tactic:
obtain rfl := Subsingleton.elim d default

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (StructuredArrow { as := default } F)
⊢ IsConnected (StructuredArrow { as := default } F)
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (CostructuredArrow F { as := default })
d : T
⊢ IsConnected (CostructuredArrow F { as := d })

Tactic:
obtain rfl := Subsingleton.elim d default

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
x✝ : IsConnected (CostructuredArrow F { as := default })
⊢ IsConnected (CostructuredArrow F { as := default })
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ (freeYoneda R).IsSeparating

Tactic:
intro M N f₁ f₂ h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M N : PresheafOfModules R
f₁ f₂ : M ⟶ N
h : ∀ (G : PresheafOfModules R), freeYoneda R G → ∀ (h : G ⟶ M), h ≫ f₁ = h ≫ f₂
⊢ f₁ = f₂
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ g.hom ≫ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm f) = g.hom ≫ f

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ g.hom ≫ f = g.hom ≫ f
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
⊢ 0 • m = 0

Tactic:
by
    obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
    simpa using smul_eq hcR hcM 0 m

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

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ (ConcreteCategory.hom (g.app (op (F.obj X)))) (freeYonedaEquiv f) =
    (ConcreteCategory.hom (((pushforward φ).map g).app (op X)))
      (freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) f))

Tactic:
Equiv.apply_symm_apply

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ (ConcreteCategory.hom (g.app (op (F.obj X)))) (freeYonedaEquiv f) =
    (ConcreteCategory.hom (((pushforward φ).map g).app (op X))) (freeYonedaEquiv f)
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ {⊤}
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {⊤}
⊢ R ∈ {⊤}

Tactic:
by
    rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS
    simpa using hR hS

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

Goal state before:
pp: case h
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)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ Ti (g ij.fst) ⋯ (p (g ij.fst) ⋯ ij.snd) ∧ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst = p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
rw [hp]

Goal state after:
case h
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)
Y : C
ij : (i : ι) × κ (g i) ⋯
⊢ ofArrows (W (g ij.fst) ⋯) (p (g ij.fst) ⋯) (p (g ij.fst) ⋯ ij.snd) ∧
    p (g ij.fst) ⋯ ij.snd ≫ g ij.fst = p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ (∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩) →
    ⟨Z, v⟩ ∈ (s.bind t).uncurry

Tactic:
rintro ⟨⟨_, f⟩, hf, ⟨Y, g⟩, hg, h⟩
    rw [Sigma.ext_iff] at h
    obtain ⟨rfl, h⟩ := h
    rw [heq_iff_eq] at h; subst h
    exact ⟨_, _, _, _, hg, rfl⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
rintro ⟨W, h, k, hk, comm⟩

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      a.Compatible → ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
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
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑x (shrinkYonedaObjObjEquiv (shrinkYonedaObjObjEquiv.symm f✝)) ⋯ = ↑x f✝ hf✝

Tactic:
Equiv.apply_symm_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑x f✝ ⋯ = ↑x f✝ hf✝
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
⊢ (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
    (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x

Tactic:
refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H : (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op E)).map f.op)) (hh.lift K) = x f hf

Tactic:
apply hh.fac K (WalkingMulticospan.left ⟨Y, f, hf⟩)

Goal state after: