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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
Polynomial.leadingCoeff_multiset_prod'

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0

case refine_2.h
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map leadingCoeff t).prod ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f : R[X]
⊢ ∀ (g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
g

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
⊢ f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f : R[X]
⊢ ∀ (g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
g

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
⊢ f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
obtain hl | hl := le_total f.natDegree g.natDegree

Goal state after:
case mpr.inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

case mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
rintro ⟨c₁, c₂, hmul, hadd⟩
      refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
      · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
        ring
      · simp

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

Goal state before:
pp: case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ x j * (X ^ k j).coeff (k i) = 0

Tactic:
coeff_X_pow,

Goal state after:
case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j✝ : Fin (n + 1)
i : Fin n
hij : i.castSucc < j✝
hj : ¬∃ j₀, j₀.castSucc = j✝
j : Fin n
a✝ : j ∈ univ
hji : j ≠ i
⊢ (x j * if k i = k j then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (p - q).Monic

Tactic:
have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
  rw [sub_eq_add_neg]
  apply Monic.add_of_right this
  rwa [degree_neg]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.support = 1 ↔ ∃ k x, ∃ (_ : x ≠ 0), f = C x * X ^ k

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
    exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩
  · rintro ⟨k, x, hx, rfl⟩
    rw [support_C_mul_X_pow k hx, card_singleton]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : p.degree < ↑p.natDegree
⊢ False

Tactic:
degree_eq_natDegree hp_zero,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : ↑p.natDegree < ↑p.natDegree
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (n : ℕ), x.coeff n ∈ I

pp: case mp.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

pp: case mp.refine_3
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]),
    x ∈ Submodule.span R[X] (⇑C '' ↑I) →
      y ∈ Submodule.span R[X] (⇑C '' ↑I) →
        (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
· intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [h]

Goal state after:
case mp.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

case mp.refine_3
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]),
    x ∈ Submodule.span R[X] (⇑C '' ↑I) →
      y ∈ Submodule.span R[X] (⇑C '' ↑I) →
        (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f : R[X]
⊢ ∀ x ∈ Submodule.span R[X] (⇑C '' ↑I), (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (f • x).coeff n ∈ I

Tactic:
g

Goal state after:
case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf : f✝ ∈ map C I
f g : R[X]
⊢ g ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), g.coeff n ∈ I) → ∀ (n : ℕ), (f • g).coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f : R[X]
⊢ ∀ {y : R[X]}, f * y ∈ map C P → f ∈ map C P ∨ y ∈ map C P

Tactic:
g

Goal state after:
case mem_or_mem'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ f * g ∈ map C P → f ∈ map C P ∨ g ∈ map C P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ IsUnit (constantCoeff (C r))

pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
h : IsUnit (C r)
⊢ Type ?u.42

Tactic:
exact h.map _

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

Tactic:
exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) m

Tactic:
exact ⟨FreeAlgebra.ι R ⟨m, hm⟩, FreeAlgebra.lift_ι_apply _ _⟩

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

Goal state before:
pp: case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
⊢ ∀ x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I),
    (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (f • x) ∈ I

Tactic:
g

Goal state after:
case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f g : MvPolynomial σ R
⊢ g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
    (∀ (m : σ →₀ ℕ), coeff m g ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (f • g) ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a

Tactic:
by
  rw [ModEq, eq_comm]
  simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]

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

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ d - c

Tactic:
by
    rw [this]
    exact Int.dvd_sub h₂.dvd h₁.dvd

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ m.toList.permutations.Disjoint n.toList.permutations ↔ ¬m = n

Tactic:
List.disjoint_iff_ne

Goal state after:
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = I ⊔ J

Tactic:
by
  ext x
  simp only [mem_comap, mem_quotient_iff_mem_sup, sup_comm]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m.gcd n) x

Tactic:
Nat.gcd_rec

Goal state after:
case refine_2
α : Type u_1
f : α → α
x : α
m✝ n✝ m n : ℕ
x✝ : 0 < m
ih : IsPeriodicPt f (n % m) x → IsPeriodicPt f m x → IsPeriodicPt f ((n % m).gcd m) x
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f ((n % m).gcd m) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ ↑n • a = a ↔ ↑(period g a) ∣ ↑n

Tactic:
| =>

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ ↑n • a = a ↔ ↑(period g a) ∣ ↑n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ n • a = a ↔ ↑(period g a) ∣ ↑n

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ n • a = a ↔ period g a ∣ n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (-↑(n + 1)) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)

Tactic:
| =>

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (-↑(n + 1)) • a = a ↔ ↑(period g a) ∣ -↑(n + 1)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ ↑(period g a) ∣ ↑(n + 1)

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
n : ℕ
⊢ g ^ (n + 1) • a = a ↔ period g a ∣ n + 1
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f✝ : α → α
x : α
g : α → α
h : Function.Commute f✝ g
hco : (minimalPeriod f✝ x).Coprime (minimalPeriod g x)
f : α → α
⊢ ∀ {g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
g

Goal state after:
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h : Function.Commute f✝ g✝
hco : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
⊢ Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a d : α
ha : a ∈ [].dropLast
⊢ some ([].nextOr a d) = [][idxOf a [] + 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d : α
ha : a ∈ [].dropLast
⊢ some ([].nextOr a d) = [][idxOf a [] + 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a d head : α
ha : a ∈ [head].dropLast
⊢ some ([head].nextOr a d) = [head][idxOf a [head] + 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d head : α
ha : a ∈ [head].dropLast
⊢ some ([head].nextOr a d) = [head][idxOf a [head] + 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
⊢ some ((x :: y :: tail).nextOr a d) = (x :: y :: tail)[idxOf a (x :: y :: tail) + 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a d x y : α
tail : List α
ha : a ∈ (x :: y :: tail).dropLast
⊢ some ((x :: y :: tail).nextOr a d) = (x :: y :: tail)[idxOf a (x :: y :: tail) + 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d : α
hl : [] ≠ []
h : [].getLast hl ∉ [].dropLast
⊢ [].nextOr ([].getLast hl) d = d

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
d : α
hl : [] ≠ []
h : [].getLast hl ∉ [].dropLast
⊢ [].nextOr ([].getLast hl) d = d
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d head✝ : α
hl : [head✝] ≠ []
h : [head✝].getLast hl ∉ [head✝].dropLast
⊢ [head✝].nextOr ([head✝].getLast hl) d = d

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
d head✝ : α
hl : [head✝] ≠ []
h : [head✝].getLast hl ∉ [head✝].dropLast
⊢ [head✝].nextOr ([head✝].getLast hl) d = d
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (x :: y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
d x y : α
tail : List α
hl : x :: y :: tail ≠ []
h : (x :: y :: tail).getLast hl ∉ (x :: y :: tail).dropLast
⊢ (x :: y :: tail).nextOr ((x :: y :: tail).getLast hl) d = d
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ []
ha₀ : a ≠ [].head ⋯
⊢ some ([].prev a ha) = [][idxOf a [] - 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ []
ha₀ : a ≠ [].head ⋯
⊢ some ([].prev a ha) = [][idxOf a [] - 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a head✝ : α
ha : a ∈ [head✝]
ha₀ : a ≠ [head✝].head ⋯
⊢ some ([head✝].prev a ha) = [head✝][idxOf a [head✝] - 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a head✝ : α
ha : a ∈ [head✝]
ha₀ : a ≠ [head✝].head ⋯
⊢ some ([head✝].prev a ha) = [head✝][idxOf a [head✝] - 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
⊢ some ((x :: y :: tail).prev a ha) = (x :: y :: tail)[idxOf a (x :: y :: tail) - 1]?

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a x y : α
tail : List α
ha : a ∈ x :: y :: tail
ha₀ : a ≠ (x :: y :: tail).head ⋯
⊢ some ((x :: y :: tail).prev a ha) = (x :: y :: tail)[idxOf a (x :: y :: tail) - 1]?
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (pmap l.reverse.prev l.reverse ⋯)[l.length - 1 - k] = (l.rotate 1)[k]

pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length

Tactic:
· simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
    rw [getElem_eq_getElem_reverse]
    · simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
⊢ ∀ g ∈ H, g • s ⊆ s

Tactic:
g

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
⊢ g ∈ H → g • s ⊆ s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s

Tactic:
g

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
⊢ g ∈ H → g ∈ stabilizer G s
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rintro ⟨p, k, hp', hk', rfl⟩
    refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
    · calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
a : α
l : List α
h✝ : Chain r ↑l → ↑l = Cycle.nil
h : Chain r ↑(a :: l)
⊢ ↑(a :: l) = Cycle.nil

Tactic:
| cons a l h =>

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
h : Chain r s
⊢ s = Cycle.nil

Tactic:
induction s with
  | nil => rfl
  | cons a l h =>
    have ha : a ∈ a :: l := mem_cons_self
    exact (irrefl_of r a <| chain_iff_pairwise.1 h a ha a ha).elim

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 0 → Prime p

Tactic:
| =>

Goal state after:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 0 → Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 1 → Prime p

Tactic:
| =>

Goal state after:
n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 1 → Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ (k + 2).primeFactorsList → Prime p

Tactic:
| =>

Goal state after:
n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ (k + 2).primeFactorsList → Prime p
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ Fintype.card ((g : G) × ↑(fixedBy X g)) = Fintype.card (Quotient (orbitRel G X) × G)

Tactic:
Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup G X)

Goal state after:
G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ Fintype.card (Quotient (orbitRel G X) × G) = Fintype.card (Quotient (orbitRel G X) × G)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 0)

Tactic:
| =>

Goal state after:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 0)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 1)

Tactic:
| =>

Goal state after:
n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 1)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k : ℕ
⊢ ∀ {a : ℕ},
    (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)

Tactic:
| =>

Goal state after:
n k : ℕ
⊢ ∀ {a : ℕ},
    (∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).primeFactorsList)