mathlib-initiative/mathlib-tactics huggingface dataset:
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
⊢ ∃ N', ∃ (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range

Tactic:
by
  obtain ⟨_, N', _, hN, _, hfin, h⟩ := exists_finite_submodule_of_setFinite' s hs
  refine ⟨N', hN, hfin, ?_⟩
  rw [← LinearMap.lTensor_comp_rTensor] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

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
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M f) ↔ Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype)

Tactic:
← EquivLike.injective_comp <| (LinearEquiv.ofInjective (e.toLinearMap ∘ₗ f)
    (e.injective.comp hf)).rTensor M,

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
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M f) ↔
    Injective (⇑(rTensor M (↑e ∘ₗ f).range.subtype) ∘ ⇑(LinearEquiv.rTensor M (LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
f g : M →ₗ[R] N
⊢ (baseChangeHom R S M N) f = (baseChangeHom R S M N) g → f = g

Tactic:
h

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R N
f g : M →ₗ[R] N
h : (baseChangeHom R S M N) f = (baseChangeHom R S M N) g
⊢ f = g
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 : ι) → AddMonoid (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarAddMonoid (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝¹⟩⟧ + star ⟦⟨i, x✝⟩⟧

Tactic:
add_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddMonoid (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarAddMonoid (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star ⟦⟨i, x✝¹ + x✝⟩⟧ = star ⟦⟨i, x✝¹⟩⟧ + star ⟦⟨i, x✝⟩⟧
Module: Mathlib.Data.Finset.Density

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

Tactic:
h

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 : ι) → AddMonoidWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
⊢ ⟦⟨Classical.arbitrary ι, ↑0⟩⟧ = ⟦⟨Classical.arbitrary ι, 0⟩⟧

Tactic:
Nat.cast_zero

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 : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
add_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹ + x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ (⟦⟨i, x✝²⟩⟧ + ⟦⟨i, x✝¹⟩⟧) * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧ + ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
add_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝² + x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧ + ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddZeroClass (G i)
inst✝² : (i : ι) → DistribSMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ r • (⟦⟨i, x✝¹⟩⟧ + ⟦⟨i, x✝⟩⟧) = r • ⟦⟨i, x✝¹⟩⟧ + r • ⟦⟨i, x✝⟩⟧

Tactic:
add_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → AddZeroClass (G i)
inst✝² : (i : ι) → DistribSMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ r • ⟦⟨i, x✝¹ + x✝⟩⟧ = r • ⟦⟨i, x✝¹⟩⟧ + r • ⟦⟨i, x✝⟩⟧
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
⊢ (↑(#s))⁻¹ • (↑(#t))⁻¹ • ∑ i ∈ t, ∑ j ∈ s, f j i = (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ s, ∑ j ∈ t, f i j

Tactic:
smul_comm,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ t, ∑ j ∈ s, f j i = (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ s, ∑ j ∈ t, f i j
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) → 0 ≤ i ∧ i < a

Tactic:
rintro ⟨i, _, rfl⟩

Goal state after:
case inr.mp
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
left✝ : n ≤ i ∧ i < n + a
⊢ 0 ≤ i % a ∧ i % a < a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ (∏ x ∈ Ico (-↑b) ↑b, f x / f (x + 1)) * (f (-(↑b + 1)) / f (-(↑b + 1) + 1) * ∏ x ∈ {↑b}, f x / f (x + 1)) =
    f (-(↑b + 1)) / f (↑b + 1)

Tactic:
prod_singleton,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ (∏ x ∈ Ico (-↑b) ↑b, f x / f (x + 1)) * (f (-(↑b + 1)) / f (-(↑b + 1) + 1) * (f ↑b / f (↑b + 1))) =
    f (-(↑b + 1)) / f (↑b + 1)
Module: Mathlib.Data.Int.Interval

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

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

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) ≤ a✝ ∧ a✝ < ↑n + 1 ↔ a✝ = -(↑m + 1) ∨ a✝ = ↑n ∨ -↑m ≤ a✝ ∧ a✝ < ↑n
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
a✝ : ι
⊢ a✝ ∈ {a | f a = m} → a✝ ∈ ↑ht.toFinset

Tactic:
h

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
a✝ : ι
h : a✝ ∈ {a | f a = m}
⊢ a✝ ∈ ↑ht.toFinset
Module: Mathlib.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
m : M
⊢ f m = h.equiv (1 ⊗ₜ[R] m)

Tactic:
h.equiv_tmul,

Goal state after:
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
m : M
⊢ f m = 1 • f m
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case mpr
α : Type u_1
xs : List α
a b : α
⊢ a ∈ xs ∧ b ∈ xs → s(a, b) ∈ xs.sym2

Tactic:
rintro ⟨ha, hb⟩
    exact mk_mem_sym2 ha hb

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

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s.sym2 = t.sym2 → s = t

Tactic:
h

Goal state after:
α : Type u_1
s t : Finset α
h : s.sym2 = t.sym2
⊢ s = t
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.val.sym2.card = (#s + 1).choose 2

Tactic:
Multiset.card_sym2,

Goal state after:
α : Type u_1
s : Finset α
⊢ (s.val.card + 1).choose 2 = (#s + 1).choose 2
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs ~ ys
⊢ xs.sym2 ~ ys.sym2

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs <+ ys
⊢ xs.sym2 <+ ys.sym2

Tactic:
induction h with

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : z ∈ List.sym (n + 1) (x :: xs)
⊢ a ∈ x :: xs

Tactic:
rw [List.sym, mem_append, mem_map] at hz

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α (n + 1)
ha : a ∈ z
hz : (∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z) ∨ z ∈ List.sym (n + 1) xs
⊢ a ∈ x :: xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (List.sym (n + 1) (x :: xs)).Nodup

Tactic:
rw [List.sym]
    refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj
    case inj =>
      intro z z'
      simp
    case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
⊢ Rel α a✝ b✝ → Rel β (Prod.map f f a✝) (Prod.map f f b✝)

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
a✝ b✝ : α × α
h : Rel α a✝ b✝
⊢ Rel β (Prod.map f f a✝) (Prod.map f f b✝)
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
h

Goal state after:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map g = F.map g
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
⊢ ∀ (y : O →ₗ[T] Q), (fun g' ↦ ↑S g' ∘ₗ h = r) y → y = q

Tactic:
· intro q' hq'
    apply hc.algHom_ext'
    apply_fun LinearMap.restrictScalars R at hq'
    rw [← LinearMap.comp_assoc]
    rw [show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq', hc.lift_comp]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
⊢ ∀ (h : Rel α (b, c) (d, e)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then e else d

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then e else d
Module: Mathlib.CategoryTheory.Functor.Basic

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
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map g = F.map g
Module: Mathlib.CategoryTheory.Functor.Category

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F ⟶ G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F ⟶ G
h : α = β
X : C
⊢ β.app X = β.app X
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
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
h

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map g = F.map g
Module: Mathlib.Tactic.CategoryTheory.Elementwise

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) x

Tactic:
h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
⊢ (ConcreteCategory.hom g) x = (ConcreteCategory.hom g) x
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f ≫ eqToHom p = g
⊢ f = g ≫ eqToHom ⋯

Tactic:
by simp [← h]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : eqToHom p ≫ g = f
⊢ g = eqToHom ⋯ ≫ f

Tactic:
by simp [← h]

Goal state after:
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
h : F = G
X : C
⊢ F.obj X = G.obj X

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ 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
⊢ G.obj Y = F.obj Y

Tactic:
rw [hY]

Goal state after:
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 ⋯
⊢ F.obj Y = G.obj Y

Tactic:
rw [hY]

Goal state after:
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
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f ≍ G.map f

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ G.map f ≍ G.map f
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.functor.map (e.unit.app (e.inverse.obj Y))) ≫
        (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
              e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (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 2 3 =>
    dsimp only [Functor.mapIso_inv, Iso.app_inv]
    rw [← map_comp e.inverse, ← e.counitInv_naturality, map_comp]

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.inverse.map (e.functor.map (e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))))) ≫
            e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (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)
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I✝ : Type u₁
G F : Discrete I✝ ⥤ C
h : ∀ (i : I✝), G.obj { as := i } = F.obj { as := i }
I : Discrete I✝
⊢ G.obj I = F.obj I

Tactic:
h

Goal state after:
case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I✝ : Type u₁
G F : Discrete I✝ ⥤ C
h : ∀ (i : I✝), G.obj { as := i } = F.obj { as := i }
I : Discrete I✝
⊢ F.obj { as := I.as } = F.obj I
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
h

Goal state after:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₁ = Hom.left φ₂

Tactic:
h

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₂ = Hom.left φ₂
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.left = Y.left

Tactic:
h

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Y.left = Y.left
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ X.right = Y.right

Tactic:
h

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Y.right = Y.right
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W f = W' f

Tactic:
h

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W' f = W' f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f = mk f'

Tactic:
h

Goal state after:
case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f' = mk f'
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
⊢ P ≤ Q → (fun x ↦ x.map F) P ≤ (fun x ↦ x.map F) Q

Tactic:
h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
⊢ (fun x ↦ x.map F) P ≤ (fun x ↦ x.map F) Q