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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ i, w i • ∑ j, A i j • v j = 0
⊢ w = 0

Tactic:
simp_rw [Finset.smul_sum, ← smul_assoc] at hw

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, ∑ x_1, (w x • A x x_1) • v x_1 = 0
⊢ w = 0
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype ι
inst✝² : Finite κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ (toLin b c') ((toMatrix b' c') f * b'.toMatrix ⇑b) = f

Tactic:
toLin_mul b b' c',

Goal state after:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype ι
inst✝² : Finite κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ (toLin b' c') ((toMatrix b' c') f) ∘ₗ (toLin b b') (b'.toMatrix ⇑b) = f
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) _root_.id

Tactic:
ext
  simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id,
    Finsupp.mapDomain_equiv_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then 1 else ↑r⁻¹ else if i_1 = i then ↑r else 1) = 1

Tactic:
funext j

Goal state after:
case refine_1
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then 1 else ↑r⁻¹ else if j = i then ↑r else 1) = 1 j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ (fun i_1 ↦ if i_1 = i then if i_1 = i then ↑r⁻¹ * ↑r else ↑r else if i_1 = i then ↑r⁻¹ else 1) = 1

Tactic:
funext j

Goal state after:
case refine_2
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i j : n
⊢ (if j = i then if j = i then ↑r⁻¹ * ↑r else ↑r else if j = i then ↑r⁻¹ else 1) = 1 j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
⊢ Matrix.toLin' ↑A ∘ₗ Matrix.toLin' ↑A⁻¹ = LinearMap.id

Tactic:
rw [← toLin'_mul, ← coe_mul, mul_inv_cancel, coe_one, toLin'_one]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) =
    diagonal fun i ↦
      match i with
      | 0 => a
      | 1 => a⁻¹

Tactic:
simp [diag2n_coe]

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

Goal state before:
pp: case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [diag2n_coe]

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

Goal state before:
pp: case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [diag2n_coe]

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

Goal state before:
pp: case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [diag2n_coe]

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

Goal state before:
pp: case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ ↑(diag2 a ha) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![a, 0; 0, a⁻¹] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [diag2n_coe]

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 : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Submodule.map ((lift Q) ⟨f, cond⟩).toLinearMap (ι Q).range = f.range

Tactic:
by
  rw [← LinearMap.range_comp, ι_comp_lift]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
h : LeftInverse ⇑g ⇑f
⊢ LeftInverse ⇑(map g) ⇑(map f)

Tactic:
intro x
  replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h
  rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ (((toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w

Tactic:
simp_rw [Matrix.toLinearMap₂'_apply, dotProduct, Matrix.mulVec, dotProduct]

Goal state after:
n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ ∑ i, ∑ j, v i •> w j •> M i j = ∑ x, v x * ∑ x_1, M x x_1 * w x_1
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (fun a b ↦ ((toAddMonoid fun x ↦ ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') = fun x ai ↦
    DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
funext x

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b ↦ ((toAddMonoid fun x_1 ↦ ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip b) a') = fun ai ↦
    DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

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

Tactic:
nondegenerate_toLinearMap₂'_iff,

Goal state after:
R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ M.Nondegenerate ↔ M.det ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
Q : QuadraticForm R N
⊢ (toMatrix b Q).IsSymm

Tactic:
ext i j
  rw [toMatrix, Matrix.transpose_apply, LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂_apply,
    ← QuadraticMap.associated_isSymm]

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

Goal state before:
pp: n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
⊢ ∃ a, ofFinEmb n β a = ⟨s, hs⟩

Tactic:
obtain ⟨f : Fin n ↪ β, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])

Goal state after:
n : ℕ
β : Type u_2
s : Finset β
hs : s ∈ powersetCard β n
f : Fin n ↪ β
hf : Finset.map f Finset.univ = s
⊢ ∃ a, ofFinEmb n β a = ⟨s, hs⟩
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
⊢ ∀ (e : Ext Y S.X₂ i), e = 0

Tactic:
x₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ x₂ = 0
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₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Epi S.g
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w

Tactic:
ModuleCat.epi_iff_surjective

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₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
have exactS := ModuleCat.shortComplex_shortExact S
      f.exact_map_mkQ_range injf (Submodule.mkQ_surjective _)

Goal state after:
case succ
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v, u'} R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
I' : ModuleCat R'
injective✝ : Injective I'
f' : N ⟶ I'
mono✝ : Mono f'
this✝ : Module.Injective R' ↑I'
injf' : Function.Injective ⇑(Hom.hom f')
S' : ShortComplex (ModuleCat R') := shortComplexOfCompEqZero (Hom.hom f') (Hom.hom f').range.mkQ ⋯
exactS' : S'.ShortExact
I : ModuleCat R :=
  let this := Module.compHom (↑I') eR.toRingHom;
  of R ↑I'
eI : ↑I ≃ₛₗ[↑eR] ↑I' :=
  let __spread.0 := AddEquiv.refl ↑I;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
this : Injective (of R ↑I)
f : ↑M →ₗ[R] ↑I := ↑eI.symm ∘ₛₗ Hom.hom f' ∘ₛₗ ↑e
injf : Function.Injective ⇑f
S : ShortComplex (ModuleCat R) := shortComplexOfCompEqZero f f.range.mkQ ⋯
exactS : S.ShortExact
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)
Module: Mathlib.CategoryTheory.Limits.FinallySmall

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

Tactic:
exact initiallySmall_of_small_weakly_initial_set s hs'

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFiltered C
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
⊢ (map f).Final

Tactic:
have := NatIso.isIso_of_isIso_app (𝟙 T)
  have : (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T)).Final := by
    apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)
  apply final_of_natIso (mapIsoMap₂ f).symm

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j j' : J
φ : j ⟶ j'
⊢ ((const J).obj (F.1 Y)).map φ ≫ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j') =
    F.partialRightAdjointHomEquiv (f ≫ c'.π.app j) ≫ (R ⋙ F.rightAdjointObjIsDefined.ι).map φ

Tactic:
dsimp
            rw [id_comp, ← c'.w φ, ← partialRightAdjointHomEquiv_map_comp,
              ← assoc]
            dsimp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
⊢ homOfLe h ≫ G'.ι = G.ι

Tactic:
ext
  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₁ M₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ M₁ ◁ 𝟙 M₂ = 𝟙 (M₁ ⊗ M₂)

Tactic:
by
    ext1 X
    apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f

Tactic:
by
  intro k
  apply J.transitive h
  intro Z g hg
  rw [← Sieve.pullback_comp]
  apply k (g ≫ f) hg

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.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
R : Presieve Y
hR : R ∈ J.coverings Y
inst✝ : R.HasPullbacks f
⊢ Presieve.pullbackArrows f R ∈ J.coverings X

Tactic:
by
  obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
  have (i : ι) : Limits.HasPullback (g i) f := Presieve.hasPullback f (Presieve.ofArrows.mk i)
  rw [← Presieve.ofArrows_pullback]
  exact mem_coverings_of_isPullback _ hR _ _ _ fun i ↦ (IsPullback.of_hasPullback _ _).flip

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = singleton (f default)

Tactic:
by
  refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩
  rw [ofArrows_le_iff]
  intro i
  obtain rfl : i = default := Subsingleton.elim _ _
  simp

Goal state after:
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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
funext x

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
⊢ (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x →
    Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)

Tactic:
· intro t Y Z f g hf
    rw [Types.limit_ext_iff'] at t
    simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPullback (𝟭 C) R = R

Tactic:
ext
  rfl

Goal state after:
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 : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)

Tactic:
ext
  rfl

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F (generate R).arrows f → Presieve.functorPushforward F R f

Tactic:
rintro ⟨X', g, f', ⟨X'', g', f'', h₁, rfl⟩, rfl⟩
    exact ⟨X'', f'', f' ≫ F.map g', h₁, by simp⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{w', w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
⊢ J.plusMap 0 = 0

Tactic:
by
  ext : 2
  refine colimit.hom_ext (fun S => ?_)
  simp [plusMap]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
⊢ Epi p ↔ range p = ⊤

Tactic:
by
  simp [NatTrans.epi_iff_epi_app, epi_iff_surjective, Subfunctor.ext_iff, funext_iff,
    Set.range_eq_univ]

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
U : Cᵒᵖ
s : F.obj U
⊢ s ∈ G.obj U → s ∈ (sheafify J G).obj U

Tactic:
hs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ s ∈ (sheafify J G).obj U
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
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
⊢ s ∈ (sheafify J G).obj U → s ∈ G.obj U

Tactic:
hs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ s ∈ G.obj U
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
⊢ s.Compatible → ∃! t, s.IsAmalgamation t

Tactic:
hs

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
⊢ ∃! t, s.IsAmalgamation t
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
this :
  (ConcreteCategory.hom (g₁.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y) =
    (ConcreteCategory.hom (g₂.hom.app (op V)))
      ((ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y)
E :
  (ConcreteCategory.hom ((Subfunctor.toRangeSheafify J f.hom).app (op V))) y =
    (ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩
⊢ (ConcreteCategory.hom (g₁.hom.app (op V))) ((ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩) =
    (ConcreteCategory.hom (g₂.hom.app (op V))) ((ConcreteCategory.hom ((Sheaf.image f).obj.map i.op)) ⟨s, hx⟩)

Tactic:
convert this <;> exact E.symm

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : ↑X ≃ₜ ↑Y
⊢ homeoOfIso (isoOfHomeo f) = f

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (⇑homeo) (induced Prod.fst X.str ⊓ induced Prod.snd Y.str) =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
simp [induced_compose]

Goal state after:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (Prod.fst ∘ ⇑homeo) X.str ⊓ induced (Prod.snd ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (const J).map (f ≫ e.inv.hom)

Tactic:
rw [Functor.map_comp, ← reassoc_of% h, this]

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ α ≫ c.ι = c''.ι ≫ (const J).map (f ≫ e.inv.hom)

Tactic:
rw [Functor.map_comp, ← reassoc_of% h, this]

Goal state after: