mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod

Tactic:
map_congr rfl fun x hx => (h (hsA hx)).symm,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
⊢ (map f₁ s).prod = (map f₂ t).prod
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : t.Nonempty
hb : ∑ x ∈ s, 1 ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 ≤ b

Tactic:
refine
    exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f s).prod = (map f t).prod ↔ s.prod = t.prod

pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B

Tactic:
hf.map_prod_eq_map_prod hsA htA hs ht

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ s.prod = t.prod ↔ s.prod = t.prod

α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B

α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
A : Set α
B : Set β
C : Set γ
f : α → β
g : β → γ
n : ℕ
hg : IsMulFreimanIso n B C g
hf : IsMulFreimanIso n A B f
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree ↑(sphere n d k)

Tactic:
refine ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _))
    ((toLp_injective 2).comp_injOn cast_injective.comp_left.injOn) (Set.subset_univ _) ?_

Goal state after:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
⊢ ThreeAPFree (⇑f '' ↑(sphere n d k))
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(U * (A * C))) ≤ ↑(#(U * A)) / ↑(#U) * ↑(#(U * C))

Tactic:
rw [← mul_div_right_comm, ← mul_assoc, le_div_iff₀ (cast_pos.2 hU.1.card_pos), mul_comm _ C,
    ← mul_assoc, mul_comm _ C]

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(C * U * A)) * ↑(#U) ≤ ↑(#(U * A)) * ↑(#(C * U))
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)

Tactic:
obtain ⟨C, hC, hCmin⟩ :=
    exists_min_image (A.powerset.erase ∅) (fun C ↦ #(C * B) / #C : _ → ℚ≥0) ⟨A, hA'⟩

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
m n : ℕ
hA' : A ∈ A.powerset.erase ∅
C : Finset G
hC : C ∈ A.powerset.erase ∅
hCmin : ∀ x' ∈ A.powerset.erase ∅, ↑(#(C * B)) / ↑(#C) ≤ ↑(#(x' * B)) / ↑(#x')
⊢ ↑(#(B ^ m / B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ (m + n) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: 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 := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
i : Fin 3
⊢ |![1, -ε 1, -ε 0] i| = 1

Tactic:
fin_cases i

Goal state after:
case «0»
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 := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨0, ⋯⟩)| = 1

case «1»
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 := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨1, ⋯⟩)| = 1

case «2»
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 := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ |![1, -ε 1, -ε 0] ((fun i ↦ i) ⟨2, ⋯⟩)| = 1
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: 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
⊢ #A ≤ #(A ^ 3)

Tactic:
exact card_le_card_pow (by simp)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype.card G.Dart = 2 * #G.edgeFinset

Tactic:
rw [← card_univ]
  rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
      by rw [mem_coe, mem_edgeFinset]; apply Dart.edge_mem]
  rw [← mul_comm, sum_const_nat]
  intro e h
  apply G.dart_edge_fiber_card e
  rwa [← mem_edgeFinset]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s).EquitableOn f ↔ ∀ a ∈ s, f a = (∑ i ∈ s, f i) / #s ∨ f a = (∑ i ∈ s, f i) / #s + 1

Tactic:
by
  simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ #⊤.edgeFinset = (Fintype.card V).choose 2

Tactic:
edgeFinset,

Goal state after:
V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ #⊤.edgeSet.toFinset = (Fintype.card V).choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ ↑G.edgeFinset ⊆ (↑s.toFinset).sym2

Tactic:
edgeFinset,

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ ↑G.edgeSet.toFinset ⊆ (↑s.toFinset).sym2
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) =
    #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts

Tactic:
hP.card_large_parts_eq_mod,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) = #s % #P.parts + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝¹ : Lattice (Subtype Pr) := ⋯
this✝ : OrderBot (Subtype Pr) := ⋯
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ↑(id i) ∈ P.parts

pp: case a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝¹ : Lattice (Subtype Pr) := ⋯
this✝ : OrderBot (Subtype Pr) := ⋯
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ↑(id i) ∉ image Subtype.val t

Tactic:
· simpa using hi

Goal state after:
case a
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝¹ : Lattice (Subtype Pr) := ⋯
this✝ : OrderBot (Subtype Pr) := ⋯
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
this : (fun i ↦ ↑(id i)) = id ∘ Subtype.val
⊢ ↑(id i) ∉ image Subtype.val t
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)

Tactic:
rcases eq_or_ne x₁ x₂ with (rfl | xdiff)

Goal state after:
case inl
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
y₂ : α
hy₂ : y₂ ∈ Q.parts
hx₂ : x₁ ∈ P.parts
h : ¬x₁ ⊓ y₂ = x₁ ⊓ y₁
⊢ Disjoint (x₁ ⊓ y₁) (x₁ ⊓ y₂)

case inr
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
x₁ y₁ : α
hx₁ : x₁ ∈ P.parts
hy₁ : y₁ ∈ Q.parts
x₂ y₂ : α
hx₂ : x₂ ∈ P.parts
hy₂ : y₂ ∈ Q.parts
h : ¬x₂ ⊓ y₂ = x₁ ⊓ y₁
xdiff : x₁ ≠ x₂
⊢ Disjoint (x₁ ⊓ y₁) (x₂ ⊓ y₂)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ (I.biUnion fun i ↦ (P i).parts).sup id = I.sup a

Tactic:
rw [sup_biUnion]
    exact sup_congr rfl fun i _ => (P i).sup_parts

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
x : (t : ↥P.parts) × ↥↑t
e : α
⊢ e ∈ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) x)).fst ↔ e ∈ ↑x.fst

Tactic:
obtain ⟨⟨p, mp⟩, ⟨f, mf⟩⟩ := x

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a e : α
p : Finset α
mp : p ∈ P.parts
f : α
mf : f ∈ ↑⟨p, mp⟩
⊢ e ∈ ↑((fun x ↦ ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩) ((fun x ↦ ⟨↑x.snd, ⋯⟩) ⟨⟨p, mp⟩, ⟨f, mf⟩⟩)).fst ↔
    e ∈ ↑⟨⟨p, mp⟩, ⟨f, mf⟩⟩.fst
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
h :
  {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty} ⊆
    image (fun P ↦ {i ∈ s | ∀ x ∈ F, x ∈ insert t P ↔ i ∈ x}) (F.erase t).powerset
⊢ #(F.erase t).powerset ≤ 2 ^ (#F - 1)

Tactic:
rw [card_powerset, card_erase_of_mem ht]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ #({i ∈ ⊥.parts | #i = 0 + 1}) = b

Tactic:
by simpa [Finset.filter_true_of_mem] using hs.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2 ≤
    ↑((increment hP G ε).energy G)

Tactic:
by
        rw [coe_energy]
        gcongr
        rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
        exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ #(induce {x}ᶜ G).edgeFinset = #(G.deleteIncidenceSet x).edgeFinset

Tactic:
edgeFinset,

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
h_notMem : x ∉ {x}ᶜ
⊢ #(induce {x}ᶜ G).edgeSet.toFinset = #(G.deleteIncidenceSet x).edgeSet.toFinset
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
f : G.Copy H
hf : Surjective ⇑f
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty W
  · have := Function.isEmpty f
    simp
  refine H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_
  obtain ⟨v, rfl⟩ := hf w
  grw [← f.degree_le, ← minDegree_le_degree]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
h : x ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
obtain ⟨d, hd, hcd⟩ := ih h vS
      exact ⟨d, List.Mem.tail _ hd, hcd⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ t ∈ p.support

Tactic:
obtain ⟨d, hd, he⟩ := List.mem_map.mp he
  rw [dart_edge_eq_mk'_iff'] at he
  rcases he with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
  · exact dart_fst_mem_support_of_mem_darts _ hd
  · exact dart_snd_mem_support_of_mem_darts _ hd

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
hp : p.Nil
hq : q.Nil
⊢ (p.append q).Nil

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
⊢ nil.dropLast.length = nil.length - 1

Tactic:
simp [← length_dropLast_add_one not_nil_cons]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
⊢ (cons h✝ p✝).dropLast.length = (cons h✝ p✝).length - 1

Tactic:
simp [← length_dropLast_add_one not_nil_cons]

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
i : ℕ
hp : Walk.nil.IsPath
hi : i ≤ Walk.nil.length
⊢ Walk.nil.getVert i = u ↔ i = 0

pp: case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0

Tactic:
· simpa using hi

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u w : V
i : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ w
hp : (cons h✝ p✝).IsPath
hi : i ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert i = u ↔ i = 0
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 1 s ↔ ∃ a, s = {a}

Tactic:
simp only [isNClique_iff, card_eq_one, and_iff_right_iff_imp]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hp : p.IsCycle
⊢ p.snd ≠ p.penultimate

Tactic:
intro h
  have := hp.three_le_length
  apply hp.getVert_injOn (by simp; lia) (by simp; lia) at h
  lia

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
v : V
w : G.Walk v v
hwp : w.IsSubwalk p
⊢ w.Nil

pp: case refine_2
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
⊢ p.support.Nodup

Tactic:
· simp [w.isPath_iff_nil.mp <| isPath_of_isSubwalk hwp hp]

Goal state after:
case refine_2
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk p → w.Nil
⊢ p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
| ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
enter [a, b]; rw [G.adj_replaceVertex_iff_of_ne _ (mt a) (mt b)]

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
mt : ∀ (x : Fin n), φ x ≠ t
a b : Fin n
| G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support ++ q'.support.reverse.tail <+ p.support ++ q.support.reverse.tail

Tactic:
refine .append ?_ <| .tail <| .reverse ?_

Goal state after:
case right.refine_1
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ p'.support <+ p.support

case right.refine_2
V : Type u
G : SimpleGraph V
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
u' v' : V
p' q' : G.Walk u' v'
hp' : p'.IsSubwalk p
hq' : q'.IsSubwalk q
hcyc : (p'.append q'.reverse).IsCycle
⊢ q'.support <+ q.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x ∈ G.neighborSet v, ∃ y ∈ G.neighborSet v, x ≠ y ∧ G.Adj x y
⊢ False

Tactic:
mem_neighborSet

Goal state after:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 3
v : α
nind : ∃ x, G.Adj v x ∧ ∃ y, G.Adj v y ∧ x ≠ y ∧ G.Adj x y
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).LocallyLinear

Tactic:
by
  classical
  refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩

Goal state after: