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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> yj •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) j)) =
    ∑ x,
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
rw [Finsupp.sum_fintype]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1,
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) i_1 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) =
    ∑ x,
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

case h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ((b₁.repr (l (b₁' i))).sum fun i xi ↦ (b₂.repr (r (b₂' j))).sum fun j yj ↦ xi •> yj •> (B (b₁ i)) (b₂ j)) =
    ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
rw [Finsupp.sum_fintype]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ (∑ i_1, (b₂.repr (r (b₂' j))).sum fun j yj ↦ (b₁.repr (l (b₁' i))) i_1 •> yj •> (B (b₁ i_1)) (b₂ j)) =
    ∑ y, ∑ x, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x

case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
⊢ ∀ (i : n), ((b₂.repr (r (b₂' j))).sum fun j yj ↦ 0 •> yj •> (B (b₁ i)) (b₂ j)) = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ((b₂.repr (r (b₂' j))).sum fun j yj ↦ (b₁.repr (l (b₁' i))) i' •> yj •> (B (b₁ i')) (b₂ j)) =
    ∑ x, (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

Tactic:
rw [Finsupp.sum_fintype]

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∑ i_1, (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) i_1 •> (B (b₁ i')) (b₂ i_1) =
    ∑ x, (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ x) * (b₂.repr (r (b₂' j))) x

case h
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : Fintype n
inst✝¹⁰ : Fintype m
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m), (b₁.repr (l (b₁' i))) i' •> 0 •> (B (b₁ i')) (b₂ i_1) = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case mp
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R
h : B = B'
⊢ (toMatrix₂' R) B = (toMatrix₂' R) B'

Tactic:
rw [h]

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
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ ↑2 • Q₁ = ↑2 • Q₂

Tactic:
simp_rw [Nat.cast_smul_eq_nsmul R, ← QuadraticMap.toQuadraticMap_polarBilin]

Goal state after:
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
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case mp
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
B B' : M₁ →ₗ[R] M₂ →ₗ[R] R
h : B = B'
⊢ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'

Tactic:
rw [h]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = ((associated' Q) x) x

Tactic:
exact (associated_eq_self_apply _ _ x).symm

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

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
m₁ m₂ : M
⊢ (ι Q) m₁ * (ι Q) m₂ ∈ (ι Q).range * (ι Q).range

Tactic:
exact
        Submodule.mul_mem_mul (LinearMap.mem_range_self (ι Q) m₁)
          (LinearMap.mem_range_self (ι Q) m₂)

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

Goal state before:
pp: case inr.succ
α : Type u_1
val✝ : Infinite α
n : ℕ
⊢ Nat.card ↑(powersetCard α (n + 1)) = (Nat.card α).choose (n + 1)

Tactic:
rw [Nat.card_eq_zero_of_infinite (α := α), Nat.choose_zero_succ]
      exact Nat.card_eq_zero_of_infinite

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] ExteriorAlgebra R M →ₗ[R] N

Tactic:
by
  suffices
    (∀ i, M [⋀^Fin i]→ₗ[R] N) →ₗ[R]
      ExteriorAlgebra R M →ₗ[R] ∀ i, M [⋀^Fin i]→ₗ[R] N by
    refine LinearMap.compr₂ this ?_
    refine (LinearEquiv.toLinearMap ?_).comp (LinearMap.proj 0)
    exact AlternatingMap.constLinearEquivOfIsEmpty.symm
  refine CliffordAlgebra.foldl _ ?_ ?_
  · refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_
    all_goals
      ext i : 1
      simp only [map_smul, map_add, Pi.add_apply, Pi.smul_apply, AlternatingMap.curryLeft_add,
        AlternatingMap.curryLeft_smul, map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply]
  · -- when applied twice with the same `m`, this recursive step produces 0
    intro m x
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ injectiveDimension X < ↑0 ↔ injectiveDimension X < 0

Tactic:
WithBot.coe_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ injectiveDimension X < 0 ↔ injectiveDimension X < 0
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
by
  have := free_shortExact hS'
  rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
    Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]
  exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
    (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ ((ιMulti R 1) fun x ↦ m₁ + m₂) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
rw [h]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ ((ιMulti R 1) fun x ↦ r • m) = r • (ιMulti R 1) fun x ↦ m

Tactic:
rw [h]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m
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✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
⊢ F.Initial

Tactic:
by
  suffices Final F.op from initial_of_final_op _
  refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)
  obtain ⟨c, ⟨f⟩⟩ := h d.unop
  exact ⟨op c, ⟨f.op⟩⟩

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
obtain ⟨Q, H, hQ⟩ := ObjectProperty.EssentiallySmall.exists_small_le'.{v} P

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
P : ObjectProperty J
inst✝ : ObjectProperty.EssentiallySmall.{v, v, u} P
hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
⊢ InitiallySmall J
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
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k = limit.π G (j, k)

Tactic:
by
  simp [limitIsoLimitCurryCompLim, Trans.simple]

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
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv (f ≫ F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map,
    ← assoc, ← partialRightAdjointHomEquiv_comp, comp_id]

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

Goal state before:
pp: case refine_2
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
i : ι' ⊕ α
⊢ (Presieve.ofArrows (fun j ↦ Y (incl i) (fibincl i j)) fun j ↦ g (incl i) (fibincl i j)) ∈ J.coverings (X (incl i))

Tactic:
· convert! hg (incl i)
      refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_
      match i with
      | .inl i => exact .mk' ⟨⟨_, _⟩, hu⟩ (by cat_disch) (by cat_disch)
      | .inr i => exact .mk' (.inr ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Ti g ⋯ f

Tactic:
rw [hTi]

Goal state after:
case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton f f
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
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (S.index P)
⊢ ∀ (b : S.shape.R), P.map (S.shape.fst b).f.op ≫ (S.index P).fst b = P.map (S.shape.snd b).f.op ≫ (S.index P).snd b

Tactic:
by
      intro I
      dsimp only [shape, index, Relation.fst, Relation.snd]
      simp only [← P.map_comp, ← op_comp, I.r.w]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ofArrows (fun x ↦ X) fun x ↦ f ≫ g) = singleton (f ≫ g)

Tactic:
ofArrows_pUnit.{0}

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ singleton (f ≫ g) = singleton (f ≫ 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
X Y✝ Z : C
f✝ : Y✝ ⟶ X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
S : Presieve X
Y : D
f : Y ⟶ F.obj X
h : functorPushforward F S f
⊢ FunctorPushforwardStructure F S f

Tactic:
choose Z f' g h₁ h using h

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
F : C ⥤ D
S : Presieve X
Y : D
f : Y ⟶ F.obj X
Z : C
f' : Z ⟶ X
g : Y ⟶ F.obj Z
h₁ : S f'
h : f = g ≫ F.map f'
⊢ FunctorPushforwardStructure F S f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd ≍
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry

Tactic:
heq_iff_eq

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : ⟨Y, u⟩ ∈ s.uncurry
v : ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst ⟶ B
h :
  ((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).snd =
    ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩.snd
⊢ ⟨((fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) ⟨Y, u⟩).fst, v⟩ ∈ (pullbackArrows b s).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd ≍
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry

Tactic:
heq_iff_eq

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
fst✝ : C
f : fst✝ ⟶ X
hf : ⟨fst✝, f⟩ ∈ s.uncurry
Y : C
g : Y ⟶ ⟨fst✝, f⟩.fst
hg : ⟨Y, g⟩ ∈ (t ⟨fst✝, f⟩.snd ⋯).uncurry
v : (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst ⟶ X
h :
  (Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).snd =
    ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩.snd
⊢ ⟨(Sigma.map id (fun Z g ↦ g ≫ ⟨fst✝, f⟩.snd) ⟨Y, g⟩).fst, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f

Tactic:
simpa using downward_closed _ h f

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
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g → ∃ i a, g = a ≫ f i

Tactic:
rintro ⟨T, a, b, ⟨i⟩, rfl⟩

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y✝ : I → C
f : (i : I) → Y✝ i ⟶ X
W Y : C
i : I
a : W ⟶ Y✝ i
⊢ ∃ i_1 a_1, a ≫ f i = a_1 ≫ f i_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
have := R.hasPullback f hk

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ : C
g : W✝ ⟶ Y
W : C
h : W✝ ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
this : HasPullback k f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ x.sieveExtend.IsAmalgamation t

Tactic:
by
  intro Y f hf
  dsimp [FamilyOfElements.sieveExtend]
  rw [← ht _, ← comp_apply, ← Functor.map_comp, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]

Goal state after: