mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_3.refine_3
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)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

Tactic:
· exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
⊢ Injective ⇑ι

Tactic:
simpa [ι, -Subtype.val_injective] using Subtype.val_injective

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
⊢ Injective ⇑ι

Tactic:
simpa [ι, -Subtype.val_injective] using Subtype.val_injective

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M ι ∘ₗ rTensor M π)

Tactic:
exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
f : Module.End R (Matrix n n R)
⊢ (∑ x,
      match x with
      | ((i, j), k, l) => (r • f) (single j k 1) i l • single i j 1 ⊗ₜ[R] op (single k l 1)) =
    (RingHom.id R) r •
      ∑ x,
        match x with
        | ((i, j), k, l) => f (single j k 1) i l • single i j 1 ⊗ₜ[R] op (single k l 1)

Tactic:
by simp [mul_smul, Finset.smul_sum]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
· refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · exact hn.symm.le.trans (add_le_add_left hi _)
    · rw [add_comm n a]
      refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
      simp only [le_add_iff_nonneg_left]
      exact Int.emod_nonneg n (ne_of_gt ha)
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

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

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s

Tactic:
refine mem_sup.trans ⟨?_, fun h ↦ ?_⟩

Goal state after:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ (∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)) → ∀ a ∈ m, a ∈ s

case succ.refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
h : ∀ a ∈ m, a ∈ s
⊢ ∃ i ∈ s, m ∈ image (Sym.cons i) (s.sym n)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
⊢ Sym.map (⇑g) ((fun p ↦ Sym.map g' p) d.attach) = d

Tactic:
simp only [Sym.map_map, Function.comp_apply, g']

Goal state after:
case refine_1.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
⊢ Sym.map (fun x ↦ g ⋯.choose) d.attach = d
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Sym2 α
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

Tactic:
by
  induction s with | _ a b
  induction t with | _ c d
  obtain hab | hba := le_total a b <;> obtain hcd | hdc := le_total c d <;>
    aesop (add unsafe le_antisymm)

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)

Tactic:
Nat.multichoose_succ_succ,

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (x :: xs).length.multichoose n + xs.length.multichoose (n + 1) =
    xs.length.multichoose (n + 1) + (xs.length + 1).multichoose n
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : (fun z ↦ {x | Sym2.Mem x z}) z = (fun z ↦ {x | Sym2.Mem x z}) z'
⊢ z = z'

Tactic:
simp only [Set.ext_iff, Set.mem_ofPred_eq] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
h : ∀ (x : α), Sym2.Mem x z ↔ Sym2.Mem x z'
⊢ z = z'
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)

Tactic:
intro X
      apply G.map_injective
      grind

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ a = a

pp: case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
· rfl

Goal state after:
case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

pp: case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Tactic:
· rfl

Goal state after:
case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ c✝ : V
q₁ : Path b b✝
f₁ : b✝ ⟶ c✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
q₂ : Path b c✝
hq : (q₁.cons f₁).length = q₂.length
h : p₁.comp (q₁.cons f₁) = p₂.comp q₂
⊢ p₁ = p₂ ∧ q₁.cons f₁ = q₂

Tactic:
rcases q₂ with _ | ⟨q₂, f₂⟩
    · cases hq
    · simp only [comp_cons, cons.injEq] at h
      obtain rfl := h.1
      obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
      rw [h.2.2.eq]
      exact ⟨rfl, rfl⟩

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

Goal state before:
pp: case h_map.inl
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inl val✝)))

pp: case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))

Tactic:
· rfl

Goal state after:
case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
⊢ (P.ι ⋙ F).essImage = P.map F

Tactic:
ext Y
  constructor
  · rintro ⟨X, ⟨e⟩⟩
    exact ⟨X.1, X.2, ⟨e⟩⟩
  · rintro ⟨X, hX, ⟨e⟩⟩
    exact ⟨⟨X, hX⟩, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ eqToHom h ≍ 𝟙 X

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≍ 𝟙 X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ eqToHom h ≍ 𝟙 Y

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≍ 𝟙 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
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
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
h : F = G
X : C
⊢ (eqToHom h).app X = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
⊢ F X = F Y

Tactic:
subst h

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X : InducedCategory D F
⊢ F X = F X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
D : Type u_3
inst✝ : Category.{u_4, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u_2
D : Type u_3
inst✝ : Category.{u_4, u_3} D
F : C → D
X : InducedCategory D F
⊢ (eqToHom ⋯).hom = eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X Y : P.FullSubcategory
h : X = Y
⊢ X.obj = Y.obj

Tactic:
subst h

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ X.obj = X.obj
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
P : ObjectProperty C
X Y : P.FullSubcategory
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (eqToHom ⋯).hom = eqToHom ⋯
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X Y : C × D
h : X = Y
⊢ (eqToHom h).1 = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).1 = eqToHom ⋯
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X Y : C × D
h : X = Y
⊢ (eqToHom h).2 = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).2 = eqToHom ⋯
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2

Tactic:
rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
⊢ IsIso f.1 ∧ IsIso f.2
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h

Goal state after:
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
x : (i : I) → C i
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
⊢ ∀ (Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
⊢ ∀ (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
⊢ C i ≌ C j

Tactic:
subst h

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ C i ≌ C i
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i j : I
h : i = j
⊢ eval C i ⋙ (eqToEquivalence C h).functor = eval C j

Tactic:
subst h

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ eval C i ⋙ (eqToEquivalence C ⋯).functor = eval C i
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' j' : J
h : i' = j'
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) h).functor

Tactic:
subst h

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' : J
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) ⋯).functor
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), (fun x ↦ x.map F) P f → (fun x ↦ x.map F) Q f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
⊢ ∀ (f : X ⟶ Y), (fun x ↦ x.map F) P f → (fun x ↦ x.map F) Q f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), ⊤ f → ⊤.map F f

Tactic:
Y

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
⊢ ∀ (f : X ⟶ Y), ⊤ f → ⊤.map F f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.isoClosure f → Q.isoClosure f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
X Y : C
⊢ ∀ (f : X ⟶ Y), P.isoClosure f → Q.isoClosure f
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X : C
⊢ ∀ {Y : C} (f : X ⟶ Y), IsIso f

Tactic:
Y

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
X Y : C
⊢ ∀ (f : X ⟶ Y), IsIso f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.isoClosure f → P f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
⊢ ∀ (f : X ⟶ Y), P.isoClosure f → P f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ P.isoClosure ≤ Q

Tactic:
exact (monotone_isoClosure h).trans (by rw [Q.isoClosure_eq_self])

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), P.map F f → (P.map (F ⋙ G)).inverseImage G f

Tactic:
Y

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : D
⊢ ∀ (f : X ⟶ Y), P.map F f → (P.map (F ⋙ G)).inverseImage G f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P f → ((P.map F).map G).inverseImage (F ⋙ G) f

Tactic:
Y

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → ((P.map F).map G).inverseImage (F ⋙ G) f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), P.map F f → P.map G f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
⊢ ∀ (f : X ⟶ Y), P.map F f → P.map G f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.inverseImage E.functor f → P.map E.inverse f

Tactic:
Y

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
⊢ ∀ (f : X ⟶ Y), P.inverseImage E.functor f → P.map E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), P f → (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
Y

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
⊢ ∀ (f : X ⟶ Y), P f → (P.inverseImage E.functor).inverseImage E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ ∀ {Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
Y

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ ∀ {Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
Y

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)