awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup N
rw : (⇑f : (a : G) → N) '' (↑(comap f H) : Set G) = (↑(f.range ⊓ H) : Set N)
rw₁ : Set.image.{u_1, u_5} (α := G) (⇑f : (a : G) → N) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) = (↑(f.range ⊓ H) : Set N)
rw₂ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑(f.range ⊓ H) : Set N)
rw₃ : (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) = (↑f.range : Set N) ∩ (↑H : Set N)
rw₄ :
  (↑H : Set N) ∩ Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) =
    Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N)
rw₅ rw₆ :
  Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N) =
    Set.range.{u_5, u_1 + 1} (ι := G) (⇑f : (a : G) → N) ∩ (↑H : Set N)
⊢ (↑(map f (comap f H)) : Set N) = (↑(f.range ⊓ H) : Set N)

Tactic:
rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Premises used: Subgroup.coe_map, Set.image_preimage_eq_inter_range, Set.inter_comm, Subgroup.coe_inf, MonoidHom.coe_range, Subgroup.coe_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) = H ⊔ f.ker

Tactic:
le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))

Premises used: Subgroup.ker_le_comap, le_antisymm, Subgroup.le_comap_map, sup_le
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
refine : comap f (map f H) ≤ H ⊔ f.ker
⊢ comap f (map f H) = H ⊔ f.ker

Tactic:
refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))

Premises used: Subgroup.ker_le_comap, le_antisymm, Subgroup.le_comap_map, sup_le
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ ∃ x_1 ∈ H, Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) x_1 : N) ((f : (a : G) → N) x : N)

Tactic:
simp only [mem_map, mem_comap] at hx

Premises used: Subgroup.mem_comap, Subgroup.mem_map
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1 ∈ H, Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) x_1 : N) ((f : (a : G) → N) x : N)
rcases :
  ∀ (y : G) (hy : y ∈ H) (hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)),
    x ∈ H ⊔ f.ker
⊢ x ∈ H ⊔ f.ker

Tactic:
rcases hx with ⟨y, hy, hy'⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)
rw : y * (y⁻¹ * x) ∈ H ⊔ f.ker
⊢ x ∈ H ⊔ f.ker

Tactic:
rw [← mul_inv_cancel_left y x]

Premises used: mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)
⊢ y⁻¹ * x ∈ f.ker

Tactic:
simp [mem_ker, hy']

Premises used: MonoidHom.mem_ker
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : Eq.{u_5 + 1} (α := N) ((f : (a : G) → N) y : N) ((f : (a : G) → N) x : N)
⊢ y * (y⁻¹ * x) ∈ H ⊔ f.ker

Tactic:
exact mul_mem_sup hy (by simp [mem_ker, hy'])

Premises used: Subgroup.mul_mem_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup N
h : H ≤ f.range
rwa : f.range ⊓ H = H
rwa₁ rwa₂ rwa₃ rwa₄ : H ≤ f.range
⊢ map f (comap f H) = H

Tactic:
rwa [map_comap_eq, inf_eq_right]

Premises used: Subgroup.map_comap_eq, inf_eq_right
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
h : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H : Subgroup N
⊢ map f (comap f H) = H

Tactic:
map_comap_eq_self (range_eq_top.2 h ▸ le_top)

Premises used: Iff.mpr, Eq.rec, MonoidHom.range_eq_top, Subgroup.map_comap_eq_self, le_top, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
K L : Subgroup N
hf : K ≤ f.range
⊢ comap f K ≤ comap f L ↔ K ≤ L

Tactic:
⟨(map_comap_eq_self hf).ge.trans ∘ map_le_iff_le_comap.mpr, comap_mono⟩

Premises used: Iff.mpr, Eq.ge, Function.comp, Subgroup.map_comap_eq_self, Subgroup.map_le_iff_le_comap, Iff.intro, Subgroup.comap_mono, LE.le.trans
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
K L : Subgroup N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ comap f K ≤ comap f L ↔ K ≤ L

Tactic:
comap_le_comap_of_le_range (range_eq_top.2 hf ▸ le_top)

Premises used: Iff.mpr, Eq.rec, MonoidHom.range_eq_top, le_top, Eq.symm, Subgroup.comap_le_comap_of_le_range
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
h : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
K L : Subgroup N
⊢ comap f K = comap f L → K = L

Tactic:
simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

Premises used: Subgroup.comap_le_comap_of_surjective, le_antisymm_iff, imp_self
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
h : f.ker ≤ H
rwa : H ⊔ f.ker = H
rwa₁ rwa₂ rwa₃ rwa₄ : f.ker ≤ H
⊢ comap f (map f H) = H

Tactic:
rwa [comap_map_eq, sup_eq_left]

Premises used: sup_eq_left, Subgroup.comap_map_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
h : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H : Subgroup G
⊢ comap f (map f H) = H

Tactic:
comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le)

Premises used: Iff.mpr, Eq.rec, MonoidHom.ker_eq_bot_iff, Subgroup.comap_map_eq_self, Eq.symm, bot_le
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
rw : H ≤ comap f (map f K) ↔ H ≤ K ⊔ f.ker
rw₁ rw₂ : H ≤ K ⊔ f.ker ↔ H ≤ K ⊔ f.ker
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

Tactic:
rw [map_le_iff_le_comap, comap_map_eq]

Premises used: Subgroup.comap_map_eq, Subgroup.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

Tactic:
simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]

Premises used: and_true, le_sup_right, Subgroup.map_le_map_iff, sup_le_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
⊢ map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker

Tactic:
simp only [le_antisymm_iff, map_le_map_iff']

Premises used: Subgroup.map_le_map_iff', le_antisymm_iff
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H : Subgroup G
rw : map f H = map f ⊤ ↔ Codisjoint H f.ker
rw₁ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ Codisjoint H f.ker
rw₂ : H ⊔ f.ker = ⊤ ⊔ f.ker ↔ H ⊔ f.ker = ⊤
rw₃ rw₄ : H ⊔ f.ker = ⊤ ↔ H ⊔ f.ker = ⊤
⊢ map f H = f.range ↔ Codisjoint H f.ker

Tactic:
rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq]

Premises used: Subgroup.map_eq_map_iff, MonoidHom.range_eq_map, codisjoint_iff, top_sup_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
rw : H ≤ comap f (map f K) ↔ H ≤ K
rw₁ rw₂ : H ≤ K ↔ H ≤ K
⊢ map f H ≤ map f K ↔ H ≤ K

Tactic:
rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf]

Premises used: Subgroup.comap_map_eq_self_of_injective, Subgroup.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
G' : Subgroup G
H K : Subgroup ↥G'
⊢ map G'.subtype H ≤ map G'.subtype K ↔ H ≤ K

Tactic:
map_le_map_iff_of_injective G'.subtype_injective

Premises used: Subgroup.map_le_map_iff_of_injective, Subgroup.subtype_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
N : Type u_5
inst_4 : Group N
H_1 : Subgroup G
f : G →* N
H : Subgroup G
⊢ ∀ {a b : Subgroup ↥H},
    LE.le (α := { H' : Subgroup G // H' ≤ H })
        (({ toFun := fun (H' : Subgroup ↥H) ↦ Subtype.mk (p := fun (H' : Subgroup G) ↦ H' ≤ H) (map H.subtype H') ⋯,
                invFun := fun (sH' : { H' : Subgroup G // H' ≤ H }) ↦ (↑sH' : Subgroup G).subgroupOf H, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Subgroup ↥H) → { H' : Subgroup G // H' ≤ H })
            a :
          { H' : Subgroup G // H' ≤ H })
        (({ toFun := fun (H' : Subgroup ↥H) ↦ Subtype.mk (p := fun (H' : Subgroup G) ↦ H' ≤ H) (map H.subtype H') ⋯,
                invFun := fun (sH' : { H' : Subgroup G // H' ≤ H }) ↦ (↑sH' : Subgroup G).subgroupOf H, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Subgroup ↥H) → { H' : Subgroup G // H' ≤ H })
            b :
          { H' : Subgroup G // H' ≤ H }) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
sH' : { H' : Subgroup G // H' ≤ H }
⊢ ((orderIso H).symm : (a : { H' : Subgroup G // H' ≤ H }) → Subgroup ↥H) sH' = (↑sH' : Subgroup G).subgroupOf H

Tactic:
rfl

Premises used: Subgroup.subgroupOf, Subgroup.comap, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
P : Subgroup ↥H → Prop
⊢ (∀ (H' : Subgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.subgroupOf H)

Tactic:
simp [(MapSubtype.orderIso H).forall_congr_left]

Premises used: Subgroup.MapSubtype.orderIso, Equiv.forall_congr_left, RelIso.toEquiv
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
⊢ map f H < map f K ↔ H < K

Tactic:
lt_iff_lt_of_le_iff_le' (map_le_map_iff_of_injective hf) (map_le_map_iff_of_injective hf)

Premises used: Subgroup.map_le_map_iff_of_injective, lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
G' : Subgroup G
H K : Subgroup ↥G'
⊢ map G'.subtype H < map G'.subtype K ↔ H < K

Tactic:
map_lt_map_iff_of_injective G'.subtype_injective

Premises used: Subgroup.subtype_injective, Subgroup.map_lt_map_iff_of_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
h : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ Injective (map f)

Tactic:
Function.LeftInverse.injective <| comap_map_eq_self_of_injective h

Premises used: Function.LeftInverse.injective, Subgroup.comap_map_eq_self_of_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
K L : Subgroup ↥H
⊢ map H.subtype K = map H.subtype L ↔ K = L

Tactic:
(map_injective H.subtype_injective).eq_iff

Premises used: Subgroup.map_injective, Function.Injective.eq_iff, Subgroup.subtype_injective
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : map f H = map f K
⊢ comap f (map f H) = comap f (map f K)

Tactic:
apply_fun comap f at hf

Premises used: Subgroup.comap
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
rwa : ∀ (hf : H ⊔ f.ker = comap f (map f K)), H = K
rwa₁ : ∀ (hf : H ⊔ f.ker = K ⊔ f.ker), H = K
rwa₂ : ∀ (hf : H = K ⊔ f.ker), H = K
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hf : H = K), H = K
⊢ H = K

Tactic:
rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf

Premises used: Subgroup.comap_map_eq, sup_of_le_left
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G →* N
⊢ (f.subgroupMap H).ker = f.ker.subgroupOf H

Tactic:
ext fun _ ↦ Subtype.ext_iff

Premises used: Subtype.ext_iff, Subgroup.ext
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup ↥(closure s)) (closure ((⇑(Subgroup.subtype (closure s)) : (a : ↥(closure s)) → G) ⁻¹' s)) ⊤

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₃ : f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
rw₄ : H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
rw₅ : H ⊔ K = f.range ⊓ (H ⊔ K)
rw₆ rw₇ : H ⊔ K = H ⊔ K
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))

Tactic:
rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]

Premises used: Iff.mpr, Subgroup.map_sup, Subgroup.map_comap_eq, sup_le, inf_eq_right
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ comap f H ⊔ comap f K = comap f (H ⊔ K)

Tactic:
comap_sup_eq_of_le_range f (range_eq_top.2 hf ▸ le_top) (range_eq_top.2 hf ▸ le_top)

Premises used: Iff.mpr, Eq.rec, MonoidHom.range_eq_top, Subgroup.comap_sup_eq_of_le_range, le_top, Eq.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_

Premises used: le_sup_left, Subgroup.map_injective_of_ker_le, Subgroup.subtype, Subgroup.ker_le_comap, le_trans
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
map_injective_of_ker_le : map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_

Premises used: le_sup_left, Subgroup.map_injective_of_ker_le, Subgroup.subtype, Subgroup.ker_le_comap, le_trans
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
simp : B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)

Tactic:
simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]

Premises used: Subgroup.map_sup, Subgroup.subgroupOf, Subgroup.map_comap_eq, Subgroup.range_subtype
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
rw : A ⊔ A' = B ⊓ A ⊔ B ⊓ A'
rw₁ : A ⊔ A' = B ⊓ A ⊔ A'
rw₂ rw₃ : A ⊔ A' = A ⊔ A'
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'

Tactic:
rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]

Premises used: inf_of_le_right, sup_le
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hA : H ≤ H ⊔ K
hA' : K ≤ H ⊔ K
⊢ Codisjoint (α := Subgroup ↥(H ⊔ K)) (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]

Premises used: Subgroup.subgroupOf_self, codisjoint_iff, Subgroup.subgroupOf_sup
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

Tactic:
exacts [le_sup_left, le_sup_right]

Premises used: le_sup_left, le_sup_right
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
e : G ≃* G'
⊢ Eq (α := Subgroup G') (MonoidHom.range (↑e : G →* G')) ⊤

Tactic:
MonoidHom.range_eq_top.mpr e.surjective

Premises used: Iff.mpr, MulEquiv.surjective, MonoidHom.range_eq_top
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
h :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := N) ((MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : (a : M) → N) x : N)
      (((MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N) : (a : M) → N) x : N)
⊢ Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
x : M
⊢ Eq.{u_6 + 1} (α := N) ((MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : (a : M) → N) x : N)
    (((MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N) : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
⊢ Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)

Tactic:
have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext : 1; simp
-- Module: Mathlib.Algebra.Group.Subgroup.Ker
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
rw :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
    (range (G := N) (powMonoidHom n))
rw₁ :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (powMonoidHom n) (↑e : M →* N)))
    (range (G := N) (powMonoidHom n))
rw₂ : Eq (α := Subgroup N) (Subgroup.map (powMonoidHom n) (range (↑e : M →* N))) (range (G := N) (powMonoidHom n))
rw₃ : Eq.{u_6 + 1} (α := Subgroup N) (Subgroup.map (G := N) (powMonoidHom n) ⊤) (range (G := N) (powMonoidHom n))
rw₄ rw₅ : Eq.{u_6 + 1} (α := Subgroup N) (range (G := N) (powMonoidHom n)) (range (G := N) (powMonoidHom n))
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))

Tactic:
rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]

Premises used: MonoidHom.map_range, MonoidHom.range_eq_map, MonoidHom.range_comp, MulEquiv.range_eq_top
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : Subgroup G
mk :
  ∀ (toSubmonoid : Submonoid G) (inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
    (fun (S : AddSubgroup (Additive G)) ↦
          let __src : Submonoid (Multiplicative (Additive G)) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
              S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
        ((fun (S : Subgroup G) ↦
            let __src : AddSubmonoid (Additive G) :=
              (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
            ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
          { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
      { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup G }
⊢ (fun (S : AddSubgroup (Additive G)) ↦
        let __src : Submonoid (Multiplicative (Additive G)) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
            S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
      ((fun (S : Subgroup G) ↦
          let __src : AddSubmonoid (Additive G) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
          ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
        x) =
    x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
toSubmonoid : Submonoid G
inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier
⊢ (fun (S : AddSubgroup (Additive G)) ↦
        let __src : Submonoid (Multiplicative (Additive G)) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
            S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
      ((fun (S : Subgroup G) ↦
          let __src : AddSubmonoid (Additive G) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
          ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
        { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
    { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup G }

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Lattice
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : AddSubgroup (Additive G)
mk :
  ∀ (toAddSubmonoid : AddSubmonoid (Additive G))
    (neg_mem' : ∀ {x : Additive G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
    (fun (S : Subgroup G) ↦
          let __src : AddSubmonoid (Additive G) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
          ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
        ((fun (S : AddSubgroup (Additive G)) ↦
            let __src : Submonoid (Multiplicative (Additive G)) :=
              (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
                S.toAddSubmonoid;
            { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
          { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
      { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup (Additive G) }
⊢ (fun (S : Subgroup G) ↦
        let __src : AddSubmonoid (Additive G) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
        ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
      ((fun (S : AddSubgroup (Additive G)) ↦
          let __src : Submonoid (Multiplicative (Additive G)) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
              S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
        x) =
    x

Tactic:
cases x