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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p : R[X]
⊢ (aeval (f x)) p = f ((aeval x) p)

Tactic:
refine Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => ?_)
    (by simp [AlgHomClass.commutes])

Goal state after:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ (aeval (f x)) (p + q) = f ((aeval x) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (C r).coeffs ⊆ {r}

Tactic:
rw [coeffs_C]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (if r = 0 then ∅ else {r}) ⊆ {r}
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
r : R
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
⊢ ((∃ n, ¬coeff n p = 0 ∧ r = coeff n p) ∨ ∃ n, ¬coeff n q = 0 ∧ r = coeff n q) →
    ∃ n, ¬coeff n p + coeff n q = 0 ∧ r = coeff n p + coeff n q

Tactic:
rintro (⟨n, hn, rfl⟩ | ⟨n, hn, rfl⟩)

Goal state after:
case refine_2.inl
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n p = 0
⊢ ∃ n_1, ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n p = coeff n_1 p + coeff n_1 q

case refine_2.inr
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ∃ n_1, ¬coeff n_1 p + coeff n_1 q = 0 ∧ coeff n q = coeff n_1 p + coeff n_1 q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ↑((map f) p).coeffs ⊆ ⇑f '' ↑p.coeffs

Tactic:
classical
  exact mod_cast coeffs_map f p

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i (p + q) < degreeOf i p
⊢ degreeOf i p = degreeOf i q

Tactic:
contrapose! h
  apply le_trans (Nat.le_max_left _ (q.degreeOf i))
  rcases Nat.lt_or_lt_of_ne h with h | h
  · simp [add_comm p q, degreeOf_add_eq_of_degreeOf_lt h, max_eq_right_of_lt h]
  · simp [degreeOf_add_eq_of_degreeOf_lt h, max_eq_left_of_lt h]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ False

Tactic:
obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : ↑n = p.support.min
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
rw [mem_support_iff, coeff_mul_X_pow'] at hy

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).degree = ↑(s.sup fun i ↦ (f i).natDegree)

Tactic:
rw [degree_sum_eq_of_disjoint]

Goal state after:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

case pos.h
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin (n + 1) →₀ ℕ
⊢ x ∈ cons i '' ↑(((finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Tactic:
simpa using congr(x ∈ $image_support_finSuccEquiv)

Goal state after:
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).natDegree ≤ ∑ i ∈ s, (f i).natDegree

Tactic:
by
  simpa using natDegree_multiset_prod_le (s.1.map f)

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
refine forall₄_congr fun a b ha hb => ?_

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
  constructor
  · rintro h g hg hdg ⟨f, rfl⟩
    exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg
  · rintro h f g - hg rfl hdg
    exact h g hg hdg (dvd_mul_left g f)

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

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

Tactic:
simpa only [tsub_add_cancel_of_le hxy] using geom_sum₂_mul_add (x - y) y n

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

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

Tactic:
simp [h.mul_left_ne_zero, hq]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
simp [h.mul_left_ne_zero, hq]

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Tactic:
refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm

Goal state after:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
t : A
ht : t ∈ l2.support
⊢ l2 t • _root_.id t * _root_.id z ∈ span R (p * q)

Tactic:
smul_mul_assoc

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t✝ : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t✝)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
t : A
ht : t ∈ l2.support
⊢ l2 t • (_root_.id t * _root_.id z) ∈ span R (p * q)
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:
rcases ih with ⟨P, rfl⟩

Goal state after:
case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = r • (MvPolynomial.aeval fun s ↦ of' R M ↑s) P
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:
rcases ih with ⟨P, rfl⟩

Goal state after:
case smul
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = r • ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P
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:
rcases ih with ⟨P, rfl⟩

Goal state after:
case smul
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = r • (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P
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:
rcases ih with ⟨P, rfl⟩

Goal state after:
case smul
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = r • ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing (MvPolynomial (Fin 0) R)

Tactic:
apply isNoetherianRing_of_ringEquiv R

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ R ≃+* MvPolynomial (Fin 0) R
Module: Mathlib.GroupTheory.GroupAction.Ring

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
n✝ : ℤ
x y : R
n : ℕ
⊢ -((n + 1) • x * y) = -((n + 1) • (x * y))

Tactic:
smul_mul_assoc

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

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ p ∣ b - a

Tactic:
← cast_eq_zero_iff R p (b - a),

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsRightCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ ↑(b - a) = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ker (RingHom.pi fun i ↦ Quotient.mk (I i)) = ⨅ i, I i

Tactic:
simp [Pi.ker_ringHom, mk_ker]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J

Tactic:
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]

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

Goal state before:
pp: case «1».«0»
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]
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
· exact coprime.symm

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

Goal state before:
pp: p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False

Tactic:
decide +revert

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

Goal state before:
pp: case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬m.Coprime n

Tactic:
· intro h
    obtain ⟨p, hp⟩ := h
    apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ comap (quotQuotMk I J) ⊥ = I ⊔ J

Tactic:
quotQuotMk,

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

Goal state before:
pp: α : Type u_1
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys id).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
show @id (List α) = ([] ++ ·) by funext _; rfl

Goal state after:
α : Type u_1
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x ↦ [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
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✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : StarRing B
inst✝⁴ : StarModule R A
inst✝³ : FunLike F A B
inst✝² : AlgHomClass F R A B
inst✝¹ : StarHomClass F A B
f g : F
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
b : A
⊢ star ((↑φ).toRingHom b) ∈ (↑φ).range.carrier

Tactic:
exact ⟨star b, map_star φ b⟩

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s

Tactic:
rw [← Nat.card_prod]; exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a : α
⊢ ∀ (x y : ↑(orbit G a)), ∃ g, g • x = y

Tactic:
by
    rintro ⟨_, g, rfl⟩ ⟨_, h, rfl⟩
    use h * g⁻¹
    ext1
    simp [mul_smul]

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

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length

Tactic:
obtain ⟨x, y, hxy, hx, hy⟩ := h

Goal state after:
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : { l // l.Nodup }
⊢ (↑↑l).Nodup

Tactic:
by simpa using l.prop

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
rw [isPrimePow_nat_iff]
  constructor
  · rintro ⟨p, k, hp', hk', rfl⟩
    refine ⟨k, ?_, hk', ⟨p, Nat.le_pow hk', rfl, hp'⟩⟩
    · calc
        k = Nat.log 2 (2 ^ k) := by simp
        _ ≤ Nat.log 2 (p ^ k) := Nat.log_mono Nat.one_lt_two Nat.AtLeastTwo.prop
                                   (Nat.pow_le_pow_left (Nat.Prime.two_le hp') k)
  · rintro ⟨k, hk, hk', ⟨p, hp, rfl, hp'⟩⟩
    exact ⟨p, k, hp', hk', rfl⟩

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
by
    induction s with
    | nil => exact fun _ b hb ↦ (notMem_nil _ hb).elim
    | cons a l => ?_
    intro hs b hb c hc
    rw [Cycle.chain_coe_cons, List.isChain_iff_pairwise] at hs
    simp only [pairwise_append, pairwise_cons, mem_append, mem_singleton, List.not_mem_nil,
      IsEmpty.forall_iff, imp_true_iff, Pairwise.nil, forall_eq, true_and] at hs
    simp only [mem_coe_iff, mem_cons] at hb hc
    rcases hb with (rfl | hb) <;> rcases hc with (rfl | hc)
    · exact hs.1 c (Or.inr rfl)
    · exact hs.1 c (Or.inl hc)
    · exact hs.2.2 b hb
    · exact _root_.trans (hs.2.2 b hb) (hs.1 c (Or.inl hc))

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

Goal state before:
pp: p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]

Tactic:
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2

Goal state after:
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : p.minFac = p
⊢ p.minFac :: (p / p.minFac).primeFactorsList = [p]
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
g : G ⧸ H
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) g) = g

Tactic:
cases g using Quotient.inductionOn' with | _ g
    simp only [Quotient.liftOn'_mk'', QuotientGroup.mk]
    rw [Quotient.eq'', leftRel_eq]
    simp only
    convert! one_mem H
    rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq G (g⁻¹ • x) x).choose_spec]

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

Goal state before:
pp: n k : ℕ
⊢ ↑k = 0 ↔ n ∣ k

Tactic:
rcases n with - | n

Goal state after:
case zero
k : ℕ
⊢ ↑k = 0 ↔ 0 ∣ k

case succ
k n : ℕ
⊢ ↑k = 0 ↔ n + 1 ∣ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).cast = if ↑n ≤ a.cast + b.cast then a.cast + b.cast - ↑n else a.cast + b.cast

Tactic:
rcases n with - | n

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).cast = if ↑0 ≤ a.cast + b.cast then a.cast + b.cast - ↑0 else a.cast + b.cast

case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).cast = if ↑(n + 1) ≤ a.cast + b.cast then a.cast + b.cast - ↑(n + 1) else a.cast + b.cast
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
⊢ cast 1 = 1

Tactic:
rcases n with - | n

Goal state after:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
refine ⟨n₂ - n₁, by lia, by lia, ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ a ^ (n₂ - n₁) ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n
⊢ ZMod 0 ≃+* ZMod n

Tactic:
rcases n with - | n

Goal state after:
case zero.zero
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
h : 0 = 0
⊢ ZMod 0 ≃+* ZMod 0

case zero.succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n + 1
⊢ ZMod 0 ≃+* ZMod (n + 1)
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
rcases n with - | n

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

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)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑n - 1

Tactic:
rcases n with - | n

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
y : M
hy : y ∈ Set.range ⇑f
x : G
⊢ #{g | f g = f x} = #{g | f g = y}

Tactic:
rcases hy with ⟨y, rfl⟩

Goal state after:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : G
⊢ #{g | f g = f x} = #{g | f g = f y}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}

Tactic:
Finset.filter_insert,

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

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

Tactic:
rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
    Nat.mod_eq_of_lt (val_lt _)]
  rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Goal state after: