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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ q = 0

Tactic:
Monic.mul_left_eq_zero_iff

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q = 0
⊢ q = 0

case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ (p * C ↑h.unit⁻¹).Monic
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Tactic:
mul_sum,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + ∑ i ∈ range n, y * (x ^ i * y ^ (n - 1 - i))
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3

Tactic:
· rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩
    exact card_support_trinomial hkm hmn hx hy hz

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

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

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine
      ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl
  · rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩
    exact card_support_trinomial hkm hmn hx hy hz

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
⊢ Submodule.span R s ≠ ⊤

Tactic:
contra

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
⊢ X ^ (n + 1) ∈ degreeLE R ↑n

Tactic:
contra

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : ⊤ ≤ degreeLE R ↑n
⊢ X ^ (n + 1) ∈ degreeLE R ↑n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (MvPolynomial.aeval fun s ↦ (of R M) ↑s) (P₁ * P₂) = (of R M) (m₁ * m₂)

Tactic:
by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) (P₁ * P₂) = (of R M) (m₁ * m₂)

Tactic:
by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ IsIdempotentElem (toSubmodule S)

Tactic:
apply le_antisymm
  · refine (mul_toSubmodule_le _ _).trans_eq ?_
    rw [sup_idem]
  · intro x hx1
    rw [← mul_one x]
    exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T = toSubmodule (S ⊔ T)

Tactic:
by
  refine le_antisymm (mul_toSubmodule_le _ _) ?_
  rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
  refine
    Algebra.adjoin_induction (fun x hx => ?_) (fun r => ?_) (fun _ _ _ _ => Submodule.add_mem _)
      (fun x y _ _ hx hy => ?_) hx
  · rcases hx with hxS | hxT
    · rw [← mul_one x]
      exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
    · rw [← one_mul x]
      exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
  · rw [← one_mul (algebraMap _ _ _)]
    exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)
  have := Submodule.mul_mem_mul hx hy
  rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
    isIdempotentElem_toSubmodule, mul_comm T.toSubmodule, ← mul_assoc,
    isIdempotentElem_toSubmodule] at this

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

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ p.support
⊢ (monomial m) (coeff m p) ∈ I

Tactic:
← mul_one (coeff m p),

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ p.support
⊢ (monomial m) (coeff m p * 1) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : ∀ (m : σ →₀ ℕ), coeff m f ∈ I
m : σ →₀ ℕ
a✝ : m ∈ f.support
⊢ coeff m f ∈ I

Tactic:
exact hf m

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

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

Tactic:
rw [← modEq_add_modulus_mul_iff, sub_add_cancel]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
by
  refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩
  rw [hf] at h
  simp at h

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x = p ∧ y = p

Tactic:
And.comm

Goal state after:
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2

Tactic:
let a := n + 2

Goal state after:
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
⊢ Finset (List α)

Tactic:
refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
⊢ (∀ a ∈ univSubsets, a.val.lists.Nodup) ∧
    Multiset.Pairwise (Function.onFun _root_.Disjoint fun s ↦ s.val.lists) univSubsets
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Fintype α
⊢ ∀ (x : List α),
    (x ∈
        let univSubsets := Finset.univ.powerset.val;
        let allPerms := univSubsets.bind fun s ↦ s.val.lists;
        { val := allPerms, nodup := ⋯ }) ↔
      x.Nodup

Tactic:
intro l
    simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset,
      Finset.subset_univ, Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]
    constructor
    · intro h
      rcases h with ⟨f, hf⟩
      convert! f.nodup
      rw [hf]
      rfl
    · intro h
      exact CanLift.prf _ h

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
h : x ∈ periodicPts f
⊢ x ∈ range f

Tactic:
rw [mem_periodicPts] at h

Goal state after:
α : Type u_1
f : α → α
x : α
h : ∃ n > 0, IsPeriodicPt f n x
⊢ x ∈ range f
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : m < minimalPeriod f x
hmn : f^[m] x = f^[n] x
⊢ m ≤ n

Tactic:
by
  by_contra! hmn'
  rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn
  exact ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
    (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
      (minimalPeriod_pos_iff_mem_periodicPts.1 hm.pos) hmn)).trans (Nat.sub_le m n)).not_gt hm

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem.star
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b z : A
hz : z ∈ s
x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p x✝ z hx✝ ⋯
⊢ p (star x✝) z ⋯ ⋯

Tactic:
| star _ _ h =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case algebraMap.star
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
r : R
x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p x✝ ((algebraMap R A) r) hx✝ ⋯
⊢ p (star x✝) ((algebraMap R A) r) ⋯ ⋯

Tactic:
| star _ _ h =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case star
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (star x) y ⋯ hy
star_right : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (star y) hx ⋯
a b : A
ha : a ∈ adjoin R s
x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p a x✝ ha hx✝
⊢ p a (star x✝) ha ⋯

Tactic:
| star _ _ h =>

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

Goal state before:
pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) x

Tactic:
← @iterate_minimalPeriod α f x

Goal state after:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[minimalPeriod f x] x)
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case star
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
p : ↥(adjoin R s) → Prop
a : ↥(adjoin R s)
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
star : ∀ (x : ↥(adjoin R s)), p x → p (Star.star x)
b x✝ : A
hx✝ : x✝ ∈ adjoin R s
h : p ⟨x✝, hx✝⟩
⊢ p ⟨Star.star x✝, ⋯⟩

Tactic:
| star _ _ h =>

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ k = k.succ

Tactic:
← @Fin.mk.inj_iff _ _ _ kl k1l

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ ⟨k, kl⟩ = ⟨k + 1, k1l⟩
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
⊢ False

Tactic:
have hl : as.length = bs.length := (ha.trans hb.symm).length_eq

Goal state after:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
hl : as.length = bs.length
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
⊢ ↑[[]] = {[]}

Tactic:
Multiset.coe_singleton

Goal state after:
α : Type u_1
⊢ {[]} = {[]}
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ p ∈ L

Tactic:
(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
x : M
hx1 : x ∈ L
hx2 : p ∣ x
⊢ x ∈ L
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
⊢ ∀ (a b : G), (leftRel H) a b → ⟦a⁻¹ • x⟧ = ⟦b⁻¹ • x⟧

Tactic:
by
    intro g₁ g₂ h
    rw [leftRel_eq] at h
    rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]
    exact ⟨⟨_, h⟩, by simp [mul_smul]⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
y : orbitRel.Quotient (↥H) X
⊢ (fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) ((fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) y) = y

Tactic:
cases y using Quotient.inductionOn'

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
a✝ : X
⊢ (fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) (Quotient.mk'' a✝)) =
    Quotient.mk'' a✝
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.gcd b).primeFactors = a.primeFactors ∩ b.primeFactors

Tactic:
grind [dvd_gcd_iff]

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

Goal state before:
pp: case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

pp: case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
· simp at hpa

Goal state after:
case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
n2 : 2 < n
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
by
  obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
  · contradiction
  · contradiction
  · simp [Nat.pow_succ, mul_assoc]
  · exact Or.inr ⟨p, hp, hdvd, hodd⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i

pp: case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
        if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i

Tactic:
· simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, hx, even_two]

Goal state after:
case refine_2
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ ∀ (n : ℕ),
    2 ≤ n →
      (if Even n then ∑ i ∈ range n, x ^ i < 0 else 1 < ∑ i ∈ range n, x ^ i) →
        if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i < 0 else 1 < ∑ i ∈ range (n + 1), x ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Tactic:
apply hlt

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ n - a.val < n

Tactic:
exact Nat.sub_lt (NeZero.pos n) (val_pos.mpr h)

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0

Tactic:
exact div_eq_of_lt h

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
⊢ d < b

Tactic:
by
  rcases b with (_ | _ | b) <;> simp_all [@digits_lt_base' _ m d]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ (b'.digits n).sum [MOD b]

Tactic:
← ofDigits_one

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
· rw [and_imp]
    apply emultiplicity_eq_of_dvd_of_not_dvd

Goal state after:
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i < b

Tactic:
by
  rw [digitsAppend, mem_append, mem_replicate] at hi
  obtain hi | ⟨_, rfl⟩ := hi
  · exact digits_lt_base hb hi
  · linarith

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Tactic:
exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]; assumption

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  rwa [← factorization_le_iff_dvd ?_ hn, factorization_prod_pow_eq_self_of_le_factorization hf]
  refine f.prod_ne_zero_iff.mpr fun _ hp ↦ ?_
  exact pow_ne_zero _ (prime_of_mem_primeFactors <| support_mono hf hp).ne_zero

Goal state after: