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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ a ∈ image k univ

Tactic:
mem_image,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1 ∈ univ, k a_1 = a
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
by
  cases n; · simp
  simp only [Nat.add_sub_cancel]
  rw [← Finset.sum_flip]
  refine Finset.sum_congr rfl fun i hi => ?_
  simpa [Nat.sub_sub_self (Nat.succ_le_succ_iff.mp (Finset.mem_range.mp hi))] using! h.pow_pow _ _

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
⊢ r ^ 0 - r ∣ r ^ 0 ^ b - r

Tactic:
zero_pow hb₀

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
⊢ r ^ 0 - r ∣ r ^ 0 - r
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree = s.sup fun i ↦ (f i).degree

Tactic:
apply le_antisymm
  · exact (degree_sum_le s _).trans <| Finset.sup_le fun i hi ↦ (degree_smul_le _ _).trans <|
      degree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).degree) hi
  · apply Finset.sup_le
    intro i hi
    by_cases hf : f i = 0
    · simp [hf]
    rw [degree_eq_natDegree hf]
    apply le_degree_of_ne_zero
    rw [finsetSum_coeff]
    conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
    intro H
    exact hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

Goal state after:
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 = 0
⊢ q = 0

Tactic:
replace hp := congr_arg (· * C ↑h.unit⁻¹) hp

Goal state after:
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 * C ↑h.unit⁻¹
⊢ q = 0
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⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
⊢ ∃ p' ∈ s, p.degree ≤ p'.degree

Tactic:
by
  by_contra! h
  by_cases hp_zero : p = 0
  · rw [hp_zero, degree_zero] at h
    rcases hs with ⟨x, hx⟩
    exact not_lt_bot (h x hx)
  · have : p ∈ degreeLT R (natDegree p) := by
      refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
      rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]
      exact lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree
    rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left✝ : p' ∈ s
hp'max : ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
exact ⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Submonoid

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup α
inst✝ : DistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (addSubmonoid M α).carrier
x✝ : M
⊢ -(x✝ • x✝¹) = -x✝¹

Tactic:
ha

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddGroup α
inst✝ : DistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (addSubmonoid M α).carrier
x✝ : M
⊢ -x✝¹ = -x✝¹
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
⊢ a ∈ I.leadingCoeff → ∀ s ∈ J.leadingCoeff, a * s ∈ (I * J).leadingCoeff

Tactic:
ha

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
I J : Ideal R[X]
a : R
ha : a ∈ I.leadingCoeff
⊢ ∀ s ∈ J.leadingCoeff, a * s ∈ (I * J).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
obtain hi | hj : i < m ∨ j < n := by
          lia

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

case inr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

Tactic:
rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, SetLike.mem_coe, hs]

Goal state after:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ x ∈ ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
⊢ I ≤ Submodule.span R[X] ↑s

Tactic:
have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl
        rw [this]
        intro p hp
        generalize hn : p.natDegree = k
        induction k using Nat.strong_induction_on generalizing p with | _ k ih
        rcases le_or_gt k N with h | h
        · subst k
          refine hs2 ⟨Polynomial.mem_degreeLE.2
            (le_trans Polynomial.degree_le_natDegree <| WithBot.coe_le_coe.2 h), hp⟩
        · have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h
          have : (0 : R) ≠ 1 := by
            intro h
            apply hp0
            ext i
            refine (mul_one _).symm.trans ?_
            rw [← h, mul_zero]
            rfl
          have : Nontrivial R := ⟨⟨0, 1, this⟩⟩
          have : p.leadingCoeff ∈ I.leadingCoeffNth N := by
            rw [HN]
            exact hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
          rw [I.mem_leadingCoeffNth] at this
          rcases this with ⟨q, hq, hdq, hlqp⟩
          have hq0 : q ≠ 0 := by
            intro H
            rw [← Polynomial.leadingCoeff_eq_zero] at H
            rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
            exact hp0 H
          have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
            rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
            · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
              rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
              · refine le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
            rw [Polynomial.leadingCoeff_X_pow, mul_one]
            exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
          have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
            rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
          have := Polynomial.degree_sub_lt_left h1 hp0 h2
          rw [Polynomial.degree_eq_natDegree hp0] at this
          rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]
          convert! (Ideal.span ↑s).add_mem _ ((Ideal.span (s : Set R[X])).mul_mem_right _ _)
          · by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
            · rw [hpq]
              exact Ideal.zero_mem _
            refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
          exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩

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

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

Tactic:
obtain hc | rfl | hc := lt_trichotomy c 0
  · rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
  · simp only [Int.zero_mul, ModEq.rfl]
  · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ ker (Quotient.mk I) ↔ x✝ ∈ I

Tactic:
rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
algHom : Unitization R ↥s →ₐ[R] ↥(Algebra.adjoin R ↑s) := (unitization s).codRestrict (Algebra.adjoin R ↑s) ⋯
x : ↥(Algebra.adjoin R ↑s)
a : Unitization R ↥s
ha : (unitization s).toRingHom a = ↑x
⊢ ∃ a, algHom a = x

Tactic:
exact ⟨a, Subtype.ext ha⟩

Goal state after:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
a b : R
⊢ a + (a + b) = b

Tactic:
by
  rw [← add_assoc, add_self_eq_zero, zero_add]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
starAlgHom : Unitization R ↥s →⋆ₐ[R] ↥(StarAlgebra.adjoin R ↑s) :=
  (unitization s).codRestrict (StarAlgebra.adjoin R ↑s) ⋯
x : ↥(StarAlgebra.adjoin R ↑s)
a : Unitization R ↥s
ha : (↑(unitization s)).toRingHom a = ↑x
⊢ ∃ a, starAlgHom a = x

Tactic:
exact ⟨a, Subtype.ext ha⟩

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

Goal state before:
pp: case mpr
α : 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
h : ¬m = n
a : List α
⊢ a ~ m.toList → ∀ (b : List α), b ~ n.toList → a ≠ b

Tactic:
ha

Goal state after:
case mpr
α : 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
h : ¬m = n
a : List α
ha : a ~ m.toList
⊢ ∀ (b : List α), b ~ n.toList → a ≠ b
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J) = RingHom.id (R ⧸ I ⊔ J)

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    (RingHom.id (R ⧸ I ⊔ J)).comp (Ideal.Quotient.mk (I ⊔ J))
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    (RingHom.id (R ⧸ I ⊔ J)).comp (Ideal.Quotient.mk (I ⊔ J))

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ ((quotQuotToQuotSup I J).comp (liftSupQuotQuotMk I J)).comp (Ideal.Quotient.mk (I ⊔ J)) =
    (RingHom.id (R ⧸ I ⊔ J)).comp (Ideal.Quotient.mk (I ⊔ J))
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J) = RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ ((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)) =
    (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ ((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)) =
    (RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    ((RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I)
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    ((RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I)

Tactic:
apply Ideal.Quotient.ringHom_ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (((liftSupQuotQuotMk I J).comp (quotQuotToQuotSup I J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I) =
    ((RingHom.id ((R ⧸ I) ⧸ map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J))).comp
      (Ideal.Quotient.mk I)
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem.mem
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
h : x✝ ∈ s
⊢ p x✝ z ⋯ ⋯

Tactic:
| mem _ h =>

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

Goal state before:
pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
p : l₁ ++ l₂ ~ is
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
exact ((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)

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

Goal state before:
pp: case algebraMap.mem
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
h : x✝ ∈ s
⊢ p x✝ ((algebraMap R A) r) ⋯ ⋯

Tactic:
| mem _ 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) (f^[0] x)

Tactic:
iterate_zero_apply

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) x
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mem
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
h : x✝ ∈ s
⊢ p ⟨x✝, ⋯⟩

Tactic:
| mem _ h =>

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

Goal state before:
pp: α : Type u_1
a b : α
l : List α
⊢ flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)

Tactic:
by
  induction l with
  | nil => exact Perm.swap [a, b] [b, a] []
  | cons c l ih => ?_
  simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]
  apply Perm.swap'
  have :
    ∀ a b,
      (map (cons c) (permutations'Aux a l)).flatMap (permutations'Aux b) ~
        map (cons b ∘ cons c) (permutations'Aux a l) ++
          map (cons c) ((permutations'Aux a l).flatMap (permutations'Aux b)) := by
    intro a' b'
    simp only [flatMap_map, permutations'Aux]
    change (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++
      map (cons c) (permutations'Aux _ a))) ~ _
    refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
    rw [← map_eq_flatMap, ← map_flatMap]
    exact Perm.refl _
  refine (((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm
  rw [← append_assoc, ← append_assoc]
  exact perm_append_comm.append (ih.map _)

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

Goal state before:
pp: α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' l)

Tactic:
refine List.recOn l ?_ ?_ <;> simp only [mk''_eq_coe, coe_nil]

Goal state after:
case refine_1
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive Cycle.nil

case refine_2
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), motive ↑tail → motive ↑(head :: tail)
Module: Mathlib.Data.Nat.Prime.Infinite

Goal state before:
pp: ⊢ ¬BddAbove {p | Prime p}

Tactic:
rw [not_bddAbove_iff]

Goal state after:
⊢ ∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

Tactic:
exact Or.inr rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card G' ∣ Nat.card G

Tactic:
← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) 0 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

pp: case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
· exact Int.cast_zero

Goal state after:
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
⊢ H.index ∣ 2

Tactic:
suffices ∀ b, b ∈ H by simp [(eq_top_iff' _).mpr this]
      exact fun b ↦ (ha b).elim (fun h ↦ by simpa using mul_mem h (inv_mem ha')) id

Goal state after: