mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
⊢ ↑(((decompose ℳ) x) j) = 0

Tactic:
by
  rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij.symm, ZeroMemClass.coe_zero]

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

Goal state before:
pp: case cons
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        (((if False then polarSym2 (⇑Q) (Sym2.map f s(a, a)) else 0) +
            ∑ x ∈ s, if ¬a = x then polarSym2 (⇑Q) (Sym2.map f s(a, x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Tactic:
if_false,

Goal state after:
case cons
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((0 + ∑ x ∈ s, if ¬a = x then polarSym2 (⇑Q) (Sym2.map f s(a, x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
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
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + ∑ x ∈ s, polar (⇑Q) (f a) (f x)) =
    2 • Q (f a) + ∑ x ∈ s, polar (⇑Q) (f a) (f x) + ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))

Tactic:
abel_nf

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

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
f g : M →ₗ[R] A
x y : M
⊢ f x * g x + f y * g x + (f x * g y + f y * g y) = f x * g x + f y * g y + (f x * g y + f y * g x)

Tactic:
abel_nf

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

Goal state before:
pp: 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)

Tactic:
rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
          rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
          · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
          · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]

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

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B : BilinMap R M N
x y : M
⊢ ⅟2 ((B x) x) + ⅟2 ((B y) x) + (⅟2 ((B x) y) + ⅟2 ((B y) y)) - ⅟2 ((B x) x) - ⅟2 ((B y) y) =
    ⅟2 ((B x) y) + ⅟2 ((B y) x)

Tactic:
abel_nf

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
i : I
⊢ i ∈ ofFinEmbEquiv f ↔ i ∈ range ⇑f

Tactic:
by
  simp [ofFinEmbEquiv_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') M₂
x y : M'
⊢ ((curryFinFinset R M₂ M' hk hl).symm ((curryFinFinset R M₂ M' hk hl) f)) (s.piecewise (fun x_1 ↦ x) fun x ↦ y) =
    f (s.piecewise (fun x_1 ↦ x) fun x ↦ y)

Tactic:
LinearEquiv.symm_apply_apply

Goal state after:
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') M₂
x y : M'
⊢ f (s.piecewise (fun x_1 ↦ x) fun x ↦ y) = f (s.piecewise (fun x_1 ↦ x) fun x ↦ y)
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
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ (algebraMap R (ExteriorAlgebra R M)) 1

Tactic:
Ne,

Goal state after:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(ι R) x = (algebraMap R (ExteriorAlgebra R M)) 1
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:
← LinearMap.comp_apply,

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
⊢ (f ∘ₗ ιInv) x = y
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 y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
apply (mono_iff_injective F'.m).1
      · infer_instance
      rw [map_add]
      change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
      simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
      rfl

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:
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:
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:
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:
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
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x = 0

Tactic:
← x.comp_mk₀_id,

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 : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x.comp (Ext.mk₀ (𝟙 X)) ⋯ = 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:
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:
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:
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.Algebra.Category.ModuleCat.Free

Goal state before:
pp: case refine_1
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inl =
    ⇑(ConcreteCategory.hom S.f) ∘ v

pp: case refine_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⊤ ≤
    span R
      (range
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))

Tactic:
· simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]

Goal state after:
case refine_2
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⊤ ≤
    span R
      (range
        (⇑(ConcreteCategory.hom S.g) ∘
          Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘ Sum.inr))
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
have : Small.{max v v'} R := small_lift R

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
this : Small.{max v v', u} R
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
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 →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n g) ((map n f) x✝) = x✝

Tactic:
← LinearMap.comp_apply,

Goal state after:
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 →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ (map n g ∘ₗ map n f) x✝ = x✝
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (Hom.hom ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂))
      (1 ⊗ₜ[R] m₁ ⊗ₜ[S] (1 ⊗ₜ[R] m₂)) =
    m₁ ⊗ₜ[S] m₂

Tactic:
tensorHom_tmul,

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom ((extendRestrictScalarsAdj f).counit.app M₁)) (1 ⊗ₜ[R] m₁) ⊗ₜ[S]
      (ConcreteCategory.hom ((extendRestrictScalarsAdj f).counit.app M₂)) (1 ⊗ₜ[R] m₂) =
    m₁ ⊗ₜ[S] m₂
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝ : X✝ ⟶ Y✝
⊢ (externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝ ≫
      (NatIso.ofComponents (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom =
    (NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
          ⋯).hom ≫
      (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝

Tactic:
ext; simp [whisker_exchange]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ ∀ ⦃X Y : P.FullSubcategory⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
rintro ⟨X, hX⟩ ⟨Y, hY⟩ ⟨f₁ : X ⟶ Y⟩ ⟨f₂ : X ⟶ Y⟩
          obtain ⟨Z, hZ, ⟨g⟩⟩ := hP (coeq f₁ f₂)
          exact ⟨⟨Z, hZ⟩, ObjectProperty.homMk (coeqHom f₁ f₂ ≫ g),
            ObjectProperty.hom_ext _ (coeq_condition_assoc _ _ _) ⟩

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 ⋙ F.leftAdjointObjIsDefined.ι).map φ ≫ F.partialLeftAdjointHomEquiv (c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f) ≫ ((const J).obj (F.1 Y)).map φ

Tactic:
dsimp
            rw [comp_id, ← c'.w φ, ← partialLeftAdjointHomEquiv_map_comp, assoc]
            dsimp

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

Goal state before:
pp: case a
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)
⊢ (ofArrows Z g).bind Ti ≤ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

Tactic:
rintro T u ⟨S, v, w, ⟨i⟩, hv, rfl⟩
        rw [hp] at hv
        obtain ⟨j⟩ := hv
        exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j

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
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        have ht := H.choose_spec.1 f.obj.hom f.property
        cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
⊢ (ofArrows (Y ∘ a) fun i ↦ f (a i)) = ofArrows Y f

Tactic:
refine le_antisymm (ofArrows_comp_le f a) ?_
  rintro - - ⟨i⟩
  obtain ⟨j, rfl⟩ := ha i
  use j

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
A✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} A✝
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
ℱ : Sheaf J A
E : A
⊢ Presieve.IsSheaf J (ℱ.obj ⋙ coyoneda.obj (op E))

Tactic:
exact ℱ.property E

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ range p ≤ G

Tactic:
rw [← image_top, image_le_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

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), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom

Tactic:
dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]

Goal state after:
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), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ 𝟙 (J.plusObj (J.plusObj P) ⋙ F) ≫
      (J.plusCompIso F (J.plusObj P)).hom ≫
        (𝟙 (J.plusObj (J.plusObj P ⋙ F)) ≫ J.plusMap (J.plusCompIso F P).hom) ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) =
    (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

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), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv

Tactic:
dsimp [sheafificationWhiskerRightIso, sheafifyCompIso]

Goal state after:
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), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ ((𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv ≫ 𝟙 (J.plusObj (J.plusObj P ⋙ F))) ≫
        (J.plusCompIso F (J.plusObj P)).inv) ≫
      𝟙 (J.plusObj (J.plusObj P) ⋙ F) =
    J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
⊢ 𝟙 F ≫ c.ι = c.ι ≫ (const J).map (𝟙 c.pt)

Tactic:
by rw [Functor.map_id, Category.comp_id, Category.id_comp]

Goal state after: