awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a : G
ha : a ∈ A ^ m
b : G
hb : b ∈ A ^ n
⊢ φ ((π : (a : G) → G ⧸ H) a) * b ∈ A ^ m * A ^ n

Tactic:
mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb

Premises used: congrArg, Set.Mem, setOf, cast, Membership.mem, Finset.mem_coe._simp_1, Set.mem_image_of_mem, congrFun', Finset.coe_pow._simp_2, Eq.symm, Eq.trans, Finset.mul_mem_mul
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
a : G
ha : a ∈ A ^ m
b : G
hb : b ∈ A ^ n
⊢ φ ((π : (a : G) → G ⧸ H) a) * b ∈ A ^ m * A ^ n

Tactic:
exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb

Premises used: Set.mem_image_of_mem, Finset.mul_mem_mul
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : (b : G ⧸ H) → G := invFunOn (⇑π : (a : G) → G ⧸ H) ((↑A : Set G) ^ m)
hφ : Set.InjOn φ ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m)
hφA : ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a), φ a ∈ A ^ m
hπφ :
  ∀ {a : G ⧸ H} (ha : Membership.mem (γ := Set (G ⧸ H)) ((⇑π : (a : G) → G ⧸ H) '' (↑A : Set G) ^ m) a),
    (π : (a : G) → G ⧸ H) (φ a) = a
A₁ :
  card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) =
    #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) * #({x ∈ A ^ n | x ∈ H})
A₂ :
  #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m))) * #({x ∈ A ^ n | x ∈ H}) ≤
    #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H})
A₃ : #(image φ (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * {x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))
⊢ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))

Tactic:
calc
    #((A ^ m).image π) * #{x ∈ A ^ n | x ∈ H}
    _ = #(((A ^ m).image π).image φ) * #{x ∈ A ^ n | x ∈ H} := by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
    _ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) := by
      rw [Finset.card_mul_iff.2]
      simp only [Set.InjOn, coe_image, coe_pow, coe_filter, Set.mem_prod, Set.mem_image,
        exists_exists_and_eq_and, Set.mem_setOf_eq, and_imp, forall_exists_index, Prod.forall,
        Prod.mk.injEq]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all
    _ ≤ #(A ^ (m + n)) := by
      gcongr
      simp only [mul_subset_iff, mem_image, exists_exists_and_eq_and, Finset.mem_filter, and_imp,
        forall_exists_index, forall_apply_eq_imp_iff₂, pow_add]
      rintro a ha b hb -
      exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb

Premises used: HMul.hMul, Membership.mem, HPow.hPow, HAdd.hAdd, Finset.filter, DFunLike.coe, Finset.image
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
set :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
set π := QuotientGroup.mk' H

Premises used: QuotientGroup.mk'
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
rw :
  ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
rw [card_eq_sum_card_image π]

Premises used: Finset.card_eq_sum_card_image, DFunLike.coe
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
⊢ ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_

Premises used: Iff.mpr, Finset.forall_mem_image, Finset.sum_le_card_nsmul
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
refine :
  ∀ (a : G) (ha : a ∈ A),
    #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
      #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_

Premises used: Iff.mpr, Finset.forall_mem_image, Finset.sum_le_card_nsmul
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ a⁻¹ ∈ ({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹

Tactic:
simpa
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
a₁ :
  ({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
      {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)} ⊆
    {x ∈ A⁻¹ * A | x ∈ H}
⊢ #(({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
        {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ A⁻¹ * A | x ∈ H})

Tactic:
gcongr
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
a₁ :
  ∀ (x : G),
    x⁻¹ ∈ A →
      Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H) →
        ∀ y ∈ A,
          Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H) →
            x * y ∈ A⁻¹ * A ∧ x * y ∈ H
⊢ ({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
      {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)} ⊆
    {x ∈ A⁻¹ * A | x ∈ H}

Tactic:
simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]

Premises used: map_inv, and_imp, Finset.mem_inv', Finset.mul_subset_iff, Finset.mem_filter
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
y : G
hy : y ∈ A
hya : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
⊢ x ∈ A⁻¹

Tactic:
simpa
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
y : G
hy : y ∈ A
hya : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
a₁ : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) (x * y) : G ⧸ H) (1 : G ⧸ H)
⊢ x * y ∈ A⁻¹ * A ∧ x * y ∈ H

Tactic:
refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
x : G
hx : x⁻¹ ∈ A
hxa : Eq (α := G ⧸ H) (((π : (a : G) → G ⧸ H) x)⁻¹ : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
y : G
hy : y ∈ A
hya : Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) y : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)
⊢ Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) (x * y) : G ⧸ H) (1 : G ⧸ H)

Tactic:
simp [hya, ← hxa]
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #({x ∈ A⁻¹ * A | x ∈ H}) = #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
simp [hAsymm, sq]

Premises used: sq
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
A₁ :
  #(({a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)})⁻¹ *
        {a' ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a' : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ A⁻¹ * A | x ∈ H})
A₂ : #({x ∈ A⁻¹ * A | x ∈ H}) = #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
    #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]

Premises used: HMul.hMul, Inv.inv, Exists.intro, Finset.card_le_card_mul_left, Finset.filter, Eq, DFunLike.coe
-- Module: Mathlib.Geometry.Group.Growth.QuotientInter
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
H : Subgroup G
inst_2 : DecidablePred fun (x : G) ↦ x ∈ H
inst_3 : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
set :
  #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₁ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  #A ≤ card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₂ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  ∑ b ∈ image (⇑π : (a : G) → G ⧸ H) A, #({a ∈ A | (π : (a : G) → G ⧸ H) a = b}) ≤
    card (α := G ⧸ H) (image (⇑π : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
set₃ :
  let π : G →* G ⧸ H := QuotientGroup.mk' H;
  ∀ (a : G) (ha : a ∈ A),
    #({a_1 ∈ A | Eq (α := G ⧸ H) ((π : (a : G) → G ⧸ H) a_1 : G ⧸ H) ((π : (a : G) → G ⧸ H) a : G ⧸ H)}) ≤
      #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})
⊢ #A ≤ card (α := G ⧸ H) (image (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H) A) * #({x ∈ HPow.hPow (β := ℕ) A 2 | x ∈ H})

Tactic:
classical
  set π := QuotientGroup.mk' H
  rw [card_eq_sum_card_image π]
  refine sum_le_card_nsmul _ _ _ <| forall_mem_image.2 fun a ha ↦ ?_
  calc
    #{a' ∈ A | π a' = π a}
    _ ≤ #({a' ∈ A | π a' = π a}⁻¹ * {a' ∈ A | π a' = π a}) :=
      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
    _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
      gcongr
      simp only [mul_subset_iff, mem_inv', map_inv, mem_filter, and_imp]
      rintro x hx hxa y hy hya
      refine ⟨mul_mem_mul (by simpa) hy, (QuotientGroup.eq_one_iff _).1 (?_ : π _ = _)⟩
      simp [hya, ← hxa]
    _ = #{x ∈ A ^ 2 | x ∈ H} := by simp [hAsymm, sq]

Premises used: Iff.mpr, Finset.forall_mem_image, Finset.sum_le_card_nsmul, QuotientGroup.mk'
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
X Y : LeftInvariantDerivation I G
h :
  (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
mk :
  ∀ (toDerivation : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (left_invariant'' :
      ∀ (g : G),
        Eq (α := PointDerivation I g)
          ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
              ((Derivation.evalAt 1 :
                  (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
                toDerivation) :
            PointDerivation I g)
          ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              toDerivation :
            PointDerivation I g))
    (h :
      (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
          Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
        (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)),
    { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } = Y
⊢ X = Y

Tactic:
cases X
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
Y : LeftInvariantDerivation I G
toDerivation : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant'' :
  ∀ (g : G),
    Eq (α := PointDerivation I g)
      ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
          ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
            toDerivation) :
        PointDerivation I g)
      ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
          toDerivation :
        PointDerivation I g)
h :
  (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
      Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    (↑Y : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
mk :
  ∀ (toDerivation_1 : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (left_invariant''_1 :
      ∀ (g : G),
        Eq (α := PointDerivation I g)
          ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
              ((Derivation.evalAt 1 :
                  (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
                toDerivation_1) :
            PointDerivation I g)
          ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
              toDerivation_1 :
            PointDerivation I g))
    (h :
      (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
          Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
        (↑{ toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 : LeftInvariantDerivation I G } :
          Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)),
    { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } =
      { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 }
⊢ { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } = Y

Tactic:
cases Y
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
toDerivation : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant'' :
  ∀ (g : G),
    Eq (α := PointDerivation I g)
      ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
          ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
            toDerivation) :
        PointDerivation I g)
      ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
          toDerivation :
        PointDerivation I g)
toDerivation_1 : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
left_invariant''_1 :
  ∀ (g : G),
    Eq (α := PointDerivation I g)
      ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
          ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
            toDerivation_1) :
        PointDerivation I g)
      ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
          toDerivation_1 :
        PointDerivation I g)
h :
  (↑{ toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } :
      Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) =
    (↑{ toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 : LeftInvariantDerivation I G } :
      Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ { toDerivation := toDerivation, left_invariant'' := left_invariant'' : LeftInvariantDerivation I G } =
    { toDerivation := toDerivation_1, left_invariant'' := left_invariant''_1 }

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
⊢ (↑(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
        C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ →ₗ[𝕜] C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯).toFun =
    (⇑X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
⊢ Function.Injective (α := LeftInvariantDerivation I G) (β := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (DFunLike.coe (β := fun (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) ↦ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
X Y : LeftInvariantDerivation I G
h :
  ∀ (f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯),
    Eq (α := C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
      ((Y : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
⊢ X = Y

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
⊢ Eq (α := (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (⇑(↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (⇑X : (a : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Monoid G
inst_7 : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
⊢ Eq (α := PointDerivation I g)
    ((𝒅ₕ (f := 𝑳 I g) ⋯ : (a : PointDerivation I 1) → PointDerivation I g)
        ((Derivation.evalAt 1 : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I 1)
          (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯)) :
      PointDerivation I g)
    ((Derivation.evalAt g : (a : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) → PointDerivation I g)
        (↑X : Derivation 𝕜 C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯) :
      PointDerivation I g)

Tactic:
left_invariant'' X g

Premises used: LeftInvariantDerivation.left_invariant''