mathlib-initiative/mathlib-tactics huggingface dataset:
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
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]

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
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree
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
this : (∑ i, C (x i) * X ^ k i).support = image k univ
⊢ #(image k univ) = n

Tactic:
univ.card_image_of_injective hk,

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
this : (∑ i, C (x i) * X ^ k i).support = image k univ
⊢ #univ = n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n

Tactic:
coeff_restriction

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ p.coeff n = p.coeff n
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case convert_3
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)) = restrictScalars A ⊤

Tactic:
restrictScalars_top,

Goal state after:
case convert_3
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)) = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hzero : f.eraseLead = 0
⊢ f.eraseLead + C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)

Tactic:
hzero,

Goal state after:
case h.inr
R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hzero : f.eraseLead = 0
⊢ 0 + C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
refine le_antisymm le_top ?_
  rw [← hS, adjoin_le_iff]
  intro f hf
  have hincl : of' R M '' f.coeff.support ⊆ ⋃ g ∈ S, of' R M '' g.coeff.support :=
    fun s hs ↦ Set.mem_iUnion₂.2 ⟨f, hf, hs⟩
  exact adjoin_mono hincl (mem_adjoin_support f)

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
exact support_gen_of_gen hS

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 = ⊤
this : ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support
⊢ adjoin R (⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support) = ⊤

Tactic:
exact support_gen_of_gen hS

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

Goal state before:
pp: case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S

Tactic:
· 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.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inl
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x = n
⊢ i x ∈ M'

Tactic:
rw [hx, ← hb, piEquiv_apply_apply]
        refine Submodule.sum_mem _ fun j _ ↦ ?_
        let b' : A := ⟨b j, Subring.subset_closure (by simp)⟩
        rw [show b j • mj j = b' • mj j from rfl]
        exact smul_mem _ _ (subset_span (by simp))

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ i (nj j) ∈ M'

Tactic:
← hc,

Goal state after:
case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ ((Module.piEquiv (Fin k) R M) mj) (c j) ∈ M'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ ∀ b ∈ F.coeff.support,
    (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i)) b ≤ m * n

Tactic:
intro d hd

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i)) d ≤ m * n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝³ : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝² : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝¹ : IsNoetherianRing ↥A
this✝ : Module.Finite ↥A ↥M'
x✝ : ↥M'
x : M
hx : x ∈ M'
this : x ∈ ((↑↥A f).domRestrict N').range
⊢ ∃ a, ((↑↥A f).restrict ⋯) a = ⟨x, hx⟩

Tactic:
by
    obtain ⟨a, ha⟩ := this
    exact ⟨a, Subtype.val_injective ha⟩

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

Goal state before:
pp: a b : ℤ
hb : 0 < b
⊢ a % b < b

Tactic:
have : a % b < |b| := emod_lt_abs _ (ne_of_gt hb)
      rwa [abs_of_pos hb] at this

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)

Tactic:
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]

Goal state after:
case mp
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : y ∈ ker f
hy : (Quotient.mk I) y = x
⊢ ∃ x ∈ ker f, (Quotient.mk I) x = (Quotient.mk I) y
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
⊢ ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0

Tactic:
rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, (Quotient.mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) e = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: 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) ⋯
⊢ Function.Bijective ⇑algHom

Tactic:
by
    refine ⟨?_, fun x ↦ ?_⟩
    · have := AlgHomClass.unitization_injective s h1
        ((Subalgebra.val _).comp algHom) fun _ ↦ by simp [algHom]
      rw [AlgHom.coe_comp] at this
      exact this.of_comp
    · obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) :=
        (unitization_range s).ge x.property
      exact ⟨a, Subtype.ext ha⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd

Tactic:
by
  induction ys generalizing f with
  | nil => simp
  | cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]

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

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

Tactic:
comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective,

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ J ⊔ comap (Ideal.Quotient.mk I) ⊥ = I ⊔ J
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd

Tactic:
rw [map_permutationsAux2' id, map_id, map_id]
  · rfl
  simp

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x

Tactic:
simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]

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

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n)

Tactic:
Nat.div_mul_cancel (gcd_dvd_right _ _),

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
ts : List α
⊢ ts.permutations ~ ts.permutations'

Tactic:
obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩

Goal state after:
α : Type u_1
ts : List α
n : ℕ
h : ts.length < n
⊢ ts.permutations ~ ts.permutations'
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
⊢ (a ∈ S ↔ b ∈ S) → ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S

Tactic:
by intros; split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ¬IsPrimePow 0

Tactic:
simp only [isPrimePow_def, not_exists, not_and', and_imp]

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦l⟧

Tactic:
rcases l with - | ⟨a, l⟩
    · rfl
    · simp [← concat_eq_append, ← map_concat, List.isChain_cons_map f]

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

Goal state before:
pp: case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList

Tactic:
apply sublist_of_subperm_of_pairwise _
    (primeFactorsList_sorted _).pairwise (primeFactorsList_sorted _).pairwise

Goal state after:
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+~ ((hn + 1) * k).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = ((a + 1 + 1).primeFactorsList ++ b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,

Goal state after:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = b.primeFactorsList.prod
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a + b).cast = a.cast + b.cast

Tactic:
by
  cases n
  · apply Int.cast_add
  symm
  dsimp [ZMod, ZMod.cast, ZMod.val]
  rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
    @CharP.cast_eq_zero_iff R _ m]
  exact h.trans (Nat.dvd_sub_mod _)

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

Goal state before:
pp: case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
apply Fin.ext

Goal state after:
case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ↑⟨x, hx⟩ = ↑⟨y, hy⟩
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by
  rw [cons_eq_insert, insert_self_properDivisors h]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: ⊢ {d ∈ ∅ | d ∣ 1} = ∅

Tactic:
filter_empty

Goal state after:
⊢ ∅ = ∅
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∣ n ∧ 1 < n ↔ 1 < n

Tactic:
and_iff_right (one_dvd _)

Goal state after:
n : ℕ
⊢ 1 < n ↔ 1 < n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

Tactic:
rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
    refine fun hn hx => h.not_ge ?_
    simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Tactic:
refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)

Tactic:
simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
  rintro n han _ha hn hbn _hb -
  exact hn.ne_one (Nat.eq_one_of_dvd_coprimes hab han hbn)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n1 * n2

Tactic:
← hn

Goal state after:
case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «0»
⊢ -(fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

Tactic:
apply Fin.ext

Goal state after:
case «0»
⊢ ↑(-(fun i ↦ i) ⟨0, ⋯⟩) = ↑((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «1»
⊢ -(fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
apply Fin.ext

Goal state after:
case «1»
⊢ ↑(-(fun i ↦ i) ⟨1, ⋯⟩) = ↑((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: case case3
n p p✝ : ℕ
hp✝ : 1 < p✝ ∧ n ≠ 0
h✝ : ¬n % p✝ = 0
⊢ (0, n).snd * p✝ ^ (0, n).fst = n ∧ ¬p✝ ∣ (0, n).snd

Tactic:
simp_all [Nat.dvd_iff_mod_eq_zero]

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

Goal state before:
pp: p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
⊢ p ^ k ∣ n ↔ k ≤ a

Tactic:
by
  subst hab
  cases Nat.lt_or_ge a k with
  | inl hlt =>
    refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd
    exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd
  | inr hle =>
    refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle
    exact Nat.pow_dvd_pow p hle

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]

Goal state after:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2

Tactic:
intro d hd

Goal state after:
case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
hd : d ∈ (b + 2).digits n
⊢ d < b + 2