mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
⊢ ∀ (x : CliffordAlgebra Q), P x

Tactic:
refine reverse_involutive.surjective.forall.2 ?_

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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)
⊢ ∀ (x : CliffordAlgebra Q), P (reverse x)
Module: Mathlib.LinearAlgebra.Alternating.Curry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i : Fin n.succ
⊢ ((fun x ↦ g) i) (Fin.cons m v i) = Fin.cons (g m) (fun i ↦ ((fun x ↦ g) i) (v i)) i

Tactic:
cases i using Fin.cases

Goal state after:
case zero
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
⊢ ((fun x ↦ g) 0) (Fin.cons m v 0) = Fin.cons (g m) (fun i ↦ ((fun x ↦ g) i) (v i)) 0

case succ
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i✝ : Fin n
⊢ ((fun x ↦ g) i✝.succ) (Fin.cons m v i✝.succ) = Fin.cons (g m) (fun i ↦ ((fun x ↦ g) i) (v i)) i✝.succ
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) 0)) (tail (update m i (x + y))) =
    (f (update m i x 0)) (tail (update m i x)) + (f (update m i y 0)) (tail (update m i y))

Tactic:
cases i using Fin.cases

Goal state after:
case zero
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
x y : M 0
⊢ (f (update m 0 (x + y) 0)) (tail (update m 0 (x + y))) =
    (f (update m 0 x 0)) (tail (update m 0 x)) + (f (update m 0 y 0)) (tail (update m 0 y))

case succ
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i✝ : Fin n
x y : M i✝.succ
⊢ (f (update m i✝.succ (x + y) 0)) (tail (update m i✝.succ (x + y))) =
    (f (update m i✝.succ x 0)) (tail (update m i✝.succ x)) + (f (update m i✝.succ y 0)) (tail (update m i✝.succ y))
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
c : R
x : M i
⊢ (f (update m i (c • x) 0)) (tail (update m i (c • x))) = c • (f (update m i x 0)) (tail (update m i x))

Tactic:
cases i using Fin.cases

Goal state after:
case zero
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
x : M 0
⊢ (f (update m 0 (c • x) 0)) (tail (update m 0 (c • x))) = c • (f (update m 0 x 0)) (tail (update m 0 x))

case succ
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 : M 0 →ₗ[R] MultilinearMap R (fun i ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
c : R
i✝ : Fin n
x : M i✝.succ
⊢ (f (update m i✝.succ (c • x) 0)) (tail (update m i✝.succ (c • x))) =
    c • (f (update m i✝.succ x 0)) (tail (update m i✝.succ x))
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
⊢ mk' (fun m ↦ f (Fin.cons (x + y) m)) ⋯ ⋯ = mk' (fun m ↦ f (Fin.cons x m)) ⋯ ⋯ + mk' (fun m ↦ f (Fin.cons y m)) ⋯ ⋯

Tactic:
by
    ext m
    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₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
⊢ (f (update m i (x + y) p)) (p.removeNth (update m i (x + y))) =
    (f (update m i x p)) (p.removeNth (update m i x)) + (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
cases i using Fin.succAboveCases p <;> simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ this.toFinset ∈ powersetCard α n

Tactic:
by
    rwa [mem_iff, ← ENat.natCast_inj, ← this.encard_eq_coe_toFinset_card]

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
⊢ ∃ s, a ∈ s ∧ b ∉ s

Tactic:
have ha' : n ≤ Set.encard {b}ᶜ := by
    rwa [← (Set.encard_add_encard_compl {b}).trans (Set.encard_univ α), Set.encard_singleton,
      add_comm, ENat.lt_add_one_iff' (ENat.natCast_ne_top n)] at hα
  obtain ⟨s, has, has', hs⟩ :=
    Set.exists_superset_subset_encard_eq (s := {a}) (by simp [Ne.symm hab]) (by simpa) ha'
  have : Set.Finite s := Set.finite_of_encard_eq_coe hs
  exact ⟨⟨Set.Finite.toFinset this, by
    rwa [mem_iff, ← ENat.natCast_inj, ← this.encard_eq_coe_toFinset_card]⟩,
      by simpa using has, by simpa using has'⟩

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₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap R (fun i ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x : R
y : M i
⊢ (f (update m i (x • y) p)) (p.removeNth (update m i (x • y))) = x • (f (update m i y p)) (p.removeNth (update m i y))

Tactic:
cases i using Fin.succAboveCases p <;> simp

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

Goal state before:
pp: case e_5.e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) = fun x_1 ↦ x

pp: case e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x ↦ y

Tactic:
· ext
    rw [finSumEquivOfFinset_inl, Finset.piecewise_eq_of_mem]
    apply Finset.orderEmbOfFin_mem

Goal state after:
case e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x ↦ y
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case succ
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
⊢ (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f (n + 1)) v

Tactic:
rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]

Goal state after:
case succ
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
⊢ (f n.succ) (Matrix.vecCons (v 0) fun i ↦ v i.succ) = (f (n + 1)) v
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
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 = ⊤
⊢ span R (⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s}) ≤ ⋀[R]^n M

Tactic:
rw [span_le]

Goal state after:
case a
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 = ⊤
⊢ ⇑(ExteriorAlgebra.ιMulti R n) '' {a | range a ⊆ s} ⊆ ↑(⋀[R]^n M)
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
⊢ Module.rank R ↑S.X₂ = ↑(n + p)

Tactic:
rw [free_shortExact_rank_add hS', ← hN, ← hP]

Goal state after:
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
⊢ Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(finrank R ↑S.X₁ + finrank R ↑S.X₃)
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
⊢ s.pt.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s)) =
    (hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f

Tactic:
apply (isLimitOfPreserves (ModuleCat.restrictScalars (R.map f).hom) (hc Y)).hom_ext
        intro j
        have h₁ := (c.π.app j).naturality f
        have h₂ := (hc X).fac ((evaluation R X).mapCone s) j
        rw [Functor.mapCone_π_app, assoc, assoc, ← Functor.map_comp, IsLimit.fac]
        dsimp at h₁ h₂ ⊢
        rw [h₁, reassoc_of% h₂, Hom.naturality]

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ (F.map fj).app k ≫ ((D.obj j').ι.app k ≫ ((const K).obj (D.obj j').pt).map fk) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp only [Functor.const_obj_map, Category.assoc]

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ (F.map fj).app k ≫ (D.obj j').ι.app k ≫ 𝟙 (D.obj j').pt ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
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''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    (ιR cR) r • (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (ιM m)

Tactic:
h₂,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    (ιR cR) r • (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
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
hro : RightOreCondition C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ {S | ∃ Y f, S.arrows f} → Sieve.pullback f S ∈ {S | ∃ Y_1 f, S.arrows f}

Tactic:
by
    rintro X Y S h ⟨Z, f, hf⟩
    rcases hro h f with ⟨W, g, k, comm⟩
    refine ⟨_, g, ?_⟩
    simp [comm, hf]

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

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ x' = (hom ↑(Fork.IsLimit.lift' t y' hy')) PUnit.unit

Tactic:
suffices (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1 by
    rw [← this]

Goal state after:
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : (hom g) y = (hom h) y
y' : PUnit.{u + 1} ⟶ Y := ↾fun x ↦ y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : (hom f) x' = y
⊢ (fun x ↦ x') = ⇑(hom ↑(Fork.IsLimit.lift' t y' hy'))
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f

Tactic:
have ht := H.choose_spec.1 f.obj.hom f.property

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
ht :
  (ConcreteCategory.hom ((yoneda.obj s.pt).map f.obj.hom.op)) (Exists.choose H) =
    S.arrows.yonedaFamilyOfElements_fromCocone s f.obj.hom ⋯
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f
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
S : Sieve X
x : FamilyOfElements P S.arrows
⊢ x.SieveCompatible → x.Compatible

Tactic:
intro h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x 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
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g

Tactic:
← hf

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : Mono f
S : Sieve Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ = g
hg₁ : S.arrows g₁
⊢ S.arrows g₁
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
⊢ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
· intro x hx
    use hS.amalgamate _ (hx.restrict h)
    intro W j hj
    apply (trans hj).ext
    intro Y f hf
    rw [← comp_apply, ← Functor.map_comp, ← op_comp, hS.valid_glue (hx.restrict h) _ hf,
      FamilyOfElements.restrict, ← hx (𝟙 _) f (h _ _ hf) _ (id_comp _)]
    simp

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p

Tactic:
· intro i x hx
    simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
    obtain ⟨y, rfl⟩ := hp _ x
    exact ⟨y, hx, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj.map i.f.op = S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
erw [← hm, Category.assoc, ← (E.π.app k).naturality, Category.assoc]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (((Functor.const K).obj E.pt).obj k).map i.f.op ≫ (E.π.app k).app (op i.Y) =
    m ≫ (W.multifork E.pt).ι i ≫ (E.π.app k).app (op i.Y)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsClosed X ↔ ∀ (j : J), IsClosed (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
by
  simp only [← isOpen_compl_iff, isOpen_iff_of_isColimit _ hc,
    Functor.const_obj_obj, Set.preimage_compl]

Goal state after: