mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ ((opEquiv a).symm f).comp z h = (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply,
    ShiftedHom.comp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ : Triangle Cᵒᵖ
hT₁ : T₁ ∈ distinguishedTriangles C
T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
by
  simp only [mem_distinguishedTriangles_iff] at hT₁ ⊢
  exact Pretriangulated.isomorphic_distinguished _ hT₁ _
    ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.IsPresentation

Tactic:
rw [isPresentation_iff]; constructor <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'

Tactic:
update_of_ne h

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (v k)) i' = (e.repr (v k)) i'
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype ι
inst✝² : Finite κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ (toLin b c') ((toMatrix b' c') f * b'.toMatrix ⇑b) = (toLin b c') ((toMatrix b c') f)

Tactic:
by
    rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G✝
G : Type u_7
inst✝¹ : CommGroup G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
G' : Type u_8
inst✝ : CommGroup G'
φ : G →* G'
⊢ ⋯.unit ∈ rootsOfUnity (Nat.card G) G'

Tactic:
simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, IsUnit.unit_spec,
      ← map_pow, pow_card_eq_one', map_one, Units.val_one]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G✝
G : Type u_7
inst✝¹ : CommGroup G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
G' : Type u_8
inst✝ : CommGroup G'
φ : G →* G'
⊢ ((fun ζ ↦ monoidHomOfForallMemZpowers hg ⋯) ((fun φ ↦ ⟨⋯.unit, ⋯⟩) φ)) g = φ g

Tactic:
simp only [IsUnit.unit_spec, monoidHomOfForallMemZpowers_apply_gen]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) =
    (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
← map_sub,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b) - Q a) - (algebraMap R A) (Q b) = (algebraMap R A) (Q (a + b) - Q a - Q b)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case pred
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ ↑(T ^ (-↑n - 1)) = !![1, -↑n - 1; 0, 1]

Tactic:
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂
i : n
j : m
⊢ (toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)

Tactic:
simp only [toMatrix₂, LinearEquiv.trans_apply, toMatrixₛₗ₂'_apply, LinearEquiv.arrowCongr_apply,
    Basis.equivFun_symm_apply, Pi.single_apply, ite_smul, one_smul, zero_smul, sum_ite_eq',
    mem_univ, ↓reduceIte, LinearEquiv.refl_apply]

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 y : M
⊢ f (y + x) - (f x + f y) = f (y + x) - (f y + f x)

Tactic:
add_comm (f x) (f y)

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ f (y + x) - (f y + f x) = f (y + x) - (f y + f x)
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✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x✝¹ x✝ : M
⊢ toFun (x✝¹ + x✝) = toFun x✝¹ + toFun x✝ + ((LinearMap.mk₂ R (polar toFun) polar_add_left polar_smul_left ⋯ ⋯) x✝¹) x✝

Tactic:
simp only [LinearMap.mk₂_apply]

Goal state after:
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✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : Module S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
polar_add_left : ∀ (x x' y : M), polar toFun (x + x') y = polar toFun x y + polar toFun x' y
polar_smul_left : ∀ (a : R) (x y : M), polar toFun (a • x) y = a • polar toFun x y
x✝¹ x✝ : M
⊢ toFun (x✝¹ + x✝) = toFun x✝¹ + toFun x✝ + polar toFun x✝¹ x✝
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) a * (of (fun i ↦ ↥(𝒜 i)) j) b) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
coe_mul_of_apply_add

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) a) i) * ↑b = ↑(((decompose 𝒜) a) i) * ↑b
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
this : Q x = 0
⊢ x = 0

Tactic:
← hQ.anisotropic

Goal state after:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
this : Q x = 0
⊢ x = ?x

case x
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
this : Q x = 0
⊢ M

case a
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
h : Q x ≤ 0
this : Q x = 0
⊢ Q ?x = 0
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)
f : (n → R) →ₗ[R] n → R
⊢ discr' (QuadraticMap.comp Q f) = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr'

Tactic:
simp [mul_left_comm, toMatrix'_comp, mul_comm, discr']

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
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (↑(MulOpposite.opLinearEquiv R) ∘ₗ ι Q).range = (ι Q).range

Tactic:
LinearMap.range_comp,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (Submodule.map (↑(MulOpposite.opLinearEquiv R)) (ι Q).range) =
    (ι Q).range
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

Goal state before:
pp: case add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 0
_hy : y ∈ evenOdd Q 0
ihx : involute x = x
ihy : involute y = y
⊢ involute (x + y) = x + y

Tactic:
| add x y _hx _hy ihx ihy =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : involute x = -x
ihy : involute y = -y
⊢ involute (x + y) = -(x + y)

Tactic:
| add x y _hx _hy ihx ihy =>

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

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm✝ : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn✝ : n ∈ (ι Q).range
hm : ∃ y, (ι Q) y = m
hn : ∃ y, (ι Q) y = n
⊢ motive (m * n * y * b) ⋯

Tactic:
obtain ⟨m₁, rfl⟩ := hm

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
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 a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
n : CliffordAlgebra Q
hn✝ : n ∈ (ι Q).range
hn : ∃ y, (ι Q) y = n
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * n * y * b) ⋯
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case succ.e_6
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
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun i ↦ v i.succ) = v

Tactic:
exact Matrix.cons_head_tail _

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
hd : injectiveDimension X = ⊥
⊢ HasInjectiveDimensionLE X 0

Tactic:
simp [← injectiveDimension_le_iff, hd]

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
this : Small.{max v v', u} R
n : ℕ
ih : ∀ {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
I : ModuleCat R
injective✝ : Injective I
f : M ⟶ I
mono✝ : Mono f
injf : Function.Injective ⇑(Hom.hom f)
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero (Hom.hom f) (Hom.hom f).range.mkQ ⋯
exactS : S.ShortExact
I' : ModuleCat R := of R (ULift.{v', v} ↑I)
f' : ↑N →ₗ[R] ↑I' := ↑ULift.moduleEquiv.symm ∘ₗ Hom.hom f ∘ₗ ↑e.symm
injf' : Function.Injective ⇑f'
S' : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f' f'.range.mkQ ⋯
exactS' : S'.ShortExact
eCoker : ↑(of R (↑I ⧸ (Hom.hom f).range)) ≃ₗ[R] ↑(of R (↑I' ⧸ f'.range)) :=
  Submodule.Quotient.equiv (Hom.hom f).range f'.range ULift.moduleEquiv.symm ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
exact (exactS.hasInjectiveDimensionLT_X₃_iff n inferInstance).symm.trans
      ((ih eCoker).trans (exactS'.hasInjectiveDimensionLT_X₃_iff n inferInstance))

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

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
exactS : S.ShortExact
eCoker : ↑(of R (↑I ⧸ f.range)) ≃ₛₗ[↑eR] ↑(of R' (↑I' ⧸ (Hom.hom f').range)) :=
  Submodule.Quotient.equiv f.range (Hom.hom f').range eI ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
exact (exactS.hasInjectiveDimensionLT_X₃_iff n inferInstance).symm.trans
      ((ih eCoker).trans (exactS'.hasInjectiveDimensionLT_X₃_iff n inferInstance))

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      ι.map
        (ι.preimage
          (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
            kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))

Tactic:
← Functor.map_comp

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map
      ((Λ.chainComplexXIso X n).hom ≫
        ι.preimage
          (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
            kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))
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}) ↔
    Nonempty (Limits.colimit (constPUnitFunctor D) ≅ PUnit.{(max v u v₂ u₂) + 1})

Tactic:
exact Equiv.nonempty_congr <| Iso.isoCongrLeft <|
    CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

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

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : (Pi.eval I s).obj c ⟶ d),
    ∃ c' t, (Pi.eval I s).map t ≫ s_1 = (Pi.eval I s).map t ≫ s'

Tactic:
· intro d c f g
    let c't : (∀ s, (c' : I s) × (c' ⟶ c s)) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨eq f g, eqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using eq_condition _ _

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
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
by
  rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
X : C
⊢ IsIso (⊤.ι.app X)

Tactic:
isIso_iff_bijective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
X : C
⊢ Function.Bijective ⇑(hom (⊤.ι.app X))
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (GrothendieckTopology C)
⊢ (sInf T).toPretopology = sInf (GrothendieckTopology.toPretopology '' T)

Tactic:
by
  ext X S
  simp [mem_sInf, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.mem_sInf]

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 : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
⊢ FamilyOfElements.restrict ⋯ x.sieveExtend = x

Tactic:
funext Y f hf
  exact extend_agrees t hf

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 : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ x₁ = x₂

Tactic:
rw [← extend_restrict t₁, ← extend_restrict t₂]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible
t₂ : x₂.Compatible
h : FamilyOfElements.restrict ⋯ x₁ = FamilyOfElements.restrict ⋯ x₂
⊢ (FamilyOfElements.restrict ⋯ x₁).sieveExtend = (FamilyOfElements.restrict ⋯ x₂).sieveExtend
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
x : FamilyOfElements P S.arrows
t : x.Compatible
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)

Tactic:
by
  simpa using t (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

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✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
⊢ GaloisInsertion (functorPushforward F) (functorPullback F)

Tactic:
by
  apply (functor_galoisConnection F X).toGaloisInsertion
  intro S Y f hf
  refine ⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, ?_⟩
  simpa using hf

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro q x hx
    apply Exists.imp _ (q _ hx.sieveExtend)
    intro t ht
    simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht

Goal state after: