mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

Tactic:
· simp only [hx, optionCongr_apply, Option.map_some, swap_apply_left,
             Option.some.injEq]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 2)).cycleType = {n + 2}

Tactic:
by
  rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f p : Perm α
l : List (Perm α)
hl : l.Nodup
hl' : (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = f
⊢ p ∈ l.toFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a

Tactic:
simpa [List.mem_toFinset, Ne, ← hl'.right.right] using
    mem_list_cycles_iff hl'.left hl'.right.left

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑(f.cycleFactorsFinset ∪ g.cycleFactorsFinset)).Pairwise Disjoint

Tactic:
coe_union,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (↑f.cycleFactorsFinset ∪ ↑g.cycleFactorsFinset).Pairwise Disjoint
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : c = c'
⊢ Commute c c'

pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'

Tactic:
· rw [hcc']

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
c' : Perm α
hc' : c' ∈ g.cycleFactorsFinset
hcc' : ¬c = c'
⊢ Commute c c'
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ (f fun i ↦ x i) = g fun i ↦ x i

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
val✝ : Fintype ι
⊢ (f fun i ↦ x i) = g fun i ↦ x i
Module: Mathlib.LinearAlgebra.Multilinear.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
⊢ f = g

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
⊢ f = g
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
x : ι → M₂
⊢ ((fun f ↦ { toFun := fun x ↦ f (x i), map_update_add' := ⋯, map_update_smul' := ⋯ })
        ((fun f ↦ { toFun := fun x ↦ f fun x_1 ↦ x, map_add' := ⋯, map_smul' := ⋯ }) f))
      x =
    f x

Tactic:
refine congr_arg f ?_

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
x : ι → M₂
⊢ (fun x_1 ↦ x i) = x
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
⊢ adjp s A none none = detp s (A.submatrix some some)

Tactic:
simp [adjp_none_right]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.mul zero) = descFunLift F s zero

Tactic:
dsimp; rw [mul_zero]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.mul_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.mul zero) = descFunLift F s zero

Tactic:
dsimp; rw [mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
σ : Perm n
M : Matrix n n R
⊢ sign σ • detRowAlternating M = ↑↑(sign σ) * M.det

Tactic:
simp [Units.smul_def, det]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (Aᵀ * adjp 1 Aᵀ) j i = (Aᵀ * adjp (-1) Aᵀ) j i

Tactic:
mul_adjp_apply_ne _ _ _ h.symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop = g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop

Tactic:
exact IsFiltered.coeq_condition f.unop g.unop

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
e : F.ColimitType ≃ c.pt :=
  { toFun := F.descColimitType c, invFun := hc.down.desc F.coconeTypes, left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (F.descColimitType c)

Tactic:
exact e.bijective

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

Goal state before:
pp: case e'_2.e'_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
e_1✝ : (fun X ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i) = (colimitCocone F).pt
⊢ (hom ((colimitCocone F).ι.app j)) xj =
    (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)).toEquiv ((hom (t.ι.app j)) xj)

Tactic:
exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommRingCat
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(F.obj x✝²)
⊢ (Hom.hom
        (F.map f ≫
          ofHom
            (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝¹))))
      x✝ =
    (Hom.hom
        (ofHom
            (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝²)) ≫
          ((Functor.const J).obj (colimit F)).map f))
      x✝

Tactic:
simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ Cᵒᵖ
X : C
s : ↑(F ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ (↑s j').op = (↑s j).op ≫ F.map f

Tactic:
exact Quiver.Hom.unop_inj (s.property f).symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv.hom ≫ (liftedLimitMapsToOriginal t).hom.hom) ≫ c.π.app j = c.π.app j

Tactic:
← Cone.category_comp_hom

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv ≫ (liftedLimitMapsToOriginal t).hom).hom ≫ c.π.app j = c.π.app j
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ s.pt.map f ≫
      (t Y).lift { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) } ≫
        (((evaluation K C).obj Y).mapCone c).π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j

Tactic:
(t Y).fac _ j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ s.pt.map f ≫ { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) }.π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
a✝ : IsIso (h.counit.app X)
⊢ L.essImage X

Tactic:
exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv = (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z

Tactic:
simp [← cancel_epi (W ◁ (α_ X Y Z).inv)]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C
inst✝¹⁵ : MonoidalCategory C
D : Type u₂
inst✝¹⁴ : Category.{v₂, u₂} D
inst✝¹³ : MonoidalCategory D
E : Type u₃
inst✝¹² : Category.{v₃, u₃} E
inst✝¹¹ : MonoidalCategory E
E' : Type u₄
inst✝¹⁰ : Category.{v₄, u₄} E'
inst✝⁹ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁸ : F₁.LaxMonoidal
inst✝⁷ : F₂.LaxMonoidal
inst✝⁶ : F₃.LaxMonoidal
F G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y) = ((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y

Tactic:
by
    ext
    · simp only [prod_comp_fst, prod'_μ_fst, prod'_app_fst,
        prodMonoidal_tensorHom, IsMonoidal.tensor]
    · simp only [prod_comp_snd, prod'_μ_snd, prod'_app_snd,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
inst✝⁸ : MonoidalCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
E' : Type u₄
inst✝⁵ : Category.{v₄, u₄} E'
inst✝⁴ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝³ : F₁.LaxMonoidal
inst✝² : F₂.LaxMonoidal
inst✝¹ : F₃.LaxMonoidal
e : F₁ ≅ F₂
inst✝ : NatTrans.IsMonoidal e.hom
X Y : C
⊢ LaxMonoidal.μ F₂ X Y ≫ e.inv.app (X ⊗ Y) = (e.inv.app X ⊗ₘ e.inv.app Y) ≫ LaxMonoidal.μ F₁ X Y

Tactic:
by
    rw [← cancel_mono (e.hom.app (X ⊗ Y)), assoc, assoc, inv_hom_id_app, comp_id,
      NatTrans.IsMonoidal.tensor, MonoidalCategory.tensorHom_comp_tensorHom_assoc,
      inv_hom_id_app, inv_hom_id_app, tensorHom_id, id_whiskerRight, id_comp]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget RingCat)).pt,
    π := { app := fun x ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x), naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ RingCat SemiRingCat)
t : IsLimit c'
⊢ IsLimit ((forget₂ RingCat SemiRingCat).mapCone c)

Tactic:
by apply SemiRingCat.HasLimits.limitConeIsLimit _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y

Tactic:
by
  apply (cancel_epi (α_ X Y Z).hom).1
  ext : 1
  apply TensorProduct.ext_threefold
  intro x y z
  rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ X ◁ g ≫ (β_ X Y').hom ≫ Y' ◁ f = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f

Tactic:
braiding_naturality_right_assoc

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ MorphismProperty.surjective C = epimorphisms C

Tactic:
rw [surjective_eq_epimorphisms_iff]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ▷ (Z₁ ⊗ Z₂) ≫ tensorμ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) Z₁ Z₂ ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ X₂) ◁ tensorμ Y₁ Y₂ Z₁ Z₂ ≫ tensorμ X₁ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)

Tactic:
dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
          X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
        (Z₁ ⊗ Z₂) ≫
      ((α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
          (X₁ ⊗ Y₁) ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫
            (X₁ ⊗ Y₁) ◁ (β_ (X₂ ⊗ Y₂) Z₁).hom ▷ Z₂ ≫
              (X₁ ⊗ Y₁) ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv) ≫
        ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁ (β_ X₂ (Y₁ ⊗ Z₁)).hom ▷ (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivOfSurj ↑f ⋯ hcd).symm ⟦f x⟧ = ↑x

Tactic:
convert! RingEquiv.symm_apply_apply _ _

Goal state after:
case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = (c.comapQuotientEquivOfSurj ↑f ⋯ hcd) ↑x
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (TensorAlgebra R M)) r

Tactic:
· rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

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

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) + (TensorProduct.map (inr R A B) (inr R A B)) (comul x))

Tactic:
simp only [map_zero, zero_add]

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inr R A B) (inr R A B)) (comul x))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ (lift f g hg hfg hgf).range = f.range ⊔ Algebra.adjoin S (Set.range ⇑g)

Tactic:
by
  simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_range_inr, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, lift_comp_inlHom, ← Set.range_comp, Function.comp_def,
    lift_apply_inr, Algebra.map_top]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa only [h] using map_sup f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa only [h] using map_sup f

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa only [h] using map_sup f

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
by
  rw [← LinearMap.lTensor_comp_rTensor, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul]
  rfl

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩

Goal state after:
case refine_2.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) (r' * y) (r * x) = (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r * x
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
ι : Type u_6
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
m : ↑{m | IsCoatom m}
⊢ ⨅ a, ↑a ≤ comap (LinearMap.proj i) ↑m

Tactic:
exact iInf_le_of_le ⟨_, (isCoatom_comap_iff <| LinearMap.proj_surjective i).mpr m.2⟩ le_rfl

Goal state after: