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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
p q : LocalizedModule S M
⊢ x • (p + q) = x • p + x • q

Tactic:
by
  induction p with | _ m s
  induction q with | _ n t
  rw [smul_def, smul_def, mk_add_mk, mk_add_mk]
  rw [show x • _ = IsLocalization.mk' T _ _ • _ by rw [IsLocalization.mk'_sec (M := S) T]]
  rw [← IsLocalization.mk'_cancel _ _ (IsLocalization.sec S x).2, mk'_smul_mk]
  congr 1
  · simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]; ring_nf
  · rw [mul_mul_mul_comm]

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mk 1 1 = 1

Tactic:
simp [OreLocalization.one_def]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (End R (LocalizedModule S M))) ↑s) ((divBy s) (mk m t)) = mk m t

Tactic:
rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]

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

Goal state before:
pp: case h
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
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y

Tactic:
| _ a b
   => 

Goal state after:
case h
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
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ * m₂) = (↑s₁ * ↑s₂) • (mk' f m₁ s₁ * mk' f m₂ s₂)

Tactic:
← smul_eq_mul

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = (↑s₁ • ↑s₂) • mk' f m₁ s₁ • mk' f m₂ s₂
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

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
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g

Tactic:
rw [h]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ f ≫ g = fg

Tactic:
rw [h]

Goal state after:
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✝ F : B ⥤ᵖ C
a b b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2
X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ binaryProductFunctor.map x✝ ≫
      (NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
          ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
          ⋯).hom ≫
      prod.functor.map x✝

Tactic:
ext : 2
    apply Limits.prod.hom_ext <;> simp <;> rfl

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
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : (ιOfLE h₁).IsEquivalence
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)

Tactic:
exact ⟨_, _, ⟨((ιOfLE h₁).asEquivalence.symm.trans
      (Shrink.equivalence.{w} Q.FullSubcategory)).trans (ShrinkHoms.equivalence.{w'} _)⟩⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.left = Y.left

Tactic:
rw [h]

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.right = Y.right

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map ↑(unop f))) (unop Y✝).snd) = uliftYonedaEquiv.symm (unop X✝).snd

Tactic:
map_snd

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYonedaEquiv.symm (unop X✝).snd = uliftYonedaEquiv.symm (unop X✝).snd
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case of.of
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : Discrete J
a b : PLift (x✝¹.as = x✝.as)
⊢ { down := a } = { down := b }

pp: case of.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ : Discrete J
⊢ PUnit.unit = PUnit.unit

pp: case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit

Tactic:
· exact congr_arg (ULift.up ∘ PLift.up) rfl

Goal state after:
case of.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝ : Discrete J
⊢ PUnit.unit = PUnit.unit

case star.star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ PUnit.unit = PUnit.unit
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
x : RXm
⊢ f (aeval_h x) = f' x

Tactic:
← f.coe_toRingHom,

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
x : RXm
⊢ ↑f (aeval_h x) = f' x
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ (m ≫ f) ≫ h = (p ≫ f) ≫ h

Tactic:
grind [Fork.ofι, PullbackCone.mk]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
⊢ (map α).Final

Tactic:
have hα' : (map α').Final := final_map_small _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map α').Final
⊢ (map α).Final
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (PushoutCocone.mk h k comm).inr ≫ m = (PushoutCocone.mk h k comm).inr ≫ p

Tactic:
erw [← cancel_epi g, ← Category.assoc, ← eq_whisker comm]
      erw [← Category.assoc, ← eq_whisker comm]
      dsimp at z; simp only [Category.assoc, z]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pushouts

Tactic:
intro X Y p hp
  exact P.pushouts_mk IsPushout.of_id_fst hp

Goal state after:
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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
⊢ (i : Fin n) → c₂.pt ⟶ f i.succ

Tactic:
· intro i
        apply c₂.snd ≫ c₁.π.app ⟨i⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.universally.RespectsIso

Tactic:
apply RespectsIso.mk
  · intro X Y Z e f hf X' Z' i₁ i₂ f' H
    have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
      IsPullback.of_horiz_isIso
        ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
    exact hf _ _ _
      (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)
  · intro X Y Z e f hf X' Z' i₁ i₂ f' H
    have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv :=
      IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
    exact hf _ _ _ (by simpa only [Category.assoc, Iso.hom_inv_id,
      Category.comp_id, Category.comp_id] using H.paste_horiz this)

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 : A ⟶ B
g : A ⟶ 𝟙_ C
this : lift f g ≫ B ◁ η ≫ μ = lift f g ≫ (ρ_ B).hom
⊢ lift f (g ≫ η) ≫ μ = f

Tactic:
rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this

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
G : C
inst✝ : GrpObj G
⊢ μ ≫ ι = (ι ⊗ₘ ι) ≫ (β_ G G).hom ≫ μ

Tactic:
by simp [tensorHom_inv_inv_mul]

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ

Tactic:
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

Goal state after:
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:
by
  ext i x
  apply dualBasis_apply

Goal state after:
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 ι
i : ι
f : Dual R M
⊢ (b.coord i) (b.toDualEquiv.symm f) = (b.dualBasis.coord i) f

Tactic:
by
  simp [Basis.dualBasis]

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ▷ (X₁ ⊗ X₂) ≫
      (α_ (X₁ ⊗ X₂) (Y₂ ⊗ Y₁) (X₁ ⊗ X₂)).hom ≫ (X₁ ⊗ X₂) ◁ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) =
    (λ_ (X₁ ⊗ X₂)).hom ≫ (ρ_ (X₁ ⊗ X₂)).inv

Tactic:
by
    calc
      _ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          (X₁ ◁ η_ X₂ Y₂) ▷ (Y₁ ⊗ X₁ ⊗ X₂) ⊗≫
          (X₁ ⊗ X₂) ◁ (Y₂ ◁ ε_ X₁ Y₁ ▷ X₂) ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by monoidal
      -- Group η₂ and ε₁ so they compose with ≫:
      --
      --   ╭── Y₁ ────────────╮       X₁   X₂
      --   │    ╭── Y₂ ───╮   │       │    │
      --   │    │         │   │       │    │
      --   │    │         │   ╰──ε₁───╯    │
      --   │    │         │                │
      --   │    │         ╰──────── ε₂ ────╯
      --   X₁   X₂
      --
      _ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          X₁ ◁ (η_ X₂ Y₂ ▷ (Y₁ ⊗ X₁) ≫ (X₂ ⊗ Y₂) ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by monoidal
      -- Slide the ε₁ cap past the η₂ cup (← whisker_exchange), separating the
      -- two zigzags into independent snakes:
      --
      --                 X₁   X₂
      --   ╭──Y₁──╮      │    │
      --   │      │      │    │
      --   │      ╰──────╯    │       ← snake for (X₁, Y₁)
      --   │                  │
      --   │   ╭──Y₂──╮       │
      --   │   │      │       │
      --   │   │      ╰───────╯       ← snake for (X₂, Y₂)
      --   X₁  X₂
      --
      _ = η_ X₁ Y₁ ▷ (X₁ ⊗ X₂) ⊗≫
          X₁ ◁ ((𝟙_ C) ◁ ε_ X₁ Y₁ ≫ η_ X₂ Y₂ ▷ (𝟙_ C)) ▷ X₂ ⊗≫
          (X₁ ⊗ X₂) ◁ ε_ X₂ Y₂ := by
        rw [← whisker_exchange]
      -- Separate into two snakes and cancel each.
      _ = 𝟙 _ ⊗≫ (η_ X₁ Y₁ ▷ X₁ ⊗≫ X₁ ◁ ε_ X₁ Y₁) ▷ X₂ ⊗≫
          X₁ ◁ (η_ X₂ Y₂ ▷ X₂ ⊗≫ X₂ ◁ ε_ X₂ Y₂) ⊗≫ 𝟙 _ := by monoidal
      _ = _ := by rw [evaluation_coevaluation'', evaluation_coevaluation'']; monoidal

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_1
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
← b.mk_eq_rank'',

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : ℵ₀ ≤ #ι
b : Module.Basis ι K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type u_2
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
← b.mk_eq_rank'',

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : ℵ₀ ≤ #ι
b : Module.Basis ι K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)
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
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
← b.mk_eq_rank'',

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Module.Basis ι K V
⊢ lift.{u, v} #ι < Module.rank Kᵐᵒᵖ (V →ₗ[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
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(comap (s ⊔ t).subtype t) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
(equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq,

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
s t : Submodule R M
⊢ Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(map (s ⊔ t).subtype (comap (s ⊔ t).subtype t)) +
      Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ (η_ X' Y ≫ i.inv ▷ Y) ≫ (α_ Y X Y).inv ≫ (Y ◁ i.hom ≫ ε_ X' Y) ▷ Y = (ρ_ Y).hom ≫ (λ_ Y).inv

Tactic:
by
    calc
      _ = Y ◁ η_ X' Y ≫ Y ◁ (i.inv ≫ i.hom) ▷ Y ⊗≫ ε_ X' Y ▷ Y := by
        monoidal
      _ = Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [coevaluation_evaluation'']
        simp

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

Goal state before:
pp: case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
· rw [ker_pow_eq_ker_pow_finrank_of_le h_cases]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
simp only [Submodule.mk_eq_zero]

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ x = 0
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✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h✝ : Infinite ι
a✝ : Nontrivial K
n : ℕ
hn : ∀ (f : Dual K V →ₗ[K] Fin n → K), ¬Function.Surjective ⇑f
g : (ι → K) ≃ₗ[K] Dual K V := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
⊢ Module.Finite K V

Tactic:
exact hn (LinearMap.funLeft K K (Fin.valEmbedding.trans (Infinite.natEmbedding ι)) ∘ₗ _)
    ((Function.Embedding.injective _).surjective_comp_right.comp g.symm.surjective) |>.elim

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

Goal state before:
pp: case neg
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
⊢ False

Tactic:
· have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
    rw [sub_eq_add_neg, ← neg_smul, add_comm] at h
    exact (Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

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

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

Tactic:
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.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₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)

Tactic:
have : finrank K ↑(LinearMap.ker f ⊔ p) = finrank K (LinearMap.ker f) + finrank K p := by
    simp [← Submodule.finrank_sup_add_finrank_inf_eq (LinearMap.ker f) p, hpf.eq_bot]

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
p : Submodule K V₁
hpf : Disjoint (LinearMap.ker f) p
hp : p ≠ ⊥
this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p
⊢ finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)