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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
r : R
r0 : r ≠ 0
⊢ n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
_

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
r : R
r0 : r ≠ 0
a✝ : n ≤ p.natDegree
⊢ (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
⊢ g.natDegree ≤ p.natDegree →
    (φ f).natDegree = fu f.natDegree → (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
_

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
⊢ (φ f).natDegree = fu f.natDegree → (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
d : WithBot ℕ
hd : ∀ k ∈ s, (f k).degree = d
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
obtain _ | d := d
  · simp_all [WithBot.none_eq_bot]
  · replace hd k (hk : k ∈ s) : (f k).natDegree = d := natDegree_eq_of_degree_eq_some <| hd k hk
    suffices (∑ k ∈ s, f k).natDegree = d by simp_all [leadingCoeff]
    apply natDegree_eq_of_le_of_coeff_ne_zero
    · aesop (add safe natDegree_sum_le_of_forall_le)
    · simp_all [leadingCoeff]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
h✝ : ¬Function.HasFiniteMulSupport f
⊢ Monic 1

Tactic:
exact monic_one

Goal state after:
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 * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun f ↦ f.natDegree) t).sum

Tactic:
rw [Multiset.sum_cons, Polynomial.natDegree_mul', ih]

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
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0

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
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:
rwa [Polynomial.leadingCoeff_multiset_prod']

Goal state after:
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.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n

Tactic:
convert! geom_sum₂_mul_of_ge hxy n using 3

Goal state after:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)
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
⊢ j ∈ univ → j ≠ i → (C (x j) * X ^ k j).coeff (k i) = 0

Tactic:
_

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
⊢ j ≠ i → (C (x j) * X ^ k j).coeff (k i) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ k ∈ (fun n ↦ X ^ n) ⁻¹' ↑(degreeLT R n)

Tactic:
apply mem_degreeLT.2

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ ((fun n ↦ X ^ n) k).degree < ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ Function.LeftInverse (fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) fun p ↦ ⟨(↑p).eraseLead, ⋯⟩

Tactic:
rintro ⟨p, hp, rfl⟩
    ext1
    simp only
    conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]
    simp [Monic.def.1 hp, add_comm]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬⊤.FG

Tactic:
Submodule.fg_def

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬∃ S, S.Finite ∧ Submodule.span R S = ⊤
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
⊢ x ∉ t → P (Algebra.adjoin R ↑t) → P (Algebra.adjoin R ↑(insert x t))

Tactic:
_

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t✝ : Finset A
x : A
t : Finset A
a✝ : x ∉ t
⊢ P (Algebra.adjoin R ↑t) → P (Algebra.adjoin R ↑(insert x t))
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 g : R[X]
⊢ g ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), g.coeff n ∈ I) → ∀ (n : ℕ), (f • g).coeff n ∈ I

Tactic:
_

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]
hx✝ : 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 mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Tactic:
rintro ⟨p, hpI, hpdeg, rfl⟩
    have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
    refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
    · apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]
    · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
by
  suffices of R M '' ⋃ f ∈ S, f.coeff.support = ⋃ f ∈ S, of R M '' f.coeff.support by
    rw [this]
    exact support_gen_of_gen hS
  simp only [Set.image_iUnion]

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

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
⊢ v ∈ ⊤ → v ∈ ((aeval f) p).range ⊔ ((aeval f) q).range

Tactic:
_

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
a✝ : v ∈ ⊤
⊢ v ∈ ((aeval f) p).range ⊔ ((aeval f) q).range
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 : σ →₀ ℕ
⊢ m ∈ p.support → (monomial m) (coeff m p) ∈ I

Tactic:
_

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) ∈ I
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 g : MvPolynomial σ R
⊢ g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
    (∀ (m : σ →₀ ℕ), coeff m g ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (f • g) ∈ I

Tactic:
_

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
hx✝ : g ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I)
⊢ (∀ (m : σ →₀ ℕ), coeff m g ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (f • g) ∈ 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 : σ →₀ ℕ
⊢ m ∈ f.support → (monomial m) (coeff m f) ∈ Ideal.map C I

Tactic:
_

Goal state after:
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
⊢ (monomial m) (coeff m f) ∈ Ideal.map C I
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R

Tactic:
cases CharP.char_is_prime_or_zero R p with
  | inl hp => simpa using h p hp
  | inr h => have : CharP R 0 := h ▸ inferInstance; exact CharP.charP_to_charZero R

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
by rw [two_nsmul, add_self_eq_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R 2
inst✝ : NoZeroDivisors R
⊢ Function.Injective fun x ↦ x ^ 2

Tactic:
by
  intro x y h
  rwa [← CharTwo.add_eq_zero, ← add_sq, pow_eq_zero_iff two_ne_zero, CharTwo.add_eq_zero] at h

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

Goal state before:
pp: 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
⊢ x = p ∧ y = p

Tactic:
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;>
      [skip; rw [And.comm]] <;>
      [skip; rw [mul_comm] at h pdvdxy] <;>
      apply this <;>
      assumption

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

Goal state before:
pp: p : ℕ
pp : Prime p
m i : ℕ
⊢ (∃ i_1, i_1 ≤ m ∧ Associated i (p ^ i_1)) ↔ ∃ k, k ≤ m ∧ i = p ^ k

Tactic:
associated_eq_eq

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

Goal state before:
pp: A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
⊢ Injective ⇑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))

Tactic:
by
  rintro ⟨a⟩ ⟨b⟩ hab
  replace hab := Quotient.eq.mp hab
  rw [← map_sub] at hab
  exact Quotient.eq.mpr hab

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

Goal state before:
pp: case cons.mp.inl
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
exact ⟨[], y :: ys, by simp⟩

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier

Tactic:
simp only [Subalgebra.mem_carrier, ← (@Algebra.gi R A _ _ _).l_sup_u _ _] at *

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
a : A
ha : a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
⊢ star a ∈ Algebra.adjoin R (↑S ⊔ ↑(star S))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.length + is.length)! * (ts.length + is.length).succ

Tactic:
← IH1,

Goal state after:
α : Type u_1
t : α
ts is : List α
IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!
IH2 : (is.permutationsAux []).length + 1 = is.length !
IH1 :
  (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ
⊢ is.length * is.length ! + (ts.permutationsAux (t :: is)).length + is.length ! =
    (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun a ↦ (b' :: c :: a) :: map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
change (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++
      map (cons c) (permutations'Aux _ a))) ~ _

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun a ↦ [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ l' : List α
⊢ l' ∈ l✝.permutations' →
    flatMap (permutations'Aux y✝) (permutations'Aux x✝ l') ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ l')

Tactic:
_

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ l' : List α
a✝ : l' ∈ l✝.permutations'
⊢ flatMap (permutations'Aux y✝) (permutations'Aux x✝ l') ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ l')
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ False ∨ minimalPeriod f x = p ∧ ¬minimalPeriod f x = 1

Tactic:
false_or,

Goal state after:
α : Type u_1
f : α → α
x : α
p : ℕ
hp : Fact (Nat.Prime p)
⊢ minimalPeriod f x = p ↔ minimalPeriod f x = p ∧ ¬minimalPeriod f x = 1
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case refine_1
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing B
inst✝³ : StarModule R A
s : Set A
inst✝² : FunLike F (↥(adjoin R s)) B
inst✝¹ : AlgHomClass F R (↥(adjoin R s)) B
inst✝ : StarHomClass F (↥(adjoin R s)) B
f g : F
h : ∀ (x : ↥(adjoin R s)), ↑x ∈ s → f x = g x
a : ↥(adjoin R s)
x : A
hx : x ∈ s
⊢ f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩

Tactic:
exact h ⟨x, subset_adjoin R s hx⟩ hx

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.next a ha = l[(idxOf a l + 1) % l.length]

Tactic:
have hl := ne_nil_of_mem ha
  by_cases ha' : a ∈ l.dropLast
  · simp [next, nextOr_eq_getElem_idxOf_succ_of_mem_dropLast ha',
      Nat.mod_eq_of_lt <| succ_idxOf_lt_length_of_mem_dropLast ha']
  grind [dropLast_append_getLast, next_getLast_eq_head_of_notMem_dropLast, Nat.mod_self]

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

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (c :: (s ++ [a])).rotate d = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a :: l₁ ~ b :: l₂
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
⊢ ∀ (hl : m ++ [a] ≠ []), Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl :: (m ++ [a]))

Tactic:
_

Goal state after:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
m : ℕ := (k + 2).minFac
⊢ (k + 2) / (k + 2).minFac < k.succ.succ

Tactic:
decreasing_by exact factors_lemma

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

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ a.val = 0 ↔ a = 0

Tactic:
rw [Fin.ext_iff]
    exact Iff.rfl

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
by
  rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (h • J).relIndex (h • K) = J.relIndex K

Tactic:
by
  rw [pointwise_smul_def K, ← relIndex_comap, pointwise_smul_def,
    comap_map_eq_self_of_injective (by intro a b; simp)]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors

Tactic:
divisors,

Goal state after:
n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ (a + b).val = a.val + b.val - n

Tactic:
by
  rw [val_add_val_of_le h]
  exact eq_tsub_of_add_eq rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mpr
a b : ℕ
hab : a * b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b

Tactic:
mul_ne_zero_iff

Goal state after:
case mpr
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b