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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
inst✝⁸ : (i : ι) → AddCommMonoid (G i)
inst✝⁷ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝⁶ : DecidableEq ι
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i j : ι
h : i ≤ j
⊢ ↑(e j).symm ∘ₗ f' i j h = f i j h ∘ₗ ↑(e i).symm

Tactic:
rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
        refl_toLinearMap, comp_id]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x y : G i
this : Nonempty ι
h : (linearEquiv G f) ((of R ι G f i) x) = (linearEquiv G f) ((of R ι G f i) y)
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y

Tactic:
simp_rw [linearEquiv_of] at h

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x y : G i
this : Nonempty ι
h : ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = (f i j hij) y
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ restrictSupport R (s + t) ≤ restrictSupport R s * restrictSupport R t

Tactic:
restrictSupport_eq_span,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' (s + t)) ≤ restrictSupport R s * restrictSupport R t
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ restrictSupport R s * restrictSupport R t ≤ restrictSupport R (s + t)

Tactic:
restrictSupport_eq_span,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' s) * restrictSupport R t ≤ restrictSupport R (s + t)
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' s) * restrictSupport R t ≤ restrictSupport R (s + t)

Tactic:
restrictSupport_eq_span,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' s) * span R ((fun x ↦ (monomial x) 1) '' t) ≤ restrictSupport R (s + t)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
inst✝ : InverseSystem f
equivLim : F i ≃ ↑(limit f i)
H : ∀ (x : F i) (l : ↑(Iio i)), ↑(equivLim x) l = f ⋯ x
i✝ : ι
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i✝
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    rw [piEquivLim, piSplitLE_lt (hi.succ_lt <| (succ_le_iff_of_not_isMax hj).mp hsj)]
    apply (pEquivOnGlue hi e).compat

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

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ restrictSupport R 0 ≤ 1

Tactic:
restrictSupport_eq_span,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ span R ((fun x ↦ (monomial x) 1) '' 0) ≤ 1
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
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (toFun Q hfg) (Submodule.Quotient.mk y) = (rTensor Q g) y

Tactic:
simp only [rTensor.toFun, Submodule.liftQ_apply]

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

Goal state before:
pp: case tmul
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
x : M
y : N
⊢ ∃ S, x ⊗ₜ[R] y = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
exact ⟨Finsupp.single x y, by simp⟩

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
y : N ⊗[R] M
N' : Submodule R N
Nfg : N'.FG
x : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) y
sub : {(rTensor M N'.subtype) x, y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = y

Tactic:
obtain ⟨y, rfl⟩ := sub (.inr rfl)

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) ((rTensor M N'.subtype) y)
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
x y : N ⊗[R] M
eq : (rTensor M f) x = (rTensor M f) y
⊢ x = y

Tactic:
have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)
  obtain ⟨x, rfl⟩ := sub (.inl rfl)
  obtain ⟨y, rfl⟩ := sub (.inr rfl)
  simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl, rTensor_comp_apply] at eq
  have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
  simp_rw [← rTensor_comp_apply] at eq
  rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ Injective
    (⇑(TensorProduct.rid R x✝⁴).toAddEquiv.toEquiv ∘
      ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv)

Tactic:
convert! Subtype.coe_injective using 1

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ ⇑(TensorProduct.rid R x✝⁴).toAddEquiv.toEquiv ∘
      ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv =
    fun a ↦ ↑a
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 : (↑(cons i s hi)).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
coe_cons,

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 : (insert i ↑s).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → 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
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ (g i) x⁻¹ = ((g i) x)⁻¹

Tactic:
map_inv₀ (g i)

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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
q : ℚ
x✝² x✝¹ : ι
x✝ : x✝² ≤ x✝¹
x : G x✝²
⊢ (f x✝² x✝¹ x✝) ↑q * (f x✝² x✝¹ x✝) x = ↑q * (f x✝² x✝¹ x✝) x

Tactic:
map_ratCast

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

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

Tactic:
simp only [hj₁]

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
⊢ (F.intervalGapsWithin h a b ↑0).1 ≤ (F.intervalGapsWithin h a b ↑0).2
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Odd (f + g)

Tactic:
by
  intro a
  simp only [hf a, hg a, Pi.add_apply, neg_add]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

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

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

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
· simp only [hj₂, natCast_eq_last, intervalGapsWithin_last_snd, ge_iff_le]
    convert! hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind)) |>.right.right using 1
    simp [hj₂, hk]

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

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

Tactic:
prod_range_succ _ (N + 1),

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0 * (f (-(↑N + 1)) * f (↑N + 1)) =
    ((∏ x ∈ range (N + 1), f ↑x) * f ↑(N + 1)) ^ 2 / f 0
Module: Mathlib.Data.Int.Interval

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

Tactic:
toNat_sub_of_le h

Goal state after:
a b : ℤ
h : a ≤ b + 1
⊢ b + 1 - a = b + 1 - a
Module: Mathlib.Data.Int.Interval

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

Tactic:
toNat_sub_of_le h

Goal state after:
a b : ℤ
h : a ≤ b
⊢ b - a = b - a
Module: Mathlib.Data.Int.Interval

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

Tactic:
toNat_sub_of_le h

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ Ico 0 (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x

Tactic:
simp only [← range_eq_Ico]

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

Goal state before:
pp: case refine_1.refine_1
α : 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
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ i ∈ s

Tactic:
rw [← hi]

Goal state after:
case refine_1.refine_1
α : 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
i : α
e : β
he : e ∈ d
hi : ⋯.choose = i
⊢ ⋯.choose ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case trans
α : Type u_1
xs ys l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih1 : l₁✝.sym2 ~ l₂✝.sym2
ih2 : l₂✝.sym2 ~ l₃✝.sym2
⊢ l₁✝.sym2 ~ l₃✝.sym2

Tactic:
| trans _ _ ih1 ih2 =>

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

Goal state before:
pp: α : Type u_1
P : α → Prop
a b : α
⊢ (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b

Tactic:
by
  simp only [mem_iff, forall_eq_or_imp, forall_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩

Tactic:
rw! [hf a₁ a₂ h, eq_swap]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: 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)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)

Tactic:
by
      rw [← h X, ← h Y]
      exact φ.map f

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y : C
f : Y ⟶ X
h : W = Y
⊢ eqToHom h ≫ f ≍ f

Tactic:
rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]

Goal state after:
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 (e.functor.obj (e.inverse.obj Y))) ≫
        ((e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
              e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 4 5 =>
    rw [← map_comp e.inverse, ← map_comp e.functor, e.unitIso.hom_inv_id_app]
    dsimp only [Functor.id_obj]
    rw [map_id, map_id]

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 (e.functor.obj (e.inverse.obj Y))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
          𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Opposites

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

Tactic:
rw [← unop_comp, IsIso.inv_hom_id, unop_id]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
have := h f
    simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this
    tauto

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((forget C).map f)

Tactic:
← @HasForget₂.forget_comp (C := C) (D := D)

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((HasForget₂.forget₂ ⋙ forget D).map f)
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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
rw [← cancel_mono (β.app _), ← cancel_epi (α.app _), F.map_comp, F.map_comp, assoc, assoc]

Goal state after:
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
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right)) ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
      yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f

Tactic:
intro X Y f
    ext a
    dsimp [yonedaEquiv]
    simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ Small.{w, u} (Skeleton C) ∧ LocallySmall.{w, v, u} C → EssentiallySmall.{w, v, u} C

Tactic:
· rintro ⟨⟨S, ⟨e⟩⟩, L⟩
    let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm
    exact ⟨⟨InducedCategory _ (e'.trans e).symm, inferInstance,
      ⟨(ShrinkHoms.equivalence C).trans
      ((skeletonEquivalence (ShrinkHoms C)).symm.trans
      (inducedFunctor _).asEquivalence.symm)⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit.{w + 1}
X : C
⊢ F.obj X = G.obj X

Tactic:
by simp only [eq_iff_true_of_subsingleton]

Goal state after: