mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
⊢ e₁ = e₁'

Tactic:
by
  ext
  rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)
⊢ (opEquiv' 0 a a ⋯).symm f = ((shiftFunctorZero Cᵒᵖ ℤ).hom.app (Opposite.op X)).unop ≫ f.unop

Tactic:
by
  simp [opEquiv'_symm_apply, opEquiv_symm_apply, shiftFunctorAdd'_add_zero,
    opShiftFunctorEquivalence_zero_unitIso_inv_app]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i : ℤ
φ : Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ Q.obj L
n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
⊢ φ = 0

Tactic:
obtain ⟨K, _, π, h, g, rfl⟩ := right_fac_of_isStrictlyLE φ i
  have hπ : IsSplitEpi π := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π
  have h₁ : inv (Q.map π) = Q.map (section_ π) := by
    rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
  have h₂ : section_ π ≫ g = 0 := by
    apply HomologicalComplex.from_single_hom_ext
    apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt
  rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ (h.desc s) (solution.var g) = s.var g

Tactic:
dsimp [desc]
  simp only [linearEquiv_symm_var, fromQuotient_toQuotient, π_single]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.IsPresentation

Tactic:
isPresentation_iff

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h₁ : Submodule.span A (Set.range solution.var) = ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Submodule.span A (Set.range solution.var) = ⊤ ∧ solution.π.ker = Submodule.span A (Set.range relations.relation)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
⊢ ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b

Tactic:
obtain ⟨u, v, h⟩ := hab
  refine match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩ <;>
  · rw [Matrix.det_fin_two_of, ← h]
    ring

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
⊢ equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

Tactic:
by
  ext x
  exact AlgHom.congr_fun (map_id Q₁) x

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ toClifford ((ι R) m) = (CliffordAlgebra.ι Q) m

Tactic:
simp [toClifford]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ l.dProd fι fA = (map fA l).prod

Tactic:
match l with
  | [] =>
    rw [List.dProd_nil, List.map_nil, List.prod_nil]
    rfl
  | head::tail =>
    rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
    rfl

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

Goal state before:
pp: case «0».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, mul_add, add_mul,
    mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
    mul_sub_one, ← sub_eq_add_neg]

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

Goal state before:
pp: case «0».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, mul_add, add_mul,
    mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
    mul_sub_one, ← sub_eq_add_neg]

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

Goal state before:
pp: case «1».«0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, mul_add, add_mul,
    mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
    mul_sub_one, ← sub_eq_add_neg]

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

Goal state before:
pp: case «1».«1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ↑(diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑(SpecialLinearGroup.transvection ⋯ c) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hc, SpecialLinearGroup.transvection_coe, diag2_coe, mul_add, add_mul,
    mul_inv_cancel₀ ha, inv_mul_cancel₀ ha, mul_comm a b, mul_assoc b a a, ← pow_two,
    mul_sub_one, ← sub_eq_add_neg]

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

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ SpecialLinearGroup.transvection h c ∈ commutator SL(2, F)

Tactic:
obtain rfl : j = 1 := by fin_cases j <;> tauto
    exact transvection_mem_commutator₀ ha hasq c

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

Goal state before:
pp: n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₂ f) = (toMatrix₂' R) B * toMatrix' f

Tactic:
← LinearMap.comp_id B,

Goal state after:
n : Type u_11
m : Type u_12
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 m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) ((B ∘ₗ id).compl₂ f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
tail_ih✝ : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) ((head :: tail).dProd fι fA) =
    (List.map (fun a ↦ (of A (fι a)) (fA a)) (head :: tail)).prod

Tactic:
| cons head tail =>

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

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

Tactic:
AddMonoidHom.dfinsuppSum_apply

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun a b ↦ ((toAddMonoid fun x ↦ ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') =
    DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)
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
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)

Tactic:
add_comm z x

Goal state after:
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
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (x + z)
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 : M
⊢ Q (x + x) = 4 • Q x

Tactic:
rw [← two_smul R x, Q.map_smul, ← Nat.cast_smul_eq_nsmul R]

Goal state after:
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 : M
⊢ (2 * 2) • Q x = ↑4 • Q x
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 ℳ
i : ι
x : ↥(ℳ i)
⊢ (decompose ℳ) ↑x = (of (fun i ↦ ↥(ℳ i)) i) x

Tactic:
rw [← decompose_symm_of _, Equiv.apply_symm_apply]

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
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₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (toMatrix₂ b₁ b₂') (B.compl₂ f) = (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) f

Tactic:
← LinearMap.comp_id B,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
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₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
f : M₂' →ₗ[R] M₂
⊢ (toMatrix₂ b₁ b₂') ((B ∘ₗ id).compl₂ f) = (toMatrix₂ b₁ b₂) (B ∘ₗ id) * (toMatrix b₂' b₂) f
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddGroupWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubgroupClass σ R
A : ι → σ
inst✝ : GradedOne A
z : ℤ
⊢ ↑z ∈ A 0

Tactic:
cases z
  · rw [Int.ofNat_eq_natCast, Int.cast_natCast]
    exact SetLike.natCast_mem_graded _ _
  · rw [Int.cast_negSucc]
    exact neg_mem (SetLike.natCast_mem_graded _ _)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.map reverse (ι Q).range = (ι Q).range

Tactic:
rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp,
    ← Submodule.map_comp]
  exact Submodule.map_id _

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
i j : ZMod 2
⊢ evenOdd Q i * evenOdd Q j ≤ evenOdd Q (i + j)

Tactic:
simp_rw [evenOdd, Submodule.iSup_eq_span, Submodule.span_mul_span]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i j : ZMod 2
⊢ Submodule.span R ((⋃ i_1, ↑((ι Q).range ^ ↑i_1)) * ⋃ i, ↑((ι Q).range ^ ↑i)) ≤
    Submodule.span R (⋃ i_1, ↑((ι Q).range ^ ↑i_1))
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
⊢ Set.univ = {0, 1}

Tactic:
have : (Finset.univ : Finset (ZMod 2)) = {0, 1} := rfl
    simpa using congr_arg ((↑) : Finset (ZMod 2) → Set (ZMod 2)) this

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ powersetCard α n = ∅ ↔ Nat.card α < n

Tactic:
rw [← Set.ncard_eq_zero, ← _root_.Nat.card_coe_set_eq, powersetCard.card, Nat.choose_eq_zero_iff]

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

Goal state before:
pp: case hij
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)
i : I
his : i ∈ ↑s
hit : i ∈ ↑t
j : Fin m
hj : (ofFinEmbEquiv.symm s) j = i
k : Fin n
hk : (ofFinEmbEquiv.symm t) k = i
⊢ Fin.castAdd n j ≠ Fin.natAdd m k

Tactic:
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
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin n → M
⊢ (liftAlternating f) ((ιMulti R n) v) = (f n) v

Tactic:
by
  rw [ιMulti_apply]
  induction n generalizing f with
  | zero => rw [List.ofFn_zero, List.prod_nil, liftAlternating_one, Subsingleton.elim 0 v]
  | succ n ih =>
    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.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
this : Free R ↑S.X₂
⊢ Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₂) = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,

Goal state after:
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
this : Free R ↑S.X₂
⊢ Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₂) = Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₁) + Module.rank R ↑S.X₃
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'
N : Type ?u.42
x✝¹ : AddCommGroup N
x✝ : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
⊢ ∀ (s : ↑(range ⇑(ιMulti R n))), f ↑s = f' ↑s

Tactic:
rintro ⟨_, ⟨f, rfl⟩⟩

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'
N : Type ?u.42
x✝¹ : AddCommGroup N
x✝ : Module R N
f✝ f' : ↥(⋀[R]^n M) →ₗ[R] N
h : (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f✝ = (relationsSolutionEquiv.symm (ιMulti R n)).postcomp f'
f : Fin n → M
⊢ f✝ ↑⟨(ιMulti R n) f, ⋯⟩ = f' ↑⟨(ιMulti R n) f, ⋯⟩
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
htop : span R (range f) = ⊤
⊢ Submodule.map (map n (span R (range v)).subtype) ⊤ = span R (range (ιMulti_family R n v))

Tactic:
← ιMulti_family_span_of_span _ htop,

Goal state after:
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : ⇑(span R (range v)).subtype ∘ f = v
htop : span R (range f) = ⊤
⊢ Submodule.map (map n (span R (range v)).subtype) (span R (range (ιMulti_family R n f))) =
    span R (range (ιMulti_family R n v))
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
T : Type w
inst✝¹ : Unique T
F : C ⥤ Discrete T
inst✝ : IsConnected C
⊢ F.Final

Tactic:
by
  rwa [← isConnected_iff_final_of_unique F]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected C
s : Cocone (constPUnitFunctor C)
j : C
⊢ (pUnitCocone C).ι.app j ≫ s.ι.app Classical.ofNonempty = s.ι.app j

Tactic:
ext ⟨⟩
    refine constant_of_preserves_morphisms (α := s.pt)
      (fun (k : C) ↦ s.ι.app k PUnit.unit) ?_ Classical.ofNonempty j
    intro X Y f
    exact ConcreteCategory.congr_hom (s.ι.naturality f).symm PUnit.unit

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
⊢ IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩
  have : Nonempty C := nonempty_of_nonempty_colimit <| Nonempty.map h.inv inferInstance
  refine zigzag_isConnected <| fun c d => ?_
  refine zigzag_of_eqvGen_colimitTypeRel _ (constPUnitFunctor C) ⟨c, PUnit.unit⟩ ⟨d, PUnit.unit⟩ ?_
  exact colimit_eq <| h.toEquiv.injective rfl

Goal state after:
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⟩ => ?_⟩
  let colimitCocone : ColimitCocone (constPUnitFunctor C) := ⟨pUnitCocone.{w} C, h⟩
  have : HasColimit (constPUnitFunctor.{w} C) := ⟨⟨colimitCocone⟩⟩
  simp only [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{w} C]
  exact ⟨colimit.isoColimitCocone colimitCocone⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ (Pi.eval I s).Final

Tactic:
by
  classical
  apply Functor.final_of_exists_of_isFiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _

Goal state after:
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₂
c₃ : Cone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsLimit c₃
j : J₁ × J₂
⊢ (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom ≫ c₃.π.app j =
    (G.map (c₁.π.app j.1)).app c₂.pt ≫ (G.obj (K₁.obj j.1)).map (c₂.π.app j.2)

Tactic:
by
  dsimp [isoObjConePointsOfIsLimit, Functor.mapCocone₂]
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
S : Set (Subfunctor F)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F.obj U✝
hx : x ∈ sSup ((fun T ↦ T.obj U✝) '' S)
⊢ x ∈ ⇑(hom (F.map f)) ⁻¹' sSup ((fun T ↦ T.obj V✝) '' S)

Tactic:
obtain ⟨_, ⟨F, h, rfl⟩, h'⟩ := hx
        simp only [Set.sSup_eq_sUnion, Set.sUnion_image, Set.preimage_iUnion,
          Set.mem_iUnion, Set.mem_preimage, exists_prop]
        exact ⟨_, h, F.map f h'⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝² x✝¹ x✝).hom ≫ (isoMk (fun X ↦ β_ (x✝².obj X) ((x✝¹ ⊗ x✝).obj X)) ⋯).hom ≫ (α_ x✝¹ x✝ x✝²).hom).app X✝ =
    ((isoMk (fun X ↦ β_ (x✝².obj X) (x✝¹.obj X)) ⋯).hom ▷ x✝ ≫
          (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (isoMk (fun X ↦ β_ (x✝².obj X) (x✝.obj X)) ⋯).hom).app
      X✝

Tactic:
apply hexagon_forward (C := ModuleCat (R.obj _))

Goal state after: