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

Goal state before:
pp: 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
⊢ (φ p).natDegree = fu p.natDegree

Tactic:
refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le

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), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

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]),
    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
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ (Polynomial.C.comp C) x = (finSuccEquiv R n) (C x)

Tactic:
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]

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

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

Tactic:
rw [hp₀, hb₀, pow_zero, pow_one, sub_self]

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ 0 ^ a - r ∣ 0
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin D (⇑(algebraMap E F) '' T))

Tactic:
adjoin_restrictScalars C D,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤)) (⇑(algebraMap E F) '' T))
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
Odd.neg_pow h y,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - -y ^ n
⊢ x + y ∣ x ^ n + y ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at s_emp
    rw [s_emp, Submodule.span_empty]
    exact ⟨0, bot_le⟩

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

Goal state before:
pp: x n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
simpa using x.sub_dvd_pow_sub_pow 1 n

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]
⊢ s.Finite → Submodule.span R s ≠ ⊤

Tactic:
hs

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
⊢ Submodule.span R s ≠ ⊤
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Subalgebra.map f (Algebra.adjoin R ↑s) = Subalgebra.map f S

Tactic:
hs

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hs✝ : S.FG
s : Finset A
hs : Algebra.adjoin R ↑s = S
⊢ Subalgebra.map f S = Subalgebra.map f S
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ Algebra.adjoin R ↑s = map f S

pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f

Tactic:
hs

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ map f S = map f S

R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ ↑s ⊆ Set.range ⇑f
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s✝ : Finset ι
f : ι → Ideal R[X]
i : ι
s : Finset ι
hi : i ∉ s
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff →
    ∏ i ∈ insert i s, (f i).leadingCoeff ≤ ((insert i s).prod f).leadingCoeff

Tactic:
hs

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_2
s✝ : Finset ι
f : ι → Ideal R[X]
i : ι
s : Finset ι
hi : i ∉ s
hs : ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
⊢ ∏ i ∈ insert i s, (f i).leadingCoeff ≤ ((insert i s).prod f).leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
⊢ x = 0

Tactic:
refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)

Goal state after:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
Set.preimage_preimage,

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure ((fun x ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s)
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
⊢ x ∈ adjoin R ↑s

Tactic:
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.Algebra.Ring.Subring.MulOpposite

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
Set.preimage_preimage,

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
s : Set Rᵐᵒᵖ
⊢ closure s = closure ((fun x ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S ↔ ∃ n f, Surjective ⇑f

Tactic:
constructor
  · rw [iff_quotient_mvPolynomial']
    rintro ⟨ι, hfintype, f, hsur⟩
    have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
    exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩
  · rintro ⟨n, f, hsur⟩
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R ↑s) = Set.univ

Tactic:
hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
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]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (p * q))) v = 0

Tactic:
by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]

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]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
h_eval₂_qpp' : ((aeval f) (q * (p * p'))) v = 0
⊢ ((aeval f) (q' * (p * q))) v = 0

Tactic:
by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]

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
hx : (Quotient.lift I f H) x = 0
y : R
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)

Tactic:
← hy,

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 : (Quotient.lift I f H) ((Quotient.mk I) y) = 0
hy : (Quotient.mk I) y = x
⊢ x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
h : a / n = b / n
⊢ a ≡ b [ZMOD n] ↔ a = b

Tactic:
grind [ext_ediv_modEq_iff]

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:
← hy,

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
⊢ (Quotient.mk I) y ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card αˣ = Nat.card α - 1

Tactic:
rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R✝ : Type u
S : Type v
F : Type w
inst✝³ : Ring R✝
inst✝² : Semiring S
ι✝ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I J : Ideal R
coprime : IsCoprime I J
f : Fin 2 → Ideal R := ![I, J]
⊢ Pairwise (IsCoprime on f)

Tactic:
by
    intro i j h
    fin_cases i <;> fin_cases j <;> try contradiction
    · assumption
    · exact coprime.symm

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
by
  apply Quotient.ringHom_ext; ext; rfl

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor ⋯

Tactic:
by
  apply Quotient.ringHom_ext; ext; rfl

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

Tactic:
by
  apply Quotient.ringHom_ext; ext; rfl

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

Tactic:
by
  apply Quotient.ringHom_ext; ext; rfl

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
I J : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ ⋯

Tactic:
ext
  rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J) = Ideal.Quotient.mk J

Tactic:
ext
  rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = quotQuotMk I J

Tactic:
ext
  rfl

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
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x * y ∈ star S.carrier

Tactic:
simp only [Set.mem_star, Subalgebra.mem_carrier] at *
        exact (star_mul x y).symm ▸ mul_mem hy hx

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype (I ^ n)) (I ^ (n + 1))

pp: case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∀ (c : ↥(I ^ n) ⧸ I • ⊤),
    ((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?refine_1) c ∈
      Submodule.restrictScalars R (map (Quotient.mk (I ^ (n + 1))) (I ^ n))

pp: case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Injective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?refine_1) c, ⋯⟩

pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?refine_1) c, ⋯⟩

Tactic:
· intro
    simp [Submodule.mem_smul_top_iff, pow_succ']

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∀ (c : ↥(I ^ n) ⧸ I • ⊤),
    ((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c ∈
      Submodule.restrictScalars R (map (Quotient.mk (I ^ (n + 1))) (I ^ n))

case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Injective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Surjective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ Function.Injective fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩

Tactic:
intro a b

Goal state after:
case refine_3
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
a b : ↥(I ^ n) ⧸ I • ⊤
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) a =
      (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) b →
    a = b
Module: Mathlib.Data.List.Cycle

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

Tactic:
simp at ha

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

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

Tactic:
simp at ha

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

Goal state before:
pp: α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup

Tactic:
by
  rw [(permutations_perm_permutations' s).nodup_iff]
  induction hs with
  | nil => simp
  | @cons x l h h' IH =>
    rw [permutations']
    rw [nodup_flatMap]
    constructor
    · intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl
    · refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _

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

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ (n ^ k).minFac = n.minFac

Tactic:
rcases eq_or_ne n 1 with (rfl | hn)
  · simp
  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff_left hk).1 hk')
  apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
  apply
    minFac_le_of_dvd (minFac_prime hnk).two_le
      ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))

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

Goal state before:
pp: case mpr.inl
⊢ primeFactorsList 0 = []

Tactic:
exact primeFactorsList_zero

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
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H

Tactic:
suffices (exists_smul_eq G (g • y₂) x).choose = (exists_smul_eq G y₂ x).choose * g⁻¹ by
      simp [this]

Goal state after:
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 : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
⊢ ⋯.choose = ⋯.choose * ↑g⁻¹
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n q : ℕ
⊢ q ∈ replicate n p → Prime q

Tactic:
hq

Goal state after:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n k : ℕ
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  induction k with
  | zero => simp
  | succ k ih => rw [pow_succ', primeFactors_mul hn (pow_ne_zero _ hn), ih, Finset.union_idempotent]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)

Tactic:
index_eq_two_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ a, ∀ (b : G), Xor (b * a ∈ H) (b ∈ H)) ↔ ∃ a, ∀ (b : G), Xor (a * b ∈ H) (b ∈ H)
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
⊢ Function.Injective ⇑((MulDistribMulAction.toMonoidEnd H G) h)

Tactic:
intro a b

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) b → a = b
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
⊢ Function.Injective ⇑((DistribMulAction.toAddMonoidEnd H G) h)

Tactic:
intro a b

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) b → a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = ↑1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]

Tactic:
Units.val_one

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ (↑u).val * (↑u⁻¹).val ≡ 1 [MOD n + 1]
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: 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
ha : a ≠ 0
⊢ a.val > 0

Tactic:
gt_iff_lt,

Goal state after:
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
ha : a ≠ 0
⊢ 0 < a.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: 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
ha : a ≠ 0
⊢ a.val > 0

Tactic:
by rwa [gt_iff_lt, ZMod.val_pos]

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

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ f.ker

Tactic:
rw [ker_intCastAddHom]

Goal state after:
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 ↔ AddSubgroup.zmultiples ↑n ≤ f.ker
Module: Mathlib.Data.Nat.Digits.Defs

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

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

Goal state after: