mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ solution.π.range = ⊤ ↔ Submodule.span A (Set.range solution.var) = ⊤

Tactic:
range_π

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Submodule.span A (Set.range solution.var) = ⊤ ↔ Submodule.span A (Set.range solution.var) = ⊤
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x = (iterateFrobenius R p n) y
⊢ x = y

Tactic:
rw [← sub_eq_zero] at H ⊢

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x - (iterateFrobenius R p n) y = 0
⊢ x - y = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
x✝¹ x✝ : m → R
hxy : M *ᵥ x✝¹ = M *ᵥ x✝
⊢ M *ᵥ x✝ - M *ᵥ x✝ = 0

Tactic:
sub_self

Goal state after:
m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
x✝¹ x✝ : m → R
hxy : M *ᵥ x✝¹ = M *ᵥ x✝
⊢ 0 = 0
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
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ ↥(rootsOfUnity k R)

Tactic:
by
    refine ⟨⟨x, ↑x ^ (k - 1 : ℕ), ?_, ?_⟩, ?_⟩
    all_goals
      rcases x with ⟨x, hx⟩; rw [mem_nthRoots <| NeZero.pos k] at hx
      simp only [← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le NeZero.one_le]
    simp only [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, hx, Units.val_one]

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

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), (((associatedHom K) Q) (v i)) (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
associated_eq_self_apply

Goal state after:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), Q (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

Tactic:
rcases isEmpty_or_nonempty n with hn | hn

Goal state after:
case inl
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

case inr
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : Nonempty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inr.refine_1
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
h : A ∈ center (SpecialLinearGroup n R)
⊢ ↑A i i ^ Fintype.card n = 1

Tactic:
have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
    simpa using! this

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

Goal state before:
pp: case e'_1
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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ ⟨g.toLinearMap ∘ₗ ι Q, ⋯⟩ = ⟨f, cond⟩

Tactic:
Subtype.mk_eq_mk

Goal state after:
case e'_1
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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ g.toLinearMap ∘ₗ ι Q = f
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
⊢ f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b

Tactic:
rw [f.map_add, mul_add, add_mul, add_mul]

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
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑((head :: tail).dProd fι fA) = (List.map (fun a ↦ ↑(fA a)) (head :: tail)).prod

Tactic:
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons,
      SetLike.coe_list_dProd _ _ _ tail]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ r • (of A i) xi = (of A 0) (GAlgebra.toFun r) * (of A i) xi

Tactic:
DirectSum.of_mul_of,

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ r • (of A i) xi = (of A (0 + i)) (GradedMonoid.GMul.mul (GAlgebra.toFun r) xi)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : AddMonoid ι
inst✝ : Semiring R
i j : ι
a b : R
⊢ (of (fun x ↦ R) i) a * (of (fun x ↦ R) j) b = (of (fun i ↦ R) (i + j)) (a * b)

Tactic:
DirectSum.of_mul_of,

Goal state after:
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : AddMonoid ι
inst✝ : Semiring R
i j : ι
a b : R
⊢ (of (fun x ↦ R) (i + j)) (GradedMonoid.GMul.mul a b) = (of (fun i ↦ R) (i + j)) (a * b)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(n✝ + 1) ∈ A 0

Tactic:
rw [Nat.cast_succ]

Goal state after:
case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 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:
rw [← separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂,
    separatingRight_toLinearMap₂'_iff]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).Nondegenerate ↔ M.det ≠ 0

Tactic:
by
  rw [nondegenerate_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]

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
m : M
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) 1) ⟨(ι Q) m, ⋯⟩ * (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) 1) ⟨(ι Q) m, ⋯⟩ =
    (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)

Tactic:
DirectSum.of_mul_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
m : M
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι Q) m, ⋯⟩ ⟨(ι Q) m, ⋯⟩) =
    (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ 1 < #↑s ↔ 1 < n

Tactic:
card_eq

Goal state after:
α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ 1 < n ↔ 1 < n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ 1 < (Nat.card α).choose n

Tactic:
by_contra!

Goal state after:
case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
this : (Nat.card α).choose n ≤ 1
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
suffices
    (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R]
      ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N by
    refine LinearMap.compr₂ this ?_
    refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
    exact AlternatingMap.constLinearEquivOfIsEmpty.symm
  refine CliffordAlgebra.foldl _ ?_ ?_
  · refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
    all_goals
      ext i : 1
      simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]
  · -- when applied twice with the same `m`, this recursive step produces 0
    intro m x
    ext
    simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
⊢ (Hom.hom S.g) m = (Hom.hom S.g) m'

Tactic:
← hm,

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
⊢ (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (Hom.hom S.g) m'
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R) m = ↑(f i)
⊢ (ExteriorAlgebra.ι R) (ExteriorAlgebra.ιInv ↑(f i)) = ↑(f i)

Tactic:
← hm,

Goal state after:
case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R) m = ↑(f i)
⊢ (ExteriorAlgebra.ι R) (ExteriorAlgebra.ιInv ((ExteriorAlgebra.ι R) m)) = (ExteriorAlgebra.ι R) m
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
⊢ ↑⊤ ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n

Tactic:
by_contra!

Goal state after:
case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
this : (↑⊤ ≠ ⊤ ∧ ∀ (n : ℕ), ¬HasInjectiveDimensionLE X n) ∨ ↑⊤ = ⊤ ∧ ∃ n, HasInjectiveDimensionLE X n
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: R : Type u_3
inst✝⁵ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
n p : ℕ
inst✝⁴ : Free R ↑S.X₁
inst✝³ : Free R ↑S.X₃
inst✝² : Module.Finite R ↑S.X₁
inst✝¹ : Module.Finite R ↑S.X₃
hN : finrank R ↑S.X₁ = n
hP : finrank R ↑S.X₃ = p
inst✝ : StrongRankCondition R
⊢ finrank R ↑S.X₂ = n + p

Tactic:
by
  apply finrank_eq_of_rank_eq
  rw [free_shortExact_rank_add hS', ← hN, ← hP]
  simp only [Nat.cast_add, finrank_eq_rank]

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 := ⋯ }
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
have : Injective (ModuleCat.of R I) := by
      rw [← Module.injective_iff_injective_object]
      exact Module.Injective.of_ringEquiv eR.symm eI.symm

Goal state after:
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)
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

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

Tactic:
← hm,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
X : Cᵒᵖ
j : J
⊢ m.app X ≫ (c.π.app j).app X = (m ≫ c.π.app j).app 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₂
⊢ m₁ ⊗ₜ[S] (ConcreteCategory.hom ((extendRestrictScalarsAdj f).counit.app M₂)) (1 ⊗ₜ[R] m₂) = m₁ ⊗ₜ[S] m₂

Tactic:
extendRestrictScalarsAdj_counit_app_apply_one_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₂
⊢ m₁ ⊗ₜ[S] m₂ = m₁ ⊗ₜ[S] m₂
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsPreconnected C
inst✝ : HasColimit (constPUnitFunctor C)
a b : colimit (constPUnitFunctor C)
⊢ a = b

Tactic:
obtain ⟨c, ⟨⟩, rfl⟩ := jointly_surjective' a
    obtain ⟨d, ⟨⟩, rfl⟩ := jointly_surjective' b
    apply constant_of_preserves_morphisms (colimit.ι (constPUnitFunctor C) · PUnit.unit)
    exact fun c d f => colimit_sound f rfl

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)

Tactic:
refine ⟨Set.range (fromInitialModel J).obj, inferInstance, fun i => ?_⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : InitiallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromInitialModel J).obj, Nonempty (j ⟶ i)
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:
← cancel_mono (colimitUncurryIsoColimitCompColim F).inv

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
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) ≫
      (colimitUncurryIsoColimitCompColim F).inv =
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j) ≫ (colimitUncurryIsoColimitCompColim F).inv
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ x ∈ G.obj U

Tactic:
← IsIso.inv_hom_id_apply (G.ι.app U) x

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
H : IsIso G.ι
U : C
x : F.obj U
⊢ (hom (G.ι.app U)) ((hom (inv (G.ι.app U))) x) ∈ G.obj U
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
X : C
S : Sieve X
⊢ S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
    ∀ (R : Sieve X),
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
        R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
H₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
⊢ ∀ (R : Sieve X),
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
        S.arrows f → Sieve.pullback f R ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}) →
      R ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
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
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
⊢ S.bind T ≤ S

Tactic:
rintro Y f ⟨Z, e1, e2, h1, _, h3⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
⊢ ∀ (f_1 : W ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1

Tactic:
a

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
⊢ pullback f (ofObjects X Y) = ofObjects X Z

Tactic:
ext
  simp [Sieve.ofObjects]

Goal state after:
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
x : FamilyOfElements P R
h : x.Compatible
⊢ (x.map f).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq
  unfold FamilyOfElements.map
  rwa [← NatTrans.naturality_apply, ← NatTrans.naturality_apply, h]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f →
    ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
      (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
        (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩

Tactic:
rintro rfl Y f hf
    simp [shrinkYonedaEquiv_naturality, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_shrinkYoneda_map]

Goal state after: