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

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

Tactic:
obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

Tactic:
normalize_idem

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (factors a).prod = normalize (factors a).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ p.roots = 0 ↔ p.IsRoot = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eq_zero_of_forall_notMem fun x hx ↦ h ▸ mem_roots hp0 |>.mp hx⟩
  ext a
  simp only [Pi.bot_apply, Prop.bot_eq_false, mem_roots hp0 |>.not.mp <| by simp [h]]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ normalizedFactors b).prod

Tactic:
rw [Multiset.prod_cons]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → x ∣ y

Tactic:
rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
⊢ (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 hy : y = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : y = 0
⊢ (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

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
hy : ¬y = 0
⊢ (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
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂

Tactic:
rw [mul_pow, hη₁, hη₂]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
⊢ p.content ∣ p.coeff n

Tactic:
by_cases h : n ∈ p.support

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∈ p.support
⊢ p.content ∣ p.coeff n

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n
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:
rw [rootSet_def, aroots_C, Multiset.toFinset_zero, Finset.coe_empty]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
x : R
hx : x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R

Tactic:
by
  simp [mem_rootSet', aeval_smul, aeval_eq_zero_of_mem_rootSet hx, (mem_rootSet'.mp hx).1]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
| p.natDegree

Tactic:
p.eq_C_content_mul_primPart,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
| (C p.content * p.primPart).natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
p.eq_C_content_mul_primPart,

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (C p.content * p.primPart * q).content ((C p.content * p.primPart).content * q.content)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mpr
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.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
q : R[X]
a✝ : q.Monic
deg_pos : 0 < q.degree
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
⊢ False

Tactic:
exact deg_pos.ne' <| degree_eq_zero_of_isUnit (h q deg_le dvd)

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]
h0 : ¬C (p * q).content = 0
| p * q

Tactic:
p.eq_C_content_mul_primPart,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C p.content * p.primPart * q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : 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:
rw [← mk_dvd_mk]
    apply dvd_of_mem_factors

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| p * q

Tactic:
p.eq_C_content_mul_primPart,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C p.content * p.primPart * q
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < s.natDegree
⊢ False

Tactic:
rw [sdeg] at hcancel

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
p : R[X]
⊢ p / C a = p * C a⁻¹

Tactic:
simpa [mul_comm] using div_C_mul (q := 1)

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 q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ p ∣ q

Tactic:
p.eq_C_content_mul_primPart,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ C p.content * p.primPart ∣ q
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl
ι✝ : Type u_1
inst✝⁴ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝¹ j : ι✝
h : i✝¹ ≤ j
ι : 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 ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝¹ : WellFoundedLT ι
inst✝ : InverseSystem f
hi : ¬IsMax i
e : PEquivOn f equivSucc (Iic i)
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i✝ : ι
hsj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hj : ¬IsMax i✝
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
cases (succ_eq_succ_iff_of_not_isMax hj hi).mp eq; simp [piEquivSucc]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
p : P
q : Q
⊢ ∃ a, (rTensor Q g) a = p ⊗ₜ[R] q

Tactic:
| tmul p q =>

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

Goal state before:
pp: case zero
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
m : ℕ
inst✝ : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

pp: case prime
σ : Type u
R : Type v
inst✝ : CommSemiring R
p m : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
exacts [ExpChar.zero, ExpChar.prime ‹_›]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx + Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum

Tactic:
Multiset.sum_add,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum + (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal B
⊢ Submodule.restrictScalars R ((lTensor S A) (↑R (Submodule.subtype I))).range =
    Submodule.restrictScalars R (Submodule.restrictScalars S (Ideal.map includeRight I))

Tactic:
exact (I.map_includeRight_eq (R := R) (A := A)).symm

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

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : x ∈ Subalgebra.map includeRight (Subalgebra.center K C)
⊢ x ∈ Subalgebra.center K (B ⊗[K] C)

Tactic:
by
  simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
  obtain ⟨c, hc0, rfl⟩ := hx
  intro bc
  induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b c' => simp [hc0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

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✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ ↑n.succ = ⟦⟨i, x⟩⟧ ^ ↑n * ⟦⟨i, x⟩⟧

Tactic:
simp_rw [HPow.hPow, Pow.pow, map_def, mul_def]

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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n * x⟩⟧
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✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ x ^ ↑n.succ = x ^ ↑n * x

Tactic:
apply DivInvMonoid.zpow_succ'

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✝³ : (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
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ ↑n.succ = ⟦⟨i, x⟩⟧ ^ ↑n * ⟦⟨i, x⟩⟧

Tactic:
simp_rw [HPow.hPow, Pow.pow, map_def, mul_def]

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✝⁴ : 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
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n * x⟩⟧
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✝³ : (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
n : ℕ
i : ι
x : G i
⊢ x ^ ↑n.succ = x ^ ↑n * x

Tactic:
apply DivInvMonoid.zpow_succ'

Goal state after:
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 : ι → M
⊢ #s • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp
  · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
    exact mod_cast hs.card_ne_zero

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = if a ∈ s then ↑(f a) else 0

Tactic:
exact Finset.sum_eq_ite _ hf

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

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 0
⊢ ∑ x ∈ s, ↑(f x) = if a ∈ s then ↑(f a) else 0

Tactic:
exact Finset.sum_eq_ite _ hf

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

Goal state before:
pp: 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}

Tactic:
rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]

Goal state after:
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}) = #⋯.toFinset
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Tactic:
constructor
  · intro h
    exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩
  · rintro ⟨ha, hb⟩
    exact mk_mem_sym2 ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ List.sym (n + 1) (map f (x :: xs)) = map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]
    simp only [map_map, List.sym, map_append, append_cancel_right_eq]
    congr
    ext s
    simp only [Function.comp_apply, Sym.map_cons]

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

Goal state before:
pp: α : Type u_4
z : Sym2 α
⊢ z.toMultiset.card = 2

Tactic:
induction z

Goal state after:
case h
α : Type u_4
x✝ y✝ : α
⊢ s(x✝, y✝).toMultiset.card = 2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_4
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset ↔ x ∈ z

Tactic:
induction z

Goal state after:
case h
α : Type u_4
x x✝ y✝ : α
⊢ x ∈ s(x✝, y✝).toMultiset ↔ x ∈ s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : z.IsDiag
⊢ #z.toFinset = 1

Tactic:
induction z

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ #s(x✝, y✝).toFinset = 1
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = 2

Tactic:
induction z

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬s(x✝, y✝).IsDiag
⊢ #s(x✝, y✝).toFinset = 2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)

Tactic:
simp at hy

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

Goal state before:
pp: case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)

Tactic:
simp at hy

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

Goal state before:
pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ False

Tactic:
simp at hy

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

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

Tactic:
induction z

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ s(x✝, y✝)
⊢ s(a, Mem.other' h) = s(x✝, y✝)
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
induction z

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
ha : a ∈ s(x✝, y✝)
hb : Mem.other' ha ∈ s(x✝, y✝)
⊢ Mem.other' hb = a