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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f - 1 = rootMultiplicity a r + rootMultiplicity a f
this : IsDomain R
⊢ False

Tactic:
Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
this : IsDomain R
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
by_cases hp0 : p = 0; · simp only [hp0, rootMultiplicity_zero, Polynomial.map_zero]
  apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)
  rw [le_rootMultiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
    Polynomial.map_pow, Polynomial.map_sub, map_X, map_C]
  apply pow_rootMultiplicity_dvd

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

Goal state before:
pp: 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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n

Tactic:
rw [mul_comm, ← heq, degree_mul, WithBot.add_lt_add_iff_left]

Goal state after:
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ q.primPart.eraseLead.degree < q.primPart.degree

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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ p.primPart.degree ≠ ⊥
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
· rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
p : R[X]
inst✝¹ : CommRing k
inst✝ : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0

Tactic:
rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹

Tactic:
have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp

Goal state after:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp : p ≠ 0
this : p.leadingCoeff ≠ 0
⊢ ↑(normUnit p) = C p.leadingCoeff⁻¹
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ UniqueFactorizationMonoid (MvPolynomial σ D)

Tactic:
rw [iff_exists_prime_factors]
  intro a ha; obtain ⟨s, a', rfl⟩ := exists_finset_rename a
  obtain ⟨w, h, u, hw⟩ :=
    iff_exists_prime_factors.1 (uniqueFactorizationMonoid_of_fintype s) a' fun h =>
      ha <| by simp [h]
  exact
    ⟨w.map (rename (↑)), fun b hb =>
      let ⟨b', hb', he⟩ := Multiset.mem_map.1 hb
      he ▸ (prime_rename_iff (σ := σ) ↑s).2 (h b' hb'),
      Units.map (@rename s σ D _ (↑)).toRingHom.toMonoidHom u, by
      rw [Multiset.prod_hom, Units.coe_map, AlgHom.toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe,
        AlgHom.toRingHom_toMonoidHom, MonoidHom.coe_coe, ← map_mul, hw]⟩

Goal state after:
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{v, u} #R[X] * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀

Tactic:
lift_le.2 cardinalMk_le_max

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
⊢ lift.{v, u} (max #R ℵ₀) * ℵ₀ ≤ max (lift.{v, u} #R) ℵ₀
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)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → p_1.count a.factors = p_1.count (p ^ p.count a.factors).factors

Tactic:
intro q hq

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = q.count (p ^ p.count a.factors).factors
Module: Mathlib.Algebra.Colimit.Module

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

Tactic:
by
  simp [linearEquiv]

Goal state after:
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]
  induction s, hs using Set.Finite.induction_on with
  | empty => exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩
  | @insert a s _ _ ih =>
  obtain ⟨M', N', hM', hN', h⟩ := ih
  refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
  · exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩
  · refine ⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
    · exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h hz)
  · obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
    obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
    refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))
    · exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))
    · exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _

Goal state after:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)

Tactic:
let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _

Goal state after:
R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    ⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) ∘ ⇑(finsuppTensorFinsupp' R ι κ).symm

Tactic:
← LinearEquiv.coe_toLinearMap,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    ⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) ∘ ⇑↑(finsuppTensorFinsupp' R ι κ).symm
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 : ι) → DivisionSemiring (G i)
inst✝² : DivisionSemiring C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (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)
q : ℚ≥0
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ↑q = ↑q

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
  rw [nnratCast_def, lift_def, map_nnratCast (g i)]

Goal state after:
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
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
intervalGapsWithin_fst_of_lt_lt (hj₁ := by omega) (hj₂ := by omega),

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

Goal state before:
pp: R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 ⊗ₜ[R] x = s ⊗ₜ[R] x

Tactic:
TensorProduct.smul_tmul'

Goal state after:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ (s • 1) ⊗ₜ[R] x = s ⊗ₜ[R] x
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
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ : S ⊗[R] M
x : S
y : M
⊢ (IsTensorProduct.equiv h) (r • x ⊗ₜ[R] y) = r • (IsTensorProduct.equiv h) (x ⊗ₜ[R] y)

Tactic:
simp [smul_tmul', Algebra.linearMap_apply, smul_comm r x]

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

Goal state before:
pp: case cons.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : a = x ∧ (b = x ∨ b = x)
⊢ a = x ∨ a ∈ xs

Tactic:
exact .inl h.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val

Tactic:
dsimp [Finset.sym2]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
⊢ Function.Injective Finset.sym2

Tactic:
intro s t 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: 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 : m ∈ image (Sym.cons a) (s.sym n)
b : α
hb : b ∈ m
⊢ b ∈ s

Tactic:
mem_image

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
m : Sym α (n + 1)
a : α
ha : a ∈ s
he : ∃ a_1 ∈ s.sym n, a ::ₛ a_1 = m
b : α
hb : b ∈ m
⊢ b ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ xs.sym2.dedup = xs.dedup.sym2

Tactic:
by
  induction xs with
  | nil => simp only [List.sym2, dedup_nil]
  | cons x xs ih =>
    simp only [List.sym2, map_cons, cons_append]
    obtain hm | hm := Decidable.em (x ∈ xs)
    · rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
      refine mem_append_left _ ?_
      rw [mem_map]
      exact ⟨_, hm, Sym2.eq_swap⟩
    · rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]
      · exact (Sym2.mkEmbedding _).injective
      · exact map_mk_disjoint_sym2 x xs hm
      · simp [hm, mem_sym2_iff]

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

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs ys : List α
h : xs <+ ys
n : ℕ
⊢ List.sym (n + 1) [] <+ List.sym (n + 1) []

Tactic:
by simp only [refl]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ Std.Irrefl r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
intro ⟨h⟩

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : ∀ (a : α), ¬r a a
⊢ ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : List α
hx : x.length = 2
y : List α
hy : y.length = 2
h : (Vector.Perm.isSetoid α 2) ⟨x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
rcases x with - | ⟨_, x⟩

Goal state after:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
hx : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[], hx⟩) (fromVector ⟨y, hy⟩)

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
rcases x with - | ⟨_, x⟩

Goal state after:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝ : α
hx : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝], hx⟩) (fromVector ⟨y, hy⟩)

case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
rcases x with - | ⟨_, x⟩

Goal state after:
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)

case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝ : α
x : List α
hx : (head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝ :: x, hx⟩⟧) = ⟦⟨head✝ :: x, hx⟩⟧

Tactic:
rcases x with - | ⟨_, x⟩

Goal state after:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝ : α
hx : [head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝], hx⟩⟧) = ⟦⟨[head✝], hx⟩⟧

case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧

Tactic:
rcases x with - | ⟨_, x⟩

Goal state after:
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝¹, head✝], hx⟩⟧) = ⟦⟨[head✝¹, head✝], hx⟩⟧

case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩⟧
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'
h : IsPushout R R' S S'
T : Type u_8
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R' T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : IsScalarTower R R' T
e : S' ≃ₐ[R'] T
he : e.toRingEquiv.toRingHom.comp (algebraMap S S') = algebraMap S T
⊢ IsPushout R R' S T

Tactic:
rw [isPushout_iff] at h ⊢
  refine IsBaseChange.of_equiv (h.equiv ≪≫ₗ e.toLinearEquiv) fun x ↦ ?_
  simpa [h.equiv_tmul] using DFunLike.congr_fun he x

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_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF h₁ h₂ : F.FullyFaithful
⊢ h₁ = h₂

Tactic:
have := h₁.faithful
    cases h₁ with | mk f₁ hf₁ _ => cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
a b b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ b
hzero : (a✝¹.cons a✝).length = 0
⊢ a = b

Tactic:
· cases Nat.succ_ne_zero _ hzero

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.isoClosure.map F = P.map F

Tactic:
by
  refine le_antisymm ?_ (map_monotone P.le_isoClosure F)
  rintro X ⟨Y, ⟨Z, hZ, ⟨e⟩⟩, ⟨e'⟩⟩
  exact ⟨Z, hZ, ⟨F.mapIso e.symm ≪≫ e'⟩⟩

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

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

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

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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)

Tactic:
simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]

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✝ : IsIso i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ i ≫ inv i ≫ f = f

Tactic:
simp only [IsIso.hom_inv_id_assoc]

Goal state after: