mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ((foldl Q f hf) n) (a * b) = ((foldl Q f hf) (((foldl Q f hf) n) a)) b

Tactic:
← foldr_reverse,

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) n) (reverse (a * b)) = ((foldl Q f hf) (((foldl Q f hf) n) a)) b
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 (a * b)) = ((foldl Q f hf) (((foldl Q f hf) n) a)) b

Tactic:
← foldr_reverse,

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) n) (reverse (a * b)) = ((foldr Q f hf) (((foldl Q f hf) n) a)) (reverse b)
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 (a * b)) = ((foldr Q f hf) (((foldl Q f hf) n) a)) (reverse b)

Tactic:
← foldr_reverse,

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) n) (reverse (a * b)) = ((foldr Q f hf) (((foldr Q f hf) n) (reverse a))) (reverse b)
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
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldl Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldl (fun m n ↦ (f n) m) n l

Tactic:
← foldr_reverse,

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
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (reverse (List.map (⇑(ι Q)) l).prod) = List.foldl (fun m n ↦ (f n) m) n l
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 : MultilinearMap R M M₂
x y : M p
⊢ mk' (fun m ↦ f (p.insertNth (x + y) m)) ⋯ ⋯ =
    mk' (fun m ↦ f (p.insertNth x m)) ⋯ ⋯ + mk' (fun m ↦ f (p.insertNth y m)) ⋯ ⋯

Tactic:
by ext; simp [map_insertNth_add]

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

Goal state before:
pp: case mem_mul_mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive ((algebraMap R (CliffordAlgebra Q)) r * b) ⋯

Tactic:
simp_rw [← Algebra.smul_def]
      exact range_ι_pow _ (Submodule.smul_mem _ _ hb)

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ ∈ powersetCard α m

Tactic:
simp [Finset.card_compl, mem_iff.mp s.2]

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
⊢ Fintype.card α - n = m
Module: Mathlib.Data.Set.PowersetCard

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

Tactic:
rw [Set.nontrivial_coe_sort, ← Set.one_lt_ncard_iff_nontrivial, ← Nat.card_coe_set_eq,
      powersetCard.card]
    by_contra!
    rw [Nat.le_one_iff_eq_zero_or_eq_one] at this
    rw [ENat.card_eq_coe_natCard] at h2
    norm_cast at h2
    rcases this with h | h
    · rw [Nat.choose_eq_zero_iff] at h
      exact (lt_self_iff_false n).mp (lt_trans h2 h)
    · rw [Nat.choose_eq_one_iff] at h
      aesop

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

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
hf0 : toTrivSqZeroExt ((algebraMap R (ExteriorAlgebra R M)) r) = (0, x)
⊢ x = 0 ∧ r = 0

Tactic:
AlgHom.commutes

Goal state after:
case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
hf0 : (algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
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:
hx.2,

Goal state after:
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)) 0 = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * ((ι R) (f (i.pred h).succ) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod) = (ι R) (f 0) * 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
Fin.succ_pred,

Goal state after:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * ((ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod) = (ι R) (f 0) * 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
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 : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
⊢ (TrivSqZeroExt.sndHom R N ∘ₗ toTrivSqZeroExt.toLinearMap) ∘ₗ (map f).toLinearMap =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ toTrivSqZeroExt.toLinearMap

Tactic:
conv_lhs => rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map,
                AlgHom.comp_toLinearMap, ← LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
⊢ (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ toTrivSqZeroExt.toLinearMap =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ toTrivSqZeroExt.toLinearMap
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
i : J
x : ↑(F.obj i)
⊢ (r + s) • M.mk F ⟨i, x⟩ = r • M.mk F ⟨i, x⟩ + s • M.mk F ⟨i, x⟩

Tactic:
simp [_root_.add_smul, colimit_add_mk_eq']

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

Goal state before:
pp: 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:
by
  apply le_antisymm
  · rw [span_le]
    rintro - ⟨y, ⟨y_mem, rfl⟩⟩
    apply ExteriorAlgebra.ιMulti_range R n
    simp
  · rw [ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map, ← hs, map_span, span_pow, span_le]
    rintro x hx
    obtain ⟨f, rfl⟩ := Set.mem_pow.mp hx
    refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩
    · rw [Set.mem_ofPred_eq, Set.range_comp, Set.image_subset_iff]
      apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)
      grind
    · rw [ExteriorAlgebra.ιMulti_apply]
      apply congrArg (List.prod ∘ List.ofFn)
      ext i
      obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2
      rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]

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

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) (f ≫ g)) =
    freeYonedaEquiv
      ((ConcreteCategory.hom ((pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).map g))
        ((freeYonedaEquiv.trans freeYonedaEquiv.symm) f))

Tactic:
dsimp
    erw [Equiv.apply_symm_apply, freeYonedaEquiv_comp]
    conv_rhs => erw [freeYonedaEquiv_comp]
    erw [Equiv.apply_symm_apply]
    rfl

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 : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (ρ_ (M.obj Y)).inv))
      ((ModuleCat.Hom.hom (M.map f)) m) =
    (ModuleCat.Hom.hom ((Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      ((ModuleCat.Hom.hom (ρ_ (M.obj X)).inv) m)

Tactic:
erw [rightUnitor_inv_apply, rightUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]

Goal state after:
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 : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (M.map f)) m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] 1 =
    (ConcreteCategory.hom (M.map f)) m ⊗ₜ[↑(R.obj Y)] 1
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
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ x✝

Tactic:
ext1; apply leftUnitor_naturality

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S

Tactic:
let fibincl (i : ι' ⊕ α) (j : fib i) : σ (incl i) := match i with
    | .inl i => j.2.idx
    | .inr i => j.elim (fun _ ↦ i.2.idx.2) (fun i ↦ i.2.idx)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
⊢ (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X

Tactic:
change S ∈ sInf ((fun J : Pretopology C ↦ J.coverings) '' T) X ↔ _
  simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
⊢ ∃ ι Y f, R = ofArrows Y f

Tactic:
let ι := { x : Σ Z, (Z ⟶ X) // R x.2 }
  use ι, fun x ↦ x.1.1, fun x ↦ x.1.2
  exact le_antisymm (fun Z g hg ↦ .mk (⟨⟨_, _⟩, hg⟩ : ι)) fun Z g ⟨x⟩ ↦ x.2

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

Goal state before:
pp: case mp
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

Tactic:
rintro ⟨T, b, c, ⟨i⟩, fac⟩
    exact ⟨_, b, _, ⟨i⟩, by simp [reassoc_of% fac]⟩

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

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : (functorPushforward (𝟭 C) R).arrows f
⊢ R.arrows f

Tactic:
obtain ⟨X, g, h, hg, rfl⟩ := hf

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝¹ : C
R : Sieve X✝¹
X✝ X : C
g : X ⟶ X✝¹
h : X✝ ⟶ (𝟭 C).obj X
hg : R.arrows g
⊢ R.arrows (h ≫ (𝟭 C).map g)
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
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
by
  refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, hg⟩ ↦ ?_⟩
  · obtain ⟨h', hh'⟩ := F.map_surjective h
    use h' ≫ g
    simp only [Functor.map_comp, hh', hcomp, true_and]
    apply R.downward_closed hg
  · use Y, g, 𝟙 _, hg
    simp [hcomp]

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
⊢ G ≤ sheafify J G

Tactic:
intro U s hs
  change _ ∈ J _
  convert! J.top_mem U.unop
  rw [eq_top_iff]
  rintro V i -
  exact G.map i.op hs

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
⊢ (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X

Tactic:
by
      refine ?_ ≪≫ HasColimit.isoOfNatIso (J.diagramCompIso F P X.unop)
      refine
        (isColimitOfPreserves F
              (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
          (colimit.isColimit _)

Goal state after:
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'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
E :
  (ConcreteCategory.hom ((Sheaf.toImage f).hom.app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op ≫ g₁.hom.app (op V))) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op ≫ g₂.hom.app (op V))) ⟨s, hx⟩

Tactic:
have := congr_arg (fun f : F ⟶ G' => f.hom.app _ y) e

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'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
E :
  (ConcreteCategory.hom ((Sheaf.toImage f).hom.app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
this :
  (ConcreteCategory.hom ((Sheaf.toImage f ≫ g₁).hom.app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.toImage f ≫ g₂).hom.app (op V))) y
⊢ (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op ≫ g₁.hom.app (op V))) ⟨s, hx⟩ =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op ≫ g₂.hom.app (op V))) ⟨s, hx⟩
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ { hom := (isoSheafify J ⋯).inv } ≫ { hom := (isoSheafify J ⋯).hom } = 𝟙 ((presheafToSheaf J D).obj P.obj)

Tactic:
by
    ext1
    apply (isoSheafify J P.2).inv_hom_id

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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
⊢ ((Functor.const K).obj S.pt).map f ≫
      (Presheaf.isLimitOfIsSheaf J (F.obj j).obj W ⋯).lift
        (Multifork.ofι (W.index (F.obj j).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app j).app (op i.Y)) ⋯) =
    (Presheaf.isLimitOfIsSheaf J (F.obj i).obj W ⋯).lift
        (Multifork.ofι (W.index (F.obj i).obj) S.pt (fun i_1 ↦ S.ι i_1 ≫ (E.π.app i).app (op i_1.Y)) ⋯) ≫
      (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
dsimp [Presheaf.isLimitOfIsSheaf]

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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
i j : K
f : i ⟶ j
⊢ 𝟙 S.pt ≫ ⋯.amalgamate W (fun x ↦ S.ι x ≫ (E.π.app j).app (op x.Y)) ⋯ =
    ⋯.amalgamate W (fun x ↦ S.ι x ≫ (E.π.app i).app (op x.Y)) ⋯ ≫ (F.map f).hom.app (op X)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫ (J.plusCompIso F P).hom.app X =
    (J.diagramCompIso F P (unop X)).hom.app W ≫ colimit.ι (J.diagram (P ⋙ F) (unop X)) W

Tactic:
delta diagramCompIso plusCompIso
  simp only [Iso.trans_hom, NatIso.ofComponents_hom_app, ←
    Category.assoc]
  erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).fac]
  simp

Goal state after: