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

Goal state before:
pp: case succ.e_a.refine_2
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)
⊢ 1 • ((⇑derivative)^[n - 0 + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
tsub_zero

Goal state after:
case succ.e_a.refine_2
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)
⊢ 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) = 1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - C a ∣ p /ₘ (X - C a) ^ rootMultiplicity a p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ i, f ((fun x ↦ i₀) i)

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ derivative (f i) * (Multiset.map f s).prod + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
mul_comm (derivative (f i))

Goal state after:
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f ≤ cofinite ↔ Coheyting.boundary f = f

Tactic:
rw [← Coheyting.inf_hnot_self, inf_eq_left, le_cofinite_iff_ker,
    Filter.hnot_def, le_principal_iff]
  constructor
  · intro h
    simp [h]
  · intro h
    rw [eq_empty_iff_forall_notMem]
    intro x hx
    exact hx f.kerᶜ h hx

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : derivative P = 0
⊢ P ∣ derivative P

Tactic:
simp [h]

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

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
simp only [notMem_support_iff] at h

Goal state after:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ f s ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize a

Tactic:
trans normalize (normalizedFactors a).prod
  · rw [normalizedFactors, ← coe_normalizeHom, ← map_multiset_prod, coe_normalizeHom,
      normalize_idem]
  · exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
h : p.roots = 0
a : R
⊢ ?m.50 ∉ p.roots

Tactic:
simp [h]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ degree f

Tactic:
simp only [notMem_support_iff] at h

Goal state after:
case neg
σ : Type u_1
R : Type u_5
inst✝² : AddCommMonoid R
inst✝¹ : PartialOrder R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : f s = 0
⊢ f s ≤ degree f
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ (normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod

Tactic:
· rw [Multiset.prod_add]
    exact
      ((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
by_cases hx : x = 0
        · simp [hx]
        by_cases hy : y = 0
        · simp [hy]
        simp [hx, hy]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
h : (C r).support = {0}
⊢ (C r).support.gcd (C r).coeff = normalize r

Tactic:
simp [h]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
x : ℕ
⊢ x ∈ p.support → p.coeff x = 0

Tactic:
simp [h]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C a).rootSet S = ∅

Tactic:
rootSet_def,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ ↑((C a).aroots S).toFinset = ∅
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
simp [h]

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

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rootSet_def,

Goal state after:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ ↑(p.aroots S).toFinset ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p = C p.content * p.primPart

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p = 0
⊢ p.primPart.IsPrimitive

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : p = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ (p * q).eraseLead - p.eraseLead * q

Tactic:
rw [← self_sub_C_mul_X_pow, ← self_sub_C_mul_X_pow, sub_mul, sub_sub, add_comm, sub_add,
    sub_sub_cancel, leadingCoeff_mul, map_mul, mul_assoc, mul_assoc]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * (X ^ p.natDegree * q) - C p.leadingCoeff * (C q.leadingCoeff * X ^ (p * q).natDegree)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬f.IsRoot a

Tactic:
eq_C_of_derivative_eq_zero haf

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
this : a.factors.prod = b.factors.prod
⊢ a = b

Tactic:
rwa [factors_prod, factors_prod] at this

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors ≤ b.factors
this : a.factors.prod ≤ b.factors.prod
⊢ a ≤ b

Tactic:
rwa [factors_prod, factors_prod] at this

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
a : MvPolynomial σ D
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
obtain ⟨s, a', rfl⟩ := exists_finset_rename a

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod ((rename Subtype.val) a')
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
s : Finset σ
a' : MvPolynomial (↥s) D
ha : (rename Subtype.val) a' ≠ 0
h : a' = 0
⊢ (rename Subtype.val) a' = 0

Tactic:
simp [h]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * u + (X - C a) * derivative ((X - C a) * u)

Tactic:
← mul_add (X - C a) u _

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * (u + derivative ((X - C a) * u))
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
⊢ #(ULift.{u, v} { x // IsAlgebraic R x }) ≤ #(ULift.{v, u} R[X]) * ℵ₀

Tactic:
refine lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le g fun f => ?_

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ lift.{u, v} #↑(g ⁻¹' {f}) ≤ ℵ₀
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
p : R[X]
h1 : p ≠ 0
h2 : (aeval ((aeval r) f)) p = 0
this : (p.comp f).coeff (p.natDegree * f.natDegree) ≠ 0
h : p.comp f = 0
⊢ (p.comp f).coeff (p.natDegree * f.natDegree) = 0

Tactic:
simp [h]

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

Goal state before:
pp: K : Type u
inst✝⁴ : CommSemiring K
D D' : Type v
inst✝³ : Semiring D
inst✝² : Algebra K D
h : IsCentral K D
inst✝¹ : Semiring D'
inst✝ : Algebra K D'
z : Dᵐᵒᵖ
hz : z ∈ Subalgebra.center K Dᵐᵒᵖ
k : K
hk : (ofId K D).toRingHom k = unop z
⊢ (ofId K Dᵐᵒᵖ).toRingHom k = z

Tactic:
simpa using congr(op $hk)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), a ∘ₗ ↑g.symm = ((↑g.symm ∘ₗ ↑f) ∘ₗ a) ∘ₗ ↑f.symm) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
eq_comp_toLinearMap_symm,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∀ (a : End R M), (a ∘ₗ ↑g.symm) ∘ₗ ↑f = (↑g.symm ∘ₗ ↑f) ∘ₗ a) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
⊢ IsAlgebraic (↥B) x

Tactic:
by
  let : Algebra A B := (Subalgebra.inclusion hle).toAlgebra
  have : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl
  exact h.extendScalars (Subalgebra.inclusion_injective hle)

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x✝³ x✝² : DirectSum ι G
x✝¹ : Eqv f x✝³ x✝²
i✝ j✝ : ι
h✝ : i✝ ≤ j✝
x✝ : G i✝
⊢ (AddCon.ker ↑(DirectSum.toModule R ι P g)) ((DirectSum.lof R ι G i✝) x✝) ((DirectSum.lof R ι G j✝) ((f i✝ j✝ h✝) x✝))

Tactic:
simpa using (Hg _ _ _ _).symm

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
⊢ (lTensor.inverse Q hfg hg).ker = ⊥

Tactic:
rw [LinearMap.ker_eq_bot]

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
⊢ Injective ⇑(lTensor.inverse Q hfg hg)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective (⇑(rTensor M Q.subtype) ∘ ⇑(lTensor (↥Q) i))

Tactic:
refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
x : ↥Q ⊗[R] N
⊢ (lTensor (↥Q) r) ((lTensor (↥Q) i) x) = x
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 g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
rw [expect, expect, sum_congr hst h, hst]

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
i : ι → κ
j : κ → ι
hi : ∀ a ∈ s, i a ∈ t
hj : ∀ a ∈ t, j a ∈ s
left_inv : ∀ a ∈ s, j (i a) = a
right_inv : ∀ a ∈ t, i (j a) = a
h : ∀ a ∈ s, f a = g (i a)
⊢ (↑(#t))⁻¹ • ∑ x ∈ s, f x = (↑(#t))⁻¹ • ∑ x ∈ t, g x

Tactic:
sum_nbij' i j hi hj left_inv right_inv h

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✝⁶ : 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 : (i : ι) → G i →ₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
i : ι := Classical.arbitrary ι
⊢ DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ ((algebraMap R (DirectLimit G f)) r) = (algebraMap R P) r

Tactic:
algebraMap_def i r,

Goal state after:
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✝⁶ : 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 : (i : ι) → G i →ₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
i : ι := Classical.arbitrary ι
⊢ DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ ⟦⟨i, (algebraMap R (G i)) r⟩⟧ = (algebraMap R P) r
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f • g)

Tactic:
by
  intro a
  simp only [Pi.smul_apply', hf a, hg a, smul_neg, neg_smul, neg_neg]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b + 1
⊢ ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ico a b)) = b - a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ioc a b)) = b - a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a < b
⊢ ↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1

Tactic:
simp [h]

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ x ∈ s, if Odd (f x) then 1 else 0) % 2 = 0 ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
← Finset.sum_filter,

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ a ∈ s with Odd (f a), 1) % 2 = 0 ↔ Even #({a ∈ s | Odd (f a)})
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (x :: xs).sym2.Nodup

Tactic:
rw [List.sym2]
    specialize ih h.of_cons
    rw [nodup_cons] at h
    refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
    case disj =>
      intro z hz hz'
      simp only [mem_cons, mem_map] at hz
      obtain ⟨_, (rfl | _), rfl⟩ := hz
        <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
    case notmem =>
      intro h'
      simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
    case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul
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
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] (M ⊗[R] P) ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
x✝ : M
y✝ : P
⊢ e (1 ⊗ₜ[S] (x✝ ⊗ₜ[R] y✝)) = (AlgebraTensorModule.map f LinearMap.id) (x✝ ⊗ₜ[R] y✝)

Tactic:
| tmul =>

Goal state after: