mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) =
    (B ((Finsupp.linearCombination R ⇑b₁) (b₁.repr x))) ((Finsupp.linearCombination S ⇑b₂) (b₂.repr y))

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ((b₁.repr x).sum fun i xi ↦ (b₂.repr y).sum fun j yj ↦ ρ₁₂ xi • σ₁₂ yj • (B (b₁ i)) (b₂ j)) =
    (B ((b₁.repr x).sum fun i a ↦ a • b₁ i)) ((b₂.repr y).sum fun i a ↦ a • b₂ i)
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi ↦ (b₂'.repr y).sum fun j yj ↦ xi • yj • (B (b₁' i)) (b₂' j)) =
    (B ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.linearCombination Rₗ ⇑b₂') (b₂'.repr y))

Tactic:
Finsupp.linearCombination_apply,

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi ↦ (b₂'.repr y).sum fun j yj ↦ xi • yj • (B (b₁' i)) (b₂' j)) =
    (B ((b₁'.repr x).sum fun i a ↦ a • b₁' i)) ((b₂'.repr y).sum fun i a ↦ a • b₂' i)
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
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ v i < 0

Tactic:
exact Ne.lt_of_le hi (h_sup i)

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

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)

Goal state after:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
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
hn : IsEmpty n
⊢ (∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A) → A ∈ center (SpecialLinearGroup n R)

Tactic:
simp [Subsingleton.elim A 1]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ (List.map f l).prod = mk (l.dProdIndex fun i ↦ (f i).fst) (l.dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
  simp_rw [Sigma.eta]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: case empty
ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ ∅, g k ∈ A (i k)
⊢ ∏ k ∈ ∅, g k ∈ A (∑ k ∈ ∅, i k)

Tactic:
simp [GradedOne.one_mem]

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
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (B ((Pi.basisFun R n) i✝)) ((Pi.basisFun R m) j✝) = (toMatrix₂' R) B i✝ j✝

Tactic:
LinearMap.toMatrix₂'_apply,

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
B : (n → R) →ₗ[R] (m → R) →ₗ[R] N₂
i✝ : n
j✝ : m
⊢ (B ((Pi.basisFun R n) i✝)) ((Pi.basisFun R m) j✝) = (B (Pi.single i✝ 1)) (Pi.single j✝ 1)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x y z : M
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion
  rw [add_comm z x]
  simp only [h, LinearMap.map_add₂]
  abel

Goal state after:
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toSemiring (fun i ↦ (f i).toAddMonoidHom) hone hmul) ((algebraMap R (⨁ (i : ι), A i)) r) = (algebraMap R B) r

Tactic:
change toModule R _ _ f (algebraMap R _ r) = _
      rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(((of (fun i ↦ ↥(ℳ i)) i) ⟨x, hx⟩) i) = x

Tactic:
DirectSum.of_eq_same,

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑⟨x, hx⟩ = x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons.e_a.e_a
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ x ∈ s, polar (⇑Q) (f a) (f x) + ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0

Tactic:
congr! with i hi

Goal state after:
case cons.e_a.e_a.a
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
i : ι
hi : i ∈ s
⊢ polar (⇑Q) (f a) (f i) = if ¬a = i then polar (⇑Q) (f a) (f i) else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ (algebraMap S R) s ∈ A 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one]
  exact (A 0).smul_mem s <| SetLike.one_mem_graded _

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

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ Q.toMatrix'.transpose i j = Q.toMatrix' i j

Tactic:
toMatrix',

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ ((LinearMap.toMatrix₂' R) (QuadraticMap.associated Q)).transpose i j =
    (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) j i = (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j

Tactic:
LinearMap.toMatrix₂'_apply,

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ ((QuadraticMap.associated Q) (Pi.single j 1)) (Pi.single i 1) =
    (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ ((QuadraticMap.associated Q) (Pi.single j 1)) (Pi.single i 1) =
    (LinearMap.toMatrix₂' R) (QuadraticMap.associated Q) i j

Tactic:
LinearMap.toMatrix₂'_apply,

Goal state after:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
Q : QuadraticForm R (n → R)
i j : n
⊢ ((QuadraticMap.associated Q) (Pi.single j 1)) (Pi.single i 1) =
    ((QuadraticMap.associated Q) (Pi.single i 1)) (Pi.single j 1)
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n m : ℕ
s : ↑(powersetCard α m)
t : ↑(powersetCard α n)
hst : Disjoint ↑s ↑t
⊢ #((↑s).disjUnion (↑t) hst) = m + n

Tactic:
Finset.card_disjUnion,

Goal state after:
α : Type u_1
n m : ℕ
s : ↑(powersetCard α m)
t : ↑(powersetCard α n)
hst : Disjoint ↑s ↑t
⊢ #↑s + #↑t = m + n
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
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t = 0

Tactic:
rw [Finset.not_disjoint_iff] at h
  obtain ⟨i, his, hit⟩ := h
  obtain ⟨j, hj⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem s i).mpr his
  obtain ⟨k, hk⟩ := (mem_range_ofFinEmbEquiv_symm_iff_mem t i).mpr hit
  simp only [ιMulti_family, ιMulti_mul_ιMulti]
  apply AlternatingMap.map_eq_zero_of_eq (i := Fin.castAdd n j) (j := Fin.natAdd m k)
  · simp [hj, hk]
  · apply ne_of_lt
    apply lt_of_lt_of_le (b := m) <;> simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ liftAlternating (ιMulti R) = LinearMap.id

Tactic:
by
  ext v
  dsimp
  induction v using CliffordAlgebra.left_induction with
  | algebraMap => rw [liftAlternating_algebraMap, ιMulti_zero_apply, Algebra.algebraMap_eq_smul_one]
  | add _ _ hx hy => rw [map_add, hx, hy]
  | ι_mul _ _ hx => simp_rw [liftAlternating_ι_mul, ιMulti_succ_curryLeft, liftAlternating_comp,
      LinearMap.comp_apply, LinearMap.mulLeft_apply, hx]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((RingHom.id R) c •
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))

Tactic:
rw [map_smul]

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (RingHom.id R) c •
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ Epi
    (kernel.lift (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).g
      (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).f ⋯)

Tactic:
convert! epi_comp (ι.map (Λ.chainComplexXIso X n).hom) (Λ.π.app _)

Goal state after:
case e'_5
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
e_3✝ :
  (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).X₁ =
    ι.obj ((Λ.chainComplex X).X (n + 2))
e_4✝ :
  kernel (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).g =
    (𝟭 A).obj (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))
⊢ kernel.lift (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).g
      (((ι.mapHomologicalComplex (ComplexShape.down ℕ)).obj (Λ.chainComplex X)).sc' (n + 2) (n + 1) n).f ⋯ =
    ι.map (Λ.chainComplexXIso X n).hom ≫ Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n)))
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) = (RingHom.id R) r • (ιMulti R 1) fun x ↦ m

Tactic:
dsimp
          rw [h]; nth_rw 2 [h]
          simp only [Fin.isValue, AlternatingMap.map_update_smul]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
rw [map_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc,
      Functor.whiskerLeft_app, Functor.whiskerLeft_app, restriction_app, restriction_app]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F.obj j).obj Z)).inv ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.obj j).map g ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected C ↔ Nonempty (IsColimit (pUnitCocone C))

Tactic:
refine ⟨fun inst => ⟨isColimitPUnitCocone C⟩, fun ⟨h⟩ => ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝ : Nonempty (IsColimit (pUnitCocone C))
h : IsColimit (pUnitCocone C)
⊢ IsConnected C
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ Z h, η ≫ h = μ ≫ h

Tactic:
refine ⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
      StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
    simpa using IsFiltered.coeq_condition _ _

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
⊢ Nonempty P.FullSubcategory

Tactic:
obtain ⟨X, hX, _⟩ := hP (Classical.arbitrary C₀)
          exact ⟨X, hX⟩

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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
S : Cocone (uncurry.obj F) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
p : J × K
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p

Tactic:
by
      have h1 := (Q p.1).fac ((Cocone.precompose (E p.1).inv).obj <|
        s.whisker (Prod.sectR p.1 K)) p.2
      simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj,
        Cocone.precompose_obj_pt, Cocone.whisker_pt, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Category.id_comp, E] at h1
      have h2 := (P.fac (S s) p.1)
      dsimp only [DiagramOfCocones.coconePoints_obj, Functor.comp_obj, Prod.sectR_obj,
        uncurry_obj_obj, NatTrans.id_app, Functor.const_obj_obj, DiagramOfCocones.coconePoints_map,
        Functor.const_obj_map, id_eq, Cocone.precompose_obj_pt, Cocone.whisker_pt,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app, S, E] at h2 ⊢
      simp [← h1, ← h2]

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 : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
⊢ (R ⋙ F.partialLeftAdjoint).map φ ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g) =
    F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g) ≫ ((const J).obj Y).map φ

Tactic:
apply F.partialLeftAdjointHomEquiv.injective
            have := c.w φ
            dsimp at this ⊢
            rw [comp_id, Equiv.apply_symm_apply, partialLeftAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, reassoc_of% this]

Goal state after: