mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ Unitization.inl r = -↑a

Tactic:
ext

Goal state after:
case pos.fst
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ (Unitization.inl r).toProd.1 = (-↑a).toProd.1

case pos.snd
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
r : R
a : ↥s
hx : (algebraMap R A) r = -↑a
hr : r = 0
⊢ ↑(Unitization.inl r).toProd.2 = ↑(-↑a).toProd.2
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
rcases finite_or_infinite {a : α // a ≠ 0}

Goal state after:
case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Tactic:
ext

Goal state after:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) =
    (factor ⋯).comp (Quotient.mk (I ⊓ J))

Tactic:
ext

Goal state after:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I ⊓ J))) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))

Tactic:
ext

Goal state after:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))

Tactic:
ext

Goal state after:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) ↔ I = ⊥

Tactic:
constructor

Goal state after:
case mp
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ Bijective ⇑(mk I) → I = ⊥

case mpr
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ I = ⊥ → Bijective ⇑(mk I)
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
⊢ factorₐ R ⋯ = AlgHom.id R (A ⧸ I)

Tactic:
ext

Goal state after:
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✝
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
⊢ ((factorₐ R₁ hJK).comp (factorₐ R₁ hIJ)).comp (mkₐ R₁ I) = (factorₐ R₁ ⋯).comp (mkₐ R₁ I)

Tactic:
ext

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

Tactic:
ext

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

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Data.Fintype.List

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

Tactic:
constructor

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

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.Data.Fintype.List

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := Finset.univ.powerset.val
allPerms : Multiset (List α) := univSubsets.bind fun s ↦ s.val.lists
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) ↔ ¬m = n

Tactic:
constructor

Goal state after:
case mp
α : 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
⊢ (∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b) → ¬m = n

case mpr
α : 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
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) ↔ l.Nodup

Tactic:
constructor

Goal state after:
case refine_2.mp
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ (∃ a, a.val = ↑l) → l.Nodup

case refine_2.mpr
α : Type u_1
inst✝ : Fintype α
l : List α
⊢ l.Nodup → ∃ a, a.val = ↑l
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
h : I = J
⊢ (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ ⋯

Tactic:
ext

Goal state after:
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
h : I = J
a✝ : A ⧸ J
⊢ (quotientEquivAlgOfEq R₁ h).symm a✝ = (quotientEquivAlgOfEq R₁ ⋯) a✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J) = Ideal.Quotient.mk J

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h)).comp (quotQuotMk I J)) x✝ = (Ideal.Quotient.mk J) x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ (↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J) = quotQuotMk I J

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
x✝ : R
⊢ ((↑(quotQuotEquivQuotOfLE h).symm).comp (Ideal.Quotient.mk J)) x✝ = (quotQuotMk I J) x✝
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : 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 α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
constructor

Goal state after:
case cons.mp
α : 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 α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

case cons.mpr
α : 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 α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
rw [IsPeriodicPt, hco.comp_iterate]

Goal state after:
α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[1 + (n - 1)] x = x

Tactic:
Nat.add_sub_cancel' (by lia)

Goal state after:
case h
α : Type u_1
f : α → α
x : α
n : ℕ
left✝ : n > 0
h : IsPeriodicPt f n x
⊢ f^[n] x = x
Module: Mathlib.Dynamics.PeriodicPts.Defs

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

Tactic:
by
  rw [periodicOrbit_chain r]
  refine ⟨fun H n => ?_, fun H n _ => H n⟩
  rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),
    ← iterate_succ_apply, minimalPeriod_apply hx]
  exact H _ (mod_lt _ (minimalPeriod_pos_of_mem_periodicPts hx))

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
⊢ ⊤.toSubalgebra = ⊤

Tactic:
ext

Goal state after:
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
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤
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 T : StarSubalgebra R A
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
ext

Goal state after:
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 T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

Tactic:
rw [← Nat.card_prod, Nat.card_congr]
  apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)
  rw [QuotientGroup.preimage_image_mk]
  convert! Equiv.refl ↑(t * s)
  aesop (add simp [Set.mem_mul])

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

Goal state before:
pp: case cons
α : 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
⊢ (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
constructor

Goal state after:
case cons.left
α : 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
⊢ ∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup

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
⊢ Pairwise (Disjoint on permutations'Aux x) l.permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.prev l ⋯ = l.rotate (l.length - 1)

Tactic:
apply List.ext_getElem
  · simp
  · intro n hn hn'
    rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m ↦ m • y) g).1 ∈ orbit M y.1

Tactic:
exact mem_orbit _ _

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

Goal state before:
pp: M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m ↦ m • y) g).2 ∈ orbit M y.2

Tactic:
exact mem_orbit _ _

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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a

Tactic:
constructor

Goal state after:
case mp
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (∀ (m : M), m • a = a) → (orbit M a).Subsingleton
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ (h * g⁻¹) • ⟨(fun m ↦ m • a✝) g, yh⟩ = ⟨(fun m ↦ m • a✝) h, zh⟩

Tactic:
ext

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ : α
g : G
yh : (fun m ↦ m • a✝) g ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
h : G
zh : (fun m ↦ m • a✝) h ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ↑((h * g⁻¹) • ⟨(fun m ↦ m • a✝) g, yh⟩) = ↑⟨(fun m ↦ m • a✝) h, zh⟩
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk

Tactic:
ext

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x✝ : ↥(stabilizer G a)
⊢ ↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh)) x✝) = ↑((stabilizerEquivStabilizer hk) x✝)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
⊢ stabilizerEquivStabilizer ⋯ = MulEquiv.refl ↥(stabilizer G a)

Tactic:
ext

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
x✝ : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer ⋯) x✝) = ↑((MulEquiv.refl ↥(stabilizer G a)) x✝)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm

Tactic:
ext

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
x✝ : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer hg) x✝) = ↑((stabilizerEquivStabilizer ⋯).symm x✝)
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s

Tactic:
← mem_stabilizer_iff

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun x ↦ g • x) (g⁻¹ • x) = x

Tactic:
constructor

Goal state after:
case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

case h.right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x ↦ g • x) (g⁻¹ • x) = x
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
⊢ (↑[]).lists = {[]}

Tactic:
lists_coe,

Goal state after:
α : Type u_1
⊢ ↑[].cyclicPermutations = {[]}
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
g : Rˣ
hg : ↑g • x = x
⊢ g ∈ ⊥

Tactic:
ext

Goal state after:
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
g : Rˣ
hg : ↑g • x = x
⊢ ↑g = ↑1
Module: Mathlib.Algebra.IsPrimePow

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

Tactic:
constructor

Goal state after:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
constructor

Goal state after:
case inr.mp
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod ↔ ∃ a, a ∈ L ∧ p ∣ a

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod → ∃ a, a ∈ L ∧ p ∣ a

case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))

Tactic:
pairwise_cons

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : G
⊢ x✝ ∈ stabilizer G ↑1 ↔ x✝ ∈ H