mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ ∃ x, l₁ ++ [t] ++ ts = l₁ ++ t :: ts

Tactic:
simpa using

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 α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ l₁ ~ is
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
⊢ x ∈ (z :: zs).dropLast

Tactic:
simpa using

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.Cycle

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

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x = z ∨ x ∈ zs
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✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using

Goal state after:
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✝⁵ : StarModule R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R B
ι : Sort u_5
inst✝ : Nonempty ι
f : A →⋆ₐ[R] B
hf : Function.Injective ⇑f
s : ι → StarSubalgebra R A
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
y z : α
xs : List α
x : α
h : x ∈ y :: z :: xs
hx : ¬x = y
⊢ x ∈ z :: xs

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
y z : α
xs : List α
x : α
h : x ∈ y :: z :: xs
hx : ¬x = y
⊢ x = z ∨ x ∈ xs
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
⊢ ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n

Tactic:
simpa using

Goal state after:
α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
⊢ ∃ m n, f^[m] x = f^[n] x ∧ ¬m = n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n✝ + 1] = (y :: s).insertIdx (n✝ + 1) x

Tactic:
simpa using

Goal state after:
case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x s)[n✝] = s.insertIdx n✝ x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: x :: l) (map (cons x) (permutations'Aux x l)) + 1 =
    (takeWhile (fun x_1 ↦ decide (x = x_1)) (x :: l)).length + 1

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ (x : α), count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
x : α
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1
Module: Mathlib.Data.List.Permutation

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

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : (permutations'Aux x s).length = s.length + 1
⊢ (permutations'Aux x s).length = s.length + 1
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
⊢ s.length = t.length

Tactic:
simpa using

Goal state after:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.length = t.length
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(QuotientGroup.mk ⁻¹' QuotientGroup.mk '' t)

Tactic:
QuotientGroup.preimage_image_mk

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' t)
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 ⋯
⊢ k.succ < (hd :: tl).length

Tactic:
simpa using

Goal state after:
α : 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 ⋯
⊢ k < tl.length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ k < (permutations'Aux x s).length

Tactic:
simpa using

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
⊢ k ≤ s.length
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
⊢ k + 1 < (permutations'Aux x s).length

Tactic:
simpa using

Goal state after:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get ⟨k, hk⟩ = x
kl : k < (permutations'Aux x s).length
⊢ k < s.length
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : Semiring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : StarModule R A
ι : Type u_3
inst✝ : Nonempty ι
S : ι → StarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : Semiring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : StarModule R A
ι : Type u_3
inst✝ : Nonempty ι
S : ι → StarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ (a : A) (x : ι), a ∈ ↑(S x) → ∀ (a_1 : A) (x : ι), a_1 ∈ ↑(S x) → a * a_1 = a_1 * a
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x ∈ z :: l

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y z : α
h : x ∈ y :: z :: l
hy : x ≠ y
hz : x ≠ z
⊢ x = z ∨ x ∈ l
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
⊢ False

Tactic:
obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'

Goal state after:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x1 x2 ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get ⟨n, hn⟩ = a
⊢ False
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.prev l ⋯).length) (h₂ : i < (l.rotate (l.length - 1)).length),
    (pmap l.prev l ⋯)[i] = (l.rotate (l.length - 1))[i]

Tactic:
intro n hn hn'
    rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < (pmap l.next l ⋯).length

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ k < l.length
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
a✝ : α
⊢ Finite ↑(orbitRel.Quotient.orbit (Quotient.mk'' a✝))

Tactic:
simpa using

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Finite G
inst✝ : Finite Ω
a✝ : α
⊢ (orbit G a✝).Finite
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
h : ∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
⊢ a ∈ S ↔ b ∈ S
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ tl = []

Tactic:
simpa using

Goal state after:
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ tl = []
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
⊢ ↑l₁.cyclicPermutations = ↑l₂.cyclicPermutations

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
⊢ l₁.cyclicPermutations ~ l₂.cyclicPermutations
Module: Mathlib.Data.List.Cycle

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : { l // l.Nodup }
⊢ (↑l).Nodup
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
⊢ y ∈ l₁ ↔ y ∈ l₂
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.next y hm = l₂.next y hm'

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.next y hm = l₂.next y hm'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.prev y hm = l₂.prev y hm'

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
y : α
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
hm : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
he' : hm ≍ hm'
⊢ l₁.prev y hm = l₂.prev y hm'
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.primeFactorsList ~ b.primeFactorsList
⊢ a = b

Tactic:
simpa using

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.primeFactorsList ~ b.primeFactorsList
⊢ a = b
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ primeFactors 1 ↔ a✝ ∈ ∅

Tactic:
simpa using

Goal state after:
a✝ : ℕ
⊢ Prime a✝ → ¬a✝ = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)

Tactic:
simpa using

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p → (p ∣ a * b ↔ p ∣ a ∨ p ∣ b)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), b * a ∈ H ∨ b ∈ H
b : G
h' : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), b * a ∈ H ∨ b ∈ H
b : G
h' : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), a * b ∈ H ∨ b ∈ H
b : G
h' : a * b ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∉ H ∧ ∀ (b : G), a * b ∈ H ∨ b ∈ H
b : G
h' : a * b ∈ H ∧ b ∈ H
⊢ a ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.relIndex ⊥ = 1

Tactic:
rw [relIndex, subgroupOf_bot_eq_top, index_top]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
b : G
h : b * a ∈ H
⊢ b ∈ H

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
b : G
h : b * a ∈ H
⊢ b ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∈ H
b : G
h : b * a ∈ H
⊢ b ∈ H

Tactic:
simpa using mul_mem h (inv_mem ha')

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
b : G
h : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H

Tactic:
simpa using

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ∨ b ∈ H
ha' : a ∉ H
b : G
h : b * a ∈ H ∧ b ∈ H
⊢ a ∈ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n ↦ ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ n₁ = n₂
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relIndex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]

Tactic:
simpa using

Goal state after:
a b c : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD c]
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝² : Ring R✝
n : ℕ
R : Type u_2
inst✝¹ : Ring R
inst✝ : Module (ZMod n) R
r : ZMod n
x : R
⊢ r • 1 * x = r • x ∧ x * r • 1 = r • x

Tactic:
by
    obtain _ | n := n
    · obtain rfl : ((inferInstance : Module ℤ R)) = ‹_› := Subsingleton.elim _ _
      simp [ZMod, Int.cast_comm]
    · obtain ⟨r, rfl⟩ := ZMod.natCast_zmod_surjective r
      simp [Nat.cast_smul_eq_nsmul, Nat.cast_comm]

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

Goal state before:
pp: case h₁
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i ≤ x

Tactic:
simpa using

Goal state after:
case h₁
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i ≤ x
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simpa using

Goal state after:
case mpr
a b : ℕ
hab : a ≠ 0 ∧ b ≠ 0
⊢ a ≤ a * b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a * b).val ≤ a.val * b.val

Tactic:
val_mul

Goal state after:
n : ℕ
a b : ZMod n
⊢ a.val * b.val % n ≤ a.val * b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
val_mul

Goal state after:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case bc
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 : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i < x

Tactic:
simpa using

Goal state after:
case bc
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 : 1 < ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i < x
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1

Tactic:
simpa using

Goal state after:
case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i ∈ range n, x ^ i ≤ 0

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i ∈ range n, x ^ i ≤ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
hdvd : m ∣ n
⊢ m = 1

Tactic:
simpa using

Goal state after:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hm : m < n
hdvd : m ∣ n
⊢ m = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.zero
⊢ Subsingleton (ZMod 0) → 0 = 1

Tactic:
simpa using

Goal state after:
case mp.zero
⊢ ¬Subsingleton ℤ
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
simpa using

Goal state after:
case mp.succ.succ
n : ℕ
⊢ ¬Subsingleton (Fin (n + 1 + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
simpa using

Goal state after:
n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (x_1 : ℤ), x_1 • x ∈ K
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ x + x = 0

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ x + x = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y z : G
⊢ x + y + (y + z) = x + z

Tactic:
simpa using

Goal state after:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y z : G
⊢ x + y + (y + z) = x + z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k

Tactic:
simpa using

Goal state after:
case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
n : ℕ
⊢ (fun p ↦ p.1.val + N * p.2) ((fun n ↦ (↑n, n / N)) n) = n

Tactic:
simpa using

Goal state after:
N : ℕ
inst✝ : NeZero N
n : ℕ
⊢ n % N + N * (n / N) = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.hxb
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b

Tactic:
exact w₁ d List.mem_cons_self

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

Goal state before:
pp: case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0

Tactic:
simpa using

Goal state after:
case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ ¬d = 0