mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

Tactic:
by_cases h : i + j = 0

Goal state after:
case pos
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : i + j = 0
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ ↑(((decompose 𝒜) (c * c')) 0) = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a b : A
n i : ι
b_mem : b ∈ 𝒜 i
h : ¬i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = 0

Tactic:
lift b to 𝒜 i using b_mem

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : A
n i : ι
h : ¬i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = 0
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = ↑(((decompose 𝒜) a) (n - i)) * b

Tactic:
lift b to 𝒜 i using b_mem

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = ↑(((decompose 𝒜) a) (n - i)) * ↑b
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * b else 0

Tactic:
lift b to 𝒜 i using b_mem

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = 0

Tactic:
← hx x

Goal state after:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = ((associated' Q) x) x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: case mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : CliffordAlgebra Q
ha : reverse (involute a) = involute (reverse a)
hb : reverse (involute b) = involute (reverse b)
⊢ reverse (involute (a * b)) = involute (reverse (a * b))

Tactic:
simp only [ha, hb, reverse.map_mul, map_mul]

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

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ ((LinearMap.toMatrix₂' R) (QuadraticMap.associated Q)).transpose i j =
    (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j

Tactic:
Matrix.transpose_apply,

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) j i = (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
⊢ ((LinearMap.toMatrix₂ b b) (QuadraticMap.associated Q)).transpose i j =
    (LinearMap.toMatrix₂ b b) (QuadraticMap.associated Q) i j

Tactic:
Matrix.transpose_apply,

Goal state after:
R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
i j : n
⊢ (LinearMap.toMatrix₂ b b) (QuadraticMap.associated Q) j i = (LinearMap.toMatrix₂ b b) (QuadraticMap.associated Q) i j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
⊢ P x

Tactic:
induction hx using Submodule.pow_induction_on_right' with

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

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

Tactic:
obtain ⟨_, rfl⟩ := hm

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i ↦ M i.castSucc) (M (last n) →ₗ[R] M₂)
⊢ f.uncurryRight.curryRight = f

Tactic:
by
  ext m x
  simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]
  rw [init_snoc]

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

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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
⊢ AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) f) ((ι R) m * x) 0) =
    AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i ↦ (f (i + 1)).curryLeft m) x
        0)

Tactic:
rw [foldl_mul, foldl_ι]

Goal state after:
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
m : M
x : ExteriorAlgebra R M
⊢ AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯)
          (((LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) f))
        x 0) =
    AlternatingMap.constLinearEquivOfIsEmpty.symm
      (((foldl 0 (LinearMap.mk₂ R (fun m f i ↦ (f (i + 1)).curryLeft m) ⋯ ⋯ ⋯ ⋯) ⋯) fun i ↦ (f (i + 1)).curryLeft m) x
        0)
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
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| TrivSqZeroExt.sndHom R N ∘ₗ (toTrivSqZeroExt.comp (map f)).toLinearMap

Tactic:
toTrivSqZeroExt_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
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
| TrivSqZeroExt.sndHom R N ∘ₗ ((TrivSqZeroExt.map f).comp toTrivSqZeroExt).toLinearMap
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 0 ⋯ = 0

Tactic:
Ext.comp_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
⊢ 0 = 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
⊢ ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₁ i), e = 0

Tactic:
rintro (_ | i) hi Y x₃

Goal state after:
case zero
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
hi : n + 1 ≤ 0
Y : C
x₃ : Ext Y S.X₁ 0
⊢ x₃ = 0

case succ
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 : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext Y S.X₁ (i + 1)
⊢ x₃ = 0
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✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
c c' : C
⊢ ∃ Z x x, True

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))
    exact ⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f),
      F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁

Tactic:
rw [Functor.initial_iff_of_isCofiltered]

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ ((∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)) ∧
      ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s') ↔
    ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
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
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
      colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
  conv_lhs => slice 1 3
  simp

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
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
⊢ (R.map φ).hom ≫ F.partialLeftAdjointHomEquiv (c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f) ≫ 𝟙 (F.1 Y)

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j j' : J
φ : j ⟶ j'
⊢ (R.map φ).hom ≫ F.partialLeftAdjointHomEquiv (c'.ι.app j' ≫ f) = F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ 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
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g) ≫ 𝟙 Y)

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g))
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 : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
⊢ F.partialRightAdjointHomEquiv (𝟙 Y ≫ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j')) =
    F.partialRightAdjointHomEquiv
      (F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j) ≫ F.partialRightAdjointMap (R.map φ))

Tactic:
rw [id_comp, Equiv.apply_symm_apply, partialRightAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, assoc, this]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ∈ J.coverings Y

Tactic:
by
  -- We need to construct `max u v`-indexed families with the same presieves.
  -- Because `f` needs not be injective, the indexing type is a sum.
  let a (i : (Presieve.ofArrows X f).uncurry ⊕ (Presieve.ofArrows P p₁).uncurry) : ι :=
    i.elim (fun i ↦ i.2.idx) (fun i ↦ i.2.idx)
  convert_to Presieve.ofArrows (P ∘ a) (fun i ↦ p₁ (a i)) ∈ _
  · refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩
    exact .mk' (Sum.inr ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)
  · refine IsStableUnderBaseChange.mem_coverings_of_isPullback (fun i ↦ f (a i)) ?_ g _
      (fun i ↦ p₂ (a i)) fun i ↦ h _
    convert! hR
    refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_
    exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

Goal state after:
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
⊢ trivial C = ⊥

Tactic:
by
      apply le_antisymm
      · intro X S hS
        rw [trivial_covering] at hS
        apply covering_of_eq_top _ hS
      · exact (completeLatticeOfInf _ isGLB_sInf).bot_le (trivial C)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ Over.Hom.left F.hom ≫ x g₂.obj.hom ⋯ = x g₁.obj.hom ⋯ ≫ 𝟙 W

Tactic:
comp_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ Over.Hom.left F.hom ≫ x g₂.obj.hom ⋯ = x g₁.obj.hom ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
⊢ ((ofArrows Z g).bind fun x f H ↦ ofArrows (W f H) (k f H)) =
    ofArrows (fun i ↦ W (g i.fst) ⋯ i.snd) fun ij ↦ k (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
funext Y
  ext f
  constructor
  · rintro ⟨_, _, _, ⟨i⟩, ⟨i'⟩, rfl⟩
    exact ofArrows.mk (Sigma.mk _ _)
  · rintro ⟨i⟩
    exact bind_comp _ (ofArrows.mk _) (ofArrows.mk _)

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
f : S.arrows.category
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f

Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)

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
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f
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
⊢ Fs = Exists.choose ⋯

Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)

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
⊢ Fs = Exists.choose ⋯
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
f₁ : Y ⟶ X
f₂ : Z ⟶ X
hf₁ : R f₁
hf₂ : R f₂
heq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ hf₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
refine injective_of_mono (f.app _) ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
f₁ : Y ⟶ X
f₂ : Z ⟶ X
hf₁ : R f₁
hf₂ : R f₂
heq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map g₁.op)) (x f₁ hf₁)) =
    (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
Y : C
u : Y ⟶ X
hu : R u
⊢ (ConcreteCategory.hom (P.map u.op)) t = x u hu

Tactic:
refine injective_of_mono (f.app _) ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
t : P.obj (op X)
ht : (x.map f).IsAmalgamation ((ConcreteCategory.hom (f.app (op X))) t)
Y : C
u : Y ⟶ X
hu : R u
⊢ (ConcreteCategory.hom (f.app (op Y))) ((ConcreteCategory.hom (P.map u.op)) t) =
    (ConcreteCategory.hom (f.app (op Y))) (x u hu)