mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : (algebraMap R S) (-q.coeff 0) = s * (aeval s) p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
eq_comm

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
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 → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
z : DirectLimit F f
x y : (i : ι) × F i
x✝ : x ≈ y
k : ι
hxk : x.fst ≤ k
hyk : y.fst ≤ k
eq : (f x.fst k hxk) x.snd = (f y.fst k hyk) y.snd
⊢ ⋯ ▸ ih x.fst x.snd = ih y.fst y.snd

Tactic:
by
    simp_rw [eq_rec_constant, compat _ _ hxk, compat _ _ hyk, eq]

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 ι
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
g✝ : (i : ι) → G i →ₗ[R] G' i
hg : ∀ (i j : ι) (h : i ≤ j), g✝ j ∘ₗ f i j h = f' i j h ∘ₗ g✝ i
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j ∘ₗ f i j h) g = (f' i j h ∘ₗ g✝ i) g
⊢ (of R ι G' f' j ∘ₗ g✝ j) ((f i j h) g) = (of R ι G' f' i ∘ₗ g✝ i) g

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply] at eq1 ⊢

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 ι
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
g✝ : (i : ι) → G i →ₗ[R] G' i
hg : ∀ (i j : ι) (h : i ≤ j), g✝ j ∘ₗ f i j h = f' i j h ∘ₗ g✝ i
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of R ι G' f' j) ((g✝ j) ((f i j h) g)) = (of R ι G' f' i) ((g✝ i) g)
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(baseChange A g)

Tactic:
LinearMap.baseChange_eq_ltensor

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R N
inst✝² : Module R P
g : N →ₗ[R] P
A : Type u_6
inst✝¹ : Semiring A
inst✝ : Algebra R A
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(lTensor A g)
Module: Mathlib.RingTheory.MvPolynomial.Basic

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

Tactic:
by_cases r = 0

Goal state after:
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

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
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
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ ((TensorProduct.mk R N Q) (h (r • p))) q - (fun x ↦ (RingHom.id R) r • x) (((TensorProduct.mk R N Q) (h p)) q) ∈
    (rTensor Q f).range

Tactic:
change h (r • p) ⊗ₜ[R] q - r • h p ⊗ₜ[R] q ∈ range (rTensor Q f)

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
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ h (r • p) ⊗ₜ[R] q - r • h p ⊗ₜ[R] q ∈ (rTensor Q f).range
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
x : M ⊗[R] N
⊢ ∃ S, x = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
by
  induction x with
  | zero => exact ⟨0, by simp⟩
  | tmul x y => exact ⟨Finsupp.single x y, by simp⟩
  | add x y hx hy =>
    obtain ⟨Sx, hx⟩ := hx
    obtain ⟨Sy, hy⟩ := hy
    use Sx + Sy
    rw [hx, hy]
    exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case add
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
x✝ y✝ : B ⊗[K] C
a✝¹ : x✝ * includeLeft b = includeLeft b * x✝
a✝ : y✝ * includeLeft b = includeLeft b * y✝
⊢ (x✝ + y✝) * includeLeft b = includeLeft b * (x✝ + y✝)

Tactic:
| add _ _ _ _ =>

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case add
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
x✝ y✝ : B ⊗[K] C
a✝¹ : x✝ * includeRight c = includeRight c * x✝
a✝ : y✝ * includeRight c = includeRight c * y✝
⊢ (x✝ + y✝) * includeRight c = includeRight c * (x✝ + y✝)

Tactic:
| add _ _ _ _ =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (↑(#(s ∪ t)) + ↑(#(s ∩ t))) / ↑(Fintype.card α) = (↑(#s) + ↑(#t)) / ↑(Fintype.card α)

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ ↑(#(s ∪ t) + #(s ∩ t)) / ↑(Fintype.card α) = ↑(#s + #t) / ↑(Fintype.card α)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s \ t).dens = s.dens

Tactic:
add_comm,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + (s ∩ t).dens = s.dens
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 : ι) → 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
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ / DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
by simp_rw [div_def, lift_def, map_div (g i)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f + g) (-a) = (f + g) a

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

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ max a b + 1 - min a b = |b - a| + ↑1

Tactic:
add_comm,

Goal state after:
a b : ℤ
⊢ 1 + max a b - min a b = |b - a| + ↑1
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
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
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
⊢ ((F.orderEmbOfFin h) ⟨j - 1, ⋯⟩).2 ≤ ((F.orderEmbOfFin h) ⟨j, ⋯⟩).1

Tactic:
set G := F.orderEmbOfFin (α := α ×ₗ α) h

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
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
⊢ (G ⟨j - 1, ⋯⟩).2 ≤ (G ⟨j, ⋯⟩).1
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ 1 + |b - a| = |b - a| + ↑1

Tactic:
add_comm,

Goal state after:
a b : ℤ
⊢ |b - a| + 1 = |b - a| + ↑1
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
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
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ y✝ : M₁ ⊗[R] M₂
a✝¹ : motive ((TensorProduct.lift f) x✝)
a✝ : motive ((TensorProduct.lift f) y✝)
⊢ motive ((TensorProduct.lift f) (x✝ + y✝))

Tactic:
| add _ _ _ _ =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
⊢ ∑ i ∈ Ico m n, f i • ∑ i ∈ range (i + 1), g i - f m • ∑ i ∈ range (m + 1), g i =
    ∑ i ∈ Ico m n, f i • ∑ i ∈ range (i + 1), g i - f (n - 1) • ∑ i ∈ range n, g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i

Tactic:
sub_add_cancel

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
⊢ ∑ i ∈ Ico m n, f i • ∑ i ∈ range (i + 1), g i - f m • ∑ i ∈ range (m + 1), g i =
    ∑ i ∈ Ico m n, f i • ∑ i ∈ range (i + 1), g i - f m • ∑ i ∈ range (m + 1), g i
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| ∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i +
      (f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i) -
    ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i

Tactic:
add_comm,

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
| f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range (m + 1), g i +
      ∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i -
    ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s

Tactic:
obtain ⟨m, he, rfl⟩ := he

Goal state after:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ a ::ₛ m
⊢ b ∈ s
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case mpr
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → ∏ j ∈ s, f j = ⊤

Tactic:
· exact fun ⟨h, h'⟩ ↦ prod_eq_top (Exists.choose_spec h).1 (Exists.choose_spec h).2 h'

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

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
⊢ z = s(a, Mem.other h)

Tactic:
rw [other_spec h]

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
m : M
⊢ (cancelBaseChange R S A B M) (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m

Tactic:
by
  change ((cancelBaseChangeAux R S A B M).symm).symm (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m
  simp [cancelBaseChangeAux, TensorProduct.one_def]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.symm.hom = β.hom ↔ β.hom = α.inv

Tactic:
eq_comm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
X Y : C
f : X ⟶ Y
⊢ IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
by
  revert F₁ F₂
  suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
    fun F₁ F₂ e => ⟨this e, this e.symm⟩
  intro F₁ F₂ e hf
  exact IsIso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, by cat_disch⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
⊢ F.Full

Tactic:
have := Full.of_iso h.symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
inst✝¹ : H.Full
inst✝ : G.Faithful
h : F ⋙ G ≅ H
this : (F ⋙ G).Full
⊢ F.Full
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ p → f True

Tactic:
intro H

Goal state after:
case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ ¬p → f False

Tactic:
intro H

Goal state after:
case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X

Tactic:
hX

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj X = G.obj X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ G.obj X = F.obj X

Tactic:
hX

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ G.obj X = G.obj 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 : C ⥤ D
X Y : C
p : X = Y
⊢ F.map (eqToHom p) = eqToHom ⋯

Tactic:
by cases p; simp

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
X : C
⊢ e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = 𝟙 (e.functor.obj X)

Tactic:
simpa [functor_unitIso_comp] using Iso.inv_eq_inv
    (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X)) (Iso.refl _)

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

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Mono (↾f) → Function.Injective f

Tactic:
intro H

Goal state after:
case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
⊢ Function.Injective f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ (P.map F).map G ≤ P.map (F ⋙ G)

pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ P.map (F ⋙ G) ≤ (P.map F).map G

Tactic:
· rw [map_le_iff]
    intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    exact ⟨X', Y', f', hf', ⟨G.mapArrow.mapIso e⟩⟩

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ P.map (F ⋙ G) ≤ (P.map F).map G
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 ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv = (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i

Tactic:
rw [← cancel_epi (α_ f g (h ≫ i)).inv, ← cancel_mono ((α_ f g h).inv ▷ i)]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by
  ext X x
  simpa [uliftCoyonedaEquiv]
    using congr_arg uliftCoyonedaEquiv.{w} (h _ (uliftCoyonedaEquiv.symm x))

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
F : J' ⥤ C
⊢ HasColimit F

Tactic:
apply hasColimit_of_equivalence_comp e

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := left } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := right } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right }

Tactic:
repeat simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := left } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := right } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := right }

Tactic:
repeat simp

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
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    { pt := f default,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m = s.ι.app default

Tactic:
by
        specialize w default
        simp_all

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
⊢ s ≅ t

Tactic:
apply Cocone.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₁
    simp only [Category.comp_id] at h₁
    have h₂ := t.ι.naturality WalkingSpan.Hom.fst
    dsimp at h₂
    simp only [Category.comp_id] at h₂
    simp_rw [← h₁, Category.assoc, w₁, h₂]
  · exact w₁
  · exact w₂

Goal state after: