awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
⊢ x = y
have rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
⊢ x = y
have rwa₆ : ∀ (hxy : y.1 = x.1 ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₆ : ∀ (hxy : y.1 = x.1 ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
⊢ x = y
have rwa₇ : ∀ (hxy : y.1 = x.1 ∧ x.2 = y.2), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₆ : ∀ (hxy : y.1 = x.1 ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₇ : ∀ (hxy : y.1 = x.1 ∧ x.2 = y.2), x = y
⊢ x = y
have rwa₈ : ∀ (hxy : x.1 = y.1 ∧ x.2 = y.2), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑(y.1⁻¹ * x.1) : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1
rwa : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑(x.2 * y.2⁻¹) : G) = 1), x = y
rwa₁ : ∀ (hxy : (↑y.1⁻¹ : G) * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₂ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2⁻¹ : G) = 1), x = y
rwa₃ : ∀ (hxy : (↑y.1 : G)⁻¹ * (↑x.1 : G) = 1 ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₄ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) * (↑y.2 : G)⁻¹ = 1), x = y
rwa₅ : ∀ (hxy : (↑y.1 : G) = (↑x.1 : G) ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₆ : ∀ (hxy : y.1 = x.1 ∧ (↑x.2 : G) = (↑y.2 : G)), x = y
rwa₇ : ∀ (hxy : y.1 = x.1 ∧ x.2 = y.2), x = y
rwa₈ : ∀ (hxy : x.1 = y.1 ∧ x.2 = y.2), x = y
⊢ x = y
have rwa₉ : ∀ (hxy : x = y), x = y
Tactic: rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
    Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
H_1 K : Subgroup G
k : Set G
N_1 : Type u_5
inst_4 : Group N_1
P : Type u_6
inst_5 : Group P
N : Type u_7
inst_6 : Group N
f : G →* N
H : Subgroup N
a : G
ha : Membership.mem (γ := Set G) ((⇑f : (a : G) → N) ⁻¹' (↑H : Set N)) a
⊢ Membership.mem (α := N) H ((f : (a : G) → N) a⁻¹ : N)
have rw : Membership.mem (α := N) H (((f : (a : G) → N) a)⁻¹ : N)
Tactic: rw [f.map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
N : Type u_5
inst : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K
have h : ∀ (x : N), x ∈ comap (MonoidHom.id N) K ↔ x ∈ K
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm : N →* G) H = K ↔ map (↑e : G →* N) K = H
have mp : map (↑e.symm : N →* G) H = K → map (↑e : G →* N) K = H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (↑e.symm : N →* G) H = K → map (↑e : G →* N) K = H
⊢ map (↑e.symm : N →* G) H = K ↔ map (↑e : G →* N) K = H
have mpr : map (↑e : G →* N) K = H → map (↑e.symm : N →* G) H = K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H
have mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H
have mp₁ : map (↑(e.symm.trans e) : N →* N) H = H
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
mp₁ : map (↑(e.symm.trans e) : N →* N) H = H
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H
have mp₂ : map (↑(MulEquiv.refl N) : N →* N) H = H
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
mp₁ : map (↑(e.symm.trans e) : N →* N) H = H
mp₂ : map (↑(MulEquiv.refl N) : N →* N) H = H
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H
have mp₃ : map (MonoidHom.id N) H = H
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup N
e : G ≃* N
mp : map (MonoidHom.comp (↑e : G →* N) (↑e.symm : N →* G)) H = H
mp₁ : map (↑(e.symm.trans e) : N →* N) H = H
mp₂ : map (↑(MulEquiv.refl N) : N →* N) H = H
mp₃ : map (MonoidHom.id N) H = H
⊢ map (↑e : G →* N) (map (↑e.symm : N →* G) H) = H
have mp₄ : H = H
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K
have mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K
have mpr₁ : map (↑(e.trans e.symm) : G →* G) K = K
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
mpr₁ : map (↑(e.trans e.symm) : G →* G) K = K
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K
have mpr₂ : map (↑(MulEquiv.refl G) : G →* G) K = K
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
mpr₁ : map (↑(e.trans e.symm) : G →* G) K = K
mpr₂ : map (↑(MulEquiv.refl G) : G →* G) K = K
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K
have mpr₃ : map (MonoidHom.id G) K = K
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
N : Type u_5
inst_1 : Group N
e : G ≃* N
mpr : map (MonoidHom.comp (↑e.symm : N →* G) (↑e : G →* N)) K = K
mpr₁ : map (↑(e.trans e.symm) : G →* G) K = K
mpr₂ : map (↑(MulEquiv.refl G) : G →* G) K = K
mpr₃ : map (MonoidHom.id G) K = K
⊢ map (↑e.symm : N →* G) (map (↑e : G →* N) K) = K
have mpr₄ : K = K
Tactic: rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
      MulEquiv.coe_monoidHom_refl, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
ι : Sort u_7
inst_2 : Nonempty ι
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
s : ι → Subgroup G
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)
have a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H K : Subgroup G
f : G →* N
hf : Injective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ map f (H ⊓ K) = map f H ⊓ map f K
have rw : (↑(map f (H ⊓ K)) : Set N) = (↑(map f H ⊓ map f K) : Set N)
Tactic: rw [← SetLike.coe_set_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
h : Disjoint H K
⊢ Disjoint (map f H) (map f K)
have rw : map f H ⊓ map f K = ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
h : Disjoint H K
rw : map f H ⊓ map f K = ⊥
⊢ Disjoint (map f H) (map f K)
have rw₁ : map f (H ⊓ K) = ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
h : Disjoint H K
rw : map f H ⊓ map f K = ⊥
rw₁ : map f (H ⊓ K) = ⊥
⊢ Disjoint (map f H) (map f K)
have rw₂ : map f ⊥ = ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
h : Disjoint H K
rw : map f H ⊓ map f K = ⊥
rw₁ : map f (H ⊓ K) = ⊥
rw₂ : map f ⊥ = ⊥
⊢ Disjoint (map f H) (map f K)
have rw₃ : Eq.{u_5 + 1} (α := Subgroup N) ⊥ ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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)
⊢ map f ⊤ = ⊤
have rw : ⊤ ≤ map f ⊤
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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)
x : N
h_1 : Membership.mem (γ := Subgroup N) ⊤ x
⊢ x ∈ map f ⊤
have obtain : ∀ (y : G) (hy : (f : (a : G) → N) y = x), x ∈ map f ⊤
Tactic: obtain ⟨y, hy⟩ := h x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)
have rw : map f H ⊔ map f K = ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Codisjoint H K
rw : map f H ⊔ map f K = ⊤
⊢ Codisjoint (map f H) (map f K)
have rw₁ : map f (H ⊔ K) = ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Codisjoint H K
rw : map f H ⊔ map f K = ⊤
rw₁ : map f (H ⊔ K) = ⊤
⊢ Codisjoint (map f H) (map f K)
have rw₂ : map f ⊤ = ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
H K : Subgroup G
h : Codisjoint H K
rw : map f H ⊔ map f K = ⊤
rw₁ : map f (H ⊔ K) = ⊤
rw₂ : map f ⊤ = ⊤
⊢ Codisjoint (map f H) (map f K)
have rw₃ : Eq.{u_5 + 1} (α := Subgroup N) ⊤ ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, map_top_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (↑(map K.subtype (H.subgroupOf K)) : Set G) = (↑(H ⊓ K) : Set G)
have refine : (↑K : Set G) ∩ H.toSubsemigroup.1 = (↑(H ⊓ K) : Set G)
Tactic: refine Subtype.image_preimage_coe _ _ |>.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ map K.subtype (H.subgroupOf K) = H
have rwa : H ⊓ K = H
Tactic: rwa [subgroupOf_map_subtype, inf_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K
have rw : (H ⊓ K).subgroupOf K = H.subgroupOf K
Tactic: rw [inf_comm, inf_subgroupOf_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : (H ⊓ K).subgroupOf K = H.subgroupOf K
⊢ (K ⊓ H).subgroupOf K = H.subgroupOf K
have rw₁ : H.subgroupOf K = H.subgroupOf K
Tactic: rw [inf_comm, inf_subgroupOf_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K
have rw : H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
Tactic: rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K
have rw₁ : H.subgroupOf K = subgroupOf ⊥ K ↔ H ⊓ K = ⊥
Tactic: rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
rw₁ : H.subgroupOf K = subgroupOf ⊥ K ↔ H ⊓ K = ⊥
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K
have rw₂ : H ⊓ K = ⊥ ⊓ K ↔ H ⊓ K = ⊥
Tactic: rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = ⊥ ↔ H ⊓ K = ⊥
rw₁ : H.subgroupOf K = subgroupOf ⊥ K ↔ H ⊓ K = ⊥
rw₂ : H ⊓ K = ⊥ ⊓ K ↔ H ⊓ K = ⊥
⊢ H.subgroupOf K = ⊥ ↔ Disjoint H K
have rw₃ : H ⊓ K = ⊥ ↔ H ⊓ K = ⊥
Tactic: rw [disjoint_iff, ← bot_subgroupOf, subgroupOf_inj, bot_inf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H
have rw : H.subgroupOf K = subgroupOf ⊤ K ↔ K ≤ H
Tactic: rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = subgroupOf ⊤ K ↔ K ≤ H
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H
have rw₁ : H ⊓ K = ⊤ ⊓ K ↔ K ≤ H
Tactic: rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = subgroupOf ⊤ K ↔ K ≤ H
rw₁ : H ⊓ K = ⊤ ⊓ K ↔ K ≤ H
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H
have rw₂ : H ⊓ K = K ↔ K ≤ H
Tactic: rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
rw : H.subgroupOf K = subgroupOf ⊤ K ↔ K ≤ H
rw₁ : H ⊓ K = ⊤ ⊓ K ↔ K ≤ H
rw₂ : H ⊓ K = K ↔ K ≤ H
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H
have rw₃ : K ≤ H ↔ K ≤ H
Tactic: rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
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
H_1 K : Subgroup G
k : Set G
N : Type u_5
inst_4 : Group N
P : Type u_6
inst_5 : Group P
H : Subgroup G
f : G →* G'
inst_6 : IsMulCommutative.{u_1} ↥H
⊢ IsMulCommutative.{u_2} ↥(map f H)
have refine : ∀ a ∈ map f H, ∀ b ∈ map f H, a * b = b * a
Tactic: refine .of_setLike_mul_comm ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
hl : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
hr : RightInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
H : Subgroup G
⊢ (↑(map f H) : Set N) = (↑(comap g H) : Set N)
have rw : (⇑f : (a : G) → N) '' (↑H : Set G) = (↑(comap g H) : Set N)
Tactic: rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
hl : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
hr : RightInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
H : Subgroup G
rw : (⇑f : (a : G) → N) '' (↑H : Set G) = (↑(comap g H) : Set N)
⊢ (↑(map f H) : Set N) = (↑(comap g H) : Set N)
have rw₁ : Eq.{u_5 + 1} (α := Set N) ((⇑f : (a : G) → N) '' (↑H : Set G)) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G))
Tactic: rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
g : N →* G
hl : LeftInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
hr : RightInverse.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑g : (a : N) → G) (⇑f : (a : G) → N)
H : Subgroup G
rw : (⇑f : (a : G) → N) '' (↑H : Set G) = (↑(comap g H) : Set N)
rw₁ : Eq.{u_5 + 1} (α := Set N) ((⇑f : (a : G) → N) '' (↑H : Set G)) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G))
⊢ (↑(map f H) : Set N) = (↑(comap g H) : Set N)
have rw₂ : Eq.{u_5 + 1} (α := Set N) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G)) ((⇑g : (a : N) → G) ⁻¹' (↑H : Set G))
Tactic: rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Map (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
e : G ≃* G'
⊢ H.equivMapOfInjective (↑e : G →* G') ⋯ = e.subgroupMap H
have h : ∀ (x : ↥H),
  Eq.{u_2 + 1} (α := G')
    (↑(((H.equivMapOfInjective (↑e : G →* G') sorry : MulEquiv.{u_1, u_2} ↥H ↥(map (↑e : G →* G') H)) :
            (a : ↥H) → ↥(map (↑e : G →* G') H))
          x) :
      G')
    (↑((e.subgroupMap H : (a : ↥H) → ↥(map (↑e : G →* G') H)) x) : G')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) (normalizer (↑H.op : Set Gᵐᵒᵖ))
have h : ∀ (x : Gᵐᵒᵖ),
  Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) x ↔
    Membership.mem (γ := Subgroup Gᵐᵒᵖ) (normalizer (↑H.op : Set Gᵐᵒᵖ)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (normalizer (↑H : Set G))) x ↔
    Membership.mem (γ := Subgroup Gᵐᵒᵖ) (normalizer (↑H.op : Set Gᵐᵒᵖ)) x
have h : (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ ∀ (n : Gᵐᵒᵖ), n * x ∈ H.op ↔ x * n ∈ H.op
Tactic: rw [mem_op, mem_normalizer_iff', mem_normalizer_iff']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
⊢ Eq (α := Subgroup G) (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))) (normalizer (↑H.unop : Set G))
have rw : Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))))
  (Subgroup.op (normalizer (↑H.unop : Set G)))
Tactic: rw [← op_inj, op_unop, op_normalizer, op_unop]