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

Goal state before:
pp: case e_a
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
⊢ f i * derivative (Multiset.map f s).prod =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
    AddMonoidHom.coe_mulLeft]

Goal state after:
case e_a
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 (HMul.hMul (f i)) (Multiset.map (fun i ↦ (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 ↦ (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
⊢ f s ≤ (weight w) f

Tactic:
by
  classical
  simp only [weight_apply, Finsupp.sum]
  by_cases h : s ∈ f.support
  · rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem h]
    refine le_trans ?_ (Nat.le_add_right _ _)
    apply Nat.le_mul_of_pos_right
    exact Nat.zero_lt_of_ne_zero hs
  · simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le

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

Goal state before:
pp: case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0 s

Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply]

Goal state after:
case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | (weight fun x ↦ 1) f ≤ n}.Finite

Tactic:
refine finite_of_nat_weight_le (Function.const σ 1) ?_ n

Goal state after:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0

Tactic:
simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
⊢ False

Tactic:
by rwa [hf, rootSet_zero] at h

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

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ (p * q).degree < ↑?n

pp: case n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ ℕ

Tactic:
apply lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 (Nat.lt_succ_self _))

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t

Tactic:
one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative)^[m] p).IsRoot t) ↔ p.IsRoot t ∧ (derivative p).IsRoot t
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
| q * p.div q + p.mod q = p

Tactic:
conv =>

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
| p %ₘ (q * C q.leadingCoeff⁻¹) + q * C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit (p.content * q.content)

Tactic:
simp_rw [hp.content_eq_one, hq.content_eq_one, mul_one, isUnit_one]

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

Goal state before:
pp: R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)

Tactic:
ih,

Goal state after:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ map f (EuclideanDomain.gcd (y % x) x) = map f (EuclideanDomain.gcd x y)
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y✝ : Associates D[X] := Associates.mk f
hy : y✝ ≠ 0
H : Type (max 0 u) := { x // x ∣ y✝ }
hfin : Fintype H := fintypeSubtypeDvd y✝ hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
x y : G
heq : i x = i y
⊢ x = y

Tactic:
Subtype.mk.injEq

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
f : D[X]
hf : f ≠ 0
G : Type u := { g // g.Monic ∧ g ∣ f }
y✝ : Associates D[X] := Associates.mk f
hy : y✝ ≠ 0
H : Type (max 0 u) := { x // x ∣ y✝ }
hfin : Fintype H := fintypeSubtypeDvd y✝ hy
i : G → H := fun x ↦ ⟨Associates.mk ↑x, ⋯⟩
x y : G
heq : Associates.mk ↑x = Associates.mk ↑y
⊢ ↑x = ↑y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: 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 * C x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y

Tactic:
map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ x * C x.leadingCoeff⁻¹ ∣ y ↔ x * C x.leadingCoeff⁻¹ ∣ y
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 α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

Tactic:
rw [count_mul ha hb hp]

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 α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : ¬b = 0
⊢ p.count a.factors + p.count b.factors = p.count a.factors ∨ p.count a.factors + p.count b.factors = p.count b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ ?m.78 q ≤ 0

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

Goal state after:
Module: Mathlib.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₂
⊢ ↑(f ≪≫ₗ g.symm) ∈ ⊥ ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
← comp_coe,

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₂
⊢ ↑g.symm ∘ₗ ↑f ∈ ⊥ ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ (e₁ ⟨i, hi⟩) (f ⋯ x) ⟨↑⟨j, hj✝⟩, hj⟩ = (e₂ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩

Tactic:
ih,

Goal state after:
case refine_1.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ (e₂ ⟨i, hi⟩) (f ⋯ x) ⟨↑⟨j, hj✝⟩, hj⟩ = (e₂ ⟨i⁺, hi✝⟩) x ⟨j, hj✝⟩
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : (i : ι) → FunLike (H i) (G i) C
inst✝⁷ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁶ : IsDirectedOrder ι
inst✝⁵ : Nonempty ι
inst✝⁴ : Zero R
inst✝³ : (i : ι) → Zero (G i)
inst✝² : (i : ι) → SMulWithZero R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0⟩⟧ = 0

Tactic:
zero_def i

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✝⁴ : Nonempty ι
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)
x✝¹ : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0⟩⟧ = 0

Tactic:
zero_def i

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun x ↦ s, ∏ i, f (p i)

Tactic:
rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ i ∈ range k, g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i).2) *
      ∏ i ∈ range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1 =
    g b / g a

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

Tactic:
prod_range_succ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ i ∈ range k, g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i).2) *
      ((∏ x ∈ range k, g (F.intervalGapsWithin h a b ↑x).2 / g (F.intervalGapsWithin h a b ↑x).1) *
        (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1)) =
    g b / g a

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ (∏ x ∈ Icc (-↑N) ↑N, f x) * (f (-(↑N + 1)) * f (↑N + 1)) = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
ih,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0 * (f (-(↑N + 1)) * f (↑N + 1)) = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ i + a * (n / a) < n + a

Tactic:
rw [add_comm n a]
      refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
      simp only [le_add_iff_nonneg_left]
      exact Int.emod_nonneg n (ne_of_gt ha)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ico m n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
have h₁ : (∑ i ∈ Ico (m + 1) n, f i • G i) = ∑ i ∈ Ico m (n - 1), f (i + 1) • G (i + 1) := by
    rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
    simp only [add_tsub_cancel_right]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
⊢ ∑ i ∈ Ico m n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
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
ist : Function.Bijective ⇑(TensorProduct.lift f)
e : M ≃ₗ[R] M'
⊢ Function.Bijective ⇑(↑e ∘ₗ TensorProduct.lift f)

Tactic:
exact e.bijective.comp ist

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:
← mem_sym2_iff

Goal state after:
α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
induction n with
  | zero =>
    refine mem_singleton.trans ⟨?_, fun _ ↦ Sym.eq_nil_of_card_zero _⟩
    rintro rfl
    exact fun a ha ↦ (Finset.notMem_empty _ ha).elim
  | succ n ih => ?_

Goal state after:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
m : Sym α (n + 1)
⊢ m ∈ s.sym (n + 1) ↔ ∀ a ∈ m, a ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(y, y) :: s(y, x) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ s(x, x) :: (List.map (fun y ↦ s(x, y)) xs ++ xs.sym2)) ~
    s(x, x) :: s(x, y) :: (List.map (fun y ↦ s(x, y)) xs ++ s(y, y) :: (List.map (fun y_1 ↦ s(y, y_1)) xs ++ xs.sym2))

Tactic:
conv =>

Goal state after:
α : Type u_1
xs✝ ys : List α
x y : α
xs : List α
| s(x, y)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ (Sym.filterNe a ↑m).snd ∈ s.sym (n - ↑(Sym.filterNe a ↑m).fst)

Tactic:
convert! sym_filterNe_mem a m.2

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ s = (insert a s).erase a
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤

Tactic:
by
  induction s using Finset.cons_induction <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithBot M
⊢ ∑ i ∈ s, f i = ⊥ ↔ ∃ i ∈ s, f i = ⊥

Tactic:
by
  induction s using Finset.cons_induction <;> simp [*]

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

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

Tactic:
by rw [← congr_right, other_spec' h, other_spec]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
h : IsBaseChange S f
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
T : Type u_4
O : Type u_5
inst✝³⁵ : CommSemiring T
inst✝³⁴ : Algebra R T
inst✝³³ : Algebra S T
inst✝³² : IsScalarTower R S T
inst✝³¹ : AddCommMonoid O
inst✝³⁰ : Module R O
inst✝²⁹ : Module S O
inst✝²⁸ : Module T O
inst✝²⁷ : IsScalarTower S T O
inst✝²⁶ : IsScalarTower R S O
inst✝²⁵ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁴ : CommSemiring R'
inst✝²³ : CommSemiring S'
inst✝²² : Algebra R R'
inst✝²¹ : Algebra S S'
inst✝²⁰ : Algebra R' S'
inst✝¹⁹ : Algebra R S'
inst✝¹⁸ : IsScalarTower R R' S'
inst✝¹⁷ : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra S B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : IsScalarTower R S B
inst✝⁸ : IsPushout R S A B
M : Type u_10
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
C : Type u_11
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower R A C
⊢ ∀ (x y : S ⊗[R] C),
    (cancelBaseChange R S A B C).symm (x * y) =
      (cancelBaseChange R S A B C).symm x * (cancelBaseChange R S A B C).symm y

Tactic:
· apply LinearMap.map_mul_of_map_mul_tmul
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), map✝¹ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝¹ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 ((G_obj ∘ obj) X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj (obj X) =
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f) ≍
      { obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map
      ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map x✝) =
    map✝ x✝

Tactic:
exact h_map

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

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

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

Tactic:
· rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp
      obtain rfl := eq_of_length_zero p hp
      obtain rfl := eq_nil_of_length_zero p hp
      exact ⟨d, q, nil, rfl, rfl⟩

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