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

Goal state before:
pp: case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ↑(diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c') ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, inv_inv, mul_add, add_mul,
      mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
      mul_sub_one, ← sub_eq_add_neg]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)

Tactic:
add_comm _ (f (x + y)),

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1, (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) i_1 •> (B (b₁ i')) (b₂ i_1) =
    ∑ x, (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

pp: case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), (b₁.repr (l (b₁' i))) i' •> 0 •> (B (b₁ i')) (b₂ i_1) = 0

Tactic:
· apply sum_congr rfl
      rintro j' -
      simp only [smul_eq_mul, mul_assoc, mul_comm,
        mul_left_comm]

Goal state after:
case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), (b₁.repr (l (b₁' i))) i' •> 0 •> (B (b₁ i')) (b₂ i_1) = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
← separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂ b₁ b₂) M).Nondegenerate ↔ M.Nondegenerate

Tactic:
← nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂' R) M).Nondegenerate ↔ M.Nondegenerate
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ ((toLinearMap₂' R) M).Nondegenerate ↔ M.Nondegenerate

Tactic:
nondegenerate_toLinearMap₂'_iff

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommRing R
inst✝⁷ : DecidableEq m
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
M : Matrix m n R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
b₁ : Basis m R M₁
b₂ : Basis n R M₂
⊢ M.Nondegenerate ↔ M.Nondegenerate
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ Q.IsOrtho x y ↔ Q.IsOrtho y x

Tactic:
simp_rw [isOrtho_def, add_comm]

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

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
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 0
⊢ involute x = x

Tactic:
induction x, h using even_induction with

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ↑⟨x', hx'⟩ = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x', hx'⟩

Tactic:
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x' = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x', hx'⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ i, ⨆ j, (ι Q).range ^ ↑j = ⨆ i, (ι Q).range ^ ↑i.snd

Tactic:
rw [iSup_sigma]

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
⊢ ↑n ≤ {b}ᶜ.encard

Tactic:
← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α),

Goal state after:
α : Type u_1
n : ℕ
hn : 1 ≤ n
a b : α
hα : ↑n < {b}.encard + {b}ᶜ.encard
hab : a ≠ b
⊢ ↑n ≤ {b}ᶜ.encard
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val), motive xv ⋯

Tactic:
intro hxv

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
hxv : xv ∈ ((ι Q).range ^ 2) ^ k * (ι Q).range ^ n.val
⊢ motive xv ⋯
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
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 ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
F'.fac,

Goal state after:
case a
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) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
x✝ : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x✝ = t.ι.app j
⊢ x✝ = colimitDesc F t

Tactic:
ext ⟨j, x⟩

Goal state after:
case mk
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
x✝¹ : (colimitCocone F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone F).ι.app j ≫ x✝¹ = t.ι.app j
x✝ : ↑(colimitCocone F).pt
j : J
x :
  ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
        forget AddMonCat).obj
    j
⊢ (Hom.hom x✝¹)
      (Quot.mk
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
            forget AddMonCat).ColimitTypeRel
        ⟨j, x⟩) =
    (Hom.hom (colimitDesc F t))
      (Quot.mk
        ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
            forget AddMonCat).ColimitTypeRel
        ⟨j, x⟩)
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c •
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)

Tactic:
F'.fac,

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c • (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)
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)
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) =
    (Hom.hom (ι f)) x

Tactic:
F'.fac,

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) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) = (Hom.hom (ι f)) x
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.comp (Ext.mk₀ (𝟙 X)) ⋯ = 0

Tactic:
← h.retract,

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₀ (h.i ≫ h.r)) ⋯ = 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
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ limMap (F.whiskerLeft (restriction R f)) ≫
      limit.π ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) j =
    limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f

Tactic:
apply limMap_π

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ α.app Y ▷ F'.obj Y = α.app X ▷ F'.obj X ≫ (tensorObj G F').map f

Tactic:
simp only [← tensorHom_id]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ 𝟙 (F'.obj Y)) = (α.app X ⊗ₘ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv =
    F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
      (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G

Tactic:
by ext X; apply hexagon_reverse

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (s.ι.app X)) PUnit.unit = (ConcreteCategory.hom (s.ι.app Y)) PUnit.unit

Tactic:
exact ConcreteCategory.congr_hom (s.ι.naturality f).symm PUnit.unit

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
⊢ IsConnected C

Tactic:
let colimitCocone : ColimitCocone (constPUnitFunctor C) := ⟨pUnitCocone.{w} C, h⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
colimitCocone : ColimitCocone (constPUnitFunctor C) := { cocone := pUnitCocone C, isColimit := h }
⊢ IsConnected C
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔ IsConnected D

Tactic:
isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ IsConnected C ↔ IsConnected D

Tactic:
rw [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,
    isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Final
⊢ Nonempty (Limits.colimit (constPUnitFunctor C) ≅ PUnit.{(max v u v₂ u₂) + 1}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})
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✝³ : IsCofiltered C
E : Type u₃
inst✝² : Category.{v₃, u₃} E
T : C ⥤ D
inst✝¹ : T.Initial
S : D ⥤ E
inst✝ : S.Initial
d : D
e : E
u : S.obj d ⟶ e
⊢ (map₂ (𝟙 (T ⋙ S)) u).Initial

Tactic:
by
  have := (T ⋙ S).initial_iff_isCofiltered_costructuredArrow.mp inferInstance e
  apply initial_of_natIso (map₂IsoPreEquivalenceInverseCompProj T S d e u).symm

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'

Tactic:
have w := (D.map fj).w k'

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj (j', k').1).π.app k' = ((Cone.postcompose (F.map fj)).obj (D.obj (j, k).1)).π.app k'
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'
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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
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

Tactic:
hφ

Goal state after:
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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝² x✝¹ x✝).hom ≫ (isoMk (fun X ↦ β_ (x✝².obj X) ((x✝¹ ⊗ x✝).obj X)) ⋯).hom ≫ (α_ x✝¹ x✝ x✝²).hom =
    (isoMk (fun X ↦ β_ (x✝².obj X) (x✝¹.obj X)) ⋯).hom ▷ x✝ ≫
      (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (isoMk (fun X ↦ β_ (x✝².obj X) (x✝.obj X)) ⋯).hom

Tactic:
ext : 1
    apply hexagon_forward (C := ModuleCat (R.obj _))

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

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
⊢ ∃! x, (hom f) x = y

Tactic:
let y' : PUnit ⟶ Y := ↾fun _ => y
  have hy' : y' ≫ g = y' ≫ h := by ext; exact hy
  refine ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_hom (Fork.IsLimit.lift' t y' _).2 ⟨⟩, ?_⟩
  intro x' hx'
  suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by
    rw [← this]
  apply TypeCat.homEquiv.symm.injective
  apply Fork.IsLimit.hom_ext t
  ext ⟨⟩
  apply hx'.trans (congr_hom (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = f

Tactic:
exact h.choose_spec.choose_spec.2

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
⊢ ∀ (b : Sieve Y), pullback f (pushforward f b) ≤ b

Tactic:
rintro S Z g ⟨g₁, hf, hg₁⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ ≫ f = g ≫ f
hg₁ : S.arrows g₁
⊢ S.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
S : Sieve X
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
            ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
enter [2, a, 1, 1, 2]; rw [(firstObjEqFamily P S.arrows).toEquiv_symm_apply]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a : Presieve.FamilyOfElements P S.arrows
| (ConcreteCategory.hom (firstObjEqFamily P S.arrows).inv) a