Mathlib.Algebra.Group.Correspondence

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Subgroup
import Mathlib.Algebra.Group.Quotient
import Mathlib.Algebra.Group.Quotient.Mul
import Mathlib.Algebra.Group.Quotient.Group
import Mathlib.Algebra.Group.Correspondence.Basic

inductive CorrespondenceImageSubgroupEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (image_one : @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal (@NormalQuotOne.{u} G one mul inv N group_args n_normal)), forall (image_mul_closed : forall (a : @NormalQuot.{u} G one mul inv N group_args n_normal), forall (b : @NormalQuot.{u} G one mul inv N group_args n_normal), forall (ha : @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal a), forall (hb : @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal b), @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal (@NormalQuotMul.{u} G one mul inv N group_args n_normal a b)), forall (image_inv_closed : forall (a : @NormalQuot.{u} G one mul inv N group_args n_normal), forall (ha : @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal a), @CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal (@NormalQuotInv.{u} G one mul inv N group_args n_normal a)), @CorrespondenceImageSubgroupEvidence.{u} G one mul inv N Hpred group_args n_normal

inductive CorrespondencePreimageSubgroupEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), forall (preimage_one : @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K one), forall (preimage_mul_closed : forall (a : G), forall (b : G), forall (ha : @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K a), forall (hb : @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K b), @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K (mul a b)), forall (preimage_inv_closed : forall (a : G), forall (ha : @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K a), @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K (inv a)), @CorrespondencePreimageSubgroupEvidence.{u} G one mul inv N group_args n_normal K k_args

inductive CorrespondenceContainmentEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), forall (preimage_contains_normal : forall (x : G), forall (hn : N x), @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K x), @CorrespondenceContainmentEvidence.{u} G one mul inv N group_args n_normal K k_args

inductive CorrespondenceSubgroupSaturationEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), forall (subgroup_to_preimage_image : forall (x : G), forall (hx : Hpred x), @CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal (@CorrespondenceImagePred.{u} G one mul inv N Hpred group_args n_normal) x), forall (subgroup_to_saturation : forall (x : G), forall (hx : Hpred x), @CorrespondenceSaturationPred.{u} G one mul inv N Hpred x), forall (saturation_to_subgroup : forall (x : G), forall (hx : @CorrespondenceSaturationPred.{u} G one mul inv N Hpred x), Hpred x), @CorrespondenceSubgroupSaturationEvidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h

inductive CorrespondenceQuotientRoundTripEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), forall (quotient_to_image_preimage : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), forall (hk : K q), @CorrespondenceImagePred.{u} G one mul inv N (@CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K) group_args n_normal q), forall (image_preimage_to_quotient : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), forall (hk : @CorrespondenceImagePred.{u} G one mul inv N (@CorrespondencePreimagePred.{u} G one mul inv N group_args n_normal K) group_args n_normal q), K q), @CorrespondenceQuotientRoundTripEvidence.{u} G one mul inv N group_args n_normal K k_args

inductive CorrespondenceTheoremEvidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), Prop where
| mk : forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), forall (image_evidence : @CorrespondenceImageSubgroupEvidence.{u} G one mul inv N Hpred group_args n_normal), forall (preimage_evidence : @CorrespondencePreimageSubgroupEvidence.{u} G one mul inv N group_args n_normal K k_args), forall (containment_evidence : @CorrespondenceContainmentEvidence.{u} G one mul inv N group_args n_normal K k_args), forall (saturation_evidence : @CorrespondenceSubgroupSaturationEvidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h), forall (quotient_evidence : @CorrespondenceQuotientRoundTripEvidence.{u} G one mul inv N group_args n_normal K k_args), @CorrespondenceTheoremEvidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h K k_args

theorem correspondence_image_subgroup_law_args.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), @CorrespondenceImageSubgroupLawArgs.{u} G one mul inv N Hpred group_args n_normal :=
  fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_args => fun (P : Prop) => fun (mk : @CorrespondenceImageSubgroupMk.{u} G one mul inv N Hpred group_args n_normal P) => mk (@correspondence_image_one.{u} G one mul inv N Hpred group_args n_normal h_args) (@correspondence_image_mul_closed.{u} G one mul inv N Hpred group_args n_normal h_args) (@correspondence_image_inv_closed.{u} G one mul inv N Hpred group_args n_normal h_args)

theorem correspondence_preimage_subgroup_law_args.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), @CorrespondencePreimageSubgroupLawArgs.{u} G one mul inv N group_args n_normal K :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun n_normal => fun K => fun k_args => fun (P : Prop) => fun (mk : @CorrespondencePreimageSubgroupMk.{u} G one mul inv N group_args n_normal K P) => mk (@correspondence_preimage_one.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_preimage_mul_closed.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_preimage_inv_closed.{u} G one mul inv N group_args n_normal K k_args)

theorem correspondence_image_subgroup_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), @CorrespondenceImageSubgroupEvidence.{u} G one mul inv N Hpred group_args n_normal :=
  fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_args => @CorrespondenceImageSubgroupEvidence.mk.{u} G one mul inv N Hpred group_args n_normal (@correspondence_image_one.{u} G one mul inv N Hpred group_args n_normal h_args) (@correspondence_image_mul_closed.{u} G one mul inv N Hpred group_args n_normal h_args) (@correspondence_image_inv_closed.{u} G one mul inv N Hpred group_args n_normal h_args)

theorem correspondence_preimage_subgroup_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), @CorrespondencePreimageSubgroupEvidence.{u} G one mul inv N group_args n_normal K k_args :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun n_normal => fun K => fun k_args => @CorrespondencePreimageSubgroupEvidence.mk.{u} G one mul inv N group_args n_normal K k_args (@correspondence_preimage_one.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_preimage_mul_closed.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_preimage_inv_closed.{u} G one mul inv N group_args n_normal K k_args)

theorem correspondence_containment_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), @CorrespondenceContainmentEvidence.{u} G one mul inv N group_args n_normal K k_args :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun n_normal => fun K => fun k_args => @CorrespondenceContainmentEvidence.mk.{u} G one mul inv N group_args n_normal K k_args (@correspondence_preimage_contains_normal.{u} G one mul inv N group_args n_normal K k_args)

theorem correspondence_subgroup_saturation_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), @CorrespondenceSubgroupSaturationEvidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h :=
  fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_args => fun n_le_h => @CorrespondenceSubgroupSaturationEvidence.mk.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h (@correspondence_subgroup_to_preimage_image.{u} G one mul inv N Hpred group_args n_normal) (@correspondence_subgroup_to_saturation.{u} G one mul inv N Hpred group_args n_normal) (@correspondence_saturation_to_subgroup.{u} G one mul inv N Hpred group_args h_args n_le_h)

theorem correspondence_quotient_round_trip_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), @CorrespondenceQuotientRoundTripEvidence.{u} G one mul inv N group_args n_normal K k_args :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun n_normal => fun K => fun k_args => @CorrespondenceQuotientRoundTripEvidence.mk.{u} G one mul inv N group_args n_normal K k_args (@correspondence_quotient_to_image_preimage.{u} G one mul inv N group_args n_normal K) (@correspondence_image_preimage_to_quotient.{u} G one mul inv N group_args n_normal K)

theorem correspondence_theorem_evidence.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (Hpred : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (n_normal : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (h_args : @SubgroupLawArgs.{succ u} G one mul inv Hpred), forall (n_le_h : forall (x : G), forall (hn : N x), Hpred x), forall (K : forall (q : @NormalQuot.{u} G one mul inv N group_args n_normal), Prop), forall (k_args : @SubgroupLawArgs.{succ u} (@NormalQuot.{u} G one mul inv N group_args n_normal) (@NormalQuotOne.{u} G one mul inv N group_args n_normal) (@NormalQuotMul.{u} G one mul inv N group_args n_normal) (@NormalQuotInv.{u} G one mul inv N group_args n_normal) K), @CorrespondenceTheoremEvidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h K k_args :=
  fun G => fun one => fun mul => fun inv => fun N => fun Hpred => fun group_args => fun n_normal => fun h_args => fun n_le_h => fun K => fun k_args => @CorrespondenceTheoremEvidence.mk.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h K k_args (@correspondence_image_subgroup_evidence.{u} G one mul inv N Hpred group_args n_normal h_args) (@correspondence_preimage_subgroup_evidence.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_containment_evidence.{u} G one mul inv N group_args n_normal K k_args) (@correspondence_subgroup_saturation_evidence.{u} G one mul inv N Hpred group_args n_normal h_args n_le_h) (@correspondence_quotient_round_trip_evidence.{u} G one mul inv N group_args n_normal K k_args)