mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
⊢ (ConcreteCategory.hom
          ((yoneda.map
                ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
                  (homologyFunctor C (up ℤ) 0).homologySequenceδ
                      (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                        ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫
                          (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
                      n₀ n₁ h ≫
                    (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
            (Opposite.op A))).toFun
      x =
    (ConcreteCategory.hom
          ((yoneda.map
                (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
                  hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
            (Opposite.op A))).toFun
      x

Tactic:
obtain ⟨A', π, _, x', w, hx'⟩ :=
    (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
⊢ (ConcreteCategory.hom
          ((yoneda.map
                ((homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
                  (homologyFunctor C (up ℤ) 0).homologySequenceδ
                      (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
                        ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫
                          (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
                      n₀ n₁ h ≫
                    (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁)).app
            (Opposite.op A))).toFun
      x =
    (ConcreteCategory.hom
          ((yoneda.map
                (HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
                  hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁))).app
            (Opposite.op A))).toFun
      x
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map (φ.unop.hom₃ ≫ (Opposite.unop T₁).mor₃).op =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op

Tactic:
← φ.unop.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T₁ T₂ : (Triangle C)ᵒᵖ
φ : T₁ ⟶ T₂
⊢ (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₁).obj₁) ≫
      (shiftFunctor Cᵒᵖ 1).map ((Opposite.unop T₂).mor₃ ≫ (shiftFunctor C 1).map φ.unop.hom₁).op =
    φ.unop.hom₁.op ≫
      (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T₂).obj₁) ≫
        (shiftFunctor Cᵒᵖ 1).map (Opposite.unop T₂).mor₃.op
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
⊢ e.toMatrix ⇑(e.unitsSMul w) = Matrix.diagonal (Units.val ∘ w)

Tactic:
by
  ext i j
  by_cases h : i = j <;>
    simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]

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

Goal state before:
pp: case mp
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
mul_eq : M *ᵥ v = 0
hv : M.det ≠ 0
⊢ v = 0

Tactic:
exact eq_zero_of_mulVec_eq_zero hv mul_eq

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: G : Type u_7
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
G' : Type u_8
inst✝ : CommGroup G'
⊢ Nonempty ((G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G'))

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  exact ⟨monoidHomMulEquivRootsOfUnityOfGenerator hg G'⟩

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ det
      { val := diagonal fun j ↦ if j = i then ↑r else 1, inv := diagonal fun j ↦ if j = i then ↑r⁻¹ else 1,
        val_inv := ?m.57, inv_val := ?m.58 } =
    r

Tactic:
simp [det]

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

Goal state before:
pp: 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
⊢ -1 • v ≠ 0

Tactic:
by simp [*]

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)
  have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ
  simp_rw [associated_eq_self_apply] at hv₂
  exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩

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

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

Tactic:
det_coe A ▸ det_fin_two A.1

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 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

Tactic:
det_coe A ▸ det_fin_two A.1

Goal state after:
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 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

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

Tactic:
det_coe A ▸ det_fin_two A.1

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
det_coe A ▸ det_fin_two A.1

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : 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 κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ ∏ k ∈ insert j F', g k ∈ A (∑ k ∈ insert j F', i k)

Tactic:
case =>

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 ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun i ↦ { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }
⊢ ∀ (m : M), motive m

Tactic:
have t : DirectSum.Decomposition ℳ' :=
    { decompose' := DirectSum.decompose ℳ
      left_inv := fun _ ↦ (decompose ℳ).left_inv _
      right_inv := fun _ ↦ (decompose ℳ).right_inv _ }

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 ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun i ↦ { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }
t : Decomposition ℳ'
⊢ ∀ (m : M), motive m
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✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r ×ˢ DFinsupp.support r',
      ↑(((of (fun i ↦ ↥(A i)) (i.1 + i.2)) (GradedMonoid.GMul.mul (r i.1) (r' i.2))) n) =
    ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)

Tactic:
simp_rw [coe_of_apply, apply_ite, ZeroMemClass.coe_zero, ← Finset.sum_filter, SetLike.coe_gMul]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
⊢ ∑ ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = k, ↑(r ij.1) * ↑(r' ij.2) = 0

Tactic:
apply Finset.sum_eq_zero fun x hx ↦ ?_

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
x : ι × ι
hx : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
⊢ ↑(r x.1) * ↑(r' x.2) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

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

Tactic:
obtain ⟨m₂, rfl⟩ := hn

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

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

Tactic:
induction ha using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      simp_rw [← Algebra.smul_def]
      exact range_ι_pow _ (Submodule.smul_mem _ _ hb)
    | add x y n hx hy ihx ihy =>
      simp_rw [add_mul]
      apply add _ _ _ _ ihx ihy
    | mem_mul x hx n'' y hy ihy =>
      revert hx
      simp_rw [pow_two]
      intro hx2
      induction hx2 using Submodule.mul_induction_on' with
      | mem_mul_mem m hm n hn =>
        simp_rw [LinearMap.mem_range] at hm hn
        obtain ⟨m₁, rfl⟩ := hm; obtain ⟨m₂, rfl⟩ := hn
        simp_rw [mul_assoc _ y b]
        exact ι_mul_ι_mul _ _ _ _ ihy
      | add x hx y hy ihx ihy =>
        simp_rw [add_mul]
        apply add _ _ _ _ ihx ihy

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:
rw [List.ofFn_succ, List.prod_cons, liftAlternating_ι_mul, ih,
      AlternatingMap.curryLeft_apply_apply]
    congr
    exact Matrix.cons_head_tail _

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 : HasInjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
this✝ : HasExt C := HasExt.standard C
this : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X i)
⊢ Subsingleton (Ext Y X i)

Tactic:
exact Ext.chgUniv.{w, max u v}.symm.subsingleton

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'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : (relations R ι M).Solution N
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ s.var v = 0

Tactic:
simpa using s.linearCombination_var_relation (.alt v i j hm hij)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : Closed A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f

Tactic:
have : Mono f := by
    rw [← lift_snd (𝟙 A) f, ← zeroMul_hom t]
    exact mono_comp _ _
  have : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩
  apply isIso_of_mono_of_isSplitEpi

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)
Q : ObjectProperty J
H : ObjectProperty.Small.{v, v, u} Q
hQ : P ≤ Q.isoClosure
⊢ InitiallySmall J

Tactic:
have : Small.{v} (show Set _ from Q) := by assumption

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
this :
  Small.{v, u}
    (have this := Q;
    ↑this)
⊢ InitiallySmall J
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: case refine_2
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
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι := { app := fun k ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
j₂ : J₂
⊢ (Q₀.obj j₁).ι.app j₂ ≫ (G.map (c₁.ι.app j₁)).app c₂.pt = (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s

Tactic:
have := (P j₁).fac s j₂

Goal state after:
case refine_2
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
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι := { app := fun k ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
j₂ : J₂
this : (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s = s.ι.app j₂
⊢ (Q₀.obj j₁).ι.app j₂ ≫ (G.map (c₁.ι.app j₁)).app c₂.pt = (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: case refine_2
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
inst✝¹ : ∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesLimit K₂ (G.obj x)
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
Q₀ : DiagramOfCones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsLimit (Q₀.obj j₁) := fun x ↦ isLimitOfPreserves (G.obj (K₁.obj x)) hc₂
E₀ : Q₀.conePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.conePoints.obj x)) ⋯
j₁ : J₁
s : Cone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    π := { app := fun k ↦ (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app k), naturality := ⋯ } }
j₂ : J₂
⊢ (G.map (c₁.π.app j₁)).app c₂.pt ≫ (Q₀.obj j₁).π.app j₂ = (P j₁).lift s ≫ (Q₀.obj j₁).π.app j₂

Tactic:
have := (P j₁).fac s j₂

Goal state after:
case refine_2
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
inst✝¹ : ∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesLimit K₂ (G.obj x)
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
Q₀ : DiagramOfCones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsLimit (Q₀.obj j₁) := fun x ↦ isLimitOfPreserves (G.obj (K₁.obj x)) hc₂
E₀ : Q₀.conePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.conePoints.obj x)) ⋯
j₁ : J₁
s : Cone (((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    π := { app := fun k ↦ (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app k), naturality := ⋯ } }
j₂ : J₂
this : (P j₁).lift s ≫ (Q₀.obj j₁).π.app j₂ = s.π.app j₂
⊢ (G.map (c₁.π.app j₁)).app c₂.pt ≫ (Q₀.obj j₁).π.app j₂ = (P j₁).lift s ≫ (Q₀.obj j₁).π.app j₂
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
h : F.IsRightAdjoint
X : C
⊢ F.leftAdjointObjIsDefined X ↔ ⊤ X

Tactic:
simpa only [Pi.top_apply, Prop.top_eq_true, iff_true]
    using leftAdjointObjIsDefined_of_adjunction (Adjunction.ofIsRightAdjoint F) X

Goal state after: