mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Subsingleton R
this : Subsingleton S
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

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

Goal state before:
pp: case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
⊢ f ∈ ⇑C '' ↑I → ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
hf

Goal state after:
case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f✝ : MvPolynomial σ R
hf✝ : f✝ ∈ Ideal.map C I
f : MvPolynomial σ R
hf : f ∈ ⇑C '' ↑I
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ (0 • x) • y = 0 • x • y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

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

Tactic:
simp

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

Goal state before:
pp: a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)

Tactic:
simp

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

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a

Tactic:
rw [ModEq, eq_comm]
  simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]

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

Goal state before:
pp: case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ 0 ≡ b ^ 0 [ZMOD n]

Tactic:
simp

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

Goal state before:
pp: n a : ℤ
⊢ n + a ≡ a [ZMOD n]

Tactic:
simp

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

Goal state before:
pp: n a : ℤ
⊢ a + n ≡ a [ZMOD n]

Tactic:
simp

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

Goal state before:
pp: a t n : ℤ
⊢ a + n * t ≡ a [ZMOD n]

Tactic:
simp

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b ≡ ↑a * a.gcdA b + ↑b * a.gcdB b [ZMOD ↑b]

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
x : R
⊢ (quotientKerEquivOfSurjective hf) ((quotientKerEquivOfSurjective hf).symm (f x)) =
    (quotientKerEquivOfSurjective hf) ((Ideal.Quotient.mk (ker f)) x)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
S : Subalgebra R C
h : (lift f).range ≤ S
x : A
⊢ (lift f).toRingHom ↑x = f x

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
x✝ : R
⊢ ((quotientKerEquivOfSurjective hf).symm.toRingHom.comp f) x✝ = (Ideal.Quotient.mk (ker f)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubsemiringClass S A
hSRA : SMulMemClass S R A
s : S
⊢ Algebra.adjoin R ↑(NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype s)) = Algebra.adjoin R ↑s

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ p = p.lcm p

Tactic:
simp

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

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

Tactic:
intro j

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
i j : ι
⊢ j ∈ {i}ᶜ → IsCoprime (I i) (I j)
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝³ : Field R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑x✝ = ↑x✝

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ Even 0

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ¬Even 1

Tactic:
simp

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

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

Tactic:
intro j

Goal state after:
case h
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
g : (i : ι) → R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (Quotient.mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (Quotient.mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (Quotient.mk (I j)) (e i) = 0
i j : ι
⊢ j ≠ i → (Quotient.mk (I i)) (f j * e j) = 0
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ 37 = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing R
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : StarRing C
inst✝¹ : Algebra R C
inst✝ : StarModule R C
f : A →⋆ₙₐ[R] C
S : StarSubalgebra R C
h : (starLift f).range ≤ S
x : A
⊢ (↑(starLift f)).toRingHom ↑x = f x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : Field R
inst✝⁶ : StarRing R
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra R A
inst✝² : StarModule R A
inst✝¹ : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
inst✝ : StarMemClass S A
s : S
h1 : 1 ∉ s
x✝ : ↥s
⊢ (unitization s) ↑x✝ = ↑x✝

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ Even 0

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
⊢ ¬Even 1

Tactic:
simp

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

Goal state before:
pp: p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n

Tactic:
rw [hn, Nat.add_sub_cancel, two_mul]

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

Goal state before:
pp: p : ℕ
hp : Prime p
h : p % 2 = 1
hf : p = 2
⊢ False

Tactic:
hf

Goal state after:
p : ℕ
hp : Prime p
h : 2 % 2 = 1
hf : p = 2
⊢ False
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
A : Type u_6
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
x✝ : A ⧸ I
⊢ (factorₐ R ⋯) x✝ = (AlgHom.id R (A ⧸ I)) x✝

Tactic:
simp

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
hIJ : I ≤ J
K : Ideal A
inst✝ : K.IsTwoSided
hJK : J ≤ K
x✝ : A
⊢ (((factorₐ R₁ hJK).comp (factorₐ R₁ hIJ)).comp (mkₐ R₁ I)) x✝ = ((factorₐ R₁ ⋯).comp (mkₐ R₁ I)) x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
hf : Surjective ⇑f
a : A
⊢ (quotientKerAlgEquivOfSurjective hf) ((quotientKerAlgEquivOfSurjective hf).symm (f a)) =
    (quotientKerAlgEquivOfSurjective hf) ((Quotient.mk (ker f)) a)

Tactic:
simp

Goal state after:
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
x✝ : A
⊢ ((f.liftOfSurjective hf g H).comp f) x✝ = g x✝

Tactic:
simp

Goal state after:
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
x✝ : A
⊢ (⇑(f.liftOfSurjective hf g H) ∘ ⇑f) x✝ = g x✝

Tactic:
simp

Goal state after:
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
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R₁
inst✝⁷ : CommSemiring R₂
inst✝⁶ : Ring A
inst✝⁵ : Algebra R₁ A
inst✝⁴ : Algebra R₂ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A ≃ₐ[R₁] B
hIJ : J = map (↑f) I
r : R₁
⊢ (I.quotientEquiv J f.toRingEquiv hIJ).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ (B ⧸ J)) r

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
hc : m = n
h : True
⊢ n.toList ∈ n.toList.permutations ∧ ∃ b ∈ n.toList.permutations, n.toList = b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
l : List α
f : Finset α
hf : f.val = ↑l
⊢ l.Nodup ↔ f.val.Nodup

Tactic:
hf

Goal state after:
α : Type u_1
inst✝ : Fintype α
l : List α
f : Finset α
hf : f.val = ↑l
⊢ l.Nodup ↔ (↑l).Nodup
Module: Mathlib.Data.List.Permutation

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd

Tactic:
simp

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

Goal state before:
pp: case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (↑(centralizer R s) ∪ star ↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer

Tactic:
StarMemClass.star_coe_eq,

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ (↑(centralizer R s) ∪ ↑(centralizer R s)).centralizer = (s ∪ star s).centralizer.centralizer
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x ↦ l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (fun x ↦ l ++ y :: x) = fun x ↦ l ++ [y] ++ x

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : Subalgebra R A
x : A
⊢ star x ∈ star S ↔ x ∈ S

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ y :: ys ≠ [] ∧ y :: ys = [] ++ y :: ys ∧ l ++ (t :: y :: ys ++ ts) = l ++ [] ++ t :: y :: ys ++ ts

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ y :: (l₁ ++ l₂) = y :: l₁ ++ l₂ ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ y :: l₁ ++ t :: l₂ ++ ts

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ y :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x ↦ l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
simp

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

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
y : R
hy : y ∈ I ^ n
hx : (Quotient.mk (I ^ (n + 1))) y ∈ map (Quotient.mk (I ^ (n + 1))) (I ^ n)
⊢ (fun c ↦ ⟨((I • ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯) c, ⋯⟩) (Submodule.Quotient.mk ⟨y, hy⟩) =
    ⟨(Quotient.mk (I ^ (n + 1))) y, hx⟩

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ [] → l.length = n
⊢ (map length []).sum = n * [].length

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (is : List α), map (map f) ([].permutationsAux is) = (map f []).permutationsAux (map f is)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
ts is' : List α
⊢ ([] ++ ts).permutationsAux is' =
    map (fun x ↦ x ++ ts) ([].permutationsAux is') ++ ts.permutationsAux ([].reverse ++ is')

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (is l : List α), l ∈ [].permutationsAux is → l ~ [] ++ is

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hn : 0 < n
hx : IsPeriodicPt f n x
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ minimalPeriod f (f^[n] x) = minimalPeriod f x

Tactic:
apply
    (IsPeriodicPt.minimalPeriod_le (minimalPeriod_pos_of_mem_periodicPts hx) _).antisymm
      ((isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate hx
            (isPeriodicPt_minimalPeriod f _)).minimalPeriod_le
        (minimalPeriod_pos_of_mem_periodicPts _))

Goal state after:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
⊢ ∀ (is : List α), ([].permutationsAux is).length + is.length ! = ([].length + is.length)!

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (is l : List α), l ~ is ++ [] → (∃ is' x, l = is' ++ []) ∨ l ∈ [].permutationsAux is

Tactic:
simp

Goal state after: