mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝¹ a b b✝ c✝ : V
a✝ : Path a b✝
e : b✝ ⟶ c✝
ih : height a ≤ height b✝
⊢ height a ≤ height c✝

Tactic:
| cons _ e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case refl
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ a = a ∧ ⟨e, ⋯⟩ ≍ ⟨e, ⋯⟩

Tactic:
constructor

Goal state after:
case refl.left
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ a = a

case refl.right
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
a c : WideSubquiver.toType V (geodesicSubtree r)
e : a ⟶ c
p : Path r a
h j : shortestPath r c = p.cons e
⊢ ⟨e, ⋯⟩ ≍ ⟨e, ⋯⟩
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v) ↔
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

Tactic:
constructor

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v) →
    ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

case mpr
V : Type u_2
inst✝ : Quiver V
v : V
⊢ (∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))) →
    ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a : V
⊢ ∀ (x : V), x ∈ {v | v = a} ↔ x = a

Tactic:
exact fun x ↦ Set.mem_ofPred

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.dropLast ++ [p.vertices.getLast ⋯] = p.vertices

Tactic:
dropLast_concat_getLast

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
⊢ (a * b) • x = a • b • x

Tactic:
ext

Goal state after:
V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
a b : M
x : SchreierGraph V ι
⊢ ((a * b) • x).toVertex = (a • b • x).toVertex
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ 1 • x = x

Tactic:
ext

Goal state after:
V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ (1 • x).toVertex = x.toVertex
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u : U
⊢ Injective (φ.pathStar u)

Tactic:
dsimp +unfoldPartialApp [Prefunctor.pathStar, Quiver.PathStar.mk]
  rintro ⟨v₁, p₁⟩
  induction p₁ with
  | nil =>
    rintro ⟨y₂, p₂⟩
    rcases p₂ with - | ⟨p₂, e₂⟩
    · intro; rfl -- Porting note: goal not present in lean3.
    · intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
      exact (Path.nil_ne_cons _ _) h'
  | cons p₁ e₁ ih =>
    rename_i x₁ y₁
    rintro ⟨y₂, p₂⟩
    rcases p₂ with - | ⟨p₂, e₂⟩
    · intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      exfalso
      obtain ⟨h, h'⟩ := h
      rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
      exact (Path.cons_ne_nil _ _) h'
    · rename_i x₂
      intro h
      simp only [mapPath_cons, Sigma.mk.inj_iff] at h
      obtain ⟨hφy, h'⟩ := h
      rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'
      have hφx := Path.obj_eq_of_cons_eq_cons h'
      have hφp := Path.heq_of_cons_eq_cons h'
      have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
      have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
        simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩
      cases ih h_path_star
      have h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩ := by
        simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]; exact ⟨hφy, hφe⟩
      cases hφ x₁ h_star
      rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ {b | b ∈ s ⊻ t ∧ b ≤ a} = {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊻ t ∧ b ≤ a} ↔ x✝ ∈ {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ {b | b ∈ s ⊼ t ∧ a ≤ b} = {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊼ t ∧ a ≤ b} ↔ x✝ ∈ {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a

case mpr
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a) → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_2) ∧ a_2 ≤ a
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔ a ∈ lowerClosure s ⊓ lowerClosure t

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) → a ∈ lowerClosure s ⊓ lowerClosure t

case mpr
α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ a ∈ lowerClosure s ⊓ lowerClosure t → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t

Tactic:
by
  ext a
  simp only [SetLike.mem_coe, mem_lowerClosure, Set.mem_infs]
  constructor
  · rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩
    exact ⟨⟨b, hb, ha.trans inf_le_left⟩, c, hc, ha.trans inf_le_right⟩
  · rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩
    exact ⟨_, ⟨b, hb, c, hc, rfl⟩, le_inf hab hac⟩

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s ↔ ∃ a_1 ∈ 𝒜, a_1.erase a = s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s → ∃ a_2 ∈ 𝒜, a_2.erase a = s

case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s ∨ s ∈ 𝒜 ∧ a ∉ s
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (memberSubfamily a 𝒜) = ∅

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ ∅
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (nonMemberSubfamily a 𝒜) = ∅

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ memberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ ∅
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (memberSubfamily a 𝒜) = memberSubfamily a 𝒜

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ memberSubfamily a 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) = nonMemberSubfamily a 𝒜

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ nonMemberSubfamily a 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ↑(#({a ∈ Ioc 0 1 | a ∈ A})) / ↑1 ≤ 1

Tactic:
by rw [Nat.cast_one, div_one, Nat.cast_le_one]; exact card_filter_le _ _

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A

Tactic:
constructor

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A → {0}ᶜ ⊆ A

case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ {0}ᶜ ⊆ A → 1 ≤ schnirelmannDensity A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ

Tactic:
constructor

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A → A = Set.univ

case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ A = Set.univ → {0}ᶜ ⊆ A
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
this : ∀ i ∈ range (n + 1), f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
⊢ ∑ i ∈ range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1

Tactic:
rw [← sum_congr rfl this, sum_range_sub', hf]
    simp [choose_zero_right]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
⊢ (s ○ t).Nonempty → s.Nonempty

Tactic:
simp_rw [Finset.Nonempty, mem_disjSups]
  exact fun ⟨_, a, ha, _⟩ => ⟨a, ha⟩

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u : Finset α
⊢ s ○ (t ○ u) = t ○ (s ○ u)

Tactic:
by
  simp_rw [← disjSups_assoc, disjSups_comm s]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
⊢ sᶜˢᶜˢ = s

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a✝ : α
⊢ a✝ ∈ sᶜˢᶜˢ ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
⊢ univᶜˢ = univ

Tactic:
ext

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univᶜˢ ↔ a✝ ∈ univ
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊼ tᶜˢ = s \\ t

Tactic:
ext

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ⊼ tᶜˢ ↔ a✝ ∈ s \\ t
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = 1 ↔ #t = #t✝ + 1

Tactic:
card_sdiff_of_subset hst,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t - #t✝ = 1 ↔ #t = #t✝ + 1
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s

Tactic:
have h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅ :=
    filter_false_of_mem fun a ha h ↦ h <| compress_mem_compression_of_mem_compression ha

Goal state after:
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
inst✝ : DecidableEq α
u v : α
s : Finset α
h : {a ∈ 𝓒 u v s | compress u v a ∉ 𝓒 u v s} = ∅
⊢ 𝓒 u v (𝓒 u v s) = 𝓒 u v s
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜) → ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k

case mpr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = k) → ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = k ↔ #t = #t✝ + k

Tactic:
card_sdiff_of_subset hst,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t - #t✝ = k ↔ #t = #t✝ + k
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = 1 ↔ #t✝ = #t + 1

Tactic:
card_sdiff_of_subset hst,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ - #t = 1 ↔ #t✝ = #t + 1
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
constructor

Goal state after:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) →
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜) →
    ∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = k ↔ #t✝ = #t + k

Tactic:
card_sdiff_of_subset hst,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t✝ - #t = k ↔ #t✝ = #t + k
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) ↔ ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

Tactic:
constructor

Goal state after:
case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s) → ∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s

case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, t ⊆ s ∧ #t + (k + 1) = #s) → ∃ t ∈ ∂⁺ 𝒜, t ⊆ s ∧ #t + k = #s
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
j : ι
hj : j ∈ cons i s hi
⊢ (f j ⊆ if hj : j ∈ cons i s hi then ⋯.choose else ∅) ∧
    2 * #(if hj : j ∈ cons i s hi then ⋯.choose else ∅) = 2 ^ Fintype.card α ∧
      (↑(if hj : j ∈ cons i s hi then ⋯.choose else ∅)).Intersecting

Tactic:
dif_pos hj,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
j : ι
hj : j ∈ cons i s hi
⊢ f j ⊆ ⋯.choose ∧ 2 * #⋯.choose = 2 ^ Fintype.card α ∧ (↑⋯.choose).Intersecting
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
f : Finset α → β
⊢ collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) + if insert a s ∈ 𝒜 then f (insert a s) else 0

Tactic:
rw [collapse, filter_collapse_eq ha]
  split_ifs <;> simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s) ↔
    #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs))

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ (∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s) →
    #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs))

case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs)) →
    ∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs))

Tactic:
constructor

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ #(s.erase (s.min' hs)) = #t

case mp.right
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
a : α
ha : a ∉ t
hst : #s = #(insert a t)
hts : toColex (insert a t) ≤ toColex s
⊢ toColex t ≤ toColex (s.erase (s.min' hs))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s) → (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

case mpr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k → s ∈ 𝒜 ∧ #s = k ∨ ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = k + 1) ∧ ∃ a ∈ s_1, s_1.erase a = s
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
refine ⟨erase v a, hv.2, ?_⟩
      rw [inter_erase, hsv, erase_insert]
      rintro ha
      rw [insert_eq_self.2 (mem_inter.1 ha).2] at hu
      exact hu.1 hu.2

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ s ∈ powersetCard (#s) univ

Tactic:
exact ⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s ↔ x ∈ {x | (mkClasses c H) x y}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

case mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Bijective (Quot.lift f f_respects_relation)

Tactic:
constructor

Goal state after:
case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Injective (Quot.lift f f_respects_relation)

case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective (Quot.lift f f_respects_relation)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

Tactic:
constructor

Goal state after:
case mp
V : Type u
G : SimpleGraph V
u v : V
⊢ G.Reachable u v → Relation.ReflTransGen G.Adj u v

case mpr
V : Type u
G : SimpleGraph V
u v : V
⊢ Relation.ReflTransGen G.Adj u v → G.Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Reachable = Relation.ReflTransGen G.Adj

Tactic:
ext

Goal state after:
V : Type u
G : SimpleGraph V
x✝¹ x✝ : V
⊢ G.Reachable x✝¹ x✝ ↔ Relation.ReflTransGen G.Adj x✝¹ x✝