mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ Q.unop.IsClosedUnderLimitsOfShape J

Tactic:
← isClosedUnderColimitsOfShape_op_iff_unop

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderColimitsOfShape Jᵒᵖ
⊢ Q.IsClosedUnderColimitsOfShape Jᵒᵖ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (𝟙 (A ⊗ A) ≫ μ) ≫ μ) ≫ μ

Tactic:
← lift_fst_snd,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (lift (fst A A) (snd A A) ≫ μ) ≫ μ) ≫ μ
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
⊢ b.dualBasis.toDual ∘ₗ b.toDual = Dual.eval R M

Tactic:
refine b.ext fun i => b.dualBasis.ext fun j => ?_

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ ((b.dualBasis.toDual ∘ₗ b.toDual) (b i)) (b.dualBasis j) = ((Dual.eval R M) (b i)) (b.dualBasis j)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i : ι
⊢ h.basis i = e i

Tactic:
rw [Basis.apply_eq_iff]

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i : ι
⊢ h.basis.repr (e i) = Finsupp.single i 1
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
have hf : Surjective (coprod db eb) := by
    rwa [← range_eq_top, range_coprod, eq_top_iff]

Goal state after:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ (db.coprod eb).ker.subtype.range ≤ (cd.prod (-ce)).range

Tactic:
range_subtype

Goal state after:
case e_a.refine_2
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
hf : Surjective ⇑(db.coprod eb)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ (db.coprod eb).ker ≤ (cd.prod (-ce)).range
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
      ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V) =
    ↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))

Tactic:
apply TensorProduct.ext

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ (TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
      (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V)) =
    (TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
      (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.lTensor V (contractLeft K V) ∘ₗ
      ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) =
    ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)

Tactic:
apply TensorProduct.ext

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
⊢ (TensorProduct.mk K K V).compr₂ₛₗ
      (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)) =
    (TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ Module.rank S (M →ₗ[R] N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)

Tactic:
by
  rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
⊢ ∀ (s : Cocone (Discrete.functor Z)) (m : (coproductCocone Z).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ m = s.ι.app j) →
      m = ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
by
    rintro s f h
    ext : 1
    refine DirectSum.linearMap_ext _ fun i ↦ ?_
    ext x
    simpa only [LinearMap.coe_comp, Function.comp_apply, hom_ofHom, toModule_lof] using!
      congr($(h ⟨i⟩) x)

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : Dual R M
n : N
g : Dual R N
p : P
⊢ (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)

Tactic:
ext m
  simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, map_smul, LinearMap.smul_apply]
  rw [smul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ j → (Finsupp.single b 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) b) = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ j ∉ Finset.univ →
    (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      ∑ x, (Finsupp.single x 1) j * (Finsupp.single b 1) i * ((Finsupp.single i' 1) b * (Finsupp.single j' 1) x) = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ i ∉ Finset.univ →
    ∑ x, (Finsupp.single x 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) x) = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ, b_1 ≠ j → ((Finsupp.single i 1) i * (Finsupp.single b_1 1) j) • b.coord i ⊗ₜ[R] c.coord b_1 = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ j ∉ Finset.univ → ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ i → ∑ x, ((Finsupp.single b_1 1) i * (Finsupp.single x 1) j) • b.coord b_1 ⊗ₜ[R] c.coord x = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ i ∉ Finset.univ → ∑ x, ((Finsupp.single i 1) i * (Finsupp.single x 1) j) • b.coord i ⊗ₜ[R] c.coord x = 0

Tactic:
{ intros; simp [*] at * }

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
⊢ FiniteDimensional K V

Tactic:
rw [FiniteDimensional, ← rank_lt_aleph0_iff]

Goal state after:
K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
⊢ Module.rank K V < ℵ₀
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))

Tactic:
convert! lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le

Goal state after:
K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ Module.rank K (Dual K V) = lift.{u_4, max u_4 u_5} (Module.rank K (Dual K V))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
h : ¬∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
push Not at h

Goal state after:
case mp
R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
h : ∃ s t, s • x + t • y = 0 ∧ (s = 0 → t ≠ 0)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
⊢ x = 0

Tactic:
have hyy : y = 0 := by
    erw [← Category.comp_id y, ← Limits.prod.lift_snd (𝟙 A) (𝟙 A), ← Category.assoc, hy,
      Category.assoc, prod.lift_snd, HasZeroMorphisms.comp_zero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
⊢ x = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd

Tactic:
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0 - a

Tactic:
← sub_self a

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a - a

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0 - a
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
h_apply_fromCoset' _ _ _ m,

Goal state after:
case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨y • ↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasZeroMorphisms C
X Y Q : Cᵒᵖ
p : Y ⟶ Q
f : X ⟶ Y
w : f ≫ p = 0
h : IsColimit (CokernelCofork.ofπ p w)
W'✝ : C
x : W'✝ ⟶ unop Y
hx : x ≫ f.unop = 0
b : W'✝ ⟶ unop Q
hb : b ≫ p.unop = x
⊢ Cofork.π (CokernelCofork.ofπ p w) ≫ b.op =
    Cofork.π (CokernelCofork.ofπ p w) ≫ (h.desc (CokernelCofork.ofπ x.op ⋯)).unop.op

Tactic:
by simpa only [Quiver.Hom.op_unop, Cofork.IsColimit.π_desc] using! Quiver.Hom.unop_inj hb

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData

Tactic:
rw [rightHomologyι_naturality']

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
by
  refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
  · simp only [assoc, ← cancel_mono φ.τ₃, zero_comp, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h₂.wi]
  · simp only [← cancel_mono h₁.i, assoc, h₁.liftK_i, cyclesMap'_i_assoc,
      IsIso.hom_inv_id, comp_id, id_comp]
  · simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc,
      IsIso.inv_hom_id, comp_id, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ IsLimit (KernelFork.ofι (F.map h.ι) wι)

Tactic:
refine IsLimit.postcomposeHomEquiv e _
      (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ (KernelFork.ofι h.ι ⋯).map F ≅ (Cone.postcompose e.hom).obj (KernelFork.ofι (F.map h.ι) wι)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a b : S₁ ⟶ S₂
⊢ a + b = b + a

Tactic:
by ext <;> apply add_comm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π = 0

Tactic:
← cancel_mono (isoHomology S hkf hcc fac).hom,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ ((hkf.lift (KernelFork.ofι S.f ⋯) ≫ 𝟙 kf.pt) ≫ π) ≫ (isoHomology S hkf hcc fac).hom =
    0 ≫ (isoHomology S hkf hcc fac).hom