mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      μ =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
congr 1

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
      ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) =
    (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }

Tactic:
congr
      ext
      · exact (@braiding_hom_fst C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_fst C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm
      · exact (@braiding_hom_snd C _ ‹_› ⟨e₁, a₁, b₁, c₁, d₁⟩ ..).trans
          (@braiding_hom_snd C _ ‹_› ⟨e₂, a₂, b₂, c₂, d₂⟩ ..).symm

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
congr 1

Goal state after:
case e_f
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm = mul' R A ∘ₗ lTensor A (mul' R A)
Module: Mathlib.RingTheory.Bialgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
⊢ ((lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv)) (comul c) =
    (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (comul c)

Tactic:
congr 1

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
⊢ (lmul' R).comp (Algebra.TensorProduct.map f.ofConv g.ofConv) = Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : GrpObj B
f g h : A ⟶ B
⊢ f = lift (g ≫ ι) h ≫ μ ↔ lift g f ≫ μ = h

Tactic:
refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [← lift_lift_assoc])

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (lift f (ι ≫ f)) f = lift (lift f (f ≫ ι)) f
⊢ ι ≫ f = f ≫ ι

Tactic:
simpa using (this =≫ fst _ _) =≫ snd _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ lift ι (𝟙 X) ≫ μ = lift ι (𝟙 X) ≫ μ

Tactic:
left_inv

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ lift ι (𝟙 X) ≫ μ = toUnit X ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ₘ curry' g) ≫ comp X Y Z

Tactic:
by
  rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
    Iso.inv_hom_id_assoc, curry'_ihom_map]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ (WType.elim (↥(closure s)) (operate s) x)⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
exact ⟨WType.mk (.inl 3) fun _ ↦ x, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ Infinite ιK

Tactic:
rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
⊢ Disjoint s (sec '' t)

Tactic:
rw [Set.disjoint_iff]

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
⊢ s ∩ sec '' t ⊆ ∅
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
hf : Surjective ⇑(db.coprod eb)
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V + Module.rank K ↥(db.coprod eb).ker

Tactic:
congr 1

Goal state after:
case e_a
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 ↥(db.coprod eb).ker
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s ≠ ⊤
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)

Tactic:
← Quotient.nontrivial_iff

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : Nontrivial (V ⧸ s)
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) + 0 ≤ finrank K V

Tactic:
add_zero

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K V
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ InvariantBasisNumber Rᵐᵒᵖ ↔ InvariantBasisNumber R

Tactic:
simp_rw [invariantBasisNumber_iff_matrix, ← opEquiv.mapMatrix.forall_congr_right,
    ← opEquiv.mapMatrix.symm.injective.eq_iff]

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      opEquiv.mapMatrix.symm (opEquiv.mapMatrix a * opEquiv.mapMatrix a_1) = opEquiv.mapMatrix.symm 1 →
        opEquiv.mapMatrix.symm (opEquiv.mapMatrix a_1 * opEquiv.mapMatrix a) = opEquiv.mapMatrix.symm 1 → n = m) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + 0

Tactic:
add_zero

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ Y ◁ f) = (ρ_ Y').hom ≫ f

Tactic:
by
  calc
    _ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation'']; monoidal

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

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ + 0 = finrank K V

Tactic:
add_zero

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ = finrank K V
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ (B 0) x = 0

Tactic:
rw [map_zero B, zero_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, q.bottom_rightRetraction, F.map_id]

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

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝ : Fintype ι
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
let φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
⊢ K ∈ span 𝕜 (Set.range L)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
← OrderIso.symm_apply_eq

Goal state after:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
rwa [← OrderIso.symm_apply_eq]

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

Goal state before:
pp: 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
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
have hle z : 0 ≤ B z z := by obtain rfl | hz := eq_or_ne z 0 <;> simp [le_of_lt, *]
  constructor
  · contrapose!
    intro h
    rw [LinearIndependent.pair_iff] at h
    push Not at h
    obtain ⟨r, s, hl, h0⟩ := h
    by_cases hr : r = 0; · simp_all
    by_cases hs : s = 0; · simp_all
    suffices
        (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
      simp only [map_smul, smul_apply, smul_eq_mul] at this
      rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
      have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
      exact le_of_eq <| mul_right_injective₀ hrs this
    simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]
  · contrapose!
    intro h
    exact not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
      (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
c : ↑s.1
⊢ (Hom.hom f) ((Hom.hom s.ι) c) = 0

Tactic:
by simp [← ConcreteCategory.comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g

Tactic:
rw [Category.assoc, equalizer.condition]

Goal state after:
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
⊢ coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) = coprod.inl ≫ 0

Tactic:
rw [cokernel.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
⊢ coprod.inr ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) = coprod.inr ≫ 0

Tactic:
rw [cokernel.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
m : cokernel (coprod.desc f g) ⟶ s.pt
h₁ : a' ≫ m = s.inl
x✝ : b' ≫ m = s.inr
⊢ b ≫ s.inr = cokernel.π (coprod.desc f g) ≫ cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯

Tactic:
by
                rw [cokernel.π_desc]

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

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

Tactic:
sub_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
| 0 - b - a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - 0 - (a - a) = a

Tactic:
sub_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - (a - a) = a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
skip

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
| 0 - 0
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (unopMap φ)

Tactic:
rw [← quasiIso_opMap_iff]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
S₁ S₂ : ShortComplex Cᵒᵖ
inst✝⁴ : S₁.HasHomology
inst✝³ : S₂.HasHomology
inst✝² : S₁.unop.HasHomology
inst✝¹ : S₂.unop.HasHomology
φ : S₁ ⟶ S₂
inst✝ : QuasiIso φ
⊢ QuasiIso (opMap (unopMap φ))
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 S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ S.g ≫ x = 0

Tactic:
S.zero_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 0 ≫ x = 0
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
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x

Tactic:
congr 1

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.descQ k ⋯ = h.g' ≫ x
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 : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ ≫ h.π = (x ≫ h.f') ≫ h.π

Tactic:
congr 1

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ h.liftK k ⋯ = x ≫ h.f'
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₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ LeftHomologyMapData φ h₁ h₂

Tactic:
let φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂)
    (by rw [assoc, φ.comm₂₃, h₁.wi_assoc, zero_comp])
  have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f' := by
    rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i,
      LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i, φ.comm₁₂]
  let φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π)
    (by rw [reassoc_of% commf', h₂.f'_π, comp_zero])
  exact ⟨φK, φH, by simp [φK], commf', by simp [φH]⟩

Goal state after: