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

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

pp: case «1»
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]
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «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]
j : Fin 2
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
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]
j : Fin 2
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

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

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

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, ⋯⟩)

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

Tactic:
<;>

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

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

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, ⋯⟩)

case «1».«1»
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) ⟨1, ⋯⟩
⊢ (IsCoprime on f) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ (¬¬∃ m n_1, m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n

Tactic:
Classical.not_not

Goal state after:
n : ℕ
h : 2 ≤ n
⊢ (∃ m n_1, m < n ∧ n_1 < n ∧ m * n_1 = n) ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p

pp: case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p

Tactic:
<;>

Goal state after:
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p

case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
⊢ univSubsets = ↑Finset.univ.powerset.toList

pp: case h.right
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
⊢ List.Pairwise (Function.onFun _root_.Disjoint fun s ↦ s.val.lists) Finset.univ.powerset.toList

Tactic:
· simp only [Finset.coe_toList]
      rfl

Goal state after:
case h.right
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
⊢ List.Pairwise (Function.onFun _root_.Disjoint fun s ↦ s.val.lists) Finset.univ.powerset.toList
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
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : (algebraMap R A) (r₁ - r₂) ∈ P
⊢ r₁ • a₁ ≈ r₂ • a₂

Tactic:
map_sub

Goal state after:
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
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
this : (algebraMap R A) r₁ - (algebraMap R A) r₂ ∈ P
⊢ r₁ • a₁ ≈ r₂ • a₂
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Fintype { l // l.Nodup }

Tactic:
by
  refine Fintype.subtype ?_ ?_
  · let univSubsets := ((Finset.univ : Finset α).powerset.1 : (Multiset (Finset α)))
    let allPerms := Multiset.bind univSubsets (fun s => (Multiset.lists s.1))
    refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
    simp only [Multiset.lists_nodup_finset, implies_true, true_and]
    unfold Multiset.Pairwise
    use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))
    constructor
    · simp only [Finset.coe_toList]
      rfl
    · -- Unfold `List.Nodup` in the type of the proof term to make it match with the goal.
      convert dsimp% [List.Nodup] Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))
        with m n
      simp only [_root_.Disjoint]
      rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
      have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
      rw [_root_.Disjoint] at this
      rw [this, List.disjoint_iff_ne]
      constructor
      · intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp
      · intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb
  · intro l
    simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset,
      Finset.subset_univ, Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]
    constructor
    · intro h
      rcases h with ⟨f, hf⟩
      convert! f.nodup
      rw [hf]
      rfl
    · intro h
      exact CanLift.prf _ h

Goal state after:
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 ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd

pp: case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd ++ r = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd ++ r = (permutationsAux2 t ts r (head✝ :: tail✝) f).snd

Tactic:
<;>

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

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd ++ r = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd ++ r = (permutationsAux2 t ts r (head✝ :: tail✝) f).snd
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 T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
← mem_toSubalgebra,

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 T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S.toSubalgebra ↔ x ∈ T
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 T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S.toSubalgebra ↔ x ∈ T

Tactic:
← mem_toSubalgebra,

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 T : StarSubalgebra R A
h : S.toSubalgebra = T.toSubalgebra
x : A
⊢ x ∈ S.toSubalgebra ↔ x ∈ T.toSubalgebra
Module: Mathlib.Data.List.Permutation

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

pp: case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd.length = tail✝.length
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd.length = (head✝ :: tail✝).length

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd.length = [].length

case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd.length = tail✝.length
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd.length = (head✝ :: tail✝).length
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
rw [IsPeriodicPt, hco.comp_iterate] at hfg
  exact hfg.left_of_comp hg

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

Goal state before:
pp: case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

pp: case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), minimalPeriod f x ∣ n ↔ minimalPeriod g y ∣ n

Tactic:
dvd_right_iff_eq

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

Goal state before:
pp: case h₁
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬minimalPeriod f x ∣ p ^ k

pp: case h₂
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)

Tactic:
<;>

Goal state after:
case h₁
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ ¬minimalPeriod f x ∣ p ^ k

case h₂
α : Type u_1
f : α → α
x : α
p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x ∣ p ^ (k + 1)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
hxy : x ∈ [y]
⊢ [y].prev x hxy = [y].getLast ⋯

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
head✝ : α
tail✝ : List α
hxy : x ∈ y :: head✝ :: tail✝
⊢ (y :: head✝ :: tail✝).prev x hxy = (y :: head✝ :: tail✝).getLast ⋯

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
hxy : x ∈ [y]
⊢ [y].prev x hxy = [y].getLast ⋯

case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
hx : x = y
head✝ : α
tail✝ : List α
hxy : x ∈ y :: head✝ :: tail✝
⊢ (y :: head✝ :: tail✝).prev x hxy = (y :: head✝ :: tail✝).getLast ⋯
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n

Tactic:
rw [length_cons] at hn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + 1 + tl.length) % (tl.length + 1) = n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn : n < (hd :: tl).length
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + tl.length + 1) % (tl.length + 1) = n

Tactic:
rw [length_cons] at hn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ (n + tl.length + 1) % (tl.length + 1) = n
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x y : α
⊢ take 2 [x, y].permutations = [[x, y], [y, x]]

pp: case cons
α : Type u_1
x y head✝ : α
tail✝ : List α
tail_ih✝ : take 2 (x :: y :: tail✝).permutations = [x :: y :: tail✝, y :: x :: tail✝]
⊢ take 2 (x :: y :: head✝ :: tail✝).permutations = [x :: y :: head✝ :: tail✝, y :: x :: head✝ :: tail✝]

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
x y : α
⊢ take 2 [x, y].permutations = [[x, y], [y, x]]

case cons
α : Type u_1
x y head✝ : α
tail✝ : List α
tail_ih✝ : take 2 (x :: y :: tail✝).permutations = [x :: y :: tail✝, y :: x :: tail✝]
⊢ take 2 (x :: y :: head✝ :: tail✝).permutations = [x :: y :: head✝ :: tail✝, y :: x :: head✝ :: tail✝]
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ⋯⟩ ∈ H.subgroupOf K

Tactic:
simp only [Subgroup.mem_subgroupOf]
      exact gp.1

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

Goal state before:
pp: case refine_1
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' [])

pp: case refine_2
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), motive (Quotient.mk'' tail) → motive (Quotient.mk'' (head :: tail))

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ motive (Quotient.mk'' [])

case refine_2
α : Type u_1
motive : Cycle α → Prop
s : Cycle α
nil : motive Cycle.nil
cons : ∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)
l : List α
⊢ ∀ (head : α) (tail : List α), motive (Quotient.mk'' tail) → motive (Quotient.mk'' (head :: tail))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.inl
α : Type u_1
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [] → x = y

pp: case h.inr
α : Type u_1
z : α
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → x = y

Tactic:
<;>

Goal state after:
case h.inl
α : Type u_1
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [] → x = y

case h.inr
α : Type u_1
z : α
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → x = y
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

Tactic:
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy

Goal state after:
case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝ : x✝ = a
⊢ b ∈ S ↔ x✝ ∈ S

pp: case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : x✝ = b
⊢ a ∈ S ↔ x✝ ∈ S

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : ¬x✝ = b
⊢ x✝ ∈ S ↔ x✝ ∈ S

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝ : x✝ = a
⊢ b ∈ S ↔ x✝ ∈ S

case pos
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : x✝ = b
⊢ a ∈ S ↔ x✝ ∈ S

case neg
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
h✝¹ : ¬x✝ = a
h✝ : ¬x✝ = b
⊢ x✝ ∈ S ↔ x✝ ∈ S
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
hab : (IsRotated.setoid α) [] b
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) b
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
hab : (IsRotated.setoid α) [] b
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

case cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : List α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) b
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c = b ∨ c ∈ l
⊢ r b c

pp: case cons.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hc : c = a ∨ c ∈ l
hb : b ∈ l
⊢ r b c

Tactic:
<;>

Goal state after:
case cons.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c = b ∨ c ∈ l
⊢ r b c

case cons.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hc : c = a ∨ c ∈ l
hb : b ∈ l
⊢ r b c
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k : ℕ
⊢ ∀ {p : ℕ}, p ∈ (k + 2).primeFactorsList → Prime p

Tactic:
intro p h

Goal state after:
n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
⊢ Prime p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp
n : ℕ
⊢ n.primeFactorsList = [] → n = 0 ∨ n = 1

pp: case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactorsList = []

Tactic:
<;>

Goal state after:
case mp
n : ℕ
⊢ n.primeFactorsList = [] → n = 0 ∨ n = 1

case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactorsList = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case zero
p : ℕ
⊢ p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ 0 ≠ 0

pp: case succ
p n✝ : ℕ
⊢ p ∈ (n✝ + 1).primeFactorsList ↔ Prime p ∧ p ∣ n✝ + 1 ∧ n✝ + 1 ≠ 0

Tactic:
<;>

Goal state after:
case zero
p : ℕ
⊢ p ∈ primeFactorsList 0 ↔ Prime p ∧ p ∣ 0 ∧ 0 ≠ 0

case succ
p n✝ : ℕ
⊢ p ∈ (n✝ + 1).primeFactorsList ↔ Prime p ∧ p ∣ n✝ + 1 ∧ n✝ + 1 ≠ 0
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mpr.inl
⊢ primeFactors 0 = ∅

pp: case mpr.inr
⊢ primeFactors 1 = ∅

Tactic:
<;>

Goal state after:
case mpr.inl
⊢ primeFactors 0 = ∅

case mpr.inr
⊢ primeFactors 1 = ∅
Module: Mathlib.Data.Nat.Factors

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

pp: case refine_2.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
<;>

Goal state after:
case refine_2.inl
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ a.primeFactorsList
⊢ Prime p

case refine_2.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp' : p ∈ b.primeFactorsList
⊢ Prime p
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ ↑a.cast = a

Tactic:
simp [ZMod.cast, ZMod]

Goal state after: