mathlib-initiative/mathlib-tactics huggingface dataset:
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
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ 0) ⋯ ⟦⟨i, x✝⟩⟧ = 1

Tactic:
map_def,

Goal state after:
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
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝ ^ 0⟩⟧ = 1
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
⊢ IsReduced (C ⊗[R] A)

Tactic:
by
  by_contra h_contra
  obtain ⟨x, hx⟩ := exists_isNilpotent_of_not_isReduced h_contra
  obtain ⟨D, hD⟩ := exists_fg_and_mem_baseChange x
  have h_inj : Function.Injective
      (Algebra.TensorProduct.map (AlgHom.id C C) D.val) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
  obtain ⟨z, rfl⟩ := hD.2
  have h_notReduced : ¬IsReduced (C ⊗[R] D) := by
    simp_rw [isReduced_iff, not_forall]
    exact ⟨z, (IsNilpotent.map_iff h_inj).mp hx.right, (by simpa [·] using hx.1)⟩
  tauto

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 : ι) → 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
⊢ map f f (fun x x_1 ↦ x_1 ^ ↑n.succ) ⋯ ⟦⟨i, x⟩⟧ = map f f (fun x x_1 ↦ x_1 ^ ↑n) ⋯ ⟦⟨i, x⟩⟧ * ⟦⟨i, x⟩⟧

Tactic:
map_def,

Goal state after:
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 ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n⟩⟧ * ⟦⟨i, x⟩⟧
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
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧ * ⟦⟨i, x✝⟩⟧ = 1

Tactic:
map_def,

Goal state after:
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
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⁻¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = 1
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
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹ / x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x✝⟩⟧

Tactic:
map_def,

Goal state after:
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
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹ / x✝⟩⟧ = ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⁻¹⟩⟧
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
i : ι
x✝ : G i
⊢ map f f (fun x x_1 ↦ x_1 ^ 0) ⋯ ⟦⟨i, x✝⟩⟧ = 1

Tactic:
map_def,

Goal state after:
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
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝ ^ 0⟩⟧ = 1
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
⊢ map f f (fun x x_1 ↦ x_1 ^ ↑n.succ) ⋯ ⟦⟨i, x⟩⟧ = map f f (fun x x_1 ↦ x_1 ^ ↑n) ⋯ ⟦⟨i, x⟩⟧ * ⟦⟨i, x⟩⟧

Tactic:
map_def,

Goal state after:
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 ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n⟩⟧ * ⟦⟨i, x⟩⟧
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
i : ι
x : G i
ne : ⟦⟨i, x⟩⟧ ≠ 0
this : x ≠ 0
⊢ ⟦⟨i, x⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x⟩⟧ = 1

Tactic:
map_def,

Goal state after:
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
i : ι
x : G i
ne : ⟦⟨i, x⟩⟧ ≠ 0
this : x ≠ 0
⊢ ⟦⟨i, x⟩⟧ * ⟦⟨i, x⁻¹⟩⟧ = 1
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f • g)

Tactic:
by
  intro a
  simp only [Pi.smul_apply', hf a, hg a, neg_smul]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (Iio (k + 1)).PairwiseDisjoint fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2

Tactic:
by
  intro j hj j' hj' hjj'
  rw [mem_Iio] at hj hj'
  wlog hij' : j < j' generalizing j j'
  · exact (this hj' hj hjj'.symm (by omega)).symm
  rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]
  suffices (F.intervalGapsWithin h a b j).2 ≤ (F.intervalGapsWithin h a b j').1 by grind
  have hj'₀ : j' - 1 + 1 = j' := by omega
  have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j' - 1) (by grind)) |>.right.left
  simp only [Nat.succ_eq_add_one, hj'₀] at this
  grw [← this]
  rw [intervalGapsWithin_snd_of_lt (hj := by omega),
      intervalGapsWithin_snd_of_lt (hj := by omega)]
  exact Prod.Lex.le_iff'.mp (F.orderEmbOfFin (α := α ×ₗ α) h |>.monotone (by grind)) |>.left

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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
simp only [← modEq_natAbs (n := n), ← ZMod.intCast_eq_intCast_iff, cast_zero, cast_sum] at *

Goal state after:
α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = ↑(f a)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : IsTensorProduct f
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ IsTensorProduct ((f ∘ₗ ↑e₁).compl₂ ↑e₂)

Tactic:
by
  simp only [IsTensorProduct] at ist ⊢
  rw [← TensorProduct.lift_comp_map, ← LinearMap.rTensor_comp_lTensor]
  exact ist.comp ((e₁.rTensor M₂).bijective.comp (e₂.lTensor N₁).bijective)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_2
ι : 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
⊢ {a | f a = m} ⊆ ↑ht.toFinset

Tactic:
intro _ h

Goal state after:
case refine_2
ι : 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
a✝ : ι
h : a✝ ∈ {a | f a = m}
⊢ a✝ ∈ ↑ht.toFinset
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2

Tactic:
induction m, m' using Quotient.inductionOn₂ with | _ xs ys
   =>  _ 

Goal state after:
case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ (map (fun y ↦ s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj

Goal state after:
case notmem
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ (fun y ↦ s(x, y)) x ∉ map (fun y ↦ s(x, y)) xs

case inj
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ Function.Injective fun y ↦ s(x, y)

case disj
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ (map (fun y ↦ s(x, y)) (x :: xs)).Disjoint xs.sym2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ s(x', x') :: (map (fun y ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
refine .cons _ ?_

Goal state after:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ map (fun y ↦ s(x', y)) xs ++ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ n✝ + 1 ≠ 0 ∧ s = ∅ → s.sym (n✝ + 1) = ∅

Tactic:
rintro ⟨_, rfl⟩

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
left✝ : n✝ + 1 ≠ 0
⊢ ∅.sym (n✝ + 1) = ∅
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
(hom_comp_eq_id _).mp h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ (p.comp q).comp (r.cons a✝) = p.comp (q.comp (r.cons a✝))

Tactic:
by rw [comp_cons, comp_cons, comp_cons, comp_assoc p q r]

Goal state after:
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
⊢ reverse f = reverse g → f = g

Tactic:
rintro h
    simpa using congr_arg Quiver.reverse h

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
by
  cases q
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯

Tactic:
by
  cases q
  simp

Goal state after:
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 G : C ⥤ D
α : F.op ⟶ G.op
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ (α.app (op Y)).unop).op = ((α.app (op X)).unop ≫ F.map f).op

Tactic:
by simpa only [Functor.op_map] using! (α.naturality f.op).symm

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

Goal state before:
pp: C : Type u_1
⊢ ∀ {X Y : Discrete C} (f : X ⟶ Y), X = Y

Tactic:
by rintro ⟨_⟩ ⟨_⟩ ⟨⟨rfl⟩⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : g.hom = r.inv ≫ f.hom ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom

Tactic:
Iso.eq_inv_comp

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : r.hom ≫ g.hom = f.hom ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : g = e₂.inv ≫ f ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom

Tactic:
Iso.eq_inv_comp

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : e₂.hom ≫ g = f ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ IsIso (homOfLE ⋯)

Tactic:
subst h
  change IsIso (𝟙 _)
  infer_instance

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom = (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom

Tactic:
by
  simp [← cancel_epi ((α_ f g h).hom ▷ i)]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ x ≫ f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩
  intro T
  rw [bijective_iff_isIso_ofHom]
  exact inferInstanceAs (IsIso ((yoneda.map f).app _))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
              (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type (max v₁ w)) ⋙
                        (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).obj
                    X).map
                f)).toFun
        g).down

Tactic:
simpa using uliftCoyonedaEquiv_comp _ _

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type (max v₁ w)) ⋙
              (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                uliftFunctor.{u₁, max v₁ w}).map
          f

Tactic:
intros Y Z f
      ext F g
      rw [← ULift.down_inj]
      simpa using (uliftCoyonedaEquiv_naturality _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝¹ : StrongEpi f
inst✝ : StrongEpi g
⊢ ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [Mono z], HasLiftingProperty (f ≫ g) z

Tactic:
by
      intros
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C

Tactic:
constructor
  intro F
  apply hasColimit_of_equivalence_comp e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ m = (P.lift s.op).unop

Tactic:
by
    dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ m = (P.desc s.op).unop

Tactic:
by
    dsimp
    rw [← P.uniq s.op m.op]
    · rfl
    · dsimp
      intro j
      rw [← w]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
⊢ IsColimit (mk Y fun x ↦ e.hom)

Tactic:
by
  refine Cofan.IsColimit.mk _ (fun s ↦ e.inv ≫ s.inj default) (fun s j ↦ ?_) fun s m hm ↦ ?_
  · obtain rfl : j = default := Subsingleton.elim _ _
    simp
  · simpa [← cancel_epi e.hom] using hm default

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
| _ i
       => 

Goal state after:
case op
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ IsZero X ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
⊢ 𝟙 X = 0 ↔ f = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ IsZero Y ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 ↔ f = 0