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

Goal state before:
pp: F : Type u_1
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✝³ : FunLike F A B
inst✝² : AlgHomClass F R A B
inst✝¹ : StarHomClass F A B
f g : F
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
b : A
⊢ star ((↑φ).toRingHom b) ∈ (↑φ).range.carrier

Tactic:
;

Goal state after:
F : Type u_1
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✝³ : FunLike F A B
inst✝² : AlgHomClass F R A B
inst✝¹ : StarHomClass F A B
f g : F
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
b : A
⊢ star ((↑φ).toRingHom b) ∈ (↑φ).range.carrier
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card ((α ⧸ s) × ↥s)
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
⊢ x ∈ map φ ⊤

Tactic:
;

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✝⁴ : 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
⊢ x ∈ map φ ⊤
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 : ↑↑φ a = x
⊢ x ∈ φ.range

Tactic:
;

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✝⁴ : 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 : ↑↑φ a = x
⊢ x ∈ φ.range
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mk
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
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
;

Goal state after:
case mk
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
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }
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
k1l : k + 1 < (permutations'Aux x s).length
⊢ ⟨k, kl⟩ = ⟨k + 1, k1l⟩

Tactic:
;

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
k1l : k + 1 < (permutations'Aux x s).length
⊢ ⟨k, kl⟩ = ⟨k + 1, k1l⟩
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: case mk
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
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }.toStarSubalgebra
        h1).toNonUnitalStarSubalgebra =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
;

Goal state after:
case mk
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
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }.toStarSubalgebra
        h1).toNonUnitalStarSubalgebra =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.succ.cons
α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : (hd :: tl).Nodup
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 + 1 = (hd :: tl).length

Tactic:
· rw [nodup_iff_injective_get] at hl
    rw [length, Nat.succ_inj]
    exact Fin.val_eq_of_eq <| @hl ⟨k, Nat.lt_of_succ_lt <| by simpa using hk⟩
      ⟨tl.length, by simp⟩ (by grind)

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
⊢ (l.rotate (Nat.succ 0)).reverse.reverse[(l.rotate (Nat.succ 0)).reverse.length - 1 - (l.length - 1 - k)] =
    (l.rotate 1)[k]

Tactic:
· simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

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

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
x b✝ : α
h : x ∈ orbit (↥(Subgroup.map K.subtype (H.subgroupOf K))) b✝
⊢ x ∈ orbit (↥(H.subgroupOf K)) b✝

Tactic:
· rcases h with ⟨⟨gv, gp⟩, rfl⟩
    simp only
    simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
    refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
    · exact gp.2
    · simp only [Subgroup.mem_subgroupOf]
      exact gp.1

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

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

Tactic:
rcases h with (rfl | ⟨z, rfl⟩) <;> simp

Goal state after:
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
x✝ : ↥(stabilizer G a)
⊢ ↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh)) x✝) = ↑((stabilizerEquivStabilizer hk) x✝)

Tactic:
;

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 : α
x✝ : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer ⋯) x✝) = ↑((MulEquiv.refl ↥(stabilizer G a)) x✝)

Tactic:
;

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
x : ↥(stabilizer G b)
⊢ ↑((stabilizerEquivStabilizer hg).symm x) = ↑((stabilizerEquivStabilizer ⋯) x)

Tactic:
;

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 b)
⊢ ↑((stabilizerEquivStabilizer hg).symm x) = ↑((stabilizerEquivStabilizer ⋯) 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
x✝ : ↥(stabilizer G a)
⊢ ↑((stabilizerEquivStabilizer hg) x✝) = ↑((stabilizerEquivStabilizer ⋯).symm x✝)

Tactic:
;

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: α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
⊢ (if x✝ = a then b else if x✝ = b then a else x✝) ∈ S ↔ x✝ ∈ S

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
S : Set α
a b : α
a✝ : a ∈ S ↔ b ∈ S
x✝ : α
⊢ (if x✝ = a then b else if x✝ = b then a else x✝) ∈ S ↔ x✝ ∈ S
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
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
⊢ x ∈ g • s

Tactic:
use g⁻¹ • x

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

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 ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁ ↔ y ∈ Quot.mk (⇑(IsRotated.setoid α)) 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₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x hm = l₂.next y hm'

Tactic:
;

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
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.next x 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₁.next y hm = l₂.next y hm'

Tactic:
;

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₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'

Tactic:
;

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
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev 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:
;

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p

Tactic:
;

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
| p
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ a * l₁.prod

Tactic:
;

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ a * l₁.prod
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (hl : l ≠ []), Chain r ↑l ↔ IsChain r (l.getLast hl :: l)) →
      ∀ (hl : l ++ [a] ≠ []), Chain r ↑(l ++ [a]) ↔ IsChain r ((l ++ [a]).getLast hl :: (l ++ [a]))

Tactic:
intro m a _H _

Goal state after:
α : Type u_1
r : α → α → Prop
l m : List α
a : α
_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ IsChain r (m.getLast hl :: m)
hl✝ : m ++ [a] ≠ []
⊢ Chain r ↑(m ++ [a]) ↔ IsChain r ((m ++ [a]).getLast hl✝ :: (m ++ [a]))
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False

Tactic:
;

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]

Goal state after:
G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦↑a⟧ = ⟦↑b⟧
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝¹ : Group G
inst✝ : MulAction G X
x : X
H : Subgroup G
ω : Quotient (orbitRel G X)
⊢ LeftInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
by
    simp only [LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl

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
H : Subgroup G
ω : Quotient (orbitRel G X)
⊢ RightInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
simp only [Function.RightInverse, LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl

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

Goal state before:
pp: case mpr.inl
⊢ primeFactorsList 0 = []

pp: case mpr.inr
⊢ primeFactorsList 1 = []

Tactic:
· exact primeFactorsList_zero

Goal state after:
case mpr.inr
⊢ primeFactorsList 1 = []
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case H
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
· exact Fintype.card_pos_iff.mpr inferInstance

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors

Tactic:
;

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex H = K.relIndex H

Tactic:
inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (K ⊓ H).relIndex H = K.relIndex H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
;

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
;

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H

Tactic:
;

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Bijective ⇑f
H : Subgroup G
⊢ ⊥ ≤ H
Module: Mathlib.Data.ZMod.Basic

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

pp: case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)

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

Goal state after:
case succ
a n✝ : ℕ
⊢ (↑a).val = a % (n✝ + 1)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (J ⊓ L.subtype.range).relIndex (K ⊓ L.subtype.range) ≠ 0

Tactic:
inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (L.subtype.range ⊓ J).relIndex (K ⊓ L.subtype.range) ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (K ⊓ L.subtype.range) ≠ 0

Tactic:
inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
J K : Subgroup G
hJK : J.relIndex K ≠ 0
L : Subgroup G
⊢ (map L.subtype (comap L.subtype J)).relIndex (L.subtype.range ⊓ K) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Tactic:
;

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = ↑a

Tactic:
;

Goal state after:
n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = ↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ℤ
⊢ cast a = a

Tactic:
;

Goal state after:
case zero
a : ℤ
⊢ cast a = a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a

Tactic:
;

Goal state after:
case succ
a : ℤ
n✝ : ℕ
⊢ (↑a).cast = ↑↑↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) b → a = b

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) b → a = b
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) b → a = b

Tactic:
;

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) b → a = b
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.mk
n : ℕ
h : 0 ≤ n
out✝ : 0 ≠ 0
⊢ Injective cast

Tactic:
;

Goal state after:
case zero.mk
n : ℕ
h : 0 ≤ n
out✝ : 0 ≠ 0
⊢ Injective cast
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:
;

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

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