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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (eval₂ C q (C r)) = eval₂ C q (derivative (C r)) * derivative q

Tactic:
rw [eval₂_C, derivative_C, eval₂_zero, zero_mul]

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

Goal state before:
pp: R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s : Multiset ι
f : ι → R[X]
⊢ derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum

Tactic:
refine Multiset.induction_on s (by simp) fun i s h => ?_
  rw [Multiset.map_cons, Multiset.prod_cons, derivative_mul, Multiset.map_cons _ i s,
    Multiset.sum_cons, Multiset.erase_cons_head, mul_comm (derivative (f i))]
  congr
  rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
    AddMonoidHom.coe_mulLeft]
  simp only [Function.comp_apply, Multiset.map_map]
  refine congr_arg _ (Multiset.map_congr rfl fun j hj => ?_)
  rw [← mul_assoc, ← Multiset.prod_cons, ← Multiset.map_cons]
  by_cases hij : i = j
  · simp [hij, Multiset.cons_erase hj]
  · simp [hij]

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

Goal state before:
pp: case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary (𝓟 q.1 ⊔ q.2) ≤ q.2

Tactic:
Coheyting.boundary_sup_le,

Goal state after:
case refine_4.refine_3
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ Coheyting.boundary (𝓟 q.1) ⊔ Coheyting.boundary q.2 ≤ q.2
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case refine_4
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
⊢ q = (f.ker, Coheyting.boundary f)

Tactic:
· have hqk := congrArg Filter.ker hq.2.2
    rw [ker_sup, ker_principal, le_cofinite_iff_ker.mp hq.1, union_empty] at hqk
    refine congrArg₂ Prod.mk hqk.symm (le_antisymm (le_inf ?_ ?_) ?_)
    · rw [hq.2.2]
      exact le_sup_right
    · rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]
      exact hq.2.1
    · grw [hq.2.2, Coheyting.boundary_sup_le, boundary_principal, bot_sup_eq]
      exact Coheyting.boundary_le

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

Goal state before:
pp: case cons
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : ∀ y ∈ c ::ₘ s, y ∈ {r | IsUnit r ∨ Prime r}
hprod : (c ::ₘ s).prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
| cons c s hind =>

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite

Tactic:
simp_rw [degree_eq_weight_one]

Goal state after:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | (weight fun x ↦ 1) f ≤ n}.Finite
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
h : e.symm a = 0
⊢ a = 0

Tactic:
convert! ← map_zero e
        simp [← h]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
inst✝ : DecidableEq R
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod = ∏ a ∈ p.roots.toFinset, (X - C a) ^ rootMultiplicity a p

Tactic:
simp only [count_roots, Finset.prod_multiset_map_count]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ FactorSet.prod ↑(a + b) = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
prod_coe,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = FactorSet.prod ↑a * FactorSet.prod ↑b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
prod_coe,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = (Multiset.map Subtype.val a).prod * FactorSet.prod ↑b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = (Multiset.map Subtype.val a).prod * FactorSet.prod ↑b

Tactic:
prod_coe,

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val (a + b)).prod = (Multiset.map Subtype.val a).prod * (Multiset.map Subtype.val b).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
prod_coe,

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val a✝).prod = 0 ↔ ↑a✝ = ⊤
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hroots : p.roots.card = p.natDegree
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod = C p.leadingCoeff * (Multiset.map (fun a ↦ X - C a) p.roots).prod

Tactic:
rw [hp.leadingCoeff, C_1, one_mul]

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero,
      rootMultiplicity_zero, le_refl]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Tactic:
degree_mul_leadingCoeff_inv q hq

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ q.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝ : Field R
x : R
H : x = 0
⊢ ¬Irreducible (C x)

Tactic:
rw [H, C_0]
    exact not_irreducible_zero

Goal state after:
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
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ ?m.78 q ≤ 0

Tactic:
by
      convert! count_le_count_of_le hph hq h
      symm
      rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', mul_zero]

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

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
halg : IsAlgebraic R a
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ IsAlgebraic S (g a)

Tactic:
by
  obtain ⟨p, h1, h2⟩ := halg
  refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩
  change aeval ((g : A →+* B) a) _ = 0
  rw [← map_aeval_eq_aeval_map h, h2, map_zero]

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

Goal state before:
pp: case neg
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
α : S
hα : ⇑f = α • ⇑g
β : S
hβ : ⇑g = β • ⇑f
x : M
hx : x ≠ 0
this : 1 • f x = (α * β) • f x
⊢ ∃ α, f = α • g

Tactic:
rw [smul_left_inj (by simpa)] at this

Goal state after:
case neg
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
α : S
hα : ⇑f = α • ⇑g
β : S
hβ : ⇑g = β • ⇑f
x : M
hx : x ≠ 0
this : 1 = α * β
⊢ ∃ α, f = α • g
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
p p' : P
q : Q
⊢ (h (p + p') - (h p + h p')) ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
apply le_comap_range_rTensor 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
p p' : P
q : Q
⊢ h (p + p') - (h p + h p') ∈ f.range
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
⊢ (h (r • p) - r • h p) ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
apply le_comap_range_rTensor 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 • h p ∈ f.range
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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ (h (g n) - n) ⊗ₜ[R] q ∈ (rTensor Q f).range

Tactic:
apply le_comap_range_rTensor 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
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
⊢ h (g n) - n ∈ f.range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.add
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
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
a b : A ⊗[R] B
ha :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hb :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
obtain ⟨x', ha'⟩ := ha

Goal state after:
case a.refine_4.add
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
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
a b : A ⊗[R] B
hb :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
x' : ↥(Submodule.restrictScalars R I) ⊗[R] B
ha' :
  (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x' =
    a • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

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

Tactic:
obtain ⟨x', ha'⟩ := ha

Goal state after:
case a.refine_4.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
hb :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
x' : A ⊗[R] ↥(Submodule.restrictScalars R I)
ha' :
  (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x' =
    a • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
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:
← LinearMap.coe_comp

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: 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 : ι) → MulOneClass (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ 1 * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
by simp_rw [one_def i, mul_def, one_mul]

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

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

Tactic:
rw [Sym.mem_cons] at ha

Goal state after:
case inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
x✝ : Module R Q := I₂
⊢ ?m.148

Tactic:
exact r • q

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
x✝ : Module R Q := I₃
⊢ Q

Tactic:
exact r • q

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

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).2, (Quot.out e).1)

Tactic:
by rw [eq_swap, Sym2.mk, e.out_eq]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ Multiset α

Tactic:
by
  refine Sym2.lift ?_ z
  use (Multiset.ofList [·, ·])
  simp [List.Perm.swap]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toFinset ↔ x ∈ z

Tactic:
rw [← Sym2.mem_toMultiset, Sym2.toFinset, Multiset.mem_toFinset]

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

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

Tactic:
exact other_mem h

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.hom.app X ≫ e.inv.app X).unop = 𝟙 (Opposite.unop (F.obj X))

Tactic:
hom_inv_id_app,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (𝟙 (F.obj X)).unop = 𝟙 (Opposite.unop (F.obj X))
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ i ≫ l₁.l = i ≫ l₂.l

Tactic:
simp only [LiftStruct.fac_left]

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom ≫ β.app Y.right =
    (F₁ ⋙ L').map (F₁.preimage φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right

Tactic:
rw [← Functor.comp_map, ← α.naturality_assoc]

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

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

Tactic:
by
    let i := asIso ((forget RingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toRingCatIso.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 : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g ↦ F.map g ≫ adj.counit.app Y) ((fun f ↦ adj.unit.app X ≫ G.map f) f) = f

Tactic:
dsimp
    rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ e.homEquiv f = (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X))

Tactic:
by
  conv_lhs => rw [← Category.id_comp f, e.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
apply yonedaEquiv.injective

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' : C
f : X' ⟶ X
F : Cᵒᵖ ⥤ Type v₁
x : F.obj (op X)
⊢ yonedaEquiv (yoneda.map f ≫ yonedaEquiv.symm x) =
    yonedaEquiv (yonedaEquiv.symm ((ConcreteCategory.hom (F.map f.op)) x))
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
apply yonedaEquiv.injective

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv (yonedaEquiv.symm x ≫ f) = yonedaEquiv (yonedaEquiv.symm ((ConcreteCategory.hom (f.app (op X))) x))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : coyoneda.obj (op X) ⟶ F
⊢ (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
      ((fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)) η) =
    η

Tactic:
ext Y (x : X ⟶ Y)
    simp [← NatTrans.naturality_apply]

Goal state after: