[GOAL]
⊢ (fun n => Real.log ↑n) 0 = 0
[PROOFSTEP]
simp
[GOAL]
⊢ ↑Λ 1 = 0
[PROOFSTEP]
simp [vonMangoldt_apply]
[GOAL]
n : ℕ
⊢ 0 ≤ ↑Λ n
[PROOFSTEP]
rw [vonMangoldt_apply]
[GOAL]
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑(minFac n) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑(minFac n)
[PROOFSTEP]
exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))
[GOAL]
case neg
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ ↑Λ (n ^ k) = ↑Λ n
[PROOFSTEP]
simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]
[GOAL]
p : ℕ
hp : Prime p
⊢ ↑Λ p = Real.log ↑p
[PROOFSTEP]
rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
[GOAL]
n : ℕ
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
[PROOFSTEP]
rcases eq_or_ne n 1 with (rfl | hn)
[GOAL]
case inl
⊢ ↑Λ 1 ≠ 0 ↔ IsPrimePow 1
[PROOFSTEP]
simp [not_isPrimePow_one]
[GOAL]
case inr
n : ℕ
hn : n ≠ 1
⊢ ↑Λ n ≠ 0 ↔ IsPrimePow n
[PROOFSTEP]
exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff
[GOAL]
n : ℕ
⊢ ∑ i in divisors n, ↑Λ i = Real.log ↑n
[PROOFSTEP]
refine' recOnPrimeCoprime _ _ _ n
[GOAL]
case refine'_1
n : ℕ
⊢ ∑ i in divisors 0, ↑Λ i = Real.log ↑0
[PROOFSTEP]
simp
[GOAL]
case refine'_2
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → ∑ i in divisors (p ^ n), ↑Λ i = Real.log ↑(p ^ n)
[PROOFSTEP]
intro p k hp
[GOAL]
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ i in divisors (p ^ k), ↑Λ i = Real.log ↑(p ^ k)
[PROOFSTEP]
rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', pow_zero, vonMangoldt_apply_one]
[GOAL]
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ k in range k, ↑Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p
[PROOFSTEP]
simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
[GOAL]
case refine'_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          ∑ i in divisors a, ↑Λ i = Real.log ↑a →
            ∑ i in divisors b, ↑Λ i = Real.log ↑b → ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
[PROOFSTEP]
intro a b ha' hb' hab ha hb
[GOAL]
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ i in divisors a, ↑Λ i = Real.log ↑a
hb : ∑ i in divisors b, ↑Λ i = Real.log ↑b
⊢ ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
[PROOFSTEP]
simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
[GOAL]
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ a in filter (fun a => IsPrimePow a) (divisors a), Real.log ↑(minFac a) = Real.log ↑a
hb : ∑ a in filter (fun a => IsPrimePow a) (divisors b), Real.log ↑(minFac a) = Real.log ↑b
⊢ ∑ a in filter (fun a => IsPrimePow a) (divisors (a * b)), Real.log ↑(minFac a) = Real.log ↑(a * b)
[PROOFSTEP]
rw [mul_divisors_filter_prime_pow hab, filter_union, sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb,
  Nat.cast_mul, Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]
[GOAL]
⊢ Λ * ↑ζ = log
[PROOFSTEP]
ext n
[GOAL]
case h
n : ℕ
⊢ ↑(Λ * ↑ζ) n = ↑log n
[PROOFSTEP]
rw [coe_mul_zeta_apply, vonMangoldt_sum]
[GOAL]
case h
n : ℕ
⊢ Real.log ↑n = ↑log n
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑ζ * Λ = log
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ Λ * ↑ζ = log
[PROOFSTEP]
simp
[GOAL]
⊢ log * ↑μ = Λ
[PROOFSTEP]
rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
[GOAL]
⊢ ↑μ * log = Λ
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ log * ↑μ = Λ
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ∑ d in divisors n, ↑(↑μ d) * ↑log d = -↑Λ n
[PROOFSTEP]
simp only [← log_mul_moebius_eq_vonMangoldt, mul_comm log, mul_apply, log_apply, intCoe_apply, ← Finset.sum_neg_distrib,
  neg_mul_eq_mul_neg]
[GOAL]
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * -Real.log ↑x.snd
[PROOFSTEP]
rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]
[GOAL]
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
[PROOFSTEP]
have :
  (∑ i : ℕ in n.divisors, (μ i : ℝ) * -Real.log (n / i : ℕ)) =
    ∑ i : ℕ in n.divisors, ((μ i : ℝ) * Real.log i - μ i * Real.log n) :=
  by
  apply sum_congr rfl
  simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne.def, neg_inj, mem_divisors]
  intro m mn hn
  have : (m : ℝ) ≠ 0 := by
    rw [cast_ne_zero]
    rintro rfl
    exact hn (by simpa using mn)
  rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
[GOAL]
n : ℕ
⊢ ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors n → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
[PROOFSTEP]
simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne.def, neg_inj, mem_divisors]
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
[PROOFSTEP]
intro m mn hn
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
[PROOFSTEP]
have : (m : ℝ) ≠ 0 := by
  rw [cast_ne_zero]
  rintro rfl
  exact hn (by simpa using mn)
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑m ≠ 0
[PROOFSTEP]
rw [cast_ne_zero]
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False
[PROOFSTEP]
exact hn (by simpa using mn)
[GOAL]
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0
[PROOFSTEP]
simpa using mn
[GOAL]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
[PROOFSTEP]
rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
[GOAL]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
[PROOFSTEP]
rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self, moebius_mul_coe_zeta]
[GOAL]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
rcases eq_or_ne n 1 with (hn | hn)
[GOAL]
case inl
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
hn : n = 1
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
simp [hn]
[GOAL]
case inr
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
hn : n ≠ 1
⊢ ↑(↑1 n) * Real.log ↑n = 0
[PROOFSTEP]
simp [hn]
[GOAL]
⊢ ↑Λ 0 ≤ Real.log ↑0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ↑Λ (n + 1) ≤ Real.log ↑(n + 1)
[PROOFSTEP]
rw [← vonMangoldt_sum]
[GOAL]
n : ℕ
⊢ ↑Λ (n + 1) ≤ ∑ i in divisors (n + 1), ↑Λ i
[PROOFSTEP]
exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg) (mem_divisors_self _ n.succ_ne_zero)
[GOAL]
n : ℕ
⊢ ∀ (i : ℕ), i ∈ divisors (n + 1) → 0 ≤ ↑Λ i
[PROOFSTEP]
exact fun _ _ => vonMangoldt_nonneg


[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ ↑(closure S)
[PROOFSTEP]
rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s⁻¹ ∈ closure S
[PROOFSTEP]
exact subset_closure (mem_inv.mp hs)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
refine'
  closure_induction hx (fun x hx => Submonoid.closure_mono (subset_union_left S S⁻¹) (Submonoid.subset_closure hx))
    (Submonoid.one_mem _) (fun x y hx hy => Submonoid.mul_mem _ hx hy) fun x hx => _
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
x✝ : G
hx✝ : x✝ ∈ (closure S).toSubmonoid
x : G
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
[PROOFSTEP]
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
[GOAL]
case refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
[PROOFSTEP]
simp only [true_and_iff, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
⊢ closure s⁻¹ = closure s
[PROOFSTEP]
simp only [← toSubmonoid_eq, closure_toSubmonoid, inv_inv, union_comm]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ ⨆ (i : ι), S i
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
rw [iSup_eq_closure] at hx
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
[PROOFSTEP]
refine' closure_induction'' hx (fun x hx => _) (fun x hx => _) h1 hmul
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
[GOAL]
case refine'_1.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
[PROOFSTEP]
exact hp _ _ hi
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
⊢ C x⁻¹
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
[GOAL]
case refine'_2.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
hx✝ : x✝ ∈ closure (⋃ (i : ι), ↑(S i))
hp : ∀ (i : ι) (x : G), x ∈ S i → C x
h1 : C 1
hmul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ (i : ι), ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x⁻¹
[PROOFSTEP]
exact hp _ _ (inv_mem hi)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ C x hx
[PROOFSTEP]
suffices : ∃ h, C x h
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
this : ∃ h, C x h
⊢ C x hx
case this
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
[PROOFSTEP]
exact this.snd
[GOAL]
case this
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ ∃ h, C x h
[PROOFSTEP]
refine' iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => _) _ fun x y => _
[GOAL]
case this.refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx✝ : x✝ ∈ ⨆ (i : ι), S i
i : ι
x : G
hx : x ∈ S i
⊢ (fun x => ∃ h, C x h) x
[PROOFSTEP]
exact ⟨_, hp i _ hx⟩
[GOAL]
case this.refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x : G
hx : x ∈ ⨆ (i : ι), S i
⊢ (fun x => ∃ h, C x h) 1
[PROOFSTEP]
exact ⟨_, h1⟩
[GOAL]
case this.refine'_3
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
⊢ (fun x => ∃ h, C x h) x → (fun x => ∃ h, C x h) y → (fun x => ∃ h, C x h) (x * y)
[PROOFSTEP]
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
[GOAL]
case this.refine'_3.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (_ : x ∈ ⨆ (i : ι), S i)
h1 : C 1 (_ : 1 ∈ ⨆ (i : ι), S i)
hmul :
  ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i),
    C x hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ (i : ι), S i)
x✝ : G
hx : x✝ ∈ ⨆ (i : ι), S i
x y : G
w✝¹ : x ∈ ⨆ (i : ι), S i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), S i
Cy : C y w✝
⊢ ∃ h, C (x * y) h
[PROOFSTEP]
refine' ⟨_, hmul _ _ _ _ Cx Cy⟩
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K
[PROOFSTEP]
rw [closure_eq, closure_eq]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
⊢ s * ↑N = ↑N * s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x : G
⊢ x ∈ s * ↑N ↔ x ∈ ↑N * s
[PROOFSTEP]
refine (exists_congr fun y => ?_).trans exists_swap
[GOAL]
case h
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x y : G
⊢ (∃ b, y ∈ s ∧ b ∈ ↑N ∧ (fun x x_1 => x * x_1) y b = x) ↔ ∃ y_1, y_1 ∈ ↑N ∧ y ∈ s ∧ (fun x x_1 => x * x_1) y_1 y = x
[PROOFSTEP]
simp only [exists_and_left, @and_left_comm _ (y ∈ s), ← eq_inv_mul_iff_mul_eq (b := y), ←
  eq_mul_inv_iff_mul_eq (c := y), exists_eq_right, SetLike.mem_coe, hN.mem_comm_iff]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(H ⊔ N) = ↑H * ↑N
[PROOFSTEP]
rw [sup_eq_closure]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N
[PROOFSTEP]
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N
[PROOFSTEP]
refine closure_induction'' (p := fun x => x ∈ (H : Set G) * (N : Set G)) hx ?_ ?_ ?_ ?_
[GOAL]
case refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case refine_1.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y ∈ ↑H * ↑N
[PROOFSTEP]
exact mul_mem_mul hx hy
[GOAL]
case refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x⁻¹
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
case refine_2.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ ((fun x x_1 => x * x_1) x y)⁻¹ ∈ ↑H * ↑N
[PROOFSTEP]
simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left] using
  mul_mem_mul (inv_mem hx) (hN.conj_mem _ (inv_mem hy) x)
[GOAL]
case refine_3
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ (fun x => x ∈ ↑H * ↑N) 1
[PROOFSTEP]
exact ⟨1, 1, one_mem _, one_mem _, mul_one 1⟩
[GOAL]
case refine_4
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x y : G), (fun x => x ∈ ↑H * ↑N) x → (fun x => x ∈ ↑H * ↑N) y → (fun x => x ∈ ↑H * ↑N) (x * y)
[PROOFSTEP]
rintro _ _ ⟨x, y, hx, hy, rfl⟩ ⟨x', y', hx', hy', rfl⟩
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y' ∈ ↑H * ↑N
[PROOFSTEP]
refine ⟨x * x', x'⁻¹ * y * x' * y', mul_mem hx hx', mul_mem ?_ hy', ?_⟩
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ x'⁻¹ * y * x' ∈ N
[PROOFSTEP]
simpa using hN.conj_mem _ hy x'⁻¹
[GOAL]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) (x * x') (x'⁻¹ * y * x' * y') = (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y'
[PROOFSTEP]
simp only [mul_assoc, mul_inv_cancel_left]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
N H : Subgroup G
inst✝ : Normal N
⊢ ↑(N ⊔ H) = ↑N * ↑H
[PROOFSTEP]
rw [← set_mul_normal_comm, sup_comm, mul_normal]
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
⊢ ↑A * ↑(B ⊓ C) = ↑A * ↑B ⊓ ↑C
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ x✝ ∈ ↑A * ↑(B ⊓ C) ↔ x✝ ∈ ↑A * ↑B ⊓ ↑C
[PROOFSTEP]
simp only [coe_inf, Set.inf_eq_inter, Set.mem_mul, Set.mem_inter_iff]
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) ↔ (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C
[PROOFSTEP]
rintro ⟨y, z, hy, ⟨hzB, hzC⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x y_1, x ∈ ↑A ∧ y_1 ∈ ↑B ∧ x * y_1 = y * z) ∧ y * z ∈ ↑C
[PROOFSTEP]
refine' ⟨_, mul_mem (h hy) hzC⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑A ∧ y_1 ∈ ↑B ∧ x * y_1 = y * z
[PROOFSTEP]
exact ⟨y, z, hy, hzB, rfl⟩
[GOAL]
case h.mpr
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x y, x ∈ ↑A ∧ y ∈ ↑B ∧ x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x y, x ∈ ↑A ∧ (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨⟨y, z, hy, hz, rfl⟩, hyz⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑A ∧ (y_1 ∈ ↑B ∧ y_1 ∈ ↑C) ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨y, z, hy, ⟨hz, _⟩, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ z ∈ ↑C
[PROOFSTEP]
suffices y⁻¹ * (y * z) ∈ C by simpa
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ ↑C
[PROOFSTEP]
simpa
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : A ≤ C
y z : G
hy : y ∈ ↑A
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ y⁻¹ * (y * z) ∈ C
[PROOFSTEP]
exact mul_mem (inv_mem (h hy)) hyz
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
⊢ ↑(A ⊓ B) * ↑C = ↑A ⊓ ↑B * ↑C
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ x✝ ∈ ↑(A ⊓ B) * ↑C ↔ x✝ ∈ ↑A ⊓ ↑B * ↑C
[PROOFSTEP]
simp only [coe_inf, Set.inf_eq_inter, Set.mem_mul, Set.mem_inter_iff]
[GOAL]
case h
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝) ↔ x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨y, z, ⟨hyA, hyB⟩, hz, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
hz : z ∈ ↑C
⊢ y * z ∈ ↑A ∧ ∃ x y_1, x ∈ ↑B ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨A.mul_mem hyA (h hz), _⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
hz : z ∈ ↑C
⊢ ∃ x y_1, x ∈ ↑B ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
exact ⟨y, z, hyB, hz, rfl⟩
[GOAL]
case h.mpr
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x y, x ∈ ↑B ∧ y ∈ ↑C ∧ x * y = x✝) → ∃ x y, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y ∈ ↑C ∧ x * y = x✝
[PROOFSTEP]
rintro ⟨hyz, y, z, hy, hz, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ ∃ x y_1, (x ∈ ↑A ∧ x ∈ ↑B) ∧ y_1 ∈ ↑C ∧ x * y_1 = y * z
[PROOFSTEP]
refine' ⟨y, z, ⟨_, hy⟩, hz, rfl⟩
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y ∈ ↑A
[PROOFSTEP]
suffices y * z * z⁻¹ ∈ A by simpa
[GOAL]
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
this : y * z * z⁻¹ ∈ A
⊢ y ∈ ↑A
[PROOFSTEP]
simpa
[GOAL]
case h.mpr.intro.intro.intro.intro.intro
α : Type u_1
G : Type u_2
A✝ : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A✝
s : Set G
A B C : Subgroup G
h : C ≤ A
y z : G
hy : y ∈ ↑B
hz : z ∈ ↑C
hyz : y * z ∈ ↑A
⊢ y * z * z⁻¹ ∈ A
[PROOFSTEP]
exact mul_mem hyz (inv_mem (h hz))
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K
[PROOFSTEP]
rw [← SetLike.mem_coe, normal_mul] at hmem ⊢
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
n : G
hmem : n ∈ ↑H * ↑K
g : G
⊢ g * n * g⁻¹ ∈ ↑H * ↑K
[PROOFSTEP]
rcases hmem with ⟨h, k, hh, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ g * (fun x x_1 => x * x_1) h k * g⁻¹ ∈ ↑H * ↑K
[PROOFSTEP]
refine ⟨g * h * g⁻¹, g * k * g⁻¹, hH.conj_mem h hh g, hK.conj_mem k hk g, ?_⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : Normal H
hK : Normal K
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ (fun x x_1 => x * x_1) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun x x_1 => x * x_1) h k * g⁻¹
[PROOFSTEP]
simp only [mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ : Set G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
[PROOFSTEP]
simp [preimage_preimage, mul_assoc]
  -- porting note: deprecate?
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S
[PROOFSTEP]
change S.map _ = S
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ map (↑(MulDistribMulAction.toMonoidEnd α G) 1) S = S
[PROOFSTEP]
simpa only [map_one] using S.map_id
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj ↑h • P ≤ H
[PROOFSTEP]
rintro - ⟨g, hg, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
g : G
hg : g ∈ ↑P
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g ∈ H
[PROOFSTEP]
exact H.mul_mem (H.mul_mem h.2 (hP hg)) (H.inv_mem h.2)
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj h • subgroupOf P H = subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ ↑MulAut.conj h • subgroupOf P H ≤ subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
rintro - ⟨g, hg, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h g : { x // x ∈ H }
hg : g ∈ ↑(subgroupOf P H)
⊢ ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ H }) h) { x // x ∈ H }) (↑MulAut.conj h)) g ∈
    subgroupOf (↑MulAut.conj ↑h • P) H
[PROOFSTEP]
exact ⟨g, hg, rfl⟩
[GOAL]
case refine'_2
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h : { x // x ∈ H }
⊢ subgroupOf (↑MulAut.conj ↑h • P) H ≤ ↑MulAut.conj h • subgroupOf P H
[PROOFSTEP]
rintro p ⟨g, hg, hp⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
P H : Subgroup G
hP : P ≤ H
h p : { x // x ∈ H }
g : G
hg : g ∈ ↑P
hp : ↑(↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut G) ↑h) G) (↑MulAut.conj ↑h)) g = ↑(Subgroup.subtype H) p
⊢ p ∈ ↑MulAut.conj h • subgroupOf P H
[PROOFSTEP]
exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T
[PROOFSTEP]
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
H : Subgroup G
h : G
hh : h ∈ H
this : {x | x ∈ H} = ↑H
⊢ ↑H * {h} = ↑H
[PROOFSTEP]
simpa [preimage, mul_mem_cancel_right (inv_mem hh)]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
H : Subgroup G
h : G
hh : h ∈ H
this : {x | x ∈ H} = ↑H
⊢ {h} * ↑H = ↑H
[PROOFSTEP]
simpa [preimage, mul_mem_cancel_left (inv_mem hh)]
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : DistribMulAction α A
S : AddSubgroup A
⊢ 1 • S = S
[PROOFSTEP]
change S.map _ = S
[GOAL]
α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : DistribMulAction α A
S : AddSubgroup A
⊢ map (↑(DistribMulAction.toAddMonoidEnd α A) 1) S = S
[PROOFSTEP]
simpa only [map_one] using S.map_id