mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ ((rename f) φ).support
⊢ False

Tactic:
replace H := mapDomain_support H

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (⇑(mapDomain.addMonoidHom f)) φ.coeff.support
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ ((rename f) ((killCompl hf) p)).support ⊆ p.support

Tactic:
rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
this : p.degrees.card = 0
⊢ p.totalDegree = 0

Tactic:
by grind [totalDegree_le_degrees_card p]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ (p - q).vars ⊆ p.vars ∪ q.vars

Tactic:
convert! vars_add_subset p (-q) using 2

Goal state after:
case e'_3
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p - q = p + -q

case e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ q.vars = (-q).vars
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
⊢ (∑ i ∈ t, φ i).vars = t.biUnion fun i ↦ (φ i).vars

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case empty
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
⊢ (∅.sum f).totalDegree ≤ ∅.sup fun i ↦ (f i).totalDegree

Tactic:
exact zero_le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ natDegree 0 ≤ p.natDegree * q.natDegree

Tactic:
natDegree_zero

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0

Tactic:
rwa [coeff_comp_degree_mul_degree hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < ↑p.natTrailingDegree

Tactic:
exact WithTop.coe_lt_coe.2 h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * X ^ n).support
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : #f.support = c + 1
⊢ #f.eraseLead.support = c

Tactic:
by
  rw [card_support_eraseLead, fc, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p + -q).natDegree ≤ n ↔ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p + -q).coeff n = p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p + -q).coeff n = -q.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ natDegree 0 = 0

Tactic:
natDegree_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ #f.eraseLead.support = 0

Tactic:
card_support_eraseLead' hf

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑p.natDegree * q.degree

Tactic:
degree_eq_natDegree (ne_zero_of_degree_gt hq),

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ (p.comp q).degree = ↑p.natDegree * ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ (p * X ^ (n + 1)).reverse = p.reverse

Tactic:
rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f - g) = reflect N f - reflect N g

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f + -g) = reflect N f - reflect N g
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f + -g) = reflect N f - reflect N g

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f + -g) = reflect N f + -reflect N g
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

Tactic:
by
  simpa only [Multiset.map_map] using! degree_multiset_prod_le (s.1.map f)

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

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

Tactic:
rw [Polynomial.leadingCoeff_mul']

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod

case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0

Tactic:
rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

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]
⊢ q * p = 0 → q = 0

pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
· intro hp
    replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
    simp only [zero_mul] at hp
    rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
    refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    simp

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : Ideal R
⊢ (map C p).leadingCoeff = p

Tactic:
by
  ext x
  constructor
  · intro hx
    rcases ((map C p).mem_leadingCoeff x).1 hx with ⟨f, hf, rfl⟩
    exact p.mem_map_C_iff.1 hf f.natDegree
  · intro hx
    exact ((map C p).mem_leadingCoeff x).2 ⟨C x, mem_map_of_mem C hx, leadingCoeff_C x⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < 0
⊢ False

Tactic:
Nat.WithBot.lt_zero_iff,

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree = ⊥
⊢ False
Module: Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

Tactic:
← op_inj,

Goal state after:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
⊢ Prime (C r) ↔ Prime r

Tactic:
have := Fintype.ofFinite σ

Goal state after:
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
⊢ Prime (C r) ↔ Prime r
Module: Mathlib.Algebra.Ring.Subring.MulOpposite

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

Tactic:
← op_inj,

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

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

Tactic:
rintro ⟨n, f, hsur⟩

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B

Tactic:
rw [FiniteType, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_3.smul
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
a : ↥A
x : M
hx✝ : x ∈ span (↥A) (Set.range mj)
hx : x ∈ ((↑↥A f).domRestrict N').range
⊢ a • x ∈ ((↑↥A f).domRestrict N').range

Tactic:
exact smul_mem _ a hx

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

Goal state before:
pp: n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]

Tactic:
sub_eq_add_neg,

Goal state after:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b - d [ZMOD n]
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x - y = x + y

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x + -y = x + 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
hf : Pairwise (IsCoprime on I)
x : (i : ι) → R ⧸ I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = x i

Tactic:
obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise (IsCoprime on I)
y : R ⧸ ⨅ i, I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = (quotientInfToPiQuotient I) y i
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = ⊤

Tactic:
← Submodule.range_mkQ I,

Goal state after:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = (Submodule.mkQ I).range
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : a * a * y = a * a
⊢ y = 1

Tactic:
Nat.mul_eq_left (Nat.mul_ne_zero hp.ne_zero hp.ne_zero)

Goal state after:
case inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : y = 1
⊢ y = 1
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) (comap (Quotient.mk I) (ker (Quotient.mk (map (Quotient.mk I) J)))) = map (Quotient.mk J) I

Tactic:
Ideal.mk_ker,

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) (comap (Quotient.mk I) (map (Quotient.mk I) J)) = map (Quotient.mk J) I
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) (J ⊔ ker (Quotient.mk I)) = map (Quotient.mk J) I

Tactic:
Ideal.mk_ker,

Goal state after:
R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
⊢ map (Quotient.mk J) (J ⊔ I) = map (Quotient.mk J) I
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
rcases le_total n m with h | h

Goal state after:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

Tactic:
by
  cases S; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l.dropLast
d : α
⊢ [a, l.nextOr a d] <:+: l

Tactic:
by
  refine infix_iff_getElem?.mpr ⟨l.idxOf a, ?_, fun i hi ↦ ?_⟩
  · have ⟨_, _⟩ := l.dropLast_prefix
    grind
  by_cases hi₁ : i = 1
  · grind [next, nextOr_eq_getElem?_idxOf_succ_of_mem_dropLast]
  · grind [getElem?_idxOf, mem_of_mem_dropLast]

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

Goal state before:
pp: case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
exact ⟨L_hd, mem_cons_self, hd⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
rw [chain_iff_pairwise] at hs

Goal state after:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k : ℕ
h : k ≠ 0
⊢ n.primeFactorsList <+ (n * k).primeFactorsList

Tactic:
rcases n with - | hn
  · simp [zero_mul]
  apply sublist_of_subperm_of_pairwise _
    (primeFactorsList_sorted _).pairwise (primeFactorsList_sorted _).pairwise
  simp only [(perm_primeFactorsList_mul (Nat.succ_ne_zero _) h).subperm_left]
  exact (sublist_append_left _ _).subperm

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

Goal state before:
pp: n : ℕ
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x

Tactic:
intro k
    rcases n with - | n
    · simp
    · exact Fin.natCast_eq_zero

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

Goal state before:
pp: n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = ↑a

Tactic:
exact ⟨a, map_intCast ..⟩

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

Goal state before:
pp: case succ.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
m n : ℕ
h : m + 1 = n + 1
⊢ ZMod (m + 1) ≃+* ZMod (n + 1)

Tactic:
· exact
      { finCongr h with
        map_mul' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_mul, Fin.val_mul, Fin.val_cast, Fin.val_cast, ← h]
        map_add' := fun a b => by
          dsimp [ZMod]
          ext
          rw [Fin.val_cast, Fin.val_add, Fin.val_add, Fin.val_cast, Fin.val_cast, ← h] }

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ (QuotientGroup.leftRel (pi Set.univ H)) x y ↔ piSetoid x y

Tactic:
rw [QuotientGroup.leftRel_pi]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ i ∈ s, f i).FiniteIndex

Tactic:
iInf_subtype'

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ x, f ↑x).FiniteIndex
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ {d ∈ range n | d ∣ n} = n.properDivisors

Tactic:
ext
  simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
  exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
h : m ∈ n.properDivisors
⊢ 1 < n / m

Tactic:
obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h

Goal state after:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ 1 < n / m
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n✝ n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
coe_mul_inv_eq_one x h

Goal state after:
m n✝ n x : ℕ
h : x.Coprime n
⊢ 1 = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩

Goal state after:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ (n✝ + 1 + 1).properDivisors = {1}
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
rw [← mul_two, ← @Nat.cast_two (ZMod n), ← ZMod.coe_unitOfCoprime 2 hn, Units.mul_left_eq_zero]

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a - b).val = a.val - b.val

Tactic:
sub_eq_add_neg,

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a + -b).val = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ ofDigits b L = (List.mapIdx (fun i a ↦ a * b ^ i) L).sum

Tactic:
rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
    ofDigits_eq_foldr, ← List.range_eq_range']

Goal state after:
b : ℕ
L : List ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 L =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)).sum
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
l2 : List ℕ
h : (hd₁ :: tl₁).length = l2.length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) l2)

Tactic:
induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
⊢ 0 < n → ¬x ^ n = 1

Tactic:
hn_pos

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
⊢ ¬x ^ n = 1
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + -b) = emultiplicity p b
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (a + -b) = multiplicity p b