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

Goal state before:
pp: n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
by_cases h : i = j₀

Goal state after:
case pos
n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

case neg
n✝ : Type u_1
inst✝⁵ : Fintype n✝
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A i) a ^ n * (of A i) a = (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
n_ih,

Goal state after:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a) * (of A i) a =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)
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
⊢ ((DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r).comp (of A i)) xi =
    ((AddMonoidHom.mul ((of A 0) (GAlgebra.toFun r))).comp (of A i)) xi

Tactic:
dsimp only [AddMonoidHom.comp_apply, DistribSMul.toAddMonoidHom_apply,
      AddMonoidHom.mul_apply]

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) (GAlgebra.toFun r) * (of A i) xi
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 ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| r

Tactic:
rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike σ M
inst✝² : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝¹ : Decomposition ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
| (decompose ℳ).symm (∑ i ∈ DFinsupp.support ((decompose ℳ) r), (of (fun i ↦ ↥(ℳ i)) i) (((decompose ℳ) r) i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: 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
g : ι → M
l : ι → R
p : Sym2 ι
⊢ polarSym2 (⇑Q) (Sym2.map (l • g) p) = (Sym2.map l p).mul • polarSym2 (⇑Q) (Sym2.map g p)

Tactic:
obtain ⟨_, _⟩ := p; simp [← smul_assoc, mul_comm]

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ F ((of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = F ((of A i) ai) * F ((of A j) aj)

Tactic:
rw [← F.map_mul (of A i ai), of_mul_of ai]

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

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
c : K
hz : c • x ∈ K ∙ x
⊢ c * ((B x) y + -(B x) y) = 0

Tactic:
add_neg_cancel,

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
y : V
c : K
hz : c • x ∈ K ∙ x
⊢ c * 0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
let b :=
    Basis.mkFinCons x v'
      (by
        rintro c y hy hc
        rw [add_eq_zero_iff_neg_eq] at hc
        rw [← hc, Submodule.neg_mem_iff] at hy
        have := (isCompl_span_singleton_orthogonal hx).disjoint
        rw [Submodule.disjoint_def] at this
        have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
        exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _)
      (by
        intro y
        refine ⟨-B x y / B x x, fun z hz => ?_⟩
        obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
        rw [map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
          div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero])

Goal state after:
case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
⊢ ∃ v, IsOrthoᵢ B ⇑v
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case e_fst.algebraMap
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
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
r : R
⊢ (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) ((algebraMap R (CliffordAlgebra Q)) r)).1 = (algebraMap R (CliffordAlgebra Q)) r

Tactic:
simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: case refine_2
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'
⊢ ∀ (m : M) (x : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    ((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m)
        (((LinearMap.mk₂ R (fun m f i ↦ (f i.succ).curryLeft m) ⋯ ⋯ ⋯ ⋯) m) x) =
      0 m • x

Tactic:
· -- when applied twice with the same `m`, this recursive step produces 0
    intro m x
    ext
    simp

Goal state after:
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 : ℕ
F : MultilinearMap R (fun x ↦ M) (ExteriorAlgebra R M) :=
  (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)).compLinearMap fun x ↦ ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ F f = 0

Tactic:
dsimp [F]
      clear F
      wlog h : x < y
      · exact this R n f y x hfxy.symm hxy.symm (hxy.lt_or_gt.resolve_left h)
      clear hxy
      induction n with
      | zero => exact x.elim0
      | succ n hn =>
        rw [List.ofFn_succ, List.prod_cons]
        by_cases hx : x = 0
        -- one of the repeated terms is on the left
        · rw [hx] at hfxy h
          rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
          exact ι_mul_prod_list (f ∘ Fin.succ) _
        -- ignore the left-most term and induct on the remaining ones, decrementing indices
        · convert! mul_zero (ι R (f 0))
          refine
            hn
              (fun i => f <| Fin.succ i) (x.pred hx)
              (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) ?_
              (Fin.pred_lt_pred_iff.mpr h)
          simp only [Fin.succ_pred]
          exact hfxy

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ (Hom.hom S.f).ker = ⊥

Tactic:
LinearMap.ker_eq_bot,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
hv : LinearIndependent R v
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
hm : Mono S.f
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Function.Injective ⇑(Hom.hom S.f)
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

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

Tactic:
let eM : M ≃ₗ[R] ModuleCat.of R (ULift.{v'} M) := ULift.moduleEquiv.symm
  rw [hasInjectiveDimensionLE_iff_of_linearEquiv_aux eM,
    ← hasInjectiveDimensionLE_iff_of_linearEquiv_aux (e.symm.trans eM)]

Goal state after:
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
hf : Surjective ⇑f
⊢ Surjective ⇑(map n f)

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, ← ιMulti_span, ← ιMulti_span,
    Submodule.map_span, ← Set.range_comp, ← LinearMap.coe_compAlternatingMap, map_comp_ιMulti,
    AlternatingMap.coe_compLinearMap, Set.range_comp]
  conv_rhs => rw [← Set.image_univ]
  congr
  rw [Set.range_eq_univ]
  exact Surjective.comp_left hf

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ mk 0 s = 0

Tactic:
zero_mk

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ 0 = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
x✝ : y ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
x : LocalizedModule S M₀
m : M₀
s : ↥S
hx : ((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (mk m s) = y
⊢ ((IsLocalizedModule.map S (mkLinearMap S M₁) (mkLinearMap S M₂)) h) y = 0

Tactic:
rw [← hx, map_LocalizedModules, map_LocalizedModules, (ex (g m)).2 ⟨m, rfl⟩, zero_mk]

Goal state after:
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
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ s.pt.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        ((hc Y).lift ((evaluation R Y).mapCone s) ≫ ((evaluation R Y).mapCone c).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)

Tactic:
IsLimit.fac

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
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
h₂ :
  (hc X).lift ((evaluation R X).mapCone s) ≫ ((evaluation R X).mapCone c).π.app j = ((evaluation R X).mapCone s).π.app j
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone s).π.app j) =
    (hc X).lift ((evaluation R X).mapCone s) ≫
      c.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (((evaluation R Y).mapCone c).π.app j)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[S] (1 ⊗ₜ[R] m) =
    (Hom.hom (↟↑(AlgebraTensorModule.rid R S S) ▷ (extendScalars f).obj M))
      ((Hom.hom (↟↑(AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M))) (1 ⊗ₜ[R] (1 ⊗ₜ[R] m)))

Tactic:
erw [AlgebraTensorModule.distribBaseChange_tmul,
          MonoidalCategory.whiskerRight_apply,
          AlgebraTensorModule.rid_tmul]

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ 1 ⊗ₜ[S] (1 ⊗ₜ[R] m) = (1 • 1) ⊗ₜ[S] (1 ⊗ₜ[R] m)
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip := ⋯
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) := ⋯
⊢ IsColimit (Cocone.whisker (Prod.braiding J₁ J₂).functor ((Cocone.precompose E₁.inv).obj (G.flip.mapCocone₂ c₁ c₂)))

Tactic:
refine IsColimit.equivOfNatIsoOfIso (Iso.refl _) (G.mapCocone₂ c₂ c₁) _ ?_ |>.toFun <|
      isColimitOfPreserves₂ G hc₂ hc₁

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
⊢ (Cocone.precompose (Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))).inv).obj
      (G.mapCocone₂ c₂ c₁) ≅
    Cocone.whisker (Prod.braiding J₁ J₂).functor ((Cocone.precompose E₁.inv).obj (G.flip.mapCocone₂ c₁ c₂))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
rw [← ModuleCat.epi_iff_surjective]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)}
R : Sieve X
H₂ : ∀ ⦃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)}
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ ∃ Z g, R.arrows (g ≫ f)

Tactic:
exact ⟨W, h ≫ g, by simpa using H₄⟩

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)

Tactic:
refine Nonempty.intro ?_

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ IsColimit S.arrows.cocone
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case inl
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 x✝³ x✝² x✝¹ : Sieve X
h₁ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝³.arrows f → x✝¹.arrows f
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), x✝².arrows f → x✝¹.arrows f
x✝ : C
f : x✝ ⟶ X
hf : x✝³.arrows f
⊢ x✝¹.arrows f

Tactic:
exact h₁ _ 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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
⊢ (FamilyOfElements.functorPullback F x).Compatible

Tactic:
intro Z₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ : D
⊢ ∀ ⦃Y₂ Z_1 : D⦄ (g₁ : Z_1 ⟶ Z₁) (g₂ : Z_1 ⟶ Y₂) ⦃f₁ : Z₁ ⟶ Z⦄ ⦃f₂ : Y₂ ⟶ Z⦄ (h₁ : Presieve.functorPullback F T f₁)
    (h₂ : Presieve.functorPullback F T f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.op ⋙ P).map g₁.op)) (FamilyOfElements.functorPullback F x f₁ h₁) =
        (ConcreteCategory.hom ((F.op ⋙ P).map g₂.op)) (FamilyOfElements.functorPullback F x f₂ h₂)
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₁

Goal state after:
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
Z₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ Z₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Z₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (Q.map g₁.op)) (x.map f f₁ h₁) = (ConcreteCategory.hom (Q.map g₂.op)) (x.map f f₂ h₂)
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
R : Sieve Y
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
x✝ : ∃ g, g ≫ f = f✝ ∧ R.arrows g
h : Z✝ ⟶ Y✝
j : Y✝ ⟶ Y
k : j ≫ f = f✝
z : R.arrows j
⊢ R.arrows (h ≫ j)

Tactic:
by simp [z]

Goal state after: