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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ (Multiset.map f s).prod ≡ 1 [ZMOD n]

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ (Multiset.map f s).prod ≡ 1 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]

Tactic:
simpa using

Goal state after:
n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).sum ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).sum [ZMOD n]

Tactic:
simpa using

Goal state after:
case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ (Multiset.map f s).sum ≡ 0 [ZMOD n]

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ (Multiset.map f s).sum ≡ 0 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 0 [ZMOD n]
⊢ s.sum ≡ 0 [ZMOD n]

Tactic:
simpa using

Goal state after:
n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 0 [ZMOD n]
⊢ s.sum ≡ 0 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [ZMOD n]

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ image f ht.toFinset = t

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ f '' f ⁻¹' ↑s = ↑s ∩ Set.range f
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
this : {a | f a = m} ⊆ ↑ht.toFinset
a : ι
⊢ a ∈ {a ∈ ht.toFinset | f a = m} ↔ a ∈ ⋯.toFinset

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
this : {a | f a = m} ⊆ ↑ht.toFinset
a : ι
⊢ f a = m → f a ∈ t
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ (AlgebraTensorModule.rid R S S) (1 ⊗ₜ[R] x) = (Algebra.linearMap R S) x

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type v₃
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ x • 1 = (algebraMap R S) x
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ xs <+~ ys
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
x : α
⊢ x ∈ s ↔ x ∈ t
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
conv => enter [1, 2, 1]; rw [Sym2.eq_swap]

Goal state after:
case swap
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
⊢ s(y, y) :: s(x, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs <+~ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
obtain ⟨xs', hx, h⟩ := h

Goal state after:
α : Type u_1
xs ys xs' : List α
hx : xs' ~ xs
h : xs' <+ ys
⊢ xs.sym2 <+~ ys.sym2
Module: Mathlib.Algebra.BigOperators.Sym

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ (i : { p // p.1 ≤ p.2 }),
    i ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag ↔ Sym2.sortEquiv.symm i ∈ {i ∈ s.sym2 | ¬i.IsDiag}

pp: case refine_2
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∀ i ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag, p s((↑i).1, (↑i).2) = p (Sym2.sortEquiv.symm i)

Tactic:
all_goals aesop

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
x y : α
⊢ r x y ↔ ⊥ x y

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
x y : α
⊢ ¬r x y
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
x y : α
⊢ r x y ↔ ⊤ x y

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
x y : α
⊢ r x y
Module: Mathlib.Data.Sym.Sym2

Goal state before:

Tactic:
first | done | constructor

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

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [b₂, a₂].Perm [a₂, b₂]

Tactic:
first | done | constructor

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

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : (f ≫ g) ≫ k = (f ≫ h) ≫ l
⊢ f ≫ g ≫ k = f ≫ h ≫ l
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✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_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 := F_obj, map := map✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using

Goal state after:
V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_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 := F_obj, map := map✝ }.map f))
X Y : V
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
X Y : V
f : X ⟶ Y
⊢ Fmap f = Gmap f

Tactic:
simpa using

Goal state after:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Fobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Fobj, map := Gmap }.map f) ⋯ ⋯
X Y : V
f : X ⟶ Y
⊢ Fmap f = Gmap f
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
s : S
m : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) (LinearMap.id s)) (((LinearMap.lsmul R M) x) m) =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x)))
      (((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) s) m)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
s : S
m : M
⊢ x • s • f m = s • x • f m
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_14
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
e_5✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_6✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_10✝ : toModule ≍ leftModule
e_11✝ : toModule ≍ leftModule
s : S
⊢ ((AlgebraTensorModule.curry (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap) 1) s =
    ((AlgebraTensorModule.curry (AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id)) 1) s

Tactic:
simpa using

Goal state after:
case e'_14
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
e_5✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_6✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_10✝ : toModule ≍ leftModule
e_11✝ : toModule ≍ leftModule
s : S
⊢ (algebraMap (A ⊗[R] S) (B ⊗[R] S)) (1 ⊗ₜ[R] s) = 1 ⊗ₜ[R] s
Module: Mathlib.CategoryTheory.Functor.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ map = map'

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj, map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ map = map'
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹³ : CommSemiring R'
inst✝¹² : CommSemiring S'
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra R' S'
inst✝⁸ : Algebra R S'
inst✝⁷ : IsScalarTower R R' S'
inst✝⁶ : IsScalarTower R S S'
h : IsBaseChange R' (toAlgHom R S S').toLinearMap
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
x : S
⊢ (h.equiv ≪≫ₗ ↑e) (1 ⊗ₜ[R] x) = (toAlgHom R S T).toLinearMap x

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type v₃
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹³ : CommSemiring R'
inst✝¹² : CommSemiring S'
inst✝¹¹ : Algebra R R'
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra R' S'
inst✝⁸ : Algebra R S'
inst✝⁷ : IsScalarTower R R' S'
inst✝⁶ : IsScalarTower R S S'
h : IsBaseChange R' (toAlgHom R S S').toLinearMap
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
x : S
⊢ e ((algebraMap S S') x) = (algebraMap S T) x
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
Y : D
⊢ P.strictMap F Y → ∃ X, P X ∧ F.obj X = Y

Tactic:
rintro ⟨X, hX⟩; exact ⟨X, hX, rfl⟩

Goal state after:
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
F : C ⥤ D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ IsIso f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ IsIso f
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ p₂.length + q₁.length = p₂.length + q₂.length

Tactic:
simpa using

Goal state after:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ q₁.length = q₂.length
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g

Tactic:
simpa using

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g
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
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
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_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 := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ map✝¹ f = map✝ f

Tactic:
simpa using

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
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
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_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 := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ map✝¹ 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 : C ≌ D
X : C
⊢ e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = 𝟙 (e.functor.obj X)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = 𝟙 (e.functor.obj 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✝
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
functor : C ⥤ D
inverse : D ⥤ C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X)

Tactic:
simpa using

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
functor : C ⥤ D
inverse : D ⥤ C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj 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

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X✝ Y✝ : Cᵒᵖ
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.op.map a₁✝ = F.op.map a₂✝
⊢ a₁✝.unop = a₂✝.unop

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X✝ Y✝ : Cᵒᵖ
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.op.map a₁✝ = F.op.map a₂✝
⊢ a₁✝.unop = a₂✝.unop
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
Y : D
⊢ e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (as ∘ h.inverse.obj ∘ mk) ((as ∘ h.functor.obj ∘ mk) a) = a

Tactic:
simpa using

Goal state after:
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : α
⊢ (h.inverse.obj (h.functor.obj { as := a })).as = a
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : β
⊢ (as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a

Tactic:
simpa using

Goal state after:
α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : β
⊢ (h.functor.obj (h.inverse.obj { as := a })).as = a
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
C' : Type u_1
e : C' ≃ D
Y : D
⊢ Nonempty ((inducedFunctor ⇑e).obj (e.symm Y) ≅ Y)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
C' : Type u_1
e : C' ≃ D
Y : D
⊢ Nonempty (Y ≅ Y)
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsGroupoid C
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), ⊤ f → isomorphisms C f

Tactic:
simp only [isomorphisms.iff, top_apply]

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsGroupoid C
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), True → IsIso f
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f
Module: Mathlib.CategoryTheory.EpiMono

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

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h
Module: Mathlib.CategoryTheory.EpiMono

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

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : Epi (f ≫ g)
⊢ Epi f