mathlib-initiative/mathlib-tactics huggingface dataset:
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:
induction y with

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

Goal state before:
pp: X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ 0 = 1

Tactic:
← f.hom.map_one,

Goal state after:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ 0 = (Hom.hom f) 1
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
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯) ((iso S f).symm (mk' f x s)) = mk' g (h x) s

Tactic:
iso_symm_apply' S f (mk' f x s) x s (mk'_cancel' f x s),

Goal state after:
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
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
x : M
s : ↥S
⊢ (LocalizedModule.lift S (g ∘ₗ h) ⋯) (LocalizedModule.mk x s) = mk' g (h x) s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ (algebraMap R S') ↑x * ↑⋯.unit⁻¹ * a = a

Tactic:
IsUnit.mul_val_inv,

Goal state after:
case map_units.right
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
x : ↥M
a : S'
⊢ 1 * a = a
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S g
inst✝ : Subsingleton M
m : M
⊢ 1 ∈ S ∧ 1 • m = 0

Tactic:
simp [one_mem, Subsingleton.elim m 0]

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

Goal state before:
pp: case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
| sup I₁ I₂ _ _ h₁ h₂ =>

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : P.FullSubcategory
X : C
hX : P X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX })

Tactic:
← h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : P.FullSubcategory
X : C
hX✝ : P X
hX : Q.inverseImage e.functor X
⊢ Q ((P.ι ⋙ e.functor).obj { obj := X, property := hX✝ })
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ P ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })

Tactic:
← h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ Q.inverseImage e.functor ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P
    exact ⟨Q.op, inferInstance, by rwa [← op_isoClosure, op_monotone_iff]⟩

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 : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ (comp f Y.id).base = f.base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber

Tactic:
· simp [comp, id]

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
⊢ fib c = (F.map (𝟙 c)).toFunctor ⋙ fib c

Tactic:
simp only [Functor.map_id]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
c : C
⊢ fib c = (𝟙 (F.obj c)).toFunctor ⋙ fib c
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j

Tactic:
rw [← s.w f]

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
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
⊢ (MvPolynomial.aeval fun i ↦ f' (MvPolynomial.X i)) x = f' x

Tactic:
← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),

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
⊢ (MvPolynomial.aeval fun i ↦ (⇑f' ∘ MvPolynomial.X) i) x = f' x
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₁ ≫ G.map k₁ = s.π.app j
⊢ s.π.app j₂ ≫ G.map k₂ = s.π.app j

Tactic:
rw [← s.w f]

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j₁ ⟶ F.obj j
k₂ : F.obj j₂ ⟶ F.obj j
f : j₁ ⟶ j₂
w : F.map f ≫ k₂ = k₁
h : s.π.app j₁ ≫ G.map k₁ = s.π.app j
⊢ (s.π.app j₁ ≫ (F ⋙ G).map f) ≫ G.map k₂ = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsColimit (ofπ f ⋯)
⊢ f.unop ≫ (pullback.fst f f).unop = f.unop ≫ (pullback.snd f f).unop

Tactic:
simp only [← unop_comp, pullback.condition]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.op ⋯)
⊢ f.op.unop ≫ (pullback.fst f.op f.op).unop = f.op.unop ≫ (pullback.snd f.op f.op).unop

Tactic:
simp only [← unop_comp, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom

Tactic:
inr_inl_pushoutAssoc_hom

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) =
    pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone coproducts.{w, v, u}

Tactic:
by
  rintro W₁ W₂ h X Y f hf
  rw [coproducts_iff] at hf
  obtain ⟨J, hf⟩ := hf
  exact W₂.colimitsOfShape_le_coproducts J _
    (colimitsOfShape_monotone h _ _ hf)

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

Goal state before:
pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯

Tactic:
intro c m hfst hsnd

Goal state after:
case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
J : Type w
hf : W.colimitsOfShape (Discrete J) f
⊢ W f

Tactic:
exact colimitsOfShape_le _ hf

Goal state after:
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
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
f g : X ⟶ M
⊢ f * g = g * f

Tactic:
simpa [-IsCommMonObj.mul_comm] using! lift g f ≫= IsCommMonObj.mul_comm M

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
M : C
inst✝ : MonObj M
⊢ μ = μ

Tactic:
change lift (fst M M) (snd M M) ≫ μ = μ

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ lift (fst M M) (snd M M) ≫ μ = μ
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
C : Type u_5
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
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
h : A →ₙₐ[R] B
f g : WithConv (C →ₗ[R] A)
⊢ ↑h ∘ₗ (f * g).ofConv = (toConv (↑h ∘ₗ f.ofConv) * toConv (↑h ∘ₗ g.ofConv)).ofConv

Tactic:
simp [convMul_def, map_comp, ← comp_assoc, NonUnitalAlgHom.comp_mul']

Goal state after:
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 = (algebraMap R A) (counit a)

Tactic:
simpa [← repr.eq, map_sum] using congr($(mul_antipode_rTensor_comul (R := R)) a)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Bialgebra R A
antipode : A →ₐ[R] A
mul_antipode_rTensor_comul :
  (Algebra.TensorProduct.lift antipode (AlgHom.id R A) ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
mul_antipode_lTensor_comul :
  (Algebra.TensorProduct.lift (AlgHom.id R A) antipode ⋯).comp (comulAlgHom R A) =
    (Algebra.ofId R A).comp (counitAlgHom R A)
⊢ (toConv antipode.toLinearMap * toConv LinearMap.id).ofConv = ofConv 1

Tactic:
simpa [← Algebra.TensorProduct.lmul'_comp_map]
        using! congr(($mul_antipode_rTensor_comul).toLinearMap)

Goal state after:
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₂ : F ⊣₂ G
X₁ Y₁ : C₁
X₂ : C₂
X₃ : C₃
f₁ : X₁ ⟶ Y₁
g : (F.obj Y₁).obj X₂ ⟶ X₃
⊢ adj₂.homEquiv ((F.map f₁).app X₂ ≫ g) = adj₂.homEquiv g ≫ (G.map f₁.op).app X₃

Tactic:
have := NatTrans.congr_app (adj₂.unit_whiskerRight_map f₁) X₂
  dsimp at this
  simp only [homEquiv_eq, Adjunction.homEquiv_unit, Functor.comp_obj, Functor.map_comp,
    Category.assoc, NatTrans.naturality, reassoc_of% this]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X✝ : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((yoneda.obj G).map f ≫ ↾fun f ↦ ⅟f) = (↾fun f ↦ ⅟f) ≫ (yoneda.obj G).map f

Tactic:
ext g

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X✝ : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : (yoneda.obj G).obj X
⊢ (ConcreteCategory.hom ((yoneda.obj G).map f ≫ ↾fun f ↦ ⅟f)).toFun g =
    (ConcreteCategory.hom ((↾fun f ↦ ⅟f) ≫ (yoneda.obj G).map f)).toFun g
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫
        (x ◁ curry (ρ_ x).hom) ▷ (ihom x).obj y ≫ (ihom.ev x).app x ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))

Tactic:
← comp_whiskerRight_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ x ◁ (λ_ ((ihom x).obj y)).inv ≫
      (α_ x (𝟙_ C) ((ihom x).obj y)).inv ≫
        (x ◁ curry (ρ_ x).hom ≫ (ihom.ev x).app x) ▷ (ihom x).obj y ≫ (ihom.ev x).app y =
    uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
w x y z : C
inst✝² : Closed w
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (α_ ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv ≫ comp w x y ▷ (ihom y).obj z ≫ comp w y z =
    (ihom w).obj x ◁ comp x y z ≫ comp w x z

Tactic:
apply uncurry_injective
  simp only [uncurry_natural_left, comp_eq]
  rw [uncurry_curry, uncurry_curry]; simp only [compTranspose_eq]
  rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc]; dsimp
  rw [← uncurry_eq, uncurry_curry, associator_inv_naturality_right_assoc, whisker_exchange_assoc,
    ← uncurry_eq, uncurry_curry]
  simp

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

Tactic:
← comp_whiskerRight_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 : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ (X ◁ curry' f ≫ (ihom.ev X).app Y) ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
h : (n :: m :: l).SortedLE
⊢ raise (lower (m :: l) n) n = m :: l

Tactic:
have : n ≤ m := List.rel_of_pairwise_cons h.pairwise List.mem_cons_self
    simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.pairwise.of_cons.sortedLE]

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

Goal state before:
pp: case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ

Goal state after:
case mk
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a ↦ lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
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'
p : Submodule R M'
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
by
  let f' : comap f p →ₗ[R] p := f.restrict (by aesop)
  have hk : Module.rank R f'.ker ≤ Module.rank R f.ker := by
    rw [← rank_map_eq (injective_subtype (comap f p))]
    exact rank_mono fun x hx ↦ by aesop (add simp Subtype.ext_iff)
  have hr : Module.rank R f'.range ≤ Module.rank R p := by grw [Submodule.rank_le f'.range]
  rw [← f'.lift_rank_range_add_rank_ker]
  gcongr <;> rwa [lift_le]

Goal state after:
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
hst : Disjoint s (sec '' t)
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩

Goal state after:
case refine_1
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
hst : Disjoint s (sec '' t)
⊢ #↑(s ∪ sec '' t) = Module.rank R M

case refine_2
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
hst : Disjoint s (sec '' t)
⊢ LinearIndepOn R _root_.id (s ∪ sec '' t)