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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
⊢ p = 0

Tactic:
by_contra hp

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Tactic:
exact (derivative_rootMultiplicity_of_root h).symm.le

Goal state after:
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✝ : NormalizationMonoid R
p : R[X]
⊢ C ↑(normUnit p.leadingCoeff) * C ↑(normUnit p.leadingCoeff)⁻¹ = 1

Tactic:
by
      rw [← map_mul, Units.mul_inv, C_1]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this

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

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

Tactic:
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb

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

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

Tactic:
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a

Tactic:
by
  constructor
  · rw [← mk_dvd_mk]
    apply dvd_of_mem_factors
  · apply mem_factors_of_dvd ha0 hp

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
⊢ ¬Prime p

Tactic:
hp

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ Associates.mk a ⊓ Associates.mk b

Tactic:
exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb)

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ (normalize p).Monic

Tactic:
rw [Monic, leadingCoeff_normalize, normalize_eq_one]

Goal state after:
R : Type u
inst✝¹ : Field R
p : R[X]
inst✝ : DecidableEq R
hp0 : IsUnit p.leadingCoeff
⊢ IsUnit p.leadingCoeff
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

Tactic:
by
  constructor
  · intro hg p ha hb hp
    refine (Associates.prime_mk.mpr hp).not_isUnit (isUnit_of_dvd_one ?_)
    rw [← hg]
    exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb)
  · contrapose
    intro hg hc
    obtain ⟨p, hp, hpa, hpb⟩ := exists_prime_dvd_of_not_inf_one ha0 hb0 hg
    exact hc hpa hpb hp

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

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

Tactic:
lcm_eq_zero_iff,

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

Goal state before:
pp: case a
α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ p.count a.factors ≤ Nat.find ⋯

Tactic:
have hph := pow_ne_zero (@Nat.find (fun n => a ∣ p ^ n) _ ⟨n, h⟩) hp.ne_zero
    rcases subsingleton_or_nontrivial α with hα | hα
    · simp [eq_iff_true_of_subsingleton] at hph
    convert! count_le_count_of_le hph hp (@Nat.find_spec (fun n => a ∣ p ^ n) _ ⟨n, h⟩)
    rw [count_pow hp.ne_zero hp, count_self hp, mul_one]

Goal state after:
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
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
⊢ (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0

Tactic:
hp

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0
⊢ p = 0
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]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
⊢ (Polynomial.aeval f) p = 0 → p = 0

Tactic:
hp

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ p = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
⊢ p.coeff 0 = 0 → a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

Tactic:
hp

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
hp : p.coeff 0 = 0
⊢ a ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
⊢ p ≠ 0 → (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
hp

Goal state after:
case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
⊢ (p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A) → p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)

Tactic:
obtain rfl | hk := le_succ_iff_eq_or_le.mp hk

Goal state after:
case inl.inl
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
x : F i⁺
hk : i⁺ ∈ Iic i⁺
h : i⁺ ≤ i⁺
⊢ (piEquivSucc equiv e hi ⟨i⁺, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)

case inl.inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
⊢ (piEquivSucc equiv e hi ⟨k, hk✝⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
⊢ nilpotencyClass x = 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}
  suffices s = univ by change sInf _ = 0; simp [s] at this; simp [this]
  exact eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : N' ⧸ f.range →ₗ[R] N'' := g.range.subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑(f.range.quotEquivOfEq g.ker ⋯)
exact1 : Function.Exact ⇑(rTensor M f) ⇑(rTensor M π)
⊢ Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)

Tactic:
rw [show g = ι.comp π from rfl, rTensor_comp]
    exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

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

Goal state before:
pp: ι : 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✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
z : ℤ
i : ι
x : G i
⊢ (g i) (x ^ z) = (g i) x ^ z

Tactic:
map_zpow₀ (g i)

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 ι
t : Finset κ
f : ι → κ → M
⊢ (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ t, ∑ j ∈ s, f j i = (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ s, ∑ j ∈ t, f i j

Tactic:
sum_comm

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ y ∈ s, ∑ x ∈ t, f y x = (↑(#t))⁻¹ • (↑(#s))⁻¹ • ∑ i ∈ s, ∑ j ∈ t, f i j
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
by_cases hj₁ : j = 0

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ f a [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum] at *

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → ↑(f a) = 0
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = ↑(f a)
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
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
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m +
      (∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
          f m • ∑ i ∈ range (m + 1), g i -
        ∑ x ∈ Ico (m + 1) n, f x • ∑ i ∈ range x, 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:
h₁

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
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m +
      (∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
          f m • ∑ i ∈ range (m + 1), g i -
        ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), 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: case refine_3
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
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
s : S
n : N
e' : g₁ n = g₂ n
⊢ s • g₁ n = g₂ (s • n)

Tactic:
g₂.map_smul,

Goal state after:
case refine_3
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
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
s : S
n : N
e' : g₁ n = g₂ n
⊢ s • g₁ n = s • g₂ n
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ b ∈ s

Tactic:
by rwa [(Sym.mem_replicate.1 hb).2]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)

Tactic:
rw [Finset.offDiag_filter_lt_eq_filter_le]
  conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]
  refine (Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm
  all_goals aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s

Tactic:
by
  ext y
  simp only [mem_map]
  constructor <;>
    · rintro ⟨w, hw, rfl⟩
      exact ⟨w, hw, by simp [hw, 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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
⊢ IsBaseChange T (↑R g ∘ₗ f)

Tactic:
by
  apply IsBaseChange.of_lift_unique
  intro Q _ _ _ _ i
  let := Module.compHom Q (algebraMap S T)
  have : IsScalarTower S T Q :=
    ⟨fun x y z => by
      rw [Algebra.smul_def, mul_smul]
      rfl⟩
  have : IsScalarTower R S Q := IsScalarTower.to₁₂₄ _ _ T _
  refine
    ⟨hg.lift (hf.lift i), by
      ext
      simp [IsBaseChange.lift_eq], ?_⟩
  rintro g' (e : _ = _)
  refine hg.algHom_ext' _ _ (hf.algHom_ext' _ _ ?_)
  rw [IsBaseChange.lift_comp, IsBaseChange.lift_comp, ← e]
  ext
  rfl

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

Goal state before:
pp: α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
⊢ map Subtype.val (pmap Subtype.mk s h) = s

Tactic:
by
  cases s; rfl

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

Goal state before:
pp: α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
⊢ map Subtype.val (s.attachWith h) = s

Tactic:
by
  cases s; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
sym : Std.Symm r
f : α → β
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ map f z ∈ fromRel sym

Tactic:
by
  cases z
  simp

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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := Module.restrictScalars R S Q
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ↑R r ∘ₗ f
q : O →ₗ[T] Q := hc.lift r'
q' : O →ₗ[T] Q
hq' : ↑S q' ∘ₗ h = r
⊢ q' = q

Tactic:
apply hc.algHom_ext'

Goal state after:
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝¹ : Module R Q := ⋯
this✝ : IsScalarTower R S Q
this : IsScalarTower R T Q
r' : M →ₗ[R] Q := ⋯
q : O →ₗ[T] Q := ⋯
q' : O →ₗ[T] Q
hq' : ↑S q' ∘ₗ h = r
⊢ ↑R q' ∘ₗ ↑R h ∘ₗ f = ↑R q ∘ₗ ↑R h ∘ₗ f