awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α)
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
⊢ t ⊆ s'

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hat] at ht

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α)
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
ht₁ : t ⊆ s'
⊢ (↑u : Set α) ⊆ (↑(insert a s') : Set α)

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hat] at ht

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α)
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
ht₁ : t ⊆ s'
hu₁ : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
⊢ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hat] at ht

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α)
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
ht₁ : t ⊆ s'
hu₁ : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu₁ : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
⊢ a ∉ t

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hat] at ht

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
pos : ∀ (hau : a ∈ u), a ∈ s'.mulSpan
neg : ∀ (hau : a ∉ u), a ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan

Tactic:
by_cases hau : a ∈ u
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∈ u
rw : a = (∏ b ∈ t, b) / ((∏ x ∈ u, x) / a)
rw₁ : a = (∏ a ∈ u, a) / ((∏ x ∈ u, x) / a)
rw₂ rw₃ : a = a
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)

Tactic:
rw [prod_erase_eq_div hau, htu.2.2, div_div_self']

Premises used: Finset.prod_erase_eq_div, And.right, div_div_self'
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∈ u
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)

Tactic:
have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
      rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∈ u
this : a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
pos : HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b) ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan

Tactic:
rw [this]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∈ u
this : a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b) ∈ s'.mulSpan

Tactic:
prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)

Premises used: Finset.prod_div_prod_mem_mulSpan, Iff.mp, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∈ u
this : a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b) ∈ s'.mulSpan

Tactic:
exact prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)

Premises used: Finset.prod_div_prod_mem_mulSpan, Iff.mp, Finset.subset_insert_iff
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∉ u
⊢ u ⊆ s'

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hau] at hu

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∉ u
hu₁ : u ⊆ s'
⊢ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hau] at hu

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∉ u
hu₁ : u ⊆ s'
htu₁ : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
⊢ a ∉ t

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hau] at hu

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∉ u
hu₁ : u ⊆ s'
htu₁ : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat₁ : a ∉ t
⊢ a ∉ u

Tactic:
rw [coe_subset, subset_insert_iff_of_notMem hau] at hu

Premises used: Finset.subset_insert_iff_of_notMem, Finset.coe_subset
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : u ⊆ s'
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
hau : a ∉ u
⊢ a ∈ s'.mulSpan

Tactic:
cases not_mulDissociated_iff_exists_disjoint.2 ⟨t, u, ht, hu, htu⟩ hs'.1.2

Premises used: Iff.mpr, not_mulDissociated_iff_exists_disjoint, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : σₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ * B)) : ℚ≥0)
inr : ∀ (hA : A.Nonempty), σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ * B)) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ Ne (α := ℚ≥0) (↑(#A) : ℚ≥0) 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)

Tactic:
exact div_mul_cancel₀ _ (by positivity)

Premises used: div_mul_cancel₀
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : δₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ / B)) : ℚ≥0)
inr : ∀ (hA : A.Nonempty), δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ / B)) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)

Tactic:
exact div_mul_cancel₀ _ (by positivity)

Premises used: div_mul_cancel₀
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
rw₁ rw₂ : Eq (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)
⊢ (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)

Tactic:
rw [mul_comm, mulConst_mul_card]

Premises used: Finset.mulConst_mul_card, mul_comm
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
rw₁ rw₂ : Eq (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#(A / B)) : ℚ≥0)
⊢ (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)

Tactic:
rw [mul_comm, divConst_mul_card]

Premises used: Finset.divConst_mul_card, mul_comm
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] = 0

Tactic:
simp [mulConst]

Premises used: Finset.mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] = 0

Tactic:
simp [divConst]

Premises used: Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
⊢ σₘ[A, ∅] = 0

Tactic:
simp [mulConst]

Premises used: Finset.mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
⊢ δₘ[A, ∅] = 0

Tactic:
simp [divConst]

Premises used: Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = δₘ[A, B]
rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₂ rw₃ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A, B⁻¹] = δₘ[A, B]

Tactic:
rw [mulConst, divConst, ← div_eq_mul_inv]

Premises used: Finset.mulConst, div_eq_mul_inv, Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : δₘ[A, B⁻¹] = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A / B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₂ rw₃ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A, B⁻¹] = σₘ[A, B]

Tactic:
rw [mulConst, divConst, div_inv_eq_mul]

Premises used: Finset.mulConst, div_inv_eq_mul, Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
rw : LE.le (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)
rw₁ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
⊢ 1 ≤ σₘ[A, B]

Tactic:
rw [mulConst, one_le_div₀]

Premises used: Finset.mulConst, one_le_div₀
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ LE.le (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)

Tactic:
mod_cast card_le_card_mul_right hB

Premises used: cast, Nat.cast_le._simp_1, Finset.card_le_card_mul_right, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ LE.le (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)

Tactic:
exact mod_cast card_le_card_mul_right hB

Premises used: Finset.card_le_card_mul_right
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA : A.Nonempty
⊢ 1 ≤ σₘ[A]

Tactic:
one_le_mulConst hA hA

Premises used: Finset.one_le_mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
rw : 1 ≤ σₘ[A, B⁻¹]
⊢ 1 ≤ δₘ[A, B]

Tactic:
rw [← mulConst_inv_right]

Premises used: Finset.mulConst_inv_right
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ B⁻¹.Nonempty

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ σₘ[A, B⁻¹]

Tactic:
apply one_le_mulConst hA (by simpa)

Premises used: Finset.one_le_mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA : A.Nonempty
⊢ 1 ≤ δₘ[A]

Tactic:
one_le_divConst hA hA

Premises used: Finset.one_le_divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : σₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
inr : ∀ (hA' : A.Nonempty), σₘ[A, B] ≤ (↑(#B) : ℚ≥0)
⊢ σₘ[A, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
inr : (↑(#(A * B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)
⊢ σₘ[A, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
rw [mulConst, div_le_iff₀' (by positivity)]

Premises used: Finset.mulConst, div_le_iff₀'
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ (↑(#(A * B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)

Tactic:
mod_cast card_mul_le

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card_mul_le, Finset.card, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ (↑(#(A * B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)

Tactic:
exact mod_cast card_mul_le

Premises used: Finset.card_mul_le
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : δₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
inr : ∀ (hA' : A.Nonempty), δₘ[A, B] ≤ (↑(#B) : ℚ≥0)
⊢ δₘ[A, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
inr : (↑(#(A / B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)
⊢ δₘ[A, B] ≤ (↑(#B) : ℚ≥0)

Tactic:
rw [divConst, div_le_iff₀' (by positivity)]

Premises used: div_le_iff₀', Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ (↑(#(A / B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)

Tactic:
mod_cast card_div_le

Premises used: Nat.cast_mul._simp_1, congrArg, cast, HDiv.hDiv, Nat.cast_le._simp_1, LE.le, Nat.cast, Finset.card_div_le, Finset.card, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ (↑(#(A / B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)

Tactic:
exact mod_cast card_div_le

Premises used: Finset.card_div_le
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, mulConst]

Premises used: Finset.mulConst, Finset.dens, inv_div
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
hab : #(A * B) ≤ Fintype.card G
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ #(A * B) ≤ Fintype.card G

Tactic:
card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ #(A * B) ≤ Fintype.card G

Tactic:
exact card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
rw :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A, B] ≤ A.dens⁻¹

Tactic:
rw [dens, inv_div, divConst]

Premises used: Finset.dens, inv_div, Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
hab : #(A / B) ≤ Fintype.card G
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ #(A / B) ≤ Fintype.card G

Tactic:
card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ #(A / B) ≤ Fintype.card G

Tactic:
exact card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ (↑σ[A, B] : 𝕜) = HDiv.hDiv (α := 𝕜) (↑(#(A + B)) : 𝕜) (↑(#A) : 𝕜)

Tactic:
simp [addConst]

Premises used: Finset.addConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ (↑δ[A, B] : 𝕜) = HDiv.hDiv (α := 𝕜) (↑(#(A - B)) : 𝕜) (↑(#A) : 𝕜)

Tactic:
simp [subConst]

Premises used: Finset.subConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G
⊢ (↑σₘ[A, B] : 𝕜) = HDiv.hDiv (α := 𝕜) (↑(#(A * B)) : 𝕜) (↑(#A) : 𝕜)

Tactic:
simp [mulConst]

Premises used: Finset.mulConst