mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ 1 = x

Tactic:
pow_one

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ x = x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ a.factorization p + b.factorization p = a.factorization p

Tactic:
← primeFactorsList_count_eq,

Goal state after:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ count p a.primeFactorsList + b.factorization p = count p a.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ count p a.primeFactorsList + b.factorization p = count p a.primeFactorsList

Tactic:
← primeFactorsList_count_eq,

Goal state after:
p a b : ℕ
hab : a.Coprime b
hpa : p ∈ a.primeFactorsList
⊢ count p a.primeFactorsList + count p b.primeFactorsList = count p a.primeFactorsList
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ 0 < ↑1

pp: case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2

Tactic:
· exact zero_lt_one

Goal state after:
case pos
h2 : _root_.Prime 2
b : Bool
ih : 0 ≠ 0 → emultiplicity 2 0! < ↑0
h : b = true
⊢ Prime 2
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
classical exact Finsupp.filter_apply_pos _ _ h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case zero
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
⊢ a ^ 1 ∈ S

Tactic:
pow_one

Goal state after:
case zero
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
⊢ a ∈ S
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y

Tactic:
orderOf_eq_orderOf_iff

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg

Tactic:
subst coeff_eq coeff_eq_deg deg_eq_deg
  rcases eq_or_ne m ⊥ with rfl | hh
  · exact bot_unique h_deg_le
  · obtain ⟨m, rfl⟩ := WithBot.ne_bot_iff_exists.mp hh
    exact degree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * (X ^ 1) ^ (n + 1) = C r * X ^ (n + 1)

Tactic:
pow_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * X ^ (n + 1) = C r * X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (p * n) = f.coeff n

Tactic:
by rw [mul_comm, coeff_expand_mul hp]

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

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0

Tactic:
intro b
    cases b
    · intros
      rw [Nat.cast_zero, mul_zero, zero_mul]
    · intro _ H
      rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ C (a * 2) * X ^ (2 - 1) = C (a * 2) * X

Tactic:
pow_one

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ C (a * 2) * X = C (a * 2) * X
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivative (X ^ 2) = C 2 * X

Tactic:
derivative_X_pow,

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ C ↑2 * X ^ (2 - 1) = C 2 * X
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ C 2 * X ^ (2 - 1) = C 2 * X

Tactic:
pow_one

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ C 2 * X = C 2 * X
Module: Mathlib.Algebra.Polynomial.CancelLeads

Goal state before:
pp: case neg.a.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
h0 : ¬C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
⊢ q.natDegree - p.natDegree + p.natDegree ≤ q.natDegree

Tactic:
rwa [Nat.sub_add_cancel]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
⊢ (p /ₘ (X - C a)).coeff n = p.coeff (n + 1) + a * (p /ₘ (X - C a)).coeff (n + 1)

Tactic:
by
  nontriviality R
  have := monic_X_sub_C a
  set q := p /ₘ (X - C a)
  rw [← p.modByMonic_add_div (X - C a)]
  have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
    |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
  simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative ((⇑derivative)^[n] (p * q)) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))

Tactic:
IH

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)) =
    derivative (∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ derivativeFinsupp X = Finsupp.single 0 X + Finsupp.single 1 1

Tactic:
ext i : 1
  match i with
  | 0 => simp
  | 1 => simp
  | (n + 2) => simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ C 2 * p ^ 1 * derivative p = C 2 * p * derivative p

Tactic:
pow_one

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ C 2 * p * derivative p = C 2 * p * derivative p
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * derivative (X ^ (n - k)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
derivative_X_pow,

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (C ↑(n - k) * X ^ (n - k - 1)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
⊢ ¬(X - C a) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
by rw [← rootMultiplicity_le_iff p0]

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

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ X ^ p.natTrailingDegree ∣ p

Tactic:
X_pow_dvd_iff

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
lift s to Finset ι using hs

Goal state after:
α : Type u
ι : Type w
f : ι → Set α
s : Finset ι
⊢ ⨅ i ∈ ↑s, 𝓟 (f i) = 𝓟 (⋂ i ∈ ↑s, f i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (p /ₘ (X - C a)).leadingCoeff = p.leadingCoeff

Tactic:
degree_eq_bot.mp <| Nat.WithBot.lt_zero_iff.mp hd,

Goal state after:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
inst✝ : Nontrivial R
hd : p.degree < 0
⊢ (0 /ₘ (X - C a)).leadingCoeff = leadingCoeff 0
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap (Prod.fst ∘ f) b ⊓ comap f (comap Prod.snd c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c

Tactic:
Filter.comap_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢(a ⊔ b)) (a ⊔ b)

Tactic:
exact codisjoint_hnot_left

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

Goal state before:
pp: α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s

Tactic:
refine ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ ?_⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ ?_⟩⟩ <;> convert!
    hx

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

Goal state before:
pp: case inr.cons
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ normalizedFactors a✝ + normalizedFactors s✝.prod = normalizedFactors a✝ + (Multiset.map normalizedFactors s✝).sum

pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

pp: case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0

Tactic:
IH

Goal state after:
case inr.cons
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ normalizedFactors a✝ + (Multiset.map normalizedFactors s✝).sum =
    normalizedFactors a✝ + (Multiset.map normalizedFactors s✝).sum

case inr.cons
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ 0 ∉ s✝

case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

case inr.cons.hy
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ s✝.prod ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : 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
⊢ a * c ~ᵤ (Classical.choose ⋯).prod

Tactic:
· rw [← b_eq]
          apply (Classical.choose_spec (pf _ _)).2.symm; assumption

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = C p.content * Classical.choose ⋯

Tactic:
← Classical.choose_spec (C_content_dvd p)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p = 0
⊢ p = p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝¹ : Nontrivial M
this✝ : StrongNormalizationMonoid M
this : DecidableEq M
⊢ Fintype { x // x ∣ y }

Tactic:
haveI := Classical.decEq (Associates M)

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
⊢ Fintype { x // x ∣ y }
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ X - C t ∣ p ∧ X - C t ∣ derivative p ↔ X - C t ∣ gcd p (derivative p)

Tactic:
dvd_gcd_iff

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
⊢ p ∣ Associates.mk a

Tactic:
have := Classical.decEq (Associates α)

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∣ Associates.mk a
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = x ^ 1

Tactic:
pow_one

Goal state after:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = x
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
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(lTensor M N.subtype)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (⨁ (i : ι), M i) N.subtype)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
← EquivLike.comp_injective _ (directSumRight R R _ _),

Goal state after:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective (⇑(directSumRight R R P M) ∘ ⇑(rTensor (⨁ (i : ι), M i) N.subtype))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ MapsTo (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Iio k) ↑F

Tactic:
intro j hj

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j ∈ Iio k
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j ∈ ↑F
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝² : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝² : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝¹ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝¹ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝¹)
g✝¹ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝¹ : IsTensorProduct g✝¹
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f✝ : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y
h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y
⊢ ∀ (c : S) (m : M₁) (n : M₂), (f m) (c • n) = c • (f m) n

Tactic:
simp [h₂]

Goal state after:
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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f)) ↔
    IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))

Tactic:
refine ⟨fun ist ↦ ?_, fun ist ↦ ?_⟩

Goal state after:
case refine_1
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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))

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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).sym2 = map (Sym2.map f) [].sym2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
a b : α
h : s(a, b) ∈ [].sym2
⊢ a ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
a b : α
ha : a ∈ []
hb : b ∈ []
⊢ s(a, b) ∈ [].sym2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
h : [].Nodup
⊢ [].sym2.Nodup

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : α
h : x ∈ []
⊢ map (fun y ↦ s(x, y)) [] <+ [].sym2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : α
h : x ∉ []
⊢ (map (fun y ↦ s(x, y)) []).Disjoint [].sym2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].sym2.dedup = [].dedup.sym2

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

Tactic:
by
  rw [← mem_sym2_iff]
  exact mk_mem_sym2_iff.trans <| and_self_iff

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

Goal state before:
pp: case nil
α : Type u_1
xs ys : List α
⊢ [].sym2 ~ [].sym2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
⊢ [].sym2.length = ([].length + 1).choose 2

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
xs : List α
⊢ List.sym 1 [] = map (fun x ↦ x ::ₛ Sym.nil) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
xs : List α
⊢ map ⇑(Sym2.equivSym α) [].sym2 = List.sym 2 []

Tactic:
| nil =>

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
⊢ r • q = r • q

Tactic:
rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
f' : X' ⟶ Y'
e : homOfEq f hX hY = f'
⊢ f ≍ f'

Tactic:
subst hX hY
  rw [Quiver.homOfEq_rfl] at e
  rw [e]

Goal state after: