mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ lift x✝¹ x✝ e ≫ snd f f = x✝

Tactic:
lift_snd

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝ = x✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g], P f → ∃ T inl inr, IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
x✝ : HasPushout f g
hg : P f
T : C
inl : S ⟶ T
inr : Y ⟶ T
h : IsPushout f g inl inr
hinl : P inr
⊢ P (inr ≫ h.isoPushout.hom)

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g], P f → ∃ T inl inr, IsPushout f g inl inr ∧ P inr
X Y S : C
f : X ⟶ S
g : X ⟶ Y
x✝ : HasPushout f g
hg : P f
T : C
inl : S ⟶ T
inr : Y ⟶ T
h : IsPushout f g inl inr
hinl : P inr
⊢ P inr
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ ObjectProperty.Small.{w, v_1, u_1} (P.strictLimitsOfShape J)

Tactic:
refine small_of_surjective
    (f := fun (F : { F : J ⥤ P.FullSubcategory // HasLimit (F ⋙ P.ι) }) ↦
      (⟨_, letI := F.2; ⟨F.1 ⋙ P.ι, fun j ↦ (F.1.obj j).2⟩⟩)) ?_

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'
inst✝³ : ObjectProperty.Small.{w, v_1, u_1} P
inst✝² : LocallySmall.{w, v_1, u_1} C
inst✝¹ : Small.{w, u'} J
inst✝ : LocallySmall.{w, v', u'} J
⊢ Function.Surjective fun F ↦ ⟨limit (↑F ⋙ P.ι), ⋯⟩
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
i : Fin n
⊢ f i.succ ⟶ c₂.pt

Tactic:
apply c₁.ι.app ⟨i⟩ ≫ c₂.inr

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯))

Tactic:
← P.cancel_right_of_respectsIso _
        (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) (by simp) (by simp)),

Goal state after:
case hprecomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
H : P.diagonal f
⊢ P
    (pullback.snd (pullback.diagonal f) (pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯) ≫
      pullback.map (e.hom ≫ f) (e.hom ≫ f) f f e.hom e.hom (𝟙 Z) ⋯ ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f e.hom).inv ≫
        pullback.snd (pullback.diagonal e.hom) (pullback.map (f ≫ e.hom) (f ≫ e.hom) e.hom e.hom f f (𝟙 Z) ⋯ ⋯))

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
case hpostcomp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
H : P.diagonal f
⊢ P (pullback.diagonal f)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)) ≫ (diagonalObjPullbackFstIso f g).inv)

Tactic:
P.cancel_right_of_respectsIso

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))
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 A
inst✝¹ : Bialgebra R C
inst✝ : IsCocomm R C
f : WithConv (C →ₐc[R] A)
n : ℕ
⊢ toConv ↑(f ^ (n + 1)).ofConv = toConv ↑f.ofConv ^ (n + 1)

Tactic:
simp only [convPow_succ, pow_succ, toAlgHom_convMul, toAlgHom_convPow]

Goal state after:
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
⊢ lift (μ ≫ ι) (μ ≫ 𝟙 A) ≫ μ = lift ((β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ) μ ≫ μ

Tactic:
rw [← comp_lift, Category.assoc, left_inv, ← Category.assoc (β_ A A).hom,
    ← lift_snd_fst, lift_map, lift_lift_assoc]

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 ≫ ι) μ ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ∀ (s : PullbackCone μ μ) (m : s.pt ⟶ (A ⊗ A) ⊗ A),
    m ≫ μ ▷ A = s.fst →
      m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
        m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)

Tactic:
by
      intro s m hm₁ hm₂
      refine CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_
      · simpa using hm₂ =≫ fst _ _
      · have h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using hm₂ =≫ fst _ _
        have := hm₁ =≫ fst _ _
        simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢
        rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this
        rwa [← assoc s.snd, eq_lift_inv_left]
      · simpa using hm₁ =≫ snd _ _

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {a b : ↥(closure s)},
    a ∈ Set.range (WType.elim (↥(closure s)) (operate s)) →
      b ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → a * b ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨WType.mk (.inl 1) (Bool.rec x y), by rfl⟩

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

Goal state before:
pp: case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ (Dual.eval R M).range = ⊤

Tactic:
← b.toDual_toDual,

Goal state after:
case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, u} (Module.rank R M) = lift.{u, v} (Module.rank R M') + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
by
  rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h]

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

Goal state before:
pp: case h₁
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{u, v} (Module.rank R ↥f'.range) ≤ lift.{u, v} (Module.rank R ↥p)

Tactic:
rwa [lift_le]

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

Goal state before:
pp: case h₂
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
f' : ↥(comap f p) →ₗ[R] ↥p := ⋯
hk : Module.rank R ↥f'.ker ≤ Module.rank R ↥f.ker
hr : Module.rank R ↥f'.range ≤ Module.rank R ↥p
⊢ lift.{v, u} (Module.rank R ↥f'.ker) ≤ lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
rwa [lift_le]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ η_ X Xᘁ ≫ Zᘁ ◁ (f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ η_ Y Yᘁ ≫
        Zᘁ ◁ (g ⊗ₘ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom)

Tactic:
simp only [← MonoidalCategory.whiskerLeft_comp]

Goal state after:
case e_a.e_a.e_a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ρ_ Zᘁ).inv ≫ Zᘁ ◁ (η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ) =
    (ρ_ Zᘁ).inv ≫
      Zᘁ ◁ (η_ Y Yᘁ ≫ (g ⊗ₘ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom))
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M ⧸ p →ₗ[R] ↥f.range ⧸ Submodule.map f.rangeRestrict p :=
  p.mapQ (Submodule.map f.rangeRestrict p) f.rangeRestrict ⋯
⊢ Surjective ⇑f'

Tactic:
rw [← range_eq_top, range_mapQ]; simp

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

Goal state before:
pp: 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)
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker

Tactic:
let L : V₁ →ₗ[K] ker (coprod db eb) :=
    LinearMap.codRestrict _ (prod cd (-ce)) <| by
      simpa [add_eq_zero_iff_eq_neg] using LinearMap.ext_iff.1 eq

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)
L : V₁ →ₗ[K] ↥(db.coprod eb).ker := LinearMap.codRestrict (db.coprod eb).ker (cd.prod (-ce)) ⋯
⊢ V₁ ≃ₗ[K] ↥(db.coprod eb).ker
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (X ◁ ᘁf) ≫ ε_ (ᘁX) X = f ▷ ᘁY ≫ ε_ (ᘁY) Y

Tactic:
apply_fun tensorLeftHomEquiv _ (ᘁX) X _
  simp

Goal state after:
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
⊢ ↑(Fintype.card (ChooseBasisIndex R M)) * lift.{v, w} (Module.rank S N) =
    lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)

Tactic:
← finrank_eq_card_chooseBasisIndex,

Goal state after:
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
⊢ ↑(finrank R M) * lift.{v, w} (Module.rank S N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
⊢ ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 =
    (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p)

Tactic:
ext <;>
    simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
      fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

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

Goal state before:
pp: K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this✝ : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Tactic:
lift_umax,

Goal state after:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this✝ : ℵ₀ ≤ Module.rank K V
this : lift.{uK, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : (RingHom.id R) (vi i) • (B (v i)) (v i) = 0
h✝ : (B (v i)) (v i) = 0
⊢ vi i = 0

Tactic:
specialize h i
      contradiction

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ Disjoint (LinearMap.ker f) p

Tactic:
rw [disjoint_iff, Submodule.eq_bot_iff]

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ ∀ x ∈ LinearMap.ker f ⊓ p, x = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
c : Cone (parallelPair 0 0)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)

Tactic:
by
    have := KernelFork.IsLimit.isIso_ι c hc rfl
    refine (KernelFork.isLimitMapConeEquiv c G).symm ?_
    refine IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) ?_
    exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ IsColimit (CokernelCofork.ofπ f' ⋯)

Tactic:
by
    refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit
    · exact parallelPair.ext (Iso.refl _) (Arrow.leftFunc.mapIso e)
    · exact Cofork.ext (Arrow.rightFunc.mapIso e) (by simp [Cofork.π])

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' : a ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
⊢ a ≫ a' = b ≫ b'

Tactic:
rw [ha', hb']

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 c d : X ⟶ Y
⊢ prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d)

Tactic:
simp only [sub_def]

Goal state after:
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.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)
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.map prod.fst prod.fst ≫ σ =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

Tactic:
prod.lift_map_assoc,

Goal state after:
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.fst) (prod.lift c d ≫ prod.fst) ≫ σ =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst
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.map prod.snd prod.snd ≫ σ =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd

Tactic:
prod.lift_map_assoc,

Goal state after:
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.snd) (prod.lift c d ≫ prod.snd) ≫ σ =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd
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 - (a - b)

Tactic:
← sub_self (0 : X ⟶ Y)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.rightHomologyIso.inv ≫ S.rightHomologyι ≫ S.descOpcycles k ⋯ = 0

Tactic:
S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.rightHomologyIso.inv ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
hg : S.g = 0
inst✝ : S.HasHomology
⊢ S.homology ≅ S.opcycles

Tactic:
by
  have := S.isIso_homologyι hg
  exact asIso S.homologyι

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
  rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
    ShortComplex.RightHomologyMapData.map_φH]

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      rightHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
simp only [RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
    ← rightHomologyMap'_comp, comp_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ IsZero S.homology ↔ IsZero h.H
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ IsZero S.homology ↔ IsZero h.H