awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer (↑A : Set ↥K)
ih : (map K.subtype B).IsSubnormal
⊢ map K.subtype B ≤ normalizer (↑(map K.subtype A) : Set G)

Tactic:
exact le_trans (map_mono hN) (le_normalizer_map _)

Premises used: Subgroup.map_mono, Subgroup.le_normalizer_map, le_trans
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Hsn : H.IsSubnormal
Ksn : K.IsSubnormal
top : (map K.subtype ⊤).IsSubnormal
step :
  ∀ (A B : Subgroup ↥K) (h_le : A ≤ B) (hSubn : B.IsSubnormal) (hN : (A.subgroupOf B).Normal)
    (ih : (map K.subtype B).IsSubnormal), (map K.subtype A).IsSubnormal
⊢ (map K.subtype H).IsSubnormal

Tactic:
induction Hsn with
  | top =>
    rwa [← MonoidHom.range_eq_map, range_subtype]
  | step A B h_le hSubn hN ih =>
    refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]
    exact le_trans (map_mono hN) (le_normalizer_map _)

Premises used: MonoidHom.range_eq_map, Subgroup.IsSubnormal.step, Subgroup.IsSubnormal.top, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
⊢ (map K.subtype (H.subgroupOf K)).IsSubnormal

Tactic:
have key := Hsn.trans' Ksn
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
key : (map K.subtype (H.subgroupOf K)).IsSubnormal
rwa rwa₁ rwa₂ rwa₃ : ∀ (key : H.IsSubnormal), H.IsSubnormal
⊢ H.IsSubnormal

Tactic:
rwa [map_subgroupOf_eq_of_le HK] at key

Premises used: Subgroup.map_subgroupOf_eq_of_le
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
top : IsSubnormal.{u_2} (G := G') ⊤
⊢ (map f ⊤).IsSubnormal

Tactic:
rw [map_top_of_surjective f hf]

Premises used: Subgroup.map_top_of_surjective
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ IsSubnormal.{u_2} (G := G') ⊤

Tactic:
apply top

Premises used: Subgroup.IsSubnormal.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
step : Normal (G := ↥(map f K)) ((map f H).subgroupOf (map f K))
⊢ (map f H).IsSubnormal

Tactic:
apply step _ (map f K) (map_mono h_le) ih

Premises used: Subgroup.map, Subgroup.IsSubnormal.step, Subgroup.map_mono
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
⊢ K ≤ normalizer (↑H : Set G)

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
hN₁ : K ≤ normalizer (↑H : Set G)
⊢ (map f K).IsSubnormal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G)
ih : (map f K).IsSubnormal
⊢ Normal (G := ↥(map f K)) ((map f H).subgroupOf (map f K))

Tactic:
normal_subgroupOf_of_le_normalizer ((map_mono hN).trans (H.le_normalizer_map f))

Premises used: Subgroup.normal_subgroupOf_of_le_normalizer, Subgroup.map_mono, LE.le.trans, Subgroup.le_normalizer_map
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G)
ih : (map f K).IsSubnormal
⊢ Normal (G := ↥(map f K)) ((map f H).subgroupOf (map f K))

Tactic:
exact normal_subgroupOf_of_le_normalizer ((map_mono hN).trans (H.le_normalizer_map f))

Premises used: Subgroup.normal_subgroupOf_of_le_normalizer, Subgroup.map_mono, LE.le.trans, Subgroup.le_normalizer_map
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
hS : H.IsSubnormal
top : (map f ⊤).IsSubnormal
step :
  ∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal)
    (ih : (map f K).IsSubnormal), (map f H).IsSubnormal
⊢ (map f H).IsSubnormal

Tactic:
induction hS with
  | top =>
    rw [map_top_of_surjective f hf]
    apply top
  | step H K h_le hSubn hN ih =>
    apply step _ (map f K) (map_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    exact normal_subgroupOf_of_le_normalizer ((map_mono hN).trans (H.le_normalizer_map f))

Premises used: Subgroup.map_top_of_surjective, Subgroup.IsSubnormal.step, Subgroup.IsSubnormal.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
inst_1 : K.Normal
hS : H.IsSubnormal
⊢ IsSubnormal (map (QuotientGroup.mk' K) H)

Tactic:
hS.map (QuotientGroup.mk'_surjective K)

Premises used: Subgroup.IsSubnormal.map, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
⊢ (comap f ⊤).IsSubnormal

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
step : Normal (G := ↥(comap f K)) ((comap f H).subgroupOf (comap f K))
⊢ (comap f H).IsSubnormal

Tactic:
apply step _ (comap f K) (comap_mono h_le) ih

Premises used: Subgroup.IsSubnormal.step, Subgroup.comap_mono, Subgroup.comap
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
⊢ K ≤ normalizer (↑H : Set G')

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
hN₁ : K ≤ normalizer (↑H : Set G')
⊢ (comap f K).IsSubnormal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G')
ih : (comap f K).IsSubnormal
step : comap f K ≤ normalizer (↑(comap f H) : Set G)
⊢ Normal (G := ↥(comap f K)) ((comap f H).subgroupOf (comap f K))

Tactic:
rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer, Subgroup.comap_mono
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G')
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer (↑(comap f H) : Set G)

Tactic:
(comap_mono hN).trans (le_normalizer_comap f)

Premises used: Subgroup.le_normalizer_comap, Subgroup.comap_mono, LE.le.trans
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G')
ih : (comap f K).IsSubnormal
⊢ comap f K ≤ normalizer (↑(comap f H) : Set G)

Tactic:
exact (comap_mono hN).trans (le_normalizer_comap f)

Premises used: Subgroup.le_normalizer_comap, Subgroup.comap_mono, LE.le.trans
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
h : H'.IsSubnormal
top : (comap f ⊤).IsSubnormal
step :
  ∀ (H K : Subgroup G') (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal)
    (ih : (comap f K).IsSubnormal), (comap f H).IsSubnormal
⊢ (comap f H').IsSubnormal

Tactic:
induction h with
  | top => simp
  | step H K h_le hSubn hN ih =>
    apply step _ (comap f K) (comap_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
    exact (comap_mono hN).trans (le_normalizer_comap f)

Premises used: Subgroup.IsSubnormal.step, Subgroup.IsSubnormal.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.IsSubnormal
⊢ (H.subgroupOf K).IsSubnormal

Tactic:
hH.comap _

Premises used: Subgroup.subgroupOf, Subgroup.IsSubnormal.comap
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hH : H.IsSubnormal
hK : K.IsSubnormal
⊢ (H ⊓ K).IsSubnormal

Tactic:
simpa using hH.subgroupOf.trans' hK

Premises used: Subgroup.IsSubnormal.trans', Subgroup.IsSubnormal.subgroupOf
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
Γ : Type u_2
inst_1 : Group Γ
inst_2 : MulDistribMulAction Γ G
hS : H.IsSubnormal
g : Γ
⊢ (g • H).IsSubnormal

Tactic:
hS.map (MulAction.surjective g)

Premises used: Subgroup.IsSubnormal.map, MulAction.surjective
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
⊢ H.IsSubnormal

Tactic:
simp [eq_bot_of_subsingleton H]

Premises used: Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
obtain : ∀ (n : ℕ) (hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
⊢ IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)

Tactic:
obtain ⟨n, hn⟩ := y.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)
rw : IsUnit (HPow.hPow (α := P) ((g : (a : M) → P) x : P) n)
⊢ IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)

Tactic:
rw [← hn, g.map_pow]

Premises used: MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)
⊢ IsUnit (HPow.hPow (α := P) ((g : (a : M) → P) x : P) n)

Tactic:
IsUnit.pow n hg

Premises used: IsUnit.pow
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)
⊢ IsUnit (HPow.hPow (α := P) ((g : (a : M) → P) x : P) n)

Tactic:
exact IsUnit.pow n hg

Premises used: IsUnit.pow
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
a : M
⊢ Eq.{u_3 + 1} (α := P) ((lift x F hg : (a : N) → P) ((F : (a : M) → N) a : N) : P) ((g : (a : M) → P) a : P)

Tactic:
Submonoid.LocalizationMap.lift_eq _ _ _

Premises used: Submonoid.LocalizationMap.lift_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
⊢ (lift x F hg).comp (↑F : M →* N) = g

Tactic:
Submonoid.LocalizationMap.lift_comp _ _

Premises used: MonoidHomClass.toMonoidHom, Submonoid.LocalizationMap.lift_comp, Submonoid.LocalizationMap.AwayMap.lift
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
rw :
  mk' G (x * y) (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) ⋯) = 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := P) 1 1
⊢ HMul.hMul (α := P) ((G : (a : M) → P) x : P)
      (mk' G y (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) ⋯)) =
    1

Tactic:
rw [mul_mk'_eq_mk'_of_mul, mk'_self]

Premises used: Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul, Submonoid.LocalizationMap.mk'_self
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
obtain : ∀ (n : ℕ) (hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)), IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)

Tactic:
obtain ⟨n, hn⟩ := y.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
rw : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) ((fun (i : ℕ) ↦ i • x) n) : C)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)

Tactic:
rw [← hn]
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
dsimp : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (n • x) : C)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) ((fun (i : ℕ) ↦ i • x) n) : C)

Tactic:
dsimp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
rw : IsAddUnit (HSMul.hSMul (β := C) n ((g : (a : A) → C) x : C))
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (n • x) : C)

Tactic:
rw [g.map_nsmul]

Premises used: AddMonoidHom.map_nsmul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
⊢ IsAddUnit (HSMul.hSMul (β := C) n ((g : (a : A) → C) x : C))

Tactic:
IsAddUnit.map (nsmulAddMonoidHom n : C →+ C) hg

Premises used: nsmulAddMonoidHom, IsAddUnit.map
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
⊢ IsAddUnit (HSMul.hSMul (β := C) n ((g : (a : A) → C) x : C))

Tactic:
exact IsAddUnit.map (nsmulAddMonoidHom n : C →+ C) hg

Premises used: nsmulAddMonoidHom, IsAddUnit.map
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
A : Type u_4
inst : AddCommMonoid A
x : A
B : Type u_5
inst_1 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_2 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
a : A
⊢ Eq.{u_6 + 1} (α := C) ((lift x F hg : (a : B) → C) ((F : (a : A) → B) a : B) : C) ((g : (a : A) → C) a : C)

Tactic:
AddSubmonoid.LocalizationMap.lift_eq _ _ _

Premises used: AddSubmonoid.LocalizationMap.lift_eq
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
A : Type u_4
inst : AddCommMonoid A
x : A
B : Type u_5
inst_1 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_2 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
⊢ (lift x F hg).comp (↑F : A →+ B) = g

Tactic:
AddSubmonoid.LocalizationMap.lift_comp _ _

Premises used: AddMonoidHomClass.toAddMonoidHom, AddSubmonoid.LocalizationMap.AwayMap.lift, AddSubmonoid.LocalizationMap.lift_comp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
rw :
  mk' G (x + y)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) ⋯) =
    0
rw₁ rw₂ : Eq.{u_6 + 1} (α := C) 0 0
⊢ HAdd.hAdd (α := C) ((G : (a : A) → C) x : C)
      (mk' G y
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) ⋯)) =
    0

Tactic:
rw [add_mk'_eq_mk'_of_add, mk'_self]

Premises used: AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add, AddSubmonoid.LocalizationMap.mk'_self
-- Module: Mathlib.GroupTheory.MonoidLocalization.Away
Goal:
M : Type u_1
inst : CommMonoid M
x : M
⊢ Eq (α := (x_1 : M) → (y : ↥(Submonoid.powers x)) → Localization (Submonoid.powers x)) mk
    (Submonoid.LocalizationMap.mk' (monoidOf x))

Tactic:
simp [Localization.mk_eq_monoidOf_mk']

Premises used: Localization.mk_eq_monoidOf_mk'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
refine_1 :
  ∀ {x y z : M × ↥S},
    (∃ (c : ↥S), (↑c : M) * ((↑y.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * y.1)) →
      (∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * y.1) = (↑c : M) * ((↑y.2 : M) * z.1)) →
        ∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * x.1) = (↑c : M) * ((↑x.2 : M) * z.1)
refine_2 :
  ∀ {w x y z : M × ↥S},
    (∃ (c : ↥S), (↑c : M) * ((↑x.2 : M) * w.1) = (↑c : M) * ((↑w.2 : M) * x.1)) →
      (∃ (c : ↥S), (↑c : M) * ((↑z.2 : M) * y.1) = (↑c : M) * ((↑y.2 : M) * z.1)) →
        ∃ (c : ↥S), (↑c : M) * ((↑(x * z).2 : M) * (w * y).1) = (↑c : M) * ((↑(w * y).2 : M) * (x * z).1)
⊢ Con (M × ↥S)

Tactic:
refine
    { r := fun a b : M × S ↦ ∃ c : S, ↑c * (↑b.2 * a.1) = c * (a.2 * b.1)
      iseqv := ⟨fun a ↦ ⟨1, rfl⟩, fun ⟨c, hc⟩ ↦ ⟨c, hc.symm⟩, ?_⟩
      mul' := ?_ }
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
h : (↑(t₂ * t₁ * b.2) : M) * ((↑c.2 : M) * a.1) = (↑(t₂ * t₁ * b.2) : M) * ((↑a.2 : M) * c.1)
⊢ ∃ (c_1 : ↥S), (↑c_1 : M) * ((↑c.2 : M) * a.1) = (↑c_1 : M) * ((↑a.2 : M) * c.1)

Tactic:
use t₂ * t₁ * b.2

Premises used: Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
h : (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑a.2 : M) * c.1)
⊢ (↑(t₂ * t₁ * b.2) : M) * ((↑c.2 : M) * a.1) = (↑(t₂ * t₁ * b.2) : M) * ((↑a.2 : M) * c.1)

Tactic:
simp only [Submonoid.coe_mul]

Premises used: Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
⊢ (↑t₂ : M) * (↑t₁ : M) * (↑b.2 : M) * ((↑c.2 : M) * a.1) = (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑b.2 : M) * a.1))

Tactic:
ac_rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Basic
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : (↑t₁ : M) * ((↑b.2 : M) * a.1) = (↑t₁ : M) * ((↑a.2 : M) * b.1)
t₂ : ↥S
ht₂ : (↑t₂ : M) * ((↑c.2 : M) * b.1) = (↑t₂ : M) * ((↑b.2 : M) * c.1)
rw :
  (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑a.2 : M) * b.1)) = (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1))
⊢ (↑t₂ : M) * (↑c.2 : M) * ((↑t₁ : M) * ((↑b.2 : M) * a.1)) = (↑t₁ : M) * (↑a.2 : M) * ((↑t₂ : M) * ((↑c.2 : M) * b.1))

Tactic:
rw [ht₁]