mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f H)

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), (Ideal.Quotient.lift I f H) x = 0 → x = 0
Module: Mathlib.Data.Int.ModEq

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by 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:
by 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:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
⊢ CharZero R

Tactic:
let p := ringChar R

Goal state after:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
⊢ CharZero R
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ⊥.IsMaximal

Tactic:
let := Quotient.divisionRing I

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
this : DivisionRing (R ⧸ I) := Quotient.divisionRing I
⊢ ⊥.IsMaximal
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:
by simp

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card αˣ = card α - 1

Tactic:
rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]

Goal state after:
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:
by 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:
by 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:
by 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:
by simp

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

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

Tactic:
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]

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:
by 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:
by 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:
by 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:
by 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:
by simp

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

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

Tactic:
by 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:
by simp

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

Goal state before:
pp: α : 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 α), l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
l

Goal state after:
α : 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 α
⊢ l ~ is ++ t :: ts → (∃ is' x, l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : 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
⊢ a :: l₂' ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁ ++ t :: a :: l₂' ++ ts

Tactic:
by simp

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
periodicOrbit_eq_nil_of_not_periodic_pt hx,

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Cycle

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

Tactic:
induction xs with
  | nil => exact hd
  | cons y ys ih => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ys : List α
ih : (∀ x ∈ ys, x ∈ xs') → ys.nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: ys, x ∈ xs'
⊢ (y :: ys).nextOr x d ∈ xs'
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 : Set (StarSubalgebra R A)
⊢ ↑(sInf S).toSubalgebra = ↑(sInf (toSubalgebra '' S))

Tactic:
by 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
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i).toSubalgebra = ↑(⨅ i, (S i).toSubalgebra)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
x : α
s : List α
⊢ ∀ ⦃a₂ : List α⦄, permutations'Aux x s = permutations'Aux x a₂ → s = a₂

Tactic:
t

Goal state after:
α : Type u_1
x : α
s t : List α
⊢ permutations'Aux x s = permutations'Aux x t → s = t
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x s).length

Tactic:
by simp

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

Goal state before:
pp: 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✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : (↑φ).toRingHom a = x
⊢ a ∈ ↑⊤.toSubsemiring

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ tl.length < (hd :: tl).length

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
⊢ l.prev a ha = l[(idxOf a l + (l.length - 1)) % l.length]

Tactic:
cases l with | nil => grind | cons head tail =>
  by_cases ha₀ : a = head
  · subst ha₀
    simp
    grind
  rw [prev_eq_getElem_idxOf_pred_of_ne_head ha ha₀]
  congr
  rw [← Nat.add_sub_assoc, Nat.sub_add_comm, Nat.add_mod_right, Nat.mod_eq_of_lt]
  all_goals grind

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

Goal state before:
pp: α : Type u_1
s : Cycle α
x✝ : List α
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) x✝)).reverse = Quot.mk (⇑(IsRotated.setoid α)) x✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), (toMultiset (Quotient.mk'' a)).card = length (Quotient.mk'' a)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α), b ∈ map f (Quotient.mk'' a) ↔ ∃ a_1 ∈ Quotient.mk'' a, f a_1 = b

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ x ∈ ↑(x :: y :: l)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ y ∈ ↑(x :: y :: l)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
hs✝ : List α
hs : Nodup (Quotient.mk'' hs✝)
⊢ (fun l ↦ ⟨↑↑l, ⋯⟩) ⟨hs✝, hs⟩ = ⟨Quotient.mk'' hs✝, hs⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Cycle α),
    x ∈ Finset.filter Nontrivial (Finset.map (Function.Embedding.subtype fun s ↦ s.Nodup) Finset.univ) ↔
      x.Nodup ∧ x.Nontrivial

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ MulAction.stabilizer Rˣ x = ⊥

Tactic:
rw [eq_bot_iff]
  intro g (hg : g.val • x = x)
  ext
  rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
p : R
hp : Prime p
⊢ p ^ 1 = p

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k = Nat.log 2 (2 ^ k)

Tactic:
by simp

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ nil, ∀ b ∈ nil, r a b) → Chain r nil

Tactic:
exact fun _ ↦ Cycle.Chain.nil r

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

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (leftRel (stabilizer G x)) g₁ g₂

Tactic:
leftRel_apply

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ g₁⁻¹ * g₂ ∈ stabilizer G x
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
h₂ : p = m
⊢ k + 2 ≠ 1

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 ≠ 0 → (primeFactorsList 0).prod = 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ 1 ≠ 0 → (primeFactorsList 1).prod = 1

Tactic:
by simp

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

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1

Tactic:
by simp

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

Goal state before:
pp: case inr.succ
n : ℕ
hn : n ≠ 0
k : ℕ
ih : (n ^ (k + 1)).primeFactors = n.primeFactors
⊢ (n ^ (k + 1 + 1)).primeFactors = n.primeFactors

Tactic:
| succ k ih =>

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

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
rw [← List.prod_append,
    List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
    Nat.prod_primeFactorsList hb.ne']

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

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

Tactic:
rw [Nat.mod_zero]
    exact Int.natAbs_natCast a

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
X : Type u_3
inst✝¹ : MulAction G X
inst✝ : MulAction.IsPretransitive G X
hi : H.index ≠ 0
⊢ Finite (MulAction.orbitRel.Quotient (↥H) X)

Tactic:
have := (MulAction.pretransitive_iff_subsingleton_quotient G X).1 inferInstance
  exact finite_quotient_of_finite_quotient_of_index_ne_zero hi

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ cast 1 = 1

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a + b).cast = a.cast + b.cast

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a * b).cast = a.cast * b.cast

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a - b).cast = a.cast - b.cast

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a : ZMod n
k : ℕ
⊢ (a ^ k).cast = a.cast ^ k

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (↑k).cast = ↑k

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0

pp: case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m

Tactic:
· simp [properDivisors]

Goal state after:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 1
⊢ 1 < n + 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.divisors ↔ n ≠ 0

Tactic:
by simp

Goal state after:
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:
val_add,

Goal state after:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ a.val + b.val = (a.val + b.val) % n + n
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝¹ : Semiring R
inst✝ : Fintype M
⊢ #R[M] = #R ^ card M

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Infinite M
inst✝ : Nontrivial R
⊢ #R[M] = max #R #M

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Cardinal

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Nonempty M
inst✝ : Infinite R
⊢ #R[M] = max #R #M

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∀ (a : ℕ × ℕ), ¬a.1 < a.1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by
  obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
  rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ n + 1 + 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ -1 * -1 = 1

Tactic:
by simp

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : { x // x.val.Coprime n }
val✝ : ZMod n
property✝ : val✝.val.Coprime n
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ unitOfCoprime (↑x).val ⋯) ⟨val✝, property✝⟩) = ⟨val✝, property✝⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, f x = f x

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k : ℕ
i : ℕ × ℕ
hi : i ∈ antidiagonal k
hk :
  ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) i ∈
    map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k)
⊢ ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) i ∈ (q ^ k).divisorsAntidiagonal

Tactic:
simp [Nat.mem_divisorsAntidiagonal, ← Finset.mem_antidiagonal.mp hi, pow_add, ne_zero_of_lt hq]

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

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
left_inv : LeftInverse inv_fun to_fun
⊢ Fintype.card (ZMod m × ZMod n) ≤ Fintype.card (ZMod (m * n))

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ 1 ∈ z.divisors ↔ z ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ -1 ∈ z.divisors ↔ z ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
by simp

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:
val_add,

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.val + (-b).val) % n = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n b : ℕ
⊢ 2 ≤ b + 2

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n✝ b : ℕ
x✝ : 1 < b + 2
⊢ 2 ≤ b + 2

Tactic:
by simp

Goal state after: