mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M'
inst✝¹⁵ : AddCommMonoid M''
A : Type u_5
inst✝¹⁴ : CommSemiring A
inst✝¹³ : Algebra R A
inst✝¹² : Module A M'
inst✝¹¹ : IsLocalization S A
inst✝¹⁰ : Module R M
inst✝⁹ : Module R M'
inst✝⁸ : Module R M''
inst✝⁷ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M₁
e : (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂
⊢ ∃ c, c • x₁ = c • x₂

Tactic:
obtain ⟨x₁, s₁, rfl⟩ := mk'_surjective S₁ f₁ x₁

Goal state after:
R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid M'
inst✝¹⁵ : AddCommMonoid M''
A : Type u_5
inst✝¹⁴ : CommSemiring A
inst✝¹³ : Algebra R A
inst✝¹² : Module A M'
inst✝¹¹ : IsLocalization S A
inst✝¹⁰ : Module R M
inst✝⁹ : Module R M'
inst✝⁸ : Module R M''
inst✝⁷ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝⁶ : IsLocalizedModule S f
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₂ : M₁
x₁ : M × ↥S₁
e : (liftOfLE S₁ S₂ h f₁ f₂) (Function.uncurry (mk' f₁) x₁) = (liftOfLE S₁ S₂ h f₁ f₂) x₂
⊢ ∃ c, c • Function.uncurry (mk' f₁) x₁ = c • x₂
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
h : g (f (↑n • x)) = g (f (↑m • y))
⊢ a = b

Tactic:
apply H at h
    rw [map_smul, map_smul] at h
    rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom

Tactic:
simp only [Category.assoc]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b) ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom

Tactic:
simp only [Category.assoc]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Algebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Algebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommAlgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (CommAlgCat.{u} R)).map f)

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Algebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Algebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommAlgCat R)).map f)
i : (forget (CommAlgCat R)).obj X ≅ (forget (CommAlgCat R)).obj Y := asIso ((forget (CommAlgCat R)).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    (asIso (F.mapComp (f ≫ g) h)).hom ≫
      (asIso (F.mapComp f g)).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫
          F.map f ◁ (asIso (F.mapComp g h)).inv ≫ (asIso (F.mapComp f (g ≫ h))).inv

Tactic:
by
    dsimp
    simp only [← assoc]
    rw [IsIso.eq_comp_inv, ← Bicategory.inv_whiskerLeft, IsIso.eq_comp_inv]
    simp only [assoc, F.map₂_associator]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I

Tactic:
← add_eq_sup,

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J + K) ^ (n + m) ≤ I
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: X : Type u_1
a b : Discrete X
h : Zigzag a b
⊢ a.as = b.as

Tactic:
by
  induction h with
  | refl => rfl
  | tail _ h eq => exact eq.trans (eq_of_zag _ h)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).EssSurj ↔ Q ≤ P.isoClosure

Tactic:
by
  refine ⟨fun _ X hX ↦ ?_, fun hPQ ↦ ⟨fun ⟨Y, hY⟩ ↦ ?_⟩⟩
  · exact ⟨_, ((ιOfLE h).objPreimage ⟨X, hX⟩).2,
      ⟨Q.ι.mapIso ((ιOfLE h).objObjPreimageIso ⟨X, hX⟩).symm⟩⟩
  · obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY
    exact ⟨⟨X, hX⟩, ⟨Q.ι.preimageIso e.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le.{w} P

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : F.Elements
f : { f // (ConcreteCategory.hom (F.map f)) X.snd = Y.snd }
g : { f // (ConcreteCategory.hom (F.map f)) Y.snd = Z.snd }
⊢ (ConcreteCategory.hom (F.map (↑f ≫ ↑g))) X.snd = Z.snd

Tactic:
simp [f.2, g.2]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ } =
    { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
      { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }

Tactic:
by ext; simp; apply Functor.map_comp colim

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ ((map (whiskerRight α Cat.asSmallFunctor)).map f ≫
        (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom).base =
    ((Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
        ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f).base

Tactic:
simp [compAsSmallFunctorEquivalenceInverse]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
X : G.Elements
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj X ≅ (𝟭 G.Elements).obj X

Tactic:
by
        cases X
        exact Iso.refl _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c : Comma (Functor.const C) (𝟭 (C ⥤ D))
x y : C
f : x ⟶ y
⊢ c.hom.app x ≫ c.right.map f = c.hom.app y

Tactic:
simpa using (c.hom.naturality f).symm

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
this : lift (lift f g) h ≫ μ ▷ B ≫ μ = lift (lift f g) h ≫ (α_ B B B).hom ≫ B ◁ μ ≫ μ
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ

Tactic:
lift_whiskerRight_assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f g h : A ⟶ B
this : lift (lift f g ≫ μ) h ≫ μ = lift (lift f g) h ≫ (α_ B B B).hom ≫ B ◁ μ ≫ μ
⊢ lift (lift f g ≫ μ) h ≫ μ = lift f (lift g h ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
this : lift f g ≫ η ▷ B ≫ μ = lift f g ≫ (λ_ B).hom
⊢ lift (f ≫ η) g ≫ μ = g

Tactic:
lift_whiskerRight_assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
this : lift (f ≫ η) g ≫ μ = lift f g ≫ (λ_ B).hom
⊢ lift (f ≫ η) g ≫ μ = g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
X : C
e : (F ⋙ forget MonCat).RepresentableBy X
⊢ yonedaMon.essImage F

Tactic:
let := MonObj.ofRepresentableBy X F e

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
X : C
e : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F e
⊢ yonedaMon.essImage F
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = counit a • 1

Tactic:
sum_antipode_mul_eq_algebraMap_counit,

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ (algebraMap R A) (counit a) = counit a • 1
Module: Mathlib.CategoryTheory.Adjunction.Parametrized

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (op X₁)
h :
  ∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) {X₂ : C₂} {X₃ : C₃} (g : (F.obj Y₁).obj X₂ ⟶ X₃),
    ((adj X₁).homEquiv X₂ X₃) ((F.map f).app X₂ ≫ g) = ((adj Y₁).homEquiv X₂ X₃) g ≫ (G.map f.op).app X₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (adj X₁).unit ≫ whiskerRight (F.map f) (G.obj (op X₁)) = (adj Y₁).unit ≫ (F.obj Y₁).whiskerLeft (G.map f.op)

Tactic:
ext X₂
    simpa [Adjunction.homEquiv_unit] using h f (X₂ := X₂) (𝟙 _)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (antipodeAlgHom R A) * toConv (AlgHom.id R A) = 1

Tactic:
by
  apply WithConv.ofConv_injective
  apply AlgHom.toLinearMap_injective
  apply WithConv.toConv_injective
  rw [AlgHom.toLinearMap_convMul, AlgHom.toLinearMap_convOne]
  simp [LinearMap.antipode_mul_id]

Goal state after:
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 : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫
        (X ⊗ (ihom X).obj Y) ◁ curry' f ≫ (ihom.ev X).app Y ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Tactic:
whisker_exchange_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (𝟭 C).obj Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (ihom.ev M).app N =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
rw [← MonoidalClosed.uncurry_id_eq_ev]
  ext : 1
  apply TensorProduct.ext'
  apply monoidalClosed_uncurry

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

Goal state before:
pp: case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ #↑s = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
add_eq_right h (this.le.trans h),

Goal state after:
case e'_4.inr
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : ℵ₀ ≤ #↑s
⊢ #↑s = max #↑s ℵ₀
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 = b.coord

Tactic:
ext i x

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 : ι
x : M
⊢ (b.dualBasis i) x = (b.coord i) x
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 [Category.assoc]

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ᘁ ≫ 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)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
by
  obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
  rw [← b.mk_eq_rank'', rank_dual_eq_card_dual_of_aleph0_le_rank' h,
      ← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq, mk_arrow]
  apply cantor'
  rw [one_lt_lift_iff, one_lt_iff_nontrivial]
  infer_instance

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ) ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    ((λ_ ᘁZ).inv ≫ η_ (ᘁY) Y ▷ ᘁZ) ≫
      ((((((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY) ≫ (ᘁX ◁ f) ▷ ᘁY) ≫ (α_ (ᘁX) Y ᘁY).hom) ≫ ᘁX ◁ ε_ (ᘁY) Y) ≫ (ρ_ ᘁX).hom ⊗ₘ g) ▷
        ᘁZ

Tactic:
simp only [Category.assoc]

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✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    (λ_ ᘁZ).inv ≫
      η_ (ᘁY) Y ▷ ᘁZ ≫
        ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ₘ g) ▷ ᘁZ
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]
  congr! 2 with n m
  refine forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right
  refine fun f ↦ .trans (forall_congr' fun g ↦ ?_) (transposeAddEquiv ..).forall_congr_right
  rw [← (transposeAddEquiv ..).injective.eq_iff, ← (transposeAddEquiv (Fin m) ..).injective.eq_iff]
  congrm (?_ = ?_ → ?_ = ?_ → _)
  iterate 2 ext; simp [map, mul_apply]; simp

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
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
⊢ IsSimpleOrder (Submodule A V)

Tactic:
by
  have := nontrivial_of_finrank_eq_succ h
  refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩
  rw [← restrictScalars_inj K] at hn ⊢
  have : FiniteDimensional _ _ := .of_finrank_eq_succ h
  refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)
  simpa only [h, finrank_bot] using! Submodule.finrank_strictMono (Ne.bot_lt hn)

Goal state after:
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
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y) = (ᘁf) ≫ (ρ_ ᘁX).inv

Tactic:
by
  dsimp [tensorLeftHomEquiv, leftAdjointMate]
  simp

Goal state after:
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✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ η_ Y Yᘁ ≫ Y ◁ fᘁ = η_ X Xᘁ ≫ f ▷ Xᘁ

Tactic:
apply_fun (tensorLeftHomEquiv _ Y (Yᘁ) _).symm

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ Y Yᘁ ≫ Y ◁ fᘁ) =
    (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
· have := Module.nontrivial K L
    rw [lift_id, Module.rank_linearMap_self]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : B.SeparatingLeft
⊢ ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft

Tactic:
intro x hx
  rw [← e₁.symm.map_eq_zero_iff]
  refine h (e₁.symm x) fun y ↦ ?_
  specialize hx (e₂ y)
  simp only [LinearEquiv.arrowCongr_apply, LinearEquiv.symm_apply_apply,
    LinearEquiv.map_eq_zero_iff] at hx
  exact hx

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 f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι

Tactic:
by rw [← F.map_comp, q.top_rightRetraction, F.map_comp]

Goal state after:
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
W : Subspace K V
⊢ dualRestrict W ∘ₗ W.dualLift = 1

Tactic:
ext φ x
  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
inst✝ : IsNormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ IsRegularMono f

Tactic:
by
    have := normalMonoOfMono f
    infer_instance

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
⊢ coprod.inl ≫ coprod.desc f g ≫ b ≫ s.inr = f ≫ b ≫ s.inr

Tactic:
by rw [coprod.inl_desc_assoc]

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 : X ⟶ Y
⊢ a - (a - a) = a

Tactic:
sub_self,

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯) ≫ F.m = kernel.ι (cokernel.π f)

Tactic:
simp only [Category.assoc]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯ ≫ F.m = kernel.ι (cokernel.π f)