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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ (σ ^ p) v = 1 v

Tactic:
hσ,

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ f p v = 1 v
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ j, ∏ i < j, if σ i < σ j then 1 else -1

Tactic:
suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert! rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [← ite_not (p := _ ≤ _)]
  refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
  rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

Goal state after:
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'

Tactic:
rw [hcc']

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : q i ≠ p i
⊢ (DFinsupp.single (p i) (m i)) (q i) = 0

Tactic:
DFinsupp.single_eq_of_ne hpqi

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
⊢ detp 1 1 = 1

Tactic:
rw [← diagonal_one, detp_one_diagonal, prod_const_one]

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
d : n → R
σ : Perm n
hσ : σ = 1
⊢ σ ∉ ofSign (-1)

Tactic:
hσ,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ : σ = 1
⊢ 1 ∉ ofSign (-1)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Surjective (F.descColimitType c)
z : c.pt
⊢ ∃ i x, c.ι i x = z

Tactic:
obtain ⟨⟨i, x⟩, rfl⟩ := h z

Goal state after:
case mp.mk
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Surjective (F.descColimitType c)
w✝ : F.ColimitType
i : J
x : F.obj i
⊢ ∃ i_1 x_1, c.ι i_1 x_1 = F.descColimitType c (Quot.mk F.ColimitTypeRel ⟨i, x⟩)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩

Tactic:
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
    IsFiltered.tulip (IsFiltered.rightToMax j₂ j₁) (IsFiltered.leftToMax j₂ j₁)
      (IsFiltered.leftToMax j₂ j₃) (IsFiltered.rightToMax j₂ j₃) f g

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
y : ↑(F.obj j₁)
j₂ : J
x : ↑(F.obj j₂)
j₃ : J
y' : ↑(F.obj j₃)
l : J
f : ⟨j₁, y⟩.fst ⟶ l
g : ⟨j₃, y'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) y = (ConcreteCategory.hom (F.map g)) y'
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.1).map f.2 ≫ (T.app Y.1).app Y.2

pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1).app X.2

Tactic:
NatTrans.naturality

Goal state after:
case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (T.app Y.1).app X.2 ≫ (Y✝.obj Y.1).map f.2

case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1).app X.2
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ X✝.map (𝟙 X ×ₘ g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y✝.map (𝟙 X ×ₘ g)

Tactic:
NatTrans.naturality

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ T.app (X, Y) ≫ Y✝.map (𝟙 X ×ₘ g) = T.app (X, Y) ≫ Y✝.map (𝟙 X ×ₘ g)
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ X✝.map (f ×ₘ 𝟙 x✝) ≫ T.app (X', x✝) = T.app (X, x✝) ≫ Y✝.map (f ×ₘ 𝟙 x✝)

Tactic:
NatTrans.naturality

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ T.app (X, x✝) ≫ Y✝.map (f ×ₘ 𝟙 x✝) = T.app (X, x✝) ≫ Y✝.map (f ×ₘ 𝟙 x✝)
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
y : ToType D.pt
⊢ (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) y → x = y

Tactic:
H

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type r
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{t, w} J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
x : E.pt
y : ToType D.pt
H : (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) x = (fun x j ↦ (ConcreteCategory.hom (D.π.app j)) x) y
⊢ x = y
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
⊢ let ff := fun a ↦ (ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
  Function.Surjective ff

Tactic:
by
  intro ff x
  let E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
  let hE : IsColimit E := isColimitOfPreserves (forget C) hD
  obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x
  exact ⟨⟨j, y⟩, hy⟩

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ ≫
      ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } =
    𝟙 (of ↥(Hom.hom f).ker)

Tactic:
apply AddCommGrpCat.ext

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ∀ (x : ↑(of ↥(Hom.hom f).ker)),
    (ConcreteCategory.hom
          (kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ ≫
            ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }))
        x =
      (ConcreteCategory.hom (𝟙 (of ↥(Hom.hom f).ker))) x
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : 𝟙_ C ⟶ Y
g : X ⟶ Z
⊢ (λ_ X).inv ≫ (f ⊗ₘ g) = g ≫ (λ_ Z).inv ≫ f ▷ Z

Tactic:
by simp [tensorHom_def']

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

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R}, X ◁ 0 = 0

pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R}, 0 ▷ X = 0

pp: case refine_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), X ◁ (f + g) = X ◁ f + X ◁ g

pp: case refine_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X

Tactic:
· intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerLeft]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R}, 0 ▷ X = 0

case refine_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), X ◁ (f + g) = X ◁ f + X ◁ g

case refine_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), X ◁ (f + g) = X ◁ f + X ◁ g

pp: case refine_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X

Tactic:
· intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerLeft]

Goal state after:
case refine_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
⊢ ∀ (X : ModuleCat R) {Y Z : ModuleCat R} (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ (r : R) {Y Z : ModuleCat R} (f : Y ⟶ Z) (X : ModuleCat R), (r • f) ▷ X = r • f ▷ X

Tactic:
· intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerLeft]

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
⊢ ∀ (r : R) {Y Z : ModuleCat R} (f : Y ⟶ Z) (X : ModuleCat R), (r • f) ▷ X = r • f ▷ X
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (λ_ (F.obj x✝)).inv = F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝

Tactic:
← cancel_epi (λ_ _).hom,

Goal state after:
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (λ_ (F.obj x✝)).hom ≫ (λ_ (F.obj x✝)).inv =
    (λ_ (F.obj x✝)).hom ≫ F.map (λ_ x✝).inv ≫ (h.μIso (𝟙_ C) x✝).inv ≫ h.εIso.inv ▷ F.obj x✝
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))

Tactic:
rw [← h] at hf

Goal state after:
case mp
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
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: case mp
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
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
rw [← h] at hf

Goal state after:
case mp
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
h : MorphismProperty.injective C = monomorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.injective C f
⊢ Function.Injective ⇑(hom ((forget C).map f))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ HasPushout f.op g.op

Tactic:
by
  rwa [hasPushout_op_iff_hasPullback]

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

Goal state before:
pp: case δ
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝² : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
simp [homEquiv_counit, homEquiv_unit, ← δ_natural_assoc]

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

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝ : e.functor.Monoidal
this✝ : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this : IsIso (LaxMonoidal.ε e.inverse)
X Y : D
⊢ IsIso (LaxMonoidal.μ e.inverse X Y)

Tactic:
by
    simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
    infer_instance

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]
      rw [fst_inv]
      apply inv_ne_zero hx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f g : A →ₗc[R] B
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by
    rcases f with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
    rcases g with ⟨⟨⟨_, _⟩, _⟩, _, _⟩
    congr

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
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
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ ∘ₗ comul) a = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
rw [LinearMap.comp_apply, ← repr.eq, map_sum]; rfl

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

Goal state before:
pp: 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
⊢ lTensor (A × B) counit ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1

Tactic:
by
    ext : 1
    · rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
    · rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

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

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
⊢ (map f) (inl r) = inl r

Tactic:
by
  rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x✝ : A
⊢ (LinearMap.rTensor A counit ∘ₗ comul) x✝ = ((TensorProduct.mk R R A) 1) x✝

Tactic:
apply (TensorProduct.map_bijective (f := .id) Function.bijective_id
        (e.linearEquiv R).bijective).injective

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := ⋯
this : Module R A := ⋯
x✝ : A
⊢ (TensorProduct.map LinearMap.id ↑(linearEquiv R e)) ((LinearMap.rTensor A counit ∘ₗ comul) x✝) =
    (TensorProduct.map LinearMap.id ↑(linearEquiv R e)) (((TensorProduct.mk R R A) 1) x✝)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (r • g)) 1 = (RingHom.id R) r • ((CoextendScalars.equiv f X) g) 1

Tactic:
dsimp
        rw [CoextendScalars.smul_apply, one_mul, ← map_smul]
        congr
        change f r = f r • (1 : S)
        simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ 1 ⊗ₜ[R] (r • x) = r • 1 ⊗ₜ[R] x

Tactic:
← TensorProduct.smul_tmul,

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
r : R
x : ↑X
m1 : Module R S := Module.compHom S f
⊢ (r • 1) ⊗ₜ[R] x = r • 1 ⊗ₜ[R] x
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
hg : IsUnit (g x)
y : ↥(powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ↑y)

Tactic:
← hn,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
hg : IsUnit (g x)
y : ↥(powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ((fun x_1 ↦ x ^ x_1) n))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ (n + 1) ∣ a ^ n * c

Tactic:
by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ↑y)

Tactic:
← hn,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g ((fun x_1 ↦ x ^ x_1) n))
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
e : R ≃+* S
⊢ (comap e.symm).comp (comap e) = OrderHom.id

Tactic:
ext; simp [mem_comap]

Goal state after: