mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: ⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
by
  refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)
  refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩
  funext α
  ext S
  refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs (f y)⟩
  by_contra hsx
  have : (↾fun _ => ULift.up true) = ↾fun _ => ULift.up false :=
    (hs PUnit (↾fun _ => x)).isSeparatedFor.ext
      fun β f hf => by
        dsimp
        ext y
        exact hsx.elim <| S.2 hf (↾fun _ => y)
  simp [ConcreteCategory.hom_ext_iff] at this

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B ↔
    A ≤ B

Tactic:
constructor
    · intro h
      have : range (Subobject.mk A.ι).arrow ≤ range (Subobject.mk B.ι).arrow :=
        leOfHom (((equivalenceMonoOver F).trans
          (ThinSkeleton.equivalence _).symm).inverse.map (homOfLE h))
      simpa using this
    · intro h
      exact leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE h))

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
have : χ' ≫ eΩ.inv = 𝒞.χ m := by
      apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
      exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
this : χ' ≫ eΩ.inv = 𝒞.χ m
⊢ χ' = 𝒞.χ m ≫ eΩ.hom
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a = f b

Tactic:
h ha hb hc (hf (mul_mem_mul ha hc) (mul_mem_mul hb hb) <| by rwa [map_mul, map_mul])

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f b = f b
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod

Tactic:
← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]),

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ f s.prod = (map (⇑f) t).prod
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ f t.prod = (map (⇑f) t).prod

Tactic:
map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n✝ : ℕ
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hfAB : MapsTo (⇑f) A B
n : ℕ
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n + 1
ht : t.card = n + 1
h : s.prod = t.prod
⊢ (map (⇑f) t).prod = (map (⇑f) t).prod
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ x ∈ Iio ↑(k + 1) ↔ x ∈ Iic ↑k

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Iio, lt_def, mem_Iic, le_iff_val_le_val,
      val_natCast, aux hm hkmn', Nat.mod_eq_of_lt]

Goal state after:
case e'_6
m n : ℕ
hm : m ≠ 0
k : ℕ
hkmn : m * (k + 1) ≤ n
hkmn' : m * k ≤ n
x : Fin (n + 1)
⊢ ↑x < ↑(↑k + 1) ↔ ↑x ≤ k
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case a
N : ℕ
hN : 4096 ≤ N
n : ℕ := ⋯
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ n - 2 ≠ 0

pp: case hab
N : ℕ
hN : 4096 ≤ N
n : ℕ := ⋯
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N ^ (↑(nValue N))⁻¹ / rexp 1 < ↑(dValue N)

Tactic:
exacts [(tsub_pos_of_lt hn₂).ne', bound hN]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) < ↑(rothNumberNat N)

Tactic:
by
  let n := nValue N
  have hn : 0 < (n : ℝ) := cast_pos.2 (nValue_pos <| hN.trans' <| by norm_num1)
  have hd : 0 < dValue N := dValue_pos (hN.trans' <| by norm_num1)
  have hN₀ : 0 < (N : ℝ) := cast_pos.2 (hN.trans' <| by norm_num1)
  have hn₂ : 2 < n := three_le_nValue <| hN.trans' <| by norm_num1
  have : (2 * dValue N - 1) ^ n ≤ N := le_N (hN.trans' <| by norm_num1)
  calc
    _ ≤ (N ^ (nValue N : ℝ)⁻¹ / rexp 1 : ℝ) ^ (n - 2) / n := ?_
    _ < _ := by gcongr; exacts [(tsub_pos_of_lt hn₂).ne', bound hN]
    _ ≤ rothNumberNat ((2 * dValue N - 1) ^ n) := bound_aux hd.ne' hn₂.le
    _ ≤ rothNumberNat N := mod_cast rothNumberNat.mono this
  rw [← rpow_natCast, div_rpow (rpow_nonneg hN₀.le _) (exp_pos _).le, ← rpow_mul hN₀.le,
    inv_mul_eq_div, cast_sub hn₂.le, cast_two, same_sub_div hn.ne', exp_one_rpow,
    div_div, rpow_sub hN₀, rpow_one, div_div, div_eq_mul_inv]
  gcongr _ * ?_
  rw [mul_inv, mul_inv, ← exp_neg, ← rpow_neg (cast_nonneg _), neg_sub, ← div_eq_mul_inv]
  have : exp (-4 * √(log N)) = exp (-2 * √(log N)) * exp (-2 * √(log N)) := by
    rw [← exp_add, ← add_mul]
    norm_num
  rw [this]
  gcongr
  · rw [← le_log_iff_exp_le (rpow_pos_of_pos hN₀ _), log_rpow hN₀, ← le_div_iff₀, mul_div_assoc,
      div_sqrt, neg_mul, neg_le_neg_iff, div_mul_eq_mul_div, div_le_iff₀ hn]
    · gcongr
      apply le_ceil
    refine Real.sqrt_pos.2 (log_pos ?_)
    rw [one_lt_cast]
    exact hN.trans_lt' (by norm_num1)
  · refine (exp_neg_two_mul_le <| Real.sqrt_pos.2 <| log_pos ?_).le
    rw [one_lt_cast]
    exact hN.trans_lt' (by norm_num1)

Goal state after:
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case h₁
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ m ⊆ ↑F₁ ^ (m - 1) * A

Tactic:
apply pow_subset_pow_mul_of_sq_subset_mul

Goal state after:
case h₁.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ 2 ⊆ ↑F₁ * A

case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ m ≠ 0
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case h₂
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ B ^ n ⊆ ↑F₂ ^ (n - 1) * B

Tactic:
apply pow_subset_pow_mul_of_sq_subset_mul

Goal state after:
case h₂.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ B ^ 2 ⊆ ↑F₂ * B

case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ n ≠ 0
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ A ^ m ∩ B⁻¹ ^ n = A ^ m ∩ B ^ n

Tactic:
hB.inv_eq_self

Goal state after:
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x

Tactic:
by
  ext : 1 <;> dsimp
  · rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]
    exact inter_subset_union
  · rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
    exact inter_subset_union

Goal state after:
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : 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

Tactic:
obtain hts | hst := lt_or_ge #t #s

Goal state after:
case inl
α : Type u_2
inst✝¹ : Group α
inst✝ : 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
hts : #t < #s
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

case inr
α : Type u_2
inst✝¹ : Group α
inst✝ : 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
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝¹ : Group α
inst✝ : 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
hts : #t < #s
⊢ #((t⁻¹, s⁻¹).1 * (t⁻¹, s⁻¹).2) = #((s, t).1 * (s, t).2) ∧
    #(t⁻¹, s⁻¹).1 + #(t⁻¹, s⁻¹).2 = #(s, t).1 + #(s, t).2 ∧ #(t⁻¹, s⁻¹).1 < #(s, t).1

Tactic:
by
          simpa only [← mul_inv_rev, add_comm, card_inv, true_and]

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂

Tactic:
isCorner_iff,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ∧
      (f x₁, f y₂) ∈ Prod.map f f '' A ∧ (f x₂, f y₁) ∈ Prod.map f f '' A ∧ f x₁ + f y₂ = f x₂ + f y₁ ↔
    IsCorner A x₁ y₁ x₂ y₂
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := ⋯
V : Finset G := ⋯
W : Finset G := ⋯
⊢ ↑(#(π (Fin.cons 1 (tail (tail ε))))) ≤ k ^ (m - 1) * ↑(#A)

Tactic:
· exact ih (Fin.cons 1 <| tail <| tail ε) <| Fin.cons (by simp) (by simp [hε, Fin.tail])

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inl.inr.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = 1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
nlinarith [small_pos_neg_pos_mul hA]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case h.mpr
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝ y✝ : W
e : Sym2 V
hadj : e ∈ G.edgeSet
he : f.sym2Map e = s(x✝, y✝)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝ ∧ f v' = y✝

Tactic:
induction e

Goal state after:
case h.mpr.h
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ y✝¹ : W
x✝ y✝ : V
hadj : s(x✝, y✝) ∈ G.edgeSet
he : f.sym2Map s(x✝, y✝) = s(x✝¹, y✝¹)
⊢ ∃ u' v', G.Adj u' v' ∧ f u' = x✝¹ ∧ f v' = y✝¹
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G ≃g G'
φst : Set.BijOn (⇑φ) s t
ψ : G' ≃g G''
ψtr : Set.BijOn (⇑ψ) t r
⊢ (ψ.induce ψtr).comp (φ.induce φst) = (ψ.comp φ).induce ⋯

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
⊢ ⊥ ∉ Finset.map (↑e).toEmbedding P.parts

Tactic:
by
    rw [mem_map_equiv]
    convert! P.bot_notMem
    exact e.symm.map_bot

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
⊢ b ∈ P.parts

Tactic:
obtain ⟨d, hd, hcd⟩ := hPQ hc

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ b ∈ P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a = b
⊢ (P.extendOfLE ⋯).parts = P.parts

Tactic:
subst hab; simp [extendOfLE]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ z ∈ i

Tactic:
← hz2.2 _ (hR hi)

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
i : Finset α
hi : i ∈ R
⊢ i ∈ R
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
rcases trichotomous_of WellOrderingRel s t with (lt | rfl | gt)

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s : Finset α
h₁ : s ≠ s
h₂ : ¬G.IsUniform ε s s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2)
            (if WellOrderingRel s s then (G.nonuniformWitnesses ε s s).1 else (G.nonuniformWitnesses ε s s).2) -
          G.edgeDensity s s|

case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤
    ↑|G.edgeDensity (if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2)
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
⊢ P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) ⊆ (increment hP G ε).parts.offDiag

Tactic:
rintro ⟨Ui, Vj⟩
  simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
    mem_product, mem_attach, true_and, Subtype.exists, and_imp,
    mem_offDiag, forall_exists_index, Ne]
  refine fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, ?_⟩
  rintro rfl
  obtain ⟨i, hi⟩ := nonempty_of_mem_parts _ hUi
  exact hUV.2.2 (P.disjoint.elim_finset hUV.1 hUV.2.1 i (Finpartition.le _ hUi hi) <|
    Finpartition.le _ hVj hi)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.spanningCoe.edgeSet = G'.edgeSet

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
e : Sym2 V
v : V
he : e ∈ G'.edgeSet
hv : v ∈ e
⊢ v ∈ G'.verts

Tactic:
induction e

Goal state after:
case h
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v x✝ y✝ : V
he : s(x✝, y✝) ∈ G'.edgeSet
hv : v ∈ s(x✝, y✝)
⊢ v ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
s : Set G.Subgraph
⊢ ∀ {v w : V}, (∃ G' ∈ s, G'.Adj v w) → v ∈ ⋃ G' ∈ s, G'.verts

Tactic:
rintro a b ⟨G', hG', hab⟩

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a✝ b✝ : V
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hG' : G' ∈ s
hab : G'.Adj a b
⊢ a ∈ ⋃ G' ∈ s, G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sSup s).edgeSet ↔ e ∈ ⋃ G' ∈ s, G'.edgeSet

Tactic:
induction e

Goal state after:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sSup s).edgeSet ↔ s(x✝, y✝) ∈ ⋃ G' ∈ s, G'.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
induction e

Goal state after:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sInf s).edgeSet ↔ s(x✝, y✝) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective ⇑(g.toHom.comp f.toHom)

Tactic:
Hom.coe_comp

Goal state after:
case injective'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective (⇑g.toHom ∘ ⇑f.toHom)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts},
    (Subgraph.map f.toHom A').coe.Adj ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) a)
        ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) b) ↔
      A'.coe.Adj a b

Tactic:
Subgraph.map_verts,

Goal state after:
case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts},
    (Subgraph.map f.toHom A').coe.Adj ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) a)
        ((Equiv.Set.image (⇑f.toHom) A'.verts ⋯) b) ↔
      A'.coe.Adj a b