mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ (I.pi fun i ↦ {f i}) ⊆ s) ↔ ∃ I, I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s

Tactic:
simp [subset_def]

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i
s : Set ((i : ι) → α i)
⊢ (s ∈ pi fun i ↦ pure (f i)) ↔ ∃ I, I.Finite ∧ ∀ (g : (i : ι) → α i), (∀ i ∈ I, g i = f i) → g ∈ s

Tactic:
by
  simp only [← principal_singleton, mem_pi_principal]
  simp [subset_def]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ￢￢a ⊔ a ⊓ ￢a = a

Tactic:
sup_inf_left,

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢￢a ⊔ a) ⊓ (￢￢a ⊔ ￢a) = a
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ Set.image2 HMul.hMul (⇑ofAdd '' s) (⇑ofAdd '' t) = ⇑ofAdd '' s * ⇑ofAdd '' t

Tactic:
Set.image2_mul

Goal state after:
M : Type u_1
inst✝ : AddMonoid M
s t : Set M
⊢ ⇑ofAdd '' s * ⇑ofAdd '' t = ⇑ofAdd '' s * ⇑ofAdd '' t
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
⊢ ∀ᶠ (i : ι) in cofinite, f i '' (I, s).1.piecewise (fun i ↦ id ((I, s).2 i)) (fun x ↦ univ) i = univ

Tactic:
filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)

Goal state after:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
f : (i : ι) → α i → β i
hf : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
l : (i : ι) → Filter (α i)
I : Set ι
s : (i : ι) → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, s i ∈ l i
i : ι
hsurj : Surjective (f i)
hiI : i ∉ I
⊢ f i '' I.piecewise (fun i ↦ id (s i)) (fun x ↦ univ) i = univ
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x ↦ b) id) ((𝓟 {a}).coprod (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)

Tactic:
rw [principal_coprod_principal, map_principal]
  congr
  ext ⟨b', i'⟩
  constructor
  · rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
    simp
  · rintro ⟨h₁, _⟩
    use (a, i')
    simpa using h₁.symm

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

Goal state before:
pp: M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
p : M₀
hp : Prime p
s : Multiset M₀
⊢ (∀ r ∈ 0, Prime r) → p ∣ Multiset.prod 0 → ∃ q ∈ 0, p ~ᵤ q

Tactic:
simp [mt isUnit_iff_dvd_one.2 hp.not_isUnit]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalize a = p

Tactic:
← normalize_normalized_factor p p_mem,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
p_mem : p ∈ normalizedFactors a
⊢ normalize a = normalize p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ X.aroots S = {0}

Tactic:
by
  rw [aroots_def, map_X, roots_X]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).natDegree < n + 1
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
Nat.lt_succ_iff_lt_or_eq,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).natDegree < n ∨ (p * q).natDegree = n
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ p.degree < q.degree

Tactic:
by
    have := EuclideanDomain.div_add_mod p q
    rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this

Goal state after:
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
| p.degree

Tactic:
rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
| q.degree + (p / q).degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ a ∈ factors' a0, ↑a = p

Tactic:
exact ⟨⟨p, irreducible_of_mem_factorSet hm⟩, mem_factorSet_some.mp hm, rfl⟩

Goal state after:
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
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
⊢ { x // ∀ (i : ι) (hzi : z.fst ≤ i) (hwi : w.fst ≤ i), x = ih i ((f₁ z.fst i hzi) z.snd) ((f₂ w.fst i hwi) w.snd) }

Tactic:
choose j hzj hwj using exists_ge_ge z.1 w.1

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
f₁ : (i j : ι) → (h : i ≤ j) → T₁ h
inst✝⁶ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)
inst✝⁵ : DirectedSystem F₁ fun x1 x2 x3 ↦ ⇑(f₁ x1 x2 x3)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
f₂ : (i j : ι) → (h : i ≤ j) → T₂ h
inst✝⁴ : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)
inst✝³ : DirectedSystem F₂ fun x1 x2 x3 ↦ ⇑(f₂ x1 x2 x3)
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
j : ι
hzj : z.fst ≤ j
hwj : w.fst ≤ j
⊢ { x // ∀ (i : ι) (hzi : z.fst ≤ i) (hwi : w.fst ≤ i), x = ih i ((f₁ z.fst i hzi) z.snd) ((f₂ w.fst i hwi) w.snd) }
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
q : Q
p : P
⊢ ∃ a, (lTensor Q g) a = q ⊗ₜ[R] p

Tactic:
obtain ⟨n, rfl⟩ := hg p
    exact ⟨q ⊗ₜ[R] n, rfl⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inr
ι✝ : 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 ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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)
lt : 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:
· rwa [piEquivSucc, piSplitLE_lt, e.compat]

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p m✝ : ℕ
s : Set (σ →₀ ℕ)
hs : IsUpperSet s
x y : MvPolynomial σ R
hy : y ∈ (restrictSupport R s).carrier
m : σ →₀ ℕ
hm : m ∈ (x * y).support
⊢ m ∈ s

Tactic:
classical
    simp only [mem_support_iff, coeff_mul, ne_eq] at hm
    obtain ⟨⟨i, j⟩, hij, e⟩ := Finset.exists_ne_zero_of_sum_ne_zero hm
    refine hs (by simp_all [eq_comm]) (hy (show j ∈ y.support by aesop))

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
inst✝ : FiniteType R S
⊢ Small.{u, u_2} S

Tactic:
have : Small.{u} (⊤ : Subalgebra R S) :=
    Subalgebra.FG.small Algebra.FiniteType.out
  rwa [← small_univ_iff]

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

Goal state before:
pp: case a.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
x : A ⊗[R] B
⊢ x ∈ ⇑includeRight '' ↑I → ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
simp only [includeRight_apply, Set.mem_image, SetLike.mem_coe]

Goal state after:
case a.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
x : A ⊗[R] B
⊢ (∃ x_1 ∈ I, 1 ⊗ₜ[R] x_1 = x) → ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ ∃ y, 0 = x

Tactic:
exists_const

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ 0 = x
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ ∃ y, 0 = x

Tactic:
exists_const

Goal state after:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ 0 = x
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ↑(#s) • (↑(#s))⁻¹ • ∑ i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
smul_inv_smul₀

Goal state after:
case inr
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i

case inr.ha
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
hs : s.Nonempty
⊢ ↑(#s) ≠ 0
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 α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Tactic:
powerset_insert,

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

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 0 [MOD n]
⊢ (List.map f l).sum ≡ 0 [MOD n]

Tactic:
by
  simpa using listSum_map h

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

Goal state before:
pp: n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 0 [MOD n]
⊢ l.sum ≡ 0 [MOD n]

Tactic:
by
  simpa using listSum_map h

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

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

Tactic:
by
  simpa using listSum_map h

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

Goal state before:
pp: case inl
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z

Tactic:
by
  convert! mem_mk_right a <| Mem.other h
  rw [other_spec h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ Rel β (f p.1 ⋯, f p.2 ⋯) (f q.1 ⋯, f q.2 ⋯)

Tactic:
rel_iff',

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
h :
  ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp
⊢ (f p.1 ⋯, f p.2 ⋯) = (f q.1 ⋯, f q.2 ⋯) ∨ (f p.1 ⋯, f p.2 ⋯) = (f q.1 ⋯, f q.2 ⋯).swap
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
by
  refine ⟨fun h ↦ ?_, (· ▸ fromRel_bot)⟩
  ext x y
  simpa [h] using fromRel_prop (sym := sym)

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
← id_comp g,

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

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)

Tactic:
dsimp [Symmetrify.lift]

Goal state after:
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f → ∀ (i : I), IsIso (f i)

Tactic:
intro _ i

Goal state after:
case mp
I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : IsIso f
i : I
⊢ IsIso (f i)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ sSup S f ↔ ∃ W ∈ S, W f

Tactic:
simp +instances [MorphismProperty]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
S : Set (MorphismProperty C)
X Y : C
f : X ⟶ Y
⊢ sInf S f ↔ ∀ W ∈ S, W f

Tactic:
simp +instances [MorphismProperty]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
⊢ ⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm

Tactic:
by
  ext x
  obtain ⟨y, rfl⟩ := (e j).surjective x
  apply (e j').injective
  dsimp
  simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply]
  exact (congr_fun (naturality f) y).symm

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget CommMonCat).map f)

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
f : X ⟶ Y
x✝ : IsIso ((forget CommMonCat).map f)
i : (forget CommMonCat).obj X ≅ (forget CommMonCat).obj Y := asIso ((forget CommMonCat).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8
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
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ coneOfHom h m = s

Tactic:
coneOfHom_fac

Goal state after:
case e_8
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
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ (limitCone h).extend m = s
Module: Mathlib.CategoryTheory.Limits.IsLimit

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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h s = s.ι.app j

Tactic:
have h := cocone_fac h s

Goal state after:
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
X : C
h✝ : F.cocones.CorepresentableBy X
s : Cocone F
j : J
h : (colimitCocone h✝).extend (homOfCocone h✝ s) = s
⊢ (colimitCocone h✝).ι.app j ≫ homOfCocone h✝ s = s.ι.app j
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ u ≫ Arrow.Hom.left h.i ≫ f = u ≫ f' ≫ Arrow.Hom.right h.i

Tactic:
RetractArrow.i_w

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
h : RetractArrow f' f
g : Z ⟶ W
inst✝ : HasLiftingProperty g f
u : Z ⟶ X'
v : W ⟶ Y'
sq : CommSq u g f' v
⊢ u ≫ f' ≫ Arrow.Hom.right h.i = u ≫ f' ≫ Arrow.Hom.right h.i
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ (adj.homEquiv A X) u ≫ F.map p = i ≫ (adj.homEquiv B Y) v

Tactic:
simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
    rw [F.map_comp, Adjunction.unit_naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
by
  simp only [HasLift.iff]
  exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

Goal state after: