mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ k * p.count a.factors

Tactic:
apply dvd_mul_right

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : k = 0
⊢ a = 1 ^ k

Tactic:
rw [hk0, pow_zero] at h ⊢

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = 1
a✝ : Nontrivial α
hk0 : k = 0
⊢ a = 1
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
⊢ IsAlgebraic R x

Tactic:
have ⟨⟨r, m⟩, h⟩ := surj M x

Goal state after:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
⊢ IsAlgebraic R x
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S

Tactic:
simp_rw [Algebra.isAlgebraic_def, isAlgebraic_bot_iff h]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ ↑0 = 0

Tactic:
Subalgebra.coe_zero

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case pos
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
simp [mem_restrictSupport_iff, support_monomial, *]

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

Goal state before:
pp: case neg
σ : Type u
R : Type v
inst✝ : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h✝ : ¬r = 0
⊢ (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

Tactic:
simp [mem_restrictSupport_iff, support_monomial, *]

Goal state after:
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
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
by
  simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]
  rw [exact_iff] at hfg
  apply LinearMap.congr_fun
  apply TensorProduct.ext'
  intro n q
  suffices Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by
    simpa
  rw [Submodule.Quotient.eq, ← TensorProduct.tmul_sub]
  apply le_comap_range_lTensor f n
  rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]

Goal state after:
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
hfg : Exact ⇑f ⇑g
⊢ (rTensor Q g ∘ₗ rTensor Q f).ker = ⊤

Tactic:
← rTensor_comp,

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

Goal state before:
pp: 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
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ M' N', Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(mapIncl M' N').range

Tactic:
simp_rw [Module.Finite.iff_fg]

Goal state after:
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
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ s ⊆ ↑(mapIncl M' N').range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert
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
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert a s ⊆ ↑(mapIncl M' N').range

Tactic:
refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_

Goal state after:
case insert.refine_1
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
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert 0 s ⊆ ↑(mapIncl M' N').range

case insert.refine_2
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
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x : M
y : N
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(mapIncl M' N').range

case insert.refine_3
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
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
hx : ∃ M' N', M'.FG ∧ N'.FG ∧ insert x s ⊆ ↑(mapIncl M' N').range
hy : ∃ M' N', M'.FG ∧ N'.FG ∧ insert y s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(mapIncl M' N').range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
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 A
⊢ ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range ⊆
    ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
rintro x ⟨y, rfl⟩

Goal state after:
case a
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 A
y : ↥(Submodule.restrictScalars R I) ⊗[R] B
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y ∈ ↑(Submodule.restrictScalars R (map includeLeft I))
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a
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
⊢ ↑(LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).range ⊆
    ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
rintro x ⟨y, rfl⟩

Goal state after:
case a
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
y : A ⊗[R] ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y ∈ ↑(Submodule.restrictScalars R (map includeRight I))
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
hs : (↑s).PairwiseDisjoint t
⊢ (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
h : (↑s).PairwiseDisjoint t
x : κ
⊢ (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x

Tactic:
by
  rw [mulIndicator_biUnion s t h]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]

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 : α
z : α × α
hz : z ∈ ↑F
⊢ z ∈ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) '' Iio k

Tactic:
← F.range_orderEmbOfFin h (α := α ×ₗ α)

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
hz : z ∈ Set.range ⇑(F.orderEmbOfFin h)
⊢ z ∈ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) '' Iio k
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-(↑0 + 1)) (↑0 + 1), f m = f (↑0 + 1) * f (-(↑0 + 1)) * ∏ m ∈ Icc (-↑0) ↑0, f m

pp: case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m

Tactic:
· rw [Icc_succ_succ]
    grind

Goal state after:
case succ
R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Ioc (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}

Tactic:
simp only [mem_Ioc, union_insert, union_singleton, mem_insert]

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) < a✝ ∧ a✝ ≤ ↑n + 1 ↔ a✝ = -↑m ∨ a✝ = ↑n + 1 ∨ -↑m < a✝ ∧ a✝ ≤ ↑n
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
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ g₁ x = g₂ x

Tactic:
refine h.inductionOn x _ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
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
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ g₁ 0 = g₂ 0

case refine_2
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
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ ∀ (m : M), g₁ (f m) = g₂ (f m)

case refine_3
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
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ ∀ (s : S) (n : N), g₁ n = g₂ n → g₁ (s • n) = g₂ (s • n)

case refine_4
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
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ ∀ (n₁ n₂ : N), g₁ n₁ = g₂ n₁ → g₁ n₂ = g₂ n₂ → g₁ (n₁ + n₂) = g₂ (n₁ + n₂)
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (x :: xs).sym2.Nodup

Tactic:
rw [List.sym2]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.val = 0 ↔ s = ∅

Tactic:
val_eq_zero

Goal state after:
α : Type u_1
s : Finset α
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Sym2 α
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

Tactic:
induction s with

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
t : Sym2 α
a b : α
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
motive : Sym2 α → Sort u_4
f : (a b : α) → motive s(a, b)
h : ∀ (a b : α), f a b ≍ f b a
z : Sym2 α
⊢ ∀ (a b : α × α), a = b ∨ a = b.swap → f a.1 a.2 ≍ f b.1 b.2

Tactic:
rintro _ _ (rfl | rfl)

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
motive : Sym2 α → Sort u_4
f : (a b : α) → motive s(a, b)
h : ∀ (a b : α), f a b ≍ f b a
z : Sym2 α
a✝ : α × α
⊢ f a✝.1 a✝.2 ≍ f a✝.1 a✝.2

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
motive : Sym2 α → Sort u_4
f : (a b : α) → motive s(a, b)
h : ∀ (a b : α), f a b ≍ f b a
z : Sym2 α
b✝ : α × α
⊢ f b✝.swap.1 b✝.swap.2 ≍ f b✝.1 b✝.2
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'
inst✝ : IsPushout R S R' S'
a : S
⊢ (equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1

Tactic:
by
  rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]

Goal state after:
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
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
m : M
⊢ (cancelBaseChangeAux R S A B M).symm (s ⊗ₜ[R] m) = (algebraMap S B) s ⊗ₜ[A] m

Tactic:
simp [IsPushout.cancelBaseChangeAux, IsPushout.equiv_tmul]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom

Tactic:
apply Functor.map_comp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

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

Tactic:
intro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X
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
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
← cancel_mono (e.hom.app Y),

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ e.hom.app Y = (eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Discrete.Basic

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

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

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

Tactic:
replace w := se.section_ ≫= w

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
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f0x1 ≫ fx11 = fx01 ≫ f1x1

Tactic:
rw [← cancel_epi f00x]
  grind

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:
by
    let i := asIso ((forget CommMonCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toCommMonCatIso.isIso_hom

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    (G ⋙ F).map f ≫ (adj.homEquiv (G.obj Y) ((𝟭 D).obj Y)).invFun (𝟙 (G.obj Y)) =
      (adj.homEquiv (G.obj X) ((𝟭 D).obj X)).invFun (𝟙 (G.obj X)) ≫ (𝟭 D).map f

Tactic:
intros
          simp [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
| h.homEquiv f

Tactic:
rw [← Category.comp_id f]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
| h.homEquiv (f ≫ 𝟙 X)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : F.IsRepresentable
X : Cᵒᵖ
f : unop X ⟶ F.reprX
⊢ (ConcreteCategory.hom (F.reprW.hom.app X)) f = (ConcreteCategory.hom (F.map f.op)) F.reprx

Tactic:
by
  apply RepresentableBy.homEquiv_eq

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
simp [yonedaEquiv, ← f.naturality_apply]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = (i ≫ i') ≫ g
⊢ sq.HasLift

Tactic:
rw [assoc] at fac

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A B B' X Y Y' : C
i : A ⟶ B
i' : B ⟶ B'
p : X ⟶ Y
p' : Y ⟶ Y'
inst✝¹ : HasLiftingProperty i p
inst✝ : HasLiftingProperty i' p
f : A ⟶ X
g : B' ⟶ Y
sq : CommSq f (i ≫ i') p g
fac : f ≫ p = i ≫ i' ≫ g
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan X Y
hc : IsLimit c
s : BinaryCofan (op X) (op Y)
m : op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) ⟶ s.pt
h₁ : c.fst.op ≫ m = s.inl
h₂ : c.snd.op ≫ m = s.inr
⊢ m.unop ≫ c.fst = (hc.lift s.unop).op.unop ≫ c.fst

Tactic:
simp [← h₁]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan X Y
hc : IsColimit c
s : BinaryFan (op X) (op Y)
m : s.pt ⟶ op (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h₁ : m ≫ c.inl.op = s.fst
h₂ : m ≫ c.inr.op = s.snd
⊢ c.inl ≫ m.unop = c.inl ≫ (hc.desc s.unop).op.unop

Tactic:
simp [← h₁]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryFan (op X) (op Y)
hc : IsLimit c
s : BinaryCofan X Y
m : unop (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) ⟶ s.pt
h₁ : c.fst.unop ≫ m = s.inl
h₂ : c.snd.unop ≫ m = s.inr
⊢ m.op ≫ c.fst = (hc.lift s.op).unop.op ≫ c.fst

Tactic:
simp [← h₁]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
c : BinaryCofan (op X) (op Y)
hc : IsColimit c
s : BinaryFan X Y
m : s.pt ⟶ unop (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })
h₁ : m ≫ c.inl.unop = s.fst
h₂ : m ≫ c.inr.unop = s.snd
⊢ c.inl ≫ m.op = c.inl ≫ (hc.desc s.op).unop.op

Tactic:
simp [← h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
s : PullbackCone g f
m : s.pt ⟶ t.pt
h₁ : m ≫ t.snd = s.fst
h₂ : m ≫ t.fst = s.snd
⊢ m = ht.lift s.flip

Tactic:
by
    apply IsLimit.hom_ext ht <;> simp [h₁, h₂]

Goal state after: