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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
j : Option S₁ →₀ ℕ
r : R
n : Option S₁ →₀ ℕ
hj : ¬j = n
hj_none : j none = n none
hj_some : j.some = n.some
⊢ ∀ (x : S₁), j (Option.some x) = n (Option.some x)

Tactic:
simpa only [Finsupp.ext_iff] using! hj_some

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
· simp [h]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree
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
⊢ r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
r0

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
⊢ n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h₁
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
            (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i))).comp
        (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X =
    ((AlgHom.id R (MvPolynomial S₁ R[X])).comp (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X]))) Polynomial.X

Tactic:
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X,
          aevalTower_X, AlgHom.coe_id, id]

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

Goal state before:
pp: case h₂
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (((aeval fun o ↦ o.elim (C Polynomial.X) X).comp
          (aevalTower (Polynomial.aeval (X none)) fun i ↦ X (Option.some i)))
        (X i✝)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial S₁ R[X])) (X i✝))

Tactic:
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X,
          aevalTower_X, AlgHom.coe_id, id]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
⊢ ¬IsUnit (X + C a)

Tactic:
rintro ⟨⟨_, g, hfg, hgf⟩, rfl⟩

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
⊢ False
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
⊢ p ∈ l → p.degree ≤ (List.map natDegree l).maximum

Tactic:
hp

Goal state after:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
⊢ p.degree ≤ (List.map natDegree l).maximum
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
⊢ p.leadingCoeff = 1

Tactic:
hp

Goal state after:
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
⊢ 1 = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).support.sup WithBot.some = ((finSuccEquiv R n) f).support.sup (WithBot.some ∘ fun x ↦ x)

Tactic:
h₁

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α β : Type} (f : α → β), (f ∘ fun x ↦ x) = f
h' : (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f
⊢ ((finSuccEquiv R n) f).support.sup WithBot.some = ((finSuccEquiv R n) f).support.sup WithBot.some
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x ↦ x * p) q = (fun x ↦ x * p) r
⊢ q = r

Tactic:
simp only at h

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : q * p = r * p
⊢ q = r
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
⊢ p ∈ degreeLE R ↑n → p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
hp

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p ∈ degreeLE R ↑n
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
⊢ p ∈ degreeLT R n → p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
hp

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
refine Submodule.smul_mem _ _ (Submodule.subset_span <| by grind)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inl.inr
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)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
· rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)

Goal state after:
case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
· simp [h]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ (∃ p ∈ I, p.leadingCoeff = x) → ∃ i, ∃ p ∈ I, p.degree ≤ ↑i ∧ p.leadingCoeff = x

Tactic:
rintro ⟨p, hpI, rfl⟩

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
p : R[X]
hpI : p ∈ I
⊢ ∃ i, ∃ p_1 ∈ I, p_1.degree ≤ ↑i ∧ p_1.leadingCoeff = p.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
hp

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
algebraize_only [f, g, g.comp f]

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
⊢ (g.comp f).FiniteType
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = f
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = r • f

Tactic:
| smul r f ih =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = r • f

Tactic:
| smul r f ih =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = f
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = r • f

Tactic:
| smul r f ih =>

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = r • f

Tactic:
| smul r f ih =>

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
⊢ ((aeval f) p).range ⊔ ((aeval f) q).range = ⊤

Tactic:
rw [eq_top_iff]
  intro v _
  rw [Submodule.mem_sup]
  rcases hpq with ⟨p', q', hpq'⟩
  use aeval f (p * p') v
  use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
  use aeval f (q * q') v
  use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
  simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add] using!
    congr_arg (fun p : R[X] => aeval f p v) hpq'

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

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : ↑a = ↑b
⊢ a = b

Tactic:
exact natCast_injOn_Iio _ _ ha hb hab

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

Goal state before:
pp: case mpr
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
hy : y ∈ ker f ∧ (Quotient.mk I) y = x
⊢ f y = 0

Tactic:
exact hy.left

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

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ¬¬n.Coprime m

Tactic:
Prime.not_coprime_iff_dvd

Goal state after:
n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ ¬∃ p, Prime p ∧ p ∣ n ∧ p ∣ m
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
hg : Surjective ⇑g
⊢ Surjective (⇑(f.liftOfSurjective hf g H) ∘ ⇑f)

Tactic:
convert! hg; ext; simp

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

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

Tactic:
by
  simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

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

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

Tactic:
rw [IsPeriodicPt, iterate_add] at hn
  exact hn.left_of_comp hm

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

Goal state before:
pp: α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ y ∈ periodicOrbit f x ↔ ∃ n, f^[n] x = y

Tactic:
simp only [periodicOrbit, Cycle.mem_coe_iff, List.mem_map, List.mem_range]

Goal state after:
α : Type u_1
f : α → α
x y : α
hx : x ∈ periodicPts f
⊢ (∃ a < minimalPeriod f x, f^[a] x = y) ↔ ∃ n, f^[n] x = y
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
⊢ (∃ is' x, l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂_1, l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
rcases l₂ with - | ⟨a, l₂'⟩

Goal state after:
case inl.nil
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
rw [nextOr, nextOr, IH]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ x ∈ (z :: zs).dropLast
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: 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')

Tactic:
apply perm_permutations'Aux_comm

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

Goal state before:
pp: α : Type u_1
s t : List α
p : s ~ t
⊢ s.permutations' ~ t.permutations'

Tactic:
induction p with

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
⊢ x ∈ xs

Tactic:
induction xs with
  | nil => simp at h
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at h
  · by_cases hx : x = y
    · simp [hx]
    · rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
⊢ (∀ x ∈ xs, x ∈ xs') → d ∈ xs' → xs.nextOr x d ∈ xs'

Tactic:
hxs'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
⊢ d ∈ xs' → xs.nextOr x d ∈ xs'
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
x : α
inst✝ : Fintype α
⊢ minimalPeriod f x ≤ card α

Tactic:
by
  rw [← periodicOrbit_length]
  exact List.Nodup.length_le_card nodup_periodicOrbit

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

Goal state before:
pp: α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).length = s.length + 1

Tactic:
by
  induction s with
  | nil => simp
  | cons y s IH => simpa using IH

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
⊢ idxOf a l - 1 < l.length

Tactic:
by grind [idxOf_lt_length_of_mem]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ b ∈ ↑(a :: l)

Tactic:
by simp [hb]

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

Goal state before:
pp: case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l.prod = n.primeFactorsList.prod

Tactic:
h₁

Goal state after:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = n.primeFactorsList.prod
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p

Tactic:
hp

Goal state after:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ++ b.primeFactorsList
⊢ Prime p
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:
by
  rw [index_eq_two_iff, (Equiv.inv G).exists_congr]
  refine fun a ↦ (Equiv.inv G).forall_congr fun b ↦ ?_
  simp only [Equiv.inv_apply, inv_mem_iff, ← mul_inv_rev]

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
rw [Nat.dvd_one] at h
    subst m
    subsingleton [CharP.CharOne.subsingleton]

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

Goal state before:
pp: case zero
a : ℤ
⊢ (↑a).cast = a % ↑0

Tactic:
rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]

Goal state after:
case zero
a : ℤ
⊢ cast a = a
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
· rintro ⟨rfl, hab⟩
    rw [mul_ne_zero_iff] at hab
    simpa [hab.1, hab.2] using Nat.le_mul_of_pos_right _ hab.2.bot_lt

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
h : m ∈ n.divisors
⊢ 0 < m

Tactic:
cases m
  · rw [mem_divisors, zero_dvd_iff (a := n)] at h
    cases h.2 h.1
  apply Nat.succ_pos

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

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 1 < x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [lt_add_iff_pos_left]

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n✝ : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
hn' : Even n
ihn : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < x * ∑ i ∈ range n, x ^ i