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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative)^[n + 1 + 1 + 2] p * X ^ 2 + (2 * (n + 1 + 1)) • (⇑derivative)^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative)^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative)^[n + 1 + 1 - k] ((⇑derivative)^[2] p) * X ^ (2 - k))

Tactic:
simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative)^[n] (derivative (derivative (derivative (derivative p)))) * X ^ 2 +
        (2 * (n + 1 + 1)) • (⇑derivative)^[n] (derivative (derivative (derivative p))) * X +
      ((n + 1 + 1) * (n + 1)) • (⇑derivative)^[n] (derivative (derivative p)) =
    (⇑derivative)^[n] (derivative (derivative (derivative (derivative p)))) * X ^ 2 +
        ((n + 1 + 1) * 2) • ((⇑derivative)^[n] (derivative (derivative (derivative p))) * X) +
      ((n + 1 + 1) * (n + 1)) • (⇑derivative)^[n] (derivative (derivative p))
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢￢a ⊔ ∂ a) \ ∂ a = ￢￢a

Tactic:
rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']

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

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ha₀s⟩ := hs

Goal state after:
case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
a₀ : α
ha₀s : a₀ ∈ s
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ derivative (X - C c) = 1

Tactic:
by
  rw [derivative_sub, derivative_X, derivative_C, sub_zero]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
h✝ : derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

pp: case neg
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
h✝ : ¬derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
case pos hP' => simp [hP']

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
h✝ : ¬derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset (Associates M)
h : p ≤ q
this✝ : DecidableEq (Associates M)
this : p.prod * 1 ≤ p.prod * (q - p).prod
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
by simpa

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

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.natDegree ≠ 0
x : R
hx : ((fun x ↦ eval x p) ⁻¹' {x}).Infinite
⊢ {x_1 | eval x_1 p = eval x_1 (C x)}.Infinite

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

Tactic:
by
  apply Multiset.induction_on_multiset_quot p
  apply Multiset.induction_on_multiset_quot q
  intro s t hs ht eq
  refine Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ ?_)
  · exact fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha
  · exact fun a ha => irreducible_mk.1 <| ht _ <| Multiset.mem_map_of_mem _ ha
  have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk
  rwa [eq', prod_mk, prod_mk, mk_eq_mk_iff_associated] at eq

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

Goal state before:
pp: case neg.calc_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
x : α
hadd : x ∈ Classical.choose ⋯ + Classical.choose ⋯
⊢ Prime x

Tactic:
Multiset.mem_add

Goal state after:
case neg.calc_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
x : α
hadd : x ∈ Classical.choose ⋯ ∨ x ∈ Classical.choose ⋯
⊢ Prime x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i ↦ f.coeff ↑i
⊢ Set.Finite fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i ↦ f.coeff ↑i
⊢ (π '' fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U) ⊆ Set.univ.pi fun x ↦ U

case refine_2
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i ↦ f.coeff ↑i
⊢ Set.InjOn π fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
⊢ False

Tactic:
eq_C_of_degree_le_zero h

Goal state after:
R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : p.degree ≤ 0
⊢ False
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)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
⊢ a.factors = b.factors

Tactic:
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
⊢ a.factors = b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : ¬a = 0
⊢ p.count a.factors ≤ p.count b.factors

Tactic:
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
h : a.factors ≤ b.factors
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
⊢ p.count a.factors ≤ p.count b.factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ % q = p₁ % q * (p₂ % q) % q

Tactic:
simp_rw [Polynomial.mod_def]
  apply Polynomial.mul_modByMonic

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ ∃ r, IsUnit r ∧ C r = C (c.coeff 0)

Tactic:
use c.leadingCoeff, unit_c

Goal state after:
case right
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : c.degree = ↑0
unit_c : IsUnit c.leadingCoeff
⊢ C c.leadingCoeff = C (c.coeff 0)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
iterate 3 rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : ¬C (lcm p.content q.content) = 0
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content) * r).content ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors

Tactic:
rw [count_mul ha hb hp, h] at habk
    exact habk

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

Goal state before:
pp: 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 x ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hinj : Function.Injective ⇑(algebraMap R S)
x : A
A_alg : IsAlgebraic R x
p : R[X]
hp₁ : p ≠ 0
hp₂ : (aeval x) p = 0
⊢ (aeval x) (map (algebraMap R S) p) = 0

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
hx : IsAlgebraic K ↑x
⊢ (↑x)⁻¹ ∈ A

Tactic:
obtain ⟨p, ne_zero, aeval_eq⟩ := hx
  rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq
  revert ne_zero aeval_eq
  refine p.recOnHorner ?_ ?_ ?_
  · intro h
    contradiction
  · intro p a hp ha _ih _ne_zero aeval_eq
    refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
    rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
  · intro p hp ih _ne_zero aeval_eq
    rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq
    rcases aeval_eq with aeval_eq | x_eq
    · exact ih hp aeval_eq
    · rw [x_eq, Subalgebra.coe_zero, inv_zero]
      exact A.zero_mem

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : g.ker = f.range
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
n : N
q : Q
this : Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q)
⊢ (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ rTensor Q g) (n ⊗ₜ[R] q) = (rTensor Q f).range.mkQ (n ⊗ₜ[R] q)

Tactic:
by simpa

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

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

Tactic:
← SetLike.coe_set_eq

Goal state after:
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
⊢ ↑(Submodule.restrictScalars R (map includeLeft I)) =
    ↑(LinearMap.rTensor B (Submodule.restrictScalars R I).subtype).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

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

Tactic:
← SetLike.coe_set_eq

Goal state after:
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
⊢ ↑(Submodule.restrictScalars R (map includeRight I)) =
    ↑(LinearMap.lTensor A (Submodule.restrictScalars R I).subtype).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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R M
w✝¹ : Submodule R N
hM : M' ≤ M₁
w✝ : w✝¹ ≤ N₁
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝¹
h : s ⊆ ↑(map (inclusion hM) (inclusion w✝)).range
⊢ ∃ M', ∃ (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor (↥N₁) (inclusion hM)).range

Tactic:
refine ⟨M', hM, hfin, ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R M
w✝¹ : Submodule R N
hM : M' ≤ M₁
w✝ : w✝¹ ≤ N₁
hfin : Module.Finite R ↥M'
left✝ : Module.Finite R ↥w✝¹
h : s ⊆ ↑(map (inclusion hM) (inclusion w✝)).range
⊢ s ⊆ ↑(LinearMap.rTensor (↥N₁) (inclusion hM)).range
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
⊢ Injective ⇑((TensorProduct.mk R S M) 1)

Tactic:
have : TensorProduct.mk R S M 1 =
      (Algebra.linearMap R S).rTensor M ∘ (TensorProduct.lid R M).symm := by ext; simp
  rw [this]
  refine Injective.comp ?_ (LinearEquiv.injective _)
  exact Flat.rTensor_preserves_injective_linearMap _ <| FaithfulSMul.algebraMap_injective R S

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

Tactic:
simp_rw [smul_def, mul_smul]

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
⊢ Function.Injective ⇑(hf.map hg i LinearMap.id)

Tactic:
have h : hf.map hg i LinearMap.id = hg.equiv ∘ i.rTensor M₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R M
inst✝⁷ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
h : ⇑(hf.map hg i LinearMap.id) = ⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg i LinearMap.id)
Module: Mathlib.RingTheory.Flat.Basic

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
⊢ Function.Injective ⇑(hf.map hg i LinearMap.id)

Tactic:
have h : hf.map hg i LinearMap.id = hg.equiv ∘ i.rTensor M₂ ∘ hf.equiv.symm :=
    funext fun x ↦ hf.inductionOn x (by simp) (by simp) (fun _ _ hx hy ↦ by simp [hx, hy])
  simpa [h] using Module.Flat.rTensor_preserves_injective_linearMap i hi

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

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact Fintype.card_le_of_injective _ f.2

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) = 𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i)

Tactic:
expect_add_distrib,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f₁ f₂ g₁ g₂ : ι → M
⊢ 𝔼 i ∈ s, f₁ i + 𝔼 i ∈ s, f₂ i + (𝔼 i ∈ s, g₁ i + 𝔼 i ∈ s, g₂ i) =
    𝔼 i ∈ s, f₁ i + 𝔼 i ∈ s, g₁ i + (𝔼 i ∈ s, f₂ i + 𝔼 i ∈ s, g₂ i)
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Set.SurjOn e ↑univ ↑univ

Tactic:
by
    simpa using he.surjective

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Odd (f + g)

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

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)
hy : a ∈ s(d, e)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ hy = if a = d then e else d

Tactic:
have {f g h} : @Eq.ndrec (Sym2 α) s(b, c)
      (fun x => a ∈ x → α) (fun _ => if a = b then c else b) f g h =
        if a = b then c else b := by subst g; rfl

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)
hy : a ∈ s(d, e)
this :
  ∀ {f : Sym2 α} {g : s(b, c) = f} {h : a ∈ f},
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) g h = if a = b then c else b
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ hy = if a = d then e else d
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c d : V
q : c ⟶ d
n✝ : ℕ
x : V
q'' : a ⟶ x
p'' : Path x c
hl : p''.length = n✝
h : ∀ {n : ℕ}, (q''.toPath.comp p'').length = n + 1 → ∃ c_1 f q x_1, q''.toPath.comp p'' = f.toPath.comp q
hp : (q''.toPath.comp p'').length = n✝ + 1
⊢ (p''.cons q).length = n✝ + 1

Tactic:
by simpa

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 : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
f : D ≌ E
X : C
⊢ (e.functor ⋙ f.functor).map
        ((e.unitIso ≪≫
                isoWhiskerRight
                    (e.functor.rightUnitor.symm ≪≫
                      e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
                    e.inverse ≪≫
                  (e.functor ⋙ f.functor).associator f.inverse e.inverse).hom.app
          X) ≫
      (((f.inverse ⋙ e.inverse).associator e.functor f.functor).symm ≪≫
              isoWhiskerRight
                  (f.inverse.associator e.inverse e.functor ≪≫
                    f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
                  f.functor ≪≫
                f.counitIso).hom.app
        ((e.functor ⋙ f.functor).obj X) =
    𝟙 ((e.functor ⋙ f.functor).obj X)

Tactic:
by
    dsimp
    simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
      functor_unit_comp_assoc, assoc]
    slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
    simp

Goal state after:
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
⊢ l₁ = l₂

Tactic:
ext
    rw [← cancel_epi i]
    simp only [LiftStruct.fac_left]

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ ∀ W' ∈ Set.range fun i ↦ W i, W'.RespectsLeft Q

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ ∀ W' ∈ Set.range fun i ↦ W i, W'.RespectsRight Q

Tactic:
by simpa

Goal state after: