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

Goal state before:
pp: case mpr.refine_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (M *ᵥ fun i ↦ f (v i) ⋯) i = 0 i

Tactic:
refine IsFractionRing.injective A K ?_

Goal state after:
case mpr.refine_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ (algebraMap A K) ((M *ᵥ fun i ↦ f (v i) ⋯) i) = (algebraMap A K) (0 i)
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr
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
h2 : ∀ (j : n), 0 < ∑ i, A i j
h✝ : Nonempty n
⊢ A.det ≠ 0

Tactic:
contrapose! h2
    obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2
    wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v
    · refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_
      · rw [Matrix.smul_vecMul, h_vA, smul_zero]
      · obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
        simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
        simp_rw [not_exists, not_lt] at h_sup
        refine ⟨i, ?_⟩
        rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
        exact Ne.lt_of_le hi (h_sup i)
    · obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
      refine ⟨j₀, ?_⟩
      rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
      rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
      refine Finset.sum_le_sum (fun i hi => ?_)
      by_cases h : i = j₀
      · rw [h]
      · exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
P : SL(2, R) → Prop
a b c d : R
hdet : a * d - b * c = 1
⊢ !![a, b; c, d].det = 1

Tactic:
rwa [det_fin_two_of]

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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) }
x : M
⊢ ((ringCon Q).liftₐ ((TensorAlgebra.lift R) ↑f) ⋯) ((ι Q) x) = ↑f x

Tactic:
exact (RingCon.liftₐ_mk _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)

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

Goal state before:
pp: R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ (RingHom.id S₂) (y x✝¹) •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
by
    rw [RingHom.id_apply, RingHom.id_apply, smul_comm]

Goal state after:
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

Goal state after:
case mk
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 ι
fst✝ snd✝ : ι
⊢ polarSym2 (⇑Q) (Sym2.map (l • g) (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))) =
    (Sym2.map l (Quot.mk (Sym2.Rel ι) (fst✝, snd✝))).mul •
      polarSym2 (⇑Q) (Sym2.map g (Quot.mk (Sym2.Rel ι) (fst✝, snd✝)))
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case negSucc
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
a✝ : ℕ
⊢ ↑(Int.negSucc a✝) ∈ A 0

Tactic:
rw [Int.cast_negSucc]
    exact neg_mem (SetLike.natCast_mem_graded _ _)

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

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

Tactic:
hB₁,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
hB₁ : LinearMap.flip B₁ = B₁
x✝ y : M
⊢ ⅟2 • ((B₁ x✝) y + (B₁ x✝) y) = (B₁ x✝) y
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: 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] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
a b : CliffordAlgebra Q
⊢ ((foldr Q f hf) n) (reverse b * reverse a) = ((foldr Q f hf) (((foldr Q f hf) n) (reverse a))) (reverse b)

Tactic:
foldr_mul

Goal state after:
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] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
a b : CliffordAlgebra Q
⊢ ((foldr Q f hf) (((foldr Q f hf) n) (reverse a))) (reverse b) =
    ((foldr Q f hf) (((foldr Q f hf) n) (reverse a))) (reverse b)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) (1 + ↑i)) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i.succ) ⟨(ι Q) w✝ * x, ⋯⟩

Tactic:
refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_)

Goal state after:
case mem.mem_mul.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ (GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).fst =
    (GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).fst

case mem.mem_mul.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
ih : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
w✝ : M
⊢ ↑(GradedMonoid.mk (1 + ↑i) (GradedMonoid.GMul.mul ⟨(ι Q) w✝, ⋯⟩ ⟨x, ⋯⟩)).snd =
    ↑(GradedMonoid.mk ↑i.succ ⟨(ι Q) w✝ * x, ⋯⟩).snd
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin n.succ) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
f : MultilinearMap R M M₂
x y : M 0
m : (i : Fin n) → M i.succ
⊢ (mk' (fun m ↦ f (Fin.cons (x + y) m)) ⋯ ⋯) m =
    (mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯ + mk' (fun m ↦ f (Fin.cons y m)) ⋯ ⋯) m

Tactic:
exact cons_add f m x y

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (x y : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (x + y)) t) =
      (f fun t ↦ Sum.rec u (update m i x) t) + f fun t ↦ Sum.rec u (update m i y) t

Tactic:
let := Classical.decEq ι; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
u : (i : ι) → N (Sum.inl i)
⊢ ∀ [inst : DecidableEq ι'] (m : (i : ι') → N (Sum.inr i)) (i : ι') (c : R) (x : N (Sum.inr i)),
    (f fun t ↦ Sum.rec u (update m i (c • x)) t) = c • f fun t ↦ Sum.rec u (update m i x) t

Tactic:
let := Classical.decEq ι; simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
a : α
s : Finset α
s_mem : s ∈ powersetCard α n
mem_s : a ∈ s
⊢ ∃ b ∈ SetLike.coe '' powersetCard α n, a ∈ b

Tactic:
exact ⟨↑s, mem_image_of_mem SetLike.coe s_mem, mem_coe.mpr mem_s⟩

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
x : M
r : R
hx : x = 0 ∧ r = 0
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) r = 0

Tactic:
rw [hx.2, map_zero]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

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 Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }

Tactic:
by
    ext1 X
    apply (hc X).uniq ((evaluation R X).mapCocone s)
    intro j
    dsimp
    rw [← hm]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)

Tactic:
by
  rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)

Tactic:
by
  rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

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
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)

Tactic:
by
  let c := limit.cone (uncurry.obj F)
  let P : IsLimit c := limit.isLimit _
  let G := DiagramOfCones.mkOfHasLimits F
  let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _
  have Q' := coneOfConeUncurryIsLimit Q P
  have Q'' := limit.isLimit (F ⋙ lim)
  exact IsLimit.conePointUniqueUpToIso Q' Q''

Goal state after:
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''
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ 1 • ιM m = ιM m

Tactic:
simpa using smul_eq hcR hcM 1 m

Goal state after:
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
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
        (ρ_ (M.obj Y)).symm.hom =
    (ρ_ (M.obj X)).symm.hom ≫ (Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f

Tactic:
by
    ext m
    dsimp [CommRingCat.forgetToRingCat_obj]
    erw [rightUnitor_inv_apply, rightUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
    rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
by
  constructor
  · intro PJ X R hR
    rw [isSheafFor_iff_generate]
    apply PJ (Sieve.generate R) ⟨_, hR, le_generate R⟩
  · rintro PK X S ⟨R, hR, RS⟩
    have gRS : ⇑(generate R) ≤ S := by
      apply giGenerate.gc.monotone_u
      rwa [generate_le_iff]
    apply isSheafFor_subsieve P gRS _
    intro Y f
    rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]
    exact PK (pullbackArrows f R) (K.pullbacks f R hR)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H : (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x

Tactic:
← PullbackCone.IsLimit.lift_fst hc _ _ h,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H : (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ (ConcreteCategory.hom (F.map (PullbackCone.IsLimit.lift hc p₁ p₂ h ≫ c.fst).op)) x =
    (ConcreteCategory.hom (F.map p₂.op)) x
Module: Mathlib.CategoryTheory.Sites.Sheaf

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

Tactic:
isSheaf_iff_isSheaf_of_type

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
⊢ ∀ {X_1 Y : WalkingMulticospan S.shape} (f : X_1 ⟶ Y),
    (S.index (P ⋙ F)).multicospan.map f ≫
        (match Y with
          | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a =>
            Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
      (match X_1 with
          | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a =>
            Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
        ((S.index P).multicospan ⋙ F).map f

Tactic:
rintro (a | b) (a | b) (f | f | f)
      all_goals cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
⊢ ∀ (h₁ : S'.arrows g₃) (h₂ : S'.arrows g₄),
    g₁ ≫ g₃ = g₂ ≫ g₄ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ h₂)

Tactic:
S₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
g₂ : V₃ ⟶ V₂
g₃ : V₁ ⟶ U
g₄ : V₂ ⟶ U
S₁ : S'.arrows g₃
⊢ ∀ (h₂ : S'.arrows g₄),
    g₁ ≫ g₃ = g₂ ≫ g₄ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' g₃ S₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' g₄ h₂)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

Tactic:
isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presieve.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
⊢ ∀ ⦃X Y : K⦄ (f : X ⟶ Y),
    (curry.obj (swap K J ⋙ F) ⋙ lim).map f ≫
        limit.π ((curry.obj (swap K J ⋙ F)).obj Y) j ≫ colimit.ι ((curry.obj F).obj j) Y =
      (limit.π ((curry.obj (swap K J ⋙ F)).obj X) j ≫ colimit.ι ((curry.obj F).obj j) X) ≫
        ((const K).obj (colimit.cocone ((curry.obj F).obj j)).1).map f

Tactic:
intro k k' f
                      simp only [Functor.comp_obj, lim_obj, colimit.cocone_x,
                        Functor.const_obj_obj, Functor.comp_map, lim_map,
                        curry_obj_obj_obj, Prod.swap_obj, limMap_π_assoc, curry_obj_map_app,
                        Prod.swap_map, Functor.const_obj_map, Category.comp_id]
                      rw [map_id_left_eq_curry_map, colimit.w]

Goal state after: