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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
⊢ ∀ (x : DirectLimit G f),
    (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (r • x) =
      (RingHom.id R) r • (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun x

Tactic:
rintro ⟨x⟩; exact map_smul (DirectSum.toModule R ι P g) r x

Goal state after:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
z w : DirectLimit G f
⊢ (lift R ι G f g Hg) z = (lift R ι G f g Hg) w → z = w

Tactic:
eq

Goal state after:
case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
z w : DirectLimit G f
eq : (lift R ι G f g Hg) z = (lift R ι G f g Hg) w
⊢ z = w
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Small.{u, u_1} R
s : Finset S
⊢ Small.{u, u_2} ↥(adjoin R ↑s)

Tactic:
exact small_adjoin

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor N M'.subtype).range

Tactic:
by
  obtain ⟨M', _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite s hs
  refine ⟨M', hfin, ?_⟩
  rw [mapIncl, ← LinearMap.rTensor_comp_lTensor] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
⊢ ∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor (↥N₁) (inclusion hM)).range

Tactic:
obtain ⟨M', _, hM, _, hfin, _, h⟩ := exists_finite_submodule_of_setFinite' s hs

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R M
w✝¹ : Submodule R N
hM : M' ≤ M₁
w✝ : w✝¹ ≤ N₁
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝¹
h : s ⊆ ↑(map (inclusion hM) (inclusion w✝)).range
⊢ ∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor (↥N₁) (inclusion hM)).range
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑((lmap fun x ↦ rTensor (M x) N.subtype) ∘ₗ ↑(directSumRight R R (↥N) M))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
coe_comp,

Goal state after:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective (⇑(lmap fun x ↦ rTensor (M x) N.subtype) ∘ ⇑↑(directSumRight R R (↥N) M))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P N : Type v'
x✝³ : AddCommMonoid P
x✝² : AddCommMonoid N
x✝¹ : Module R P
x✝ : Module R N
⊢ ∀ (f : P →ₗ[R] N), Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
let := Module.addCommMonoidToAddCommGroup R (M := P)
      let := Module.addCommMonoidToAddCommGroup R (M := N)
      apply h

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → One (G i)
inst✝² : One C
inst✝¹ : ∀ (i : ι), OneHomClass (H i) (G i) C
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h 1 = 1

Tactic:
by
  let ⟨i⟩ := ‹Nonempty ι›
  rw [one_def, lift_def, map_one (g i)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ Function.Injective ⇑includeLeft

Tactic:
convert!
    Module.Flat.lTensor_preserves_injective_linearMap (M := A) (Algebra.linearMap R B) hb |>.comp
      (_root_.TensorProduct.rid R A).symm.injective

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
⊢ ⇑includeLeft = ⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
obtain hst | hst := (s ∩ t).eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : s ∩ t = ∅
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

case inr
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f * g)

Tactic:
by
  intro a
  simp only [Pi.mul_apply, hf a, hg a, mul_neg, neg_mul, neg_neg]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ ∏ n ∈ Ico (-↑(b + 1)) ↑(b + 1), f n / f (n + 1) = f (-↑(b + 1)) / f ↑(b + 1)

Tactic:
| succ b ihb =>

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ 0 [MOD n]

Tactic:
by
  simpa using ModEq.sum h

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ ↑x✝¹.sym2 = ↑x✝.sym2

Tactic:
by rw [coe_eq_coe]; exact h.sym2

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a s(b, c)

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(b, a)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mpr
α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ z = s(x, y) → x ∈ z ∧ y ∈ z

Tactic:
rintro rfl
    simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝ }.map f))
⊢ F_obj = G_obj

Tactic:
ext X

Goal state after:
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝ }.map f))
X : V
⊢ F_obj X = G_obj X
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_8
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
C : Type u_11
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : A
⊢ ((AlgHom.restrictScalars R
            ((↑(cancelBaseChangeAlg R S A (S ⊗[R] A) C).symm).comp (TensorProduct.lTensor S (toAlgHom R A C)))).comp
        TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R TensorProduct.includeLeft).comp TensorProduct.includeRight) x✝

Tactic:
simp [← TensorProduct.one_def, ← TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f f' : X ⟶ Y
g : Y ≅ Z
⊢ f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Tactic:
by
  simp only [cancel_mono]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
⊢ g = h

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ g.app X = h.app X
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
⊢ ofObj Subtype.val = P

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
⊢ ofObj Subtype.val X ↔ P X
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z

Tactic:
rintro (rfl | rfl)

Goal state after:
case mpr.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y X

case mpr.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y Y
Module: Mathlib.CategoryTheory.Functor.Category

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
⊢ α ≫ β = β ≫ α

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α β : 𝟭 C ⟶ 𝟭 C
X : C
⊢ (α ≫ β).app X = (β ≫ α).app X
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
revert F₁ F₂

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Tactic:
by_cases hp : p <;> simp only [hp]

Goal state after:
case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True

case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ F_obj = G_obj

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
X : C
⊢ F_obj X = G_obj X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ e.hom.app X ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y

Tactic:
happ,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y

Tactic:
happ,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
X : C
⊢ a₁✝.app X = a₂✝.app X
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
x y : J
f : { as := x } ⟶ { as := y }
⊢ (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                  map_comp := ⋯ }).obj
            F).map
        f ≫
      (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := y })).hom =
    (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom ≫
      ((𝟭 (Discrete J ⥤ C)).obj F).map f

Tactic:
obtain rfl : x = y := Discrete.eq_of_hom f

Goal state after:
J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
x : J
f : { as := x } ⟶ { as := x }
⊢ (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                  map_comp := ⋯ }).obj
            F).map
        f ≫
      (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom =
    (Iso.refl
          ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                      map_id := ⋯, map_comp := ⋯ }).obj
                F).obj
            { as := x })).hom ≫
      ((𝟭 (Discrete J ⥤ C)).obj F).map f
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
⊢ ((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
      (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F) =
    𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : D
⊢ (((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
          (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F)).app
      X =
    (𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)).app X
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
X : C
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
D : Type u_3
inst✝² : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
obj : C → D
h_obj : ∀ (X : C), (forget D).obj (obj X) = (forget C).obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, (forget D).map (map f) ≍ (forget C).map f
⊢ Functor.Faithful.div (forget C) (forget D) obj h_obj map h_map ⋙ forget D = forget C

Tactic:
by apply Functor.Faithful.div_comp

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
⊢ ↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)) = 𝟙 (m α)

Tactic:
ext X

Goal state after:
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : m α
⊢ (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)))).toFun X = (ConcreteCategory.hom (𝟙 (m α))).toFun X
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾_root_.Functor.map ⇑(Hom.hom (f ≫ g)) = ↾_root_.Functor.map ⇑(Hom.hom f) ≫ ↾_root_.Functor.map ⇑(Hom.hom g)

Tactic:
by
    ext x
    exact comp_map (f := m) f.hom g.hom x

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj.counit = adj'.counit

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.counit.app X = adj'.counit.app X