mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
this : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
⊢ w.head ∈ toSubgroup A B u

Tactic:
have := (d.compl u).rightCosetEquivalence_equiv_snd w.head

Goal state after:
G : Type u_1
inst✝² : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
this✝ : (p : Prop) → Decidable p := Classical.dec
g' : ↥(toSubgroup A B (-u)) × ↑(d.set u) := unitsSMulGroup φ d u w.head
h : w.head ∈ toSubgroup A B u → ∀ (x : G), ¬w.toList.head? = some (-u, x)
u' : ℤˣ
x : G
hx : w.toList.head? = some (u', x)
hmem : ↑(⋯.equiv w.head).2 ∈ toSubgroup A B u
this : RightCosetEquivalence (↑(toSubgroup A B u)) w.head ↑(⋯.equiv w.head).2
⊢ w.head ∈ toSubgroup A B u
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
this : f m ∣ f (s * (m₁, s₁).1)
⊢ f m ∣ n₁ ∨ f m ∣ n₂

pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
·

Goal state after:
case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
this : f m ∣ f (s * (m₁, s₁).1)
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ α

pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ?m.116 * (↑c.2 * a.1) ≤ ?m.116 * (↑a.2 * c.1)

Tactic:
·

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ α
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : M
⊢ f x = 1 → x = 1

pp: case refine_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : N
⊢ g x = 1 → x = 1

pp: case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
·

Goal state after:
case refine_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : M
⊢ f x = 1 → x = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ mk a✝¹ b✝¹ ≤ mk a✝ b✝ → mk a✝ b✝ ≤ mk a✝¹ b✝¹ → mk a✝¹ b✝¹ = mk a✝ b✝

pp: case f.H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a✝¹ : α
b✝¹ : ↥s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯

Tactic:
·

Goal state after:
case f.f
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝¹ : α
b✝¹ : ↥s
a✝ : α
b✝ : ↥s
⊢ mk a✝¹ b✝¹ ≤ mk a✝ b✝ → mk a✝ b✝ ≤ mk a✝¹ b✝¹ → mk a✝¹ b✝¹ = mk a✝ b✝
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : N
⊢ g x = 1 → x = 1

pp: case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
·

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
x : N
⊢ g x = 1 → x = 1
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
·

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
·

Goal state after:
case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
h : ¬Cancels u w
⊢ Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul.inl
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hia : Irreducible (f i) ∧ IsUnit (f a)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

pp: case mul.inr
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hai : Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
·

Goal state after:
case mul.inl
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hia : Irreducible (f i) ∧ IsUnit (f a)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_3
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
h : ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
⊢ f.range ⊓ g.range ≤ ⊥

Tactic:
intro x ⟨⟨y, hy⟩, z, hz⟩
    rwa [(h y z⁻¹ (by rw [map_inv, hy, hz, mul_inv_cancel])).1, map_one, eq_comm] at hy

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case mul.inr
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hai : Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'

Tactic:
·

Goal state after:
case mul.inr
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
inst✝ : WfDvdMonoid M
f : S.LocalizationMap N
a i : M
ha0 : a ≠ 0
hi : Irreducible i
ha : Irreducible (f a) → ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ a = u * m'
hai : Irreducible (f a) ∧ IsUnit (f i)
⊢ ∃ u m', IsUnit (f u) ∧ Irreducible m' ∧ i * a = u * m'
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w

pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1

Tactic:
·

Goal state after:
case refine_4
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (∀ (a : M), f a = 1 → a = 1) ∧ (∀ (a : N), g a = 1 → a = 1) ∧ f.range ⊓ g.range ≤ ⊥ →
    ∀ (a : M) (b : N), f a * g b = 1 → a = 1 ∧ b = 1
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c

pp: case h.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
·

Goal state after:
case h.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
·

Goal state after:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : x ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))
⊢ Prime x

pp: case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)

Tactic:
·

Goal state after:
case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
x : N
hx : x ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))
⊢ Prime x
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
·

Goal state after:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range

pp: case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
·

Goal state after:
case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup

pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
·

Goal state after:
case h.right.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
·

Goal state after:
case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)

Tactic:
·

Goal state after:
case h.refine_2
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
⊢ Associated (Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))).prod (f (m, s).1)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
·

Goal state after:
case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)