awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x = (s, t)
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
have hx₁ : x.1 = s ∧ x.2 = t
Tactic: simp only [Prod.ext_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
x : Finset α × Finset α
hx : x.1 = s ∧ x.2 = t
⊢ min (minOrder α) (↑(#s + #t - 1) : ℕ∞) ≤ (↑(#(s * t)) : ℕ∞)
have obtain : ∀ (hs : x.1.Nonempty) (ht : x.2.Nonempty), min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)
Tactic: obtain ⟨rfl, rfl⟩ := hx
Cleared hypotheses: s, t, hs, ht, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
x : Finset α × Finset α
hs : x.1.Nonempty
ht : x.2.Nonempty
⊢ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)
have refine : ∀ (y : Finset α × Finset α),
  Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} y →
    (∀ (z : Finset α × Finset α),
        Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} z →
          DevosMulRel z y →
            (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) z) →
      (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) y
Tactic: refine wellFoundedOn_devosMulRel.induction (P := fun x : Finset α × Finset α ↦
    min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ #(x.1 * x.2)) ⟨hs, ht⟩ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : (s, t).1.Nonempty
ht : (s, t).2.Nonempty
ih :
  ∀ (z : Finset α × Finset α),
    Membership.mem (γ := Set (Finset α × Finset α)) {x : Finset α × Finset α | x.1.Nonempty ∧ x.2.Nonempty} z →
      DevosMulRel z (s, t) →
        (fun (x : Finset α × Finset α) ↦ min (minOrder α) (↑(#x.1 + #x.2 - 1) : ℕ∞) ≤ (↑(#(x.1 * x.2)) : ℕ∞)) z
⊢ min (minOrder α) (↑(#(s, t).1 + #(s, t).2 - 1) : ℕ∞) ≤ (↑(#((s, t).1 * (s, t).2)) : ℕ∞)
have simp : ∀
  (ih :
    ∀ (a b : Finset α),
      a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1),
  minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: simp only [min_le_iff, tsub_le_iff_right, Prod.forall, Set.mem_setOf_eq, and_imp,
    Nat.cast_le] at *
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inl : ∀ (hts : #t < #s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hts | hst := lt_or_ge #t #s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
inl : ∀ (hts : #t < #s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (hst : #s ≤ #t), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hts | hst := lt_or_ge #t #s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (a : α) (hs : Finset.Nonempty (α := α) {a})
  (ih :
    ∀ (a_1 b : Finset α),
      a_1.Nonempty →
        b.Nonempty → DevosMulRel (a_1, b) ({a}, t) → minOrder α ≤ (↑(#(a_1 * b)) : ℕ∞) ∨ #a_1 + #b ≤ #(a_1 * b) + 1)
  (hst : card (α := α) {a} ≤ #t), minOrder α ≤ (↑(#({a} * t)) : ℕ∞) ∨ card (α := α) {a} + #t ≤ #({a} * t) + 1
Tactic: obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
Cleared hypotheses: s, hs, ih, hst
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
inr :
  ∀ (a : α) (hs : Finset.Nonempty (α := α) {a})
    (ih :
      ∀ (a_1 b : Finset α),
        a_1.Nonempty →
          b.Nonempty → DevosMulRel (a_1, b) ({a}, t) → minOrder α ≤ (↑(#(a_1 * b)) : ℕ∞) ∨ #a_1 + #b ≤ #(a_1 * b) + 1)
    (hst : card (α := α) {a} ≤ #t), minOrder α ≤ (↑(#({a} * t)) : ℕ∞) ∨ card (α := α) {a} + #t ≤ #({a} * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr₁ : ∀ (a : α) (ha : a ∈ (↑s : Set α)) (b : α) (hb : b ∈ (↑s : Set α)) (hab : a ≠ b),
  minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (g : α) (hg : g ≠ 1) (hgs : (s ∩ op g • s).Nonempty), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain ⟨g, hg, hgs⟩ : ∃ g : α, g ≠ 1 ∧ (s ∩ op g • s).Nonempty :=
    ⟨b⁻¹ * a, inv_mul_eq_one.not.2 hab.symm, _,
      mem_inter.2 ⟨ha, mem_smul_finset.2 ⟨_, hb, by simp⟩⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (hsg : op g • s = s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hsg | hsg := eq_or_ne (op g • s) s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
inr : ∀ (hsg : op g • s = s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr₁ : ∀ (hsg : op g • s ≠ s), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hsg | hsg := eq_or_ne (op g • s) s
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
⊢ (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
have refine_1 : ∀ (c : α) (hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c), (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g)
Tactic: refine forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
refine_1 : ∀ (c : α) (hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c), (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g)
⊢ (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
have refine_2 : ∀ (c : α) (hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c), (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g⁻¹)
Tactic: refine forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
⊢ (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) (c * g)
have refine_1 : (fun (x : α) ↦ x ∈ op g • a⁻¹ • (↑s : Set α)) (c * g)
Tactic: rw [← hsg, coe_smul_finset, smul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)
have refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)
have refine_2₁ : (op g)⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₁ : (op g)⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)
have refine_2₂ : c ∈ op g • a⁻¹ • (↑s : Set α)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₁ : (op g)⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₂ : c ∈ op g • a⁻¹ • (↑s : Set α)
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)
have refine_2₃ : c ∈ a⁻¹ • op g • (↑s : Set α)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : (fun (x : α) ↦ x ∈ a⁻¹ • (↑s : Set α)) c
refine_2 : op g⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₁ : (op g)⁻¹ • c ∈ a⁻¹ • (↑s : Set α)
refine_2₂ : c ∈ op g • a⁻¹ • (↑s : Set α)
refine_2₃ : c ∈ a⁻¹ • op g • (↑s : Set α)
⊢ c * g⁻¹ ∈ a⁻¹ • (↑s : Set α)
have refine_2₄ : c ∈ a⁻¹ • (↑(op g • s) : Set α)
Tactic: rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
Tactic: have hS : (zpowers g : Set α) ⊆ a⁻¹ • (s : Set α) := by
      refine forall_mem_zpowers.2 <| @zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α))
        ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_
      · rw [← hsg, coe_smul_finset, smul_comm]
        exact Set.smul_mem_smul_set hc
      · simp only
        rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm,
          ← coe_smul_finset, hsg]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : Nat.card.{u_2} (↑(a⁻¹ • (↑s : Set α)) : Type u_2) = #s
Tactic: refine Or.inl ((minOrder_le_natCard (zpowers_ne_bot.2 hg) <|
      s.finite_toSet.smul_set.subset hS).trans <| WithTop.coe_le_coe.2 <|
        ((Nat.card_mono s.finite_toSet.smul_set hS).trans_eq <| ?_).trans <|
          card_le_card_mul_right ht)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
hS : (↑(zpowers g) : Set α) ⊆ a⁻¹ • (↑s : Set α)
⊢ Nat.card.{u_2} (↑(a⁻¹ • (↑s : Set α)) : Type u_2) = #s
have inr : Nat.card.{u_2} (↑(↑(a⁻¹ • s) : Set α) : Type u_2) = #s
Tactic: rw [← coe_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s ≠ s
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have hsg₁ : #(s ∩ op g • s) < #s
Tactic: replace hsg : #(s ∩ op g • s) < #s := card_lt_card ⟨inter_subset_left, fun h ↦
    hsg <| eq_of_superset_of_card_ge (h.trans inter_subset_right) (card_smul_finset _ _).le⟩
Cleared hypotheses: hsg
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
Tactic: replace aux1 := card_mono <| mulETransformLeft.fst_mul_snd_subset g (s, t)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (hypothesis)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
Tactic: replace aux2 := card_mono <| mulETransformRight.fst_mul_snd_subset g (s, t)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : ∀ (hgt : Disjoint t (g⁻¹ • t)), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
inr : ∀ (hgt : Disjoint t (g⁻¹ • t)), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr₁ : ∀ (hgt : (t ∩ g⁻¹ • t).Nonempty), minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
Tactic: obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : Disjoint t (g⁻¹ • t)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #t ≤ #(s * t) + 1
have inr : minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #(g⁻¹ • t) ≤ #(s * t) + 1
Tactic: rw [← card_smul_finset g⁻¹ t]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : Disjoint t (g⁻¹ • t)
⊢ minOrder α ≤ (↑(#(s * t)) : ℕ∞) ∨ #s + #(g⁻¹ • t) ≤ #(s * t) + 1
have inr : #s + #(g⁻¹ • t) ≤ #(s * t) + 1
Tactic: right
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.CauchyDavenport (goal)
Goal:
α : Type u_2
inst : Group α
inst_1 : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ (↑(#(a * b)) : ℕ∞) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ (↑s : Set α)
b : α
hb : b ∈ (↑s : Set α)
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : Disjoint t (g⁻¹ • t)
⊢ #s + #(g⁻¹ • t) ≤ #(s * t) + 1
have inr : #(t ∪ g⁻¹ • t) ≤ #(s * t) + 1
Tactic: grw [hst, ← card_union_of_disjoint hgt]