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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree

Tactic:
exact Nat.le_add_right _ _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic

Tactic:
by
  delta Subalgebra.IsAlgebraic
  simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ t ∈ ⨅ i, l i → ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p i_1 (i.2 i_1)) ∧ ⋂ i_1 ∈ i.1, s i_1 (i.2 i_1) ⊆ t

Tactic:
simp only [mem_iInf', (hl _).mem_iff]
      rintro ⟨I, hI, V, hV, -, rfl, -⟩
      choose u hu using hV
      exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (C ↑n * (f ^ (n - 1) * derivative f)))

Tactic:
C_eq_natCast,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ ↑n ∣ eval c ((⇑derivative)^[m] (↑n * (f ^ (n - 1) * derivative f)))
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) * (C ↑(n - k) * X ^ (n - k - 1)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
C_eq_natCast,

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) * (↑(n - k) * X ^ (n - k - 1)) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

Tactic:
simp only [pi, mem_iInf', mem_comap, pi_def]

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I,
      I.Finite ∧
        ∃ V, (∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i) ∧ (∀ i ∉ I, V i = univ) ∧ s = ⋂ i ∈ I, V i ∧ s = ⋂ i, V i) →
    ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I, eval a ⁻¹' t a ⊆ s
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Tactic:
· rintro ⟨I, If, t, htf, hts⟩
    exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

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

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

Tactic:
derivative_sq,

Goal state after:
R : Type u
inst✝ : CommSemiring R
c : R
⊢ C 2 * (X + C c) * derivative (X + C c) = C 2 * (X + C c)
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Tactic:
by
  rw [sdiff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]

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

Goal state before:
pp: case mp
α : Type u_2
f : Filter α
⊢ f.ker = ∅ → f.kerᶜ ∈ f

pp: case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅

Tactic:
· intro h
    simp [h]

Goal state after:
case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
derivative_sq,

Goal state after:
R : Type u
inst✝ : CommRing R
c : R
⊢ C 2 * (X - C c) * derivative (X - C c) = C 2 * (X - C c)
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ~ᵤ g i
⊢ ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i

Tactic:
by
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.prod_empty]
    rfl
  | insert j s hjs IH =>
    classical
    convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
    grind [Associated.mul_mul]

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
p : R[X]
inst✝ : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
by
  rename_i iR ip0
  obtain rfl := Subsingleton.elim iR (Classical.decEq R)
  obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))
  rfl

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ (weight w) f

Tactic:
classical
  simp only [weight_apply, Finsupp.sum]
  trans f s • w s
  · apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs
  · rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
⊢ normalizedFactors 0 = 0

Tactic:
simp [normalizedFactors, factors]

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ (C a * p).roots = p.roots

Tactic:
by
  by_cases hp : p = 0 <;>
    simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
      zero_add, mul_zero]

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

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

Tactic:
by
  simp_rw [degree_eq_weight_one]
  refine finite_of_nat_weight_le (Function.const σ 1) ?_ n
  intro _
  simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)

Tactic:
refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hn : 0 < n
a x : R
⊢ x ∈ nthRoots n a ↔ x ^ n = a

Tactic:
by
  rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
    eval_X, sub_eq_zero]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ (C 0).aroots S = 0

Tactic:
aroots_C

Goal state after:
T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝ = 0
hq0 : ¬b✝ = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)

Tactic:
← leadingCoeff_eq_zero

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ ↑hu.unit⁻¹ • q ∣ q

Tactic:
Polynomial.smul_eq_C_mul,

Goal state after:
case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ C ↑hu.unit⁻¹ * q ∣ q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: 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
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq b) (Multiset.map (⇑f) p.roots))).prod ∣ map f p

Tactic:
refine
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| Multiset.filter_le (Eq b) _).trans ?_

Goal state after:
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
hmap : map f p ≠ 0
b : B
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.map (⇑f) p.roots)).prod ∣ map f p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (q * C q.leadingCoeff⁻¹).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Goal state after:
case refine_1
k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
by_cases H : x = 0

Goal state after:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
x : R
⊢ ¬Irreducible (C x)

Tactic:
by_cases H : x = 0

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

case neg
R : Type u
inst✝ : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (C x)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case inl
R : Type u
inst✝ : Field R
p₁ p₂ : R[X]
h : 0 ∣ p₁ - p₂
⊢ p₁ % 0 = p₂ % 0

Tactic:
simpa [sub_eq_zero] using h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
⊢ ∃ d, a = d ^ k

Tactic:
refine is_pow_of_dvd_count ha fun p hp ↦ ?_

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ k ∣ p.count a.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
by
  classical
  nontriviality α
  by_cases hk0 : k = 0
  · use 1
    rw [hk0, pow_zero] at h ⊢
    apply (mul_eq_one.1 h).1
  · refine is_pow_of_dvd_count ha fun p hp ↦ ?_
    apply dvd_count_of_dvd_count_mul hb hp hab
    rw [h]
    apply dvd_count_pow _ hp
    rintro rfl
    rw [zero_pow hk0] at h
    cases mul_eq_zero.mp h <;> contradiction

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
| ↑f k ⟨↑l, hl⟩

Tactic:
rw [← (piLTLim hi).right_inv f]

Goal state after:
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
k l : ↑(Iio i)
hl : ↑l < ↑k
| ↑((piLTLim hi).toFun ((piLTLim hi).invFun f)) k ⟨↑l, hl⟩
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)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝³ : DecidableEq ι
P : Type u_4
inst✝² : AddCommMonoid P
g : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
e : (i : ι) → G i ≃+ G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i j : ι
h : i ≤ j
x : G' i
eq1 : (e j) ((f i j h) ((e i).symm x)) = (f' i j h) x
⊢ (e j).symm ((f' i j h) x) = (f i j h) ((e i).symm x)

Tactic:
simp [← eq1]

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
hg : Surjective ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg ⋯) ((rTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
rTensor.inverse_of_rightInverse_apply

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
y : N ⊗[R] Q
⊢ Submodule.Quotient.mk y = Submodule.Quotient.mk y
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
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (toFun Q hfg) ((inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y)) = (rTensor Q g) y

Tactic:
rTensor.inverse_of_rightInverse_apply

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
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (toFun Q hfg) (Submodule.Quotient.mk y) = (rTensor Q g) y
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M f) ↔ Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype)

Tactic:
simp_rw [← EquivLike.injective_comp <| (LinearEquiv.ofInjective (e.toLinearMap ∘ₗ f)
    (e.injective.comp hf)).rTensor M, ← EquivLike.comp_injective _ (e.rTensor M),
    ← LinearEquiv.coe_coe, ← coe_comp, LinearEquiv.coe_rTensor, ← rTensor_comp]
  rfl

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ univ.dens = 1

Tactic:
by simp [dens, card_univ]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ (↑(#t))⁻¹ • ∑ x ∈ s, f x = (↑(#t))⁻¹ • ∑ x ∈ t, g x

Tactic:
sum_equiv e hst hfg

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
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
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✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
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✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

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
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

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
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
ext x
  induction x using DirectLimit.induction with | _ i x
  exact congr($(h i) x)

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ (Multiset.map f s).prod ≡ 1 [MOD n]

Tactic:
simpa using multisetProd_map h

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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ (Multiset.map f s).prod ≡ 1 [ZMOD n]

Tactic:
simpa using multisetProd_map h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ ∑ b ∈ image f ht.toFinset, #({a ∈ ht.toFinset | f a = b}) = ∑ b ∈ t, Nat.card ↑{a | f a = b}

Tactic:
refine Finset.sum_congr ?_ fun m hm ↦ ?_

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

case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = Nat.card ↑{a | f a = m}
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
⊢ ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d

Tactic:
let g' : {x // x ∈ d} → α := fun ⟨x, hx⟩ ↦ (hd x hx).choose

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
hd : ∀ a ∈ d, ∃ a_2 ∈ s, g a_2 = a
g' : { x // x ∈ d } → α :=
  fun x ↦
    match x with
    | ⟨x, hx⟩ => ⋯.choose
⊢ ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d