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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
i j : Fin 2
⊢ ↑(diag2 a ha) i j =
    ↑(SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
                SpecialLinearGroup.transvection ⋯ a *
              SpecialLinearGroup.transvection ⋯ (-1) *
            SpecialLinearGroup.transvection ⋯ 1 *
          SpecialLinearGroup.transvection ⋯ (-1))
      i j

Tactic:
fin_cases i

Goal state after:
case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
                SpecialLinearGroup.transvection ⋯ a *
              SpecialLinearGroup.transvection ⋯ (-1) *
            SpecialLinearGroup.transvection ⋯ 1 *
          SpecialLinearGroup.transvection ⋯ (-1))
      ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
j : Fin 2
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑(SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
                SpecialLinearGroup.transvection ⋯ a *
              SpecialLinearGroup.transvection ⋯ (-1) *
            SpecialLinearGroup.transvection ⋯ 1 *
          SpecialLinearGroup.transvection ⋯ (-1))
      ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: 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)
i j : Fin 2
hij : i ≠ j
c : F
hc : c ≠ 0
⊢ P (diag2n hij c hc)

Tactic:
fin_cases i

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)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ P (diag2n hij c hc)

case «1»
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)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ P (diag2n hij c hc)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B ∘ₗ f) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: i j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) i j = ↑T⁻¹ i j

Tactic:
fin_cases i

Goal state after:
case «0»
j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑T⁻¹ ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑T⁻¹ ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ polar (⇑(f.compQuadraticMap' Q)) x✝¹ x✝ = f (polar (⇑Q) x✝¹ x✝)

Tactic:
LinearMap.compQuadraticMap_polar

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ f (polar (⇑Q) x✝¹ x✝) = f (polar (⇑Q) x✝¹ x✝)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
m : Type u_12
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : IsDomain R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
b : Basis m R M₁
B : M₁ →ₗ[R] M₁ →ₗ[R] R
⊢ B.SeparatingLeft ↔ ((toMatrix₂ b b) B).det ≠ 0

Tactic:
by
  rw [← Matrix.separatingLeft_iff_det_ne_zero, separatingLeft_toMatrix₂_iff]

Goal state after:
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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = 0

Tactic:
classical
    rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

Goal state after:
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
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
by
  have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
  have l := v_mul.compl₂ (LinearMap.fst _ _ N)
  exact
    { toFun := fun m => (l m).prod (f m)
      map_add' := fun v₂ v₂ =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
      map_smul' := fun c v =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x)
            (LinearMap.congr_fun (f.map_smul _ _) x) }

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
n : ℕ
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (map f n)) (mk x) = mk (⇑(ConcreteCategory.hom f) ∘ x)

Tactic:
apply exteriorPower.map_apply_ιMulti

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (Hom.hom (lift F' ≫ F'.m)) x = (Hom.hom (ι f)) x

Tactic:
change (F'.e ≫ F'.m) _ = _

Goal state after:
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x : ↑(image f)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ : Equiv.Perm.sign σ • (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ ∃ b, ↑↑(Equiv.Perm.sign σ) * b = 1

Tactic:
use (σ.sign : R)

Goal state after:
case h
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
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ : Equiv.Perm.sign σ • (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ ↑↑(Equiv.Perm.sign σ) * ↑↑(Equiv.Perm.sign σ) = 1
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) = ⊤
⊢ ⋀[R]^n M ≤ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))

Tactic:
rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]

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) = ⊤
⊢ ⇑(ExteriorAlgebra.ιMulti R n) '' {a | Set.range a ⊆ Set.range v} ⊆
    ↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
m : M
i : Fin 1
⊢ m = update (fun x ↦ 0) 0 m i

Tactic:
fin_cases i

Goal state after:
case «0»
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
m : M
⊢ m = update (fun x ↦ 0) 0 m ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ : (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X = (s.π.app j).app X
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((s.π.app j).app Y) =
    (s.π.app j).app X ≫ (F.obj j).map f

Tactic:
Hom.naturality

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ : (hc X).lift ((evaluation R X).mapCone s) ≫ (c.π.app j).app X = (s.π.app j).app X
⊢ (s.π.app j).app X ≫ (F.obj j).map f = (s.π.app j).app X ≫ (F.obj j).map f
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[S] (1 ⊗ₜ[R] m) = (1 • 1) ⊗ₜ[S] (1 ⊗ₜ[R] m)

Tactic:
rw [one_smul]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[S] (1 ⊗ₜ[R] m) = 1 ⊗ₜ[S] (1 ⊗ₜ[R] m)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[R] m ⊗ₜ[S] 1 = 1 ⊗ₜ[R] m ⊗ₜ[S] (1 • 1)

Tactic:
rw [one_smul]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[R] m ⊗ₜ[S] 1 = 1 ⊗ₜ[R] m ⊗ₜ[S] 1
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ r • 1 = f r

Tactic:
RingHom.smul_toAlgebra,

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
this : Algebra R S := f.toAlgebra
⊢ f r * 1 = f r
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
⊢ IsLimit (G.flip.mapCone₂ c₁ c₂)

Tactic:
refine IsLimit.postcomposeHomEquiv E₁ _ ?_

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
⊢ IsLimit ((Cone.postcompose E₁.hom).obj (G.flip.mapCone₂ c₁ c₂))
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 : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
⊢ ∃ U x x', ιM x = m ∧ ιM x' = m'

Tactic:
by
  obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, m'⟩
  rw [Prod.ext_iff] at h
  obtain ⟨rfl, rfl⟩ := h
  exact ⟨U, x, x', rfl, rfl⟩

Goal state after:
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 Y Z : F.PartialLeftAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap (f ≫ g)) =
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g)

Tactic:
simp [partialLeftAdjointHomEquiv_comp, ← F.partialLeftAdjointHomEquiv_comp]

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

Goal state before:
pp: case refine_1
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
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
h :
  ∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)),
    (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
      (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ α ((ιR cR) r • ιM m) = (ιR cR) r • α (ιM m)

Tactic:
refine Eq.trans ?_ ((homEquiv'_app_apply ..).symm.trans (h U r m))

Goal state after:
case refine_1
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
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
h :
  ∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)),
    (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
      (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ α ((ιR cR) r • ιM m) = α ((ConcreteCategory.hom (cM.ι.app U)) (r • m))
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toPretopology

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K ≤ J.toPretopology → K.toGrothendieck ≤ J

Tactic:
· intro h X R hR
      exact h _ ⟨_, hR, Sieve.le_generate R⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
J : GrothendieckTopology C
⊢ K ≤ J.toPretopology → K.toGrothendieck ≤ J
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
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ Fs = Exists.choose ⋯

Tactic:
apply H.choose_spec.2 Fs

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
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation Fs
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = singleton (f default)

Tactic:
refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f ≤ singleton (f default)
Module: Mathlib.CategoryTheory.Sites.Sieves

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

Tactic:
by
  ext W g
  constructor
  · rintro ⟨_, h, k, ⟨W, g, hg⟩, rfl⟩
    have := R.hasPullback f hg
    rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]
    exact Sieve.downward_closed _ (by exact Sieve.le_generate R W _ hg) (h ≫ pullback.fst g f)
  · rintro ⟨W, h, k, hk, comm⟩
    have := R.hasPullback f hk
    exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩

Goal state after:
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
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.1.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
pullback.condition

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
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd ≫ ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Sieves

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✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f

Tactic:
use Y, g, 𝟙 _, hg

Goal state after:
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ f = 𝟙 (F.obj Y) ≫ F.map g
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.fst f g ≫ f).op = P.map g.op ≫ P.map (pullback.snd f g).op

Tactic:
pullback.condition

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
inst✝¹ : HasProducts A
inst✝ : HasPullbacks C
Y : C
f : Y ⟶ U
hf : R f
Z : C
g : Z ⟶ U
hg : R g
⊢ P.map (pullback.snd f g ≫ g).op = P.map g.op ≫ P.map (pullback.snd f g).op
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))

Tactic:
rintro W _ ⟨T, _, a, ⟨_, b, _, ⟨i⟩, rfl⟩, rfl⟩

Goal state after:
case e'_2.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ (generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))).arrows
    (a ≫ (Over.map p).map (b ≫ g i))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ pullback.fst (π i) (π j) ≫ π i = pullback.snd (π i) (π j) ≫ π j

Tactic:
exact pullback.condition

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt

Tactic:
by
  rw [Presheaf.isSheaf_iff_multifork]
  intro X S
  exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [iSup_le_iff]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)