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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ (lTensor Q g).ker = (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g).ker

Tactic:
apply symm

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ (lTensor.inverse Q hfg hg ∘ₗ lTensor Q g).ker = (lTensor Q g).ker
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map ((↑(map (AlgHom.id R A) g)).comp ↑includeLeft) (RingHom.ker f)

Tactic:
rw [← AlgHom.comp_toRingHom, Algebra.TensorProduct.map_comp_includeLeft]

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map (↑(includeLeft.comp (AlgHom.id R A))) (RingHom.ker f)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Bijective f
s : Finset α
⊢ (image f s).dens = s.dens

Tactic:
simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf)

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

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j

Tactic:
cons_eq_insert,

Goal state after:
case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ insert i s, t i_1).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : 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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ Int.negSucc n = map f f (fun x x_1 ↦ x_1⁻¹) ⋯ (⟦⟨i, x⟩⟧ ^ ↑n.succ)

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow, map_def]; congr; apply DivInvMonoid.zpow_neg'

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

Goal state before:
pp: R : Type u_1
ι : 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 : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ Int.negSucc n = map f f (fun x x_1 ↦ x_1⁻¹) ⋯ (⟦⟨i, x⟩⟧ ^ ↑n.succ)

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow, map_def]; congr; apply DivInvMonoid.zpow_neg'

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

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ 𝔼 x, balance f x = 0

Tactic:
by simp [expect]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ 𝔼 i ∈ ∅, f i = 0

Tactic:
by simp [expect]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
i : ι
⊢ 𝔼 j ∈ {i}, f j = f i

Tactic:
by simp [expect]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
⊢ 𝔼 _i ∈ s, 0 = 0

Tactic:
by simp [expect]

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

Goal state before:
pp: R : Type u_1
ι : 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 : ι) → Mul (G i)
inst✝³ : (i : ι) → SMul R (G i)
inst✝² : ∀ (i : ι), IsScalarTower R (G i) (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ (r • ⟦⟨i, x✝¹⟩⟧) • ⟦⟨i, x✝⟩⟧ = r • ⟦⟨i, x✝¹⟩⟧ • ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [smul_eq_mul, smul_def, mul_def, smul_def, smul_mul_assoc]

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

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
⊢ 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / ↑(#s)

Tactic:
rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
π : α → Type u_7
inst✝¹ : (a : α) → CommSemiring (π a)
inst✝ : (a : α) → Module ℚ≥0 (π a)
s : Finset ι
f : ι → (a : α) → π a
a : α
⊢ (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a

Tactic:
by simp [expect]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
⊢ ∏ m ∈ Icc (-↑0) ↑0, f m = (∏ m ∈ range (0 + 1), f ↑m) ^ 2 / f 0

Tactic:
simp [sq]

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

Goal state before:
pp: a b : ℤ
h : a < b
⊢ ↑(b - a - 1).toNat = b - a - 1

Tactic:
sub_sub,

Goal state after:
a b : ℤ
h : a < b
⊢ ↑(b - (a + 1)).toNat = b - (a + 1)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ (∏ x ∈ s.powerset, f x) * ∏ x ∈ image (insert a) s.powerset, f x =
    (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)

Tactic:
prod_image

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset, f (insert a x) =
    (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Set.InjOn (insert a) ↑s.powerset

α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ i ∈ s, f i) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
← Finset.sum_filter_add_sum_filter_not _ (fun x ↦ Even (f x)),

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ s with Even (f x), f x + ∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup

Tactic:
refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj

Goal state after:
case inj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p ↦ x ::ₛ p

case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s

Tactic:
simp only [mem_map]

Goal state after:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
x : List α
hx : x.length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨x, hx⟩⟧) = ⟦⟨x, hx⟩⟧

Tactic:
obtain - | ⟨-, x⟩ := x

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
hx : [].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[], hx⟩⟧) = ⟦⟨[], hx⟩⟧

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝ :: x, hx⟩⟧) = ⟦⟨head✝ :: x, hx⟩⟧
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

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✝ 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)
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj
        X

Tactic:
intro X

Goal state after:
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj X
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P

Tactic:
intro X

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ P.isoClosure X ≤ P 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
e : C ≌ D
X : C
⊢ e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Tactic:
simpa using Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)) (f := e.counit.app _)

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
by rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]

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

Goal state before:
pp: case h_obj
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), f.obj X = f'.obj X

Tactic:
intro X

Goal state after:
case h_obj
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
⊢ f.obj X = f'.obj X
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
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1

Tactic:
intro X

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 : A
⊢ ∀ (Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ 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
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map F

Tactic:
intro X

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 : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), ⊤ f → ⊤.map F f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
f : Arrow C
hf : f ∈ P.toSet
⊢ P (P.homFamily ⟨f, hf⟩)

Tactic:
exact hf

Goal state after:
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 Y : C} (f : X ⟶ Y), IsIso f

Tactic:
intro X

Goal state after:
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
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
⊢ P.isoClosure ≤ P

Tactic:
intro X

Goal state after:
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
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
⊢ P.map F ≤ (P.map (F ⋙ G)).inverseImage G

Tactic:
intro X

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 : D
⊢ ∀ ⦃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
⊢ P ≤ ((P.map F).map G).inverseImage (F ⋙ G)

Tactic:
intro X

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 : C
⊢ ∀ ⦃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: 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
⊢ P.inverseImage E.functor ≤ P.map E.inverse

Tactic:
intro X

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 : C
⊢ ∀ ⦃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
⊢ P ≤ (P.inverseImage E.functor).inverseImage E.inverse

Tactic:
intro X

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 : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), P f → (P.inverseImage E.functor).inverseImage E.inverse 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 D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor = P.map E.inverse

Tactic:
apply le_antisymm
  · intro X Y f hf
    refine ⟨_, _, _, hf, ⟨?_⟩⟩
    exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)
  · rw [map_le_iff]
    intro X Y f hf
    exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

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

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

Tactic:
intro X

Goal state after:
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)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
intro X

Goal state after:
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)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

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

Tactic:
intro X

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

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

Tactic:
intro X

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

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

Tactic:
intro X

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

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

Tactic:
intro X

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv

Tactic:
by
        rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h,
          Category.assoc, ← R₁.map_comp]
        simp

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'

Tactic:
conv =>
      rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'