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

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
i : n
hi : v i ≠ 0 i
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
⊢ IsometryEquiv Q (weightedSumSquares K fun i ↦ Q (v i))

Tactic:
by
  let iso := Q.isometryEquivBasisRepr v
  refine ⟨iso, fun m => ?_⟩
  convert! iso.map_app m
  rw [basisRepr_eq_of_iIsOrtho _ _ hv₁]

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ IsCoprime (↑A i 0) (↑A i 1)

Tactic:
refine match i with
  | 0 => ⟨A 1 1, -(A 1 0), ?_⟩
  | 1 => ⟨-(A 0 1), A 0 0, ?_⟩

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 1 0 * ↑A 0 1 = 1

case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : ℤ
⊢ ↑(T ^ n) = !![1, n; 0, 1]

Tactic:
induction n with
  | zero => rw [zpow_zero, coe_one, Matrix.one_fin_two]
  | succ n h =>
    simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
    congrm !![_, ?_; _, _]
    rw [mul_one, mul_one, add_comm]
  | pred n h =>
    simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
    congrm !![?_, ?_; _, _] <;> ring

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

Goal state before:
pp: R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂' R

Tactic:
ext M

Goal state after:
R : Type u_1
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m N₂
i✝¹ : n
i✝ : m
⊢ (((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M ∘ₗ LinearMap.single R (fun i ↦ R) i✝¹) 1 ∘ₗ
        LinearMap.single R (fun i ↦ R) i✝)
      1 =
    (((toLinearMap₂' R) M ∘ₗ LinearMap.single R (fun i ↦ R) i✝¹) 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
⊢ SMulWithZero (A 0) (A i)

Tactic:
letI := SMulWithZero.compHom (⨁ i, A i) (of A 0).toZeroHom

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
this : SMulWithZero (A 0) (⨁ (i : ι), A i) := SMulWithZero.compHom (⨁ (i : ι), A i) ↑(of A 0)
⊢ SMulWithZero (A 0) (A i)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ {i : ι} (m : ↥(𝒜 i)) (y : A), ↑(((decompose 𝒜) (↑m * y)) 0) = ↑(((decompose 𝒜) ↑m) 0) * ↑(((decompose 𝒜) y) 0)

pp: case refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A), ↑(((decompose 𝒜) (m * y)) 0) = ↑(((decompose 𝒜) m) 0) * ↑(((decompose 𝒜) y) 0)) →
      (∀ (y : A), ↑(((decompose 𝒜) (m' * y)) 0) = ↑(((decompose 𝒜) m') 0) * ↑(((decompose 𝒜) y) 0)) →
        ∀ (y : A), ↑(((decompose 𝒜) ((m + m') * y)) 0) = ↑(((decompose 𝒜) (m + m')) 0) * ↑(((decompose 𝒜) y) 0)

Tactic:
· rintro i ⟨c, hc⟩
      refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
      · simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
      · rintro j ⟨c', hc'⟩
        simp only
        by_cases h : i + j = 0
        · rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
        · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
          rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
          · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
          · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]
      · intro _ _ hd he
        simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]

Goal state after:
case refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A), ↑(((decompose 𝒜) (m * y)) 0) = ↑(((decompose 𝒜) m) 0) * ↑(((decompose 𝒜) y) 0)) →
      (∀ (y : A), ↑(((decompose 𝒜) (m' * y)) 0) = ↑(((decompose 𝒜) m') 0) * ↑(((decompose 𝒜) y) 0)) →
        ∀ (y : A), ↑(((decompose 𝒜) ((m + m') * y)) 0) = ↑(((decompose 𝒜) (m + m')) 0) * ↑(((decompose 𝒜) y) 0)
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
⊢ ∀ (m m' : A),
    (∀ (y : A), ↑(((decompose 𝒜) (m * y)) 0) = ↑(((decompose 𝒜) m) 0) * ↑(((decompose 𝒜) y) 0)) →
      (∀ (y : A), ↑(((decompose 𝒜) (m' * y)) 0) = ↑(((decompose 𝒜) m') 0) * ↑(((decompose 𝒜) y) 0)) →
        ∀ (y : A), ↑(((decompose 𝒜) ((m + m') * y)) 0) = ↑(((decompose 𝒜) (m + m')) 0) * ↑(((decompose 𝒜) y) 0)

Tactic:
rintro _ _ ha hb _

Goal state after:
case refine_3
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
m✝ m'✝ : A
ha : ∀ (y : A), ↑(((decompose 𝒜) (m✝ * y)) 0) = ↑(((decompose 𝒜) m✝) 0) * ↑(((decompose 𝒜) y) 0)
hb : ∀ (y : A), ↑(((decompose 𝒜) (m'✝ * y)) 0) = ↑(((decompose 𝒜) m'✝) 0) * ↑(((decompose 𝒜) y) 0)
y✝ : A
⊢ ↑(((decompose 𝒜) ((m✝ + m'✝) * y✝)) 0) = ↑(((decompose 𝒜) (m✝ + m'✝)) 0) * ↑(((decompose 𝒜) y✝) 0)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ (DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑r * ↑rj else 0) = 0

Tactic:
rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Fintype α
⊢ Fintype ↑(powersetCard α n)

Tactic:
by
  rw [coe_finset]
  infer_instance

Goal state after:
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:
| succ n ih =>

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
i : ℕ
hi : n ≤ i
Y : C
e₁ e₂ : Ext Y X i
⊢ e₁ = e₂

Tactic:
by simp only [hX i hi]

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 Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ (x.comp (Ext.mk₀ h.i) ⋯).comp (Ext.mk₀ h.r) ⋯ = 0

Tactic:
(x.comp (Ext.mk₀ h.i) (add_zero i)).eq_zero_of_hasInjectiveDimensionLT n hi,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ Ext.comp 0 (Ext.mk₀ h.r) ⋯ = 0
Module: Mathlib.Algebra.Category.ModuleCat.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
this : Small.{max v v', u} R
n : ℕ
ih : ∀ {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N), HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
| succ n ih =>

Goal state after:
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
⊢ HasInjectiveDimensionLE M (n + 1) ↔ HasInjectiveDimensionLE N (n + 1)

Tactic:
| succ n ih =>

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) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
nth_rw 2 [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) (update (fun x ↦ 0) 0 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) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m

Tactic:
nth_rw 2 [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) (update (fun x ↦ 0) 0 m)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ snd A I = uncurry (t.to (A ⟹ I))

Tactic:
rw [← curry_eq_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ curry (snd A I) = t.to (A ⟹ I)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ PreservesLimitsOfShape (Discrete WalkingPair) colim

Tactic:
constructor
  intro F
  apply preservesLimit_of_iso_diagram colim (diagramIsoPair F).symm

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
⊢ FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
h : ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
⊢ IsColimit (G.flip.mapCocone₂ c₁ c₂)

Tactic:
let E₀ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G).flip :=
      Iso.refl _

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
⊢ IsColimit (G.flip.mapCocone₂ c₁ c₂)
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
⊢ IsLimit (G.flip.mapCone₂ c₁ c₂)

Tactic:
let E₀ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G).flip :=
      Iso.refl _

Goal state after:
J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
E₀ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).flip :=
  Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
⊢ IsLimit (G.flip.mapCone₂ c₁ c₂)
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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
⊢ m = P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } }

Tactic:
refine P.uniq
      { pt := s.pt
        π := _ } m ?_

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
⊢ ∀ (j : J × K),
    m ≫ c.π.app j = { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } }.π.app j
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
⊢ pullbackObjIsDefined φ = ⊤

Tactic:
ext M

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M ↔ ⊤ M
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: case convert_4
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (P ∘ a) fun i ↦ p₁ (a i)) ∈ J.coverings Y

Tactic:
refine IsStableUnderBaseChange.mem_coverings_of_isPullback (fun i ↦ f (a i)) ?_ g _
      (fun i ↦ p₂ (a i)) fun i ↦ h _
    convert! hR
    refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_
    exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

Tactic:
rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
        simp

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

Goal state before:
pp: case refine_2
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
W : C
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)

Tactic:
ext K

Goal state after:
case refine_2
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
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

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

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

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
⊢ (bindOfArrows X f fun i ↦ ofArrows (Y i) (g i)) = ofArrows (fun p ↦ Y p.fst p.snd) fun p ↦ g p.fst p.snd ≫ f p.fst

Tactic:
refine le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
⊢ (bindOfArrows X f fun i ↦ ofArrows (Y i) (g i)) ≤ ofArrows (fun p ↦ Y p.fst p.snd) fun p ↦ g p.fst p.snd ≫ f p.fst
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ pushforward f (ofArrows U g) = ofArrows U fun x ↦ g x ≫ f

Tactic:
refine le_antisymm ?_ ?_
  · rintro _ _ ⟨u, rfl, ⟨i⟩⟩
    exact ⟨i⟩
  · rw [ofArrows_le_iff]
    intro i
    use g i, rfl
    exact ⟨i⟩

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 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
  exact ⟨Z, f', g, h₁, h⟩

Goal state after: