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

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
have hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end := by
      simpa using (mem_vertices_cons pPrev e).1 hv
    have h_case₁ : v = (pPrev.cons e).end → ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
        pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      rintro rfl
      exact ⟨pPrev.cons e, Path.nil, by simp [comp_nil], by simp [vertices_nil]⟩
    have h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end →
        ∃ (p₁ : Path a v) (p₂ : Path v (pPrev.cons e).end),
          pPrev.cons e = p₁.comp p₂ ∧ v ∉ p₂.vertices.tail := by
      intro hxPrev hxe_ne
      obtain ⟨q₁, q₂, h_prev, h_not_tail⟩ := ih hxPrev
      let q₂' : Path v (pPrev.cons e).end := q₂.cons e
      have h_no_tail : v ∉ q₂'.vertices.tail := by grind [vertices_cons, end_cons]
      exact ⟨q₁, q₂', by simp [q₂', h_prev], h_no_tail⟩
    cases hv' with
    | inl h_in_prefix =>
      by_cases h_eq_end : v = (pPrev.cons e).end
      · exact h_case₁ h_eq_end
      · exact h_case₂ h_in_prefix h_eq_end
    | inr h_eq_end => exact h_case₁ h_eq_end

Goal state after:
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 v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂

Tactic:
;

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.obj x₁ = φ.obj x₂ ∧ φ.mapPath p₁ ≍ φ.mapPath p₂
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 v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂

Tactic:
;

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂
Module: Mathlib.Data.Set.Sups

Goal state before:
pp: α : 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}

Tactic:
;

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 x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊼ t ∧ a ≤ b} ↔ x✝ ∈ {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
;

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.Combinatorics.SetFamily.Compression.Down

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

Tactic:
refine ⟨?_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ (∃ a_1, (a_1 ∈ 𝒜 ∧ a ∈ a_1) ∧ a_1.erase a = s) → insert a s ∈ 𝒜 ∧ a ∉ s
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
;

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ #({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n) ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x

Tactic:
;

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n) ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n

Tactic:
;

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) = fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n

Tactic:
;

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) = fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A})) / ↑↑⟨n, hn⟩ = ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B})) / ↑↑⟨n, hn⟩

Tactic:
;

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A})) / ↑↑⟨n, hn⟩ = ↑(#({a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B})) / ↑↑⟨n, hn⟩
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} = {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}

Tactic:
;

Goal state after:
case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} = {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} ↔ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}

Tactic:
;

Goal state after:
case e_a
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ A} ↔ x ∈ {a ∈ Ioc 0 ↑⟨n, hn⟩ | a ∈ B}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case a
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⋯
hn : 0 < n
⊢ {a ∈ Ioc 0 n | a ∈ ↑A} ⊆ A

Tactic:
;

Goal state after:
case a
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⋯
hn : 0 < n
⊢ {a ∈ Ioc 0 n | a ∈ ↑A} ⊆ A
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ x ∈ range (card α + 1), (↑x)⁻¹

Tactic:
have (n) (hn : n ∈ range (card α + 1)) :
      ((card α).choose n / ((card α - n) * (card α).choose n) : ℚ) = (card α - n : ℚ)⁻¹ := by
    rw [div_mul_cancel_right₀]
    exact cast_ne_zero.2 (choose_pos <| mem_range_succ_iff.1 hn).ne'

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this✝ :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ x ∈ range (card α + 1), (↑x)⁻¹
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case a
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := ⋯
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ := ⋯
sA : Finset ℕ := ⋯
sB : Finset ℕ := ⋯
⊢ image f (sA.disjSum sB) ⊆ Ioo 0 n

Tactic:
;

Goal state after:
case a
A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := ⋯
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ := ⋯
sA : Finset ℕ := ⋯
sB : Finset ℕ := ⋯
⊢ image f (sA.disjSum sB) ⊆ Ioo 0 n
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then {b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x else ⊤) = if a ≤ b then b else ⊤

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
b a : α
⊢ (if h : a ≤ b then {b ∈ {b} | a ≤ b}.sup' ⋯ fun x ↦ x else ⊤) = if a ≤ b then b else ⊤
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∉ upperClosure ↑s
ht : a ∉ upperClosure ↑t
⊢ a ∉ upperClosure ↑s ⊓ upperClosure ↑t
Module: Mathlib.Data.Finset.Sups

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

Tactic:
;

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 α
a✝ : α
⊢ a✝ ∈ univᶜˢ ↔ a✝ ∈ univ

Tactic:
;

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 α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊻ t) = image compl s ⊼ image compl t

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊻ t) = image compl s ⊼ image compl t
Module: Mathlib.Data.Finset.Sups

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

Tactic:
;

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

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupIrred ⊥
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupIrred ⊥
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfIrred ⊤
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfIrred ⊤
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfPrime ⊤
⊢ False

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfPrime ⊤
⊢ False
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a
b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊔ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∪
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
a b : α
⊢ (if h : IsEmpty α then ofIsEmpty
      else
        have this := Fintype.toOrderBot α;
        RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
          { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
      (a ⊓ b) =
    (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        a ∩
      (if h : IsEmpty α then ofIsEmpty
        else
          have this := Fintype.toOrderBot α;
          RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
            { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ })
        b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a ≤ b
⊢ a ≤ b

Tactic:
;

Goal state after:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a ≤ b
⊢ a ≤ b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b ≤ a
⊢ b ≤ a

Tactic:
;

Goal state after:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b ≤ a
⊢ b ≤ a
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b

Tactic:
;

Goal state after:
case sep
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : Disjoint a b
⊢ Disjoint a b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a < b
⊢ a < b

Tactic:
;

Goal state after:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a < b
⊢ a < b
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b < a
⊢ b < a

Tactic:
;

Goal state after:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b < a
⊢ b < a
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized r ↑(𝓒 u v 𝒜)

Tactic:
simp_rw [Set.Sized, mem_coe, mem_compression]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
hs : s ∉ ∅
h𝒜₁ : (insert s ∅).Nonempty
h𝒜₂ : univ ∉ insert s ∅
h𝒜₃ : (insert s ∅).Nontrivial
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < #∅ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #∅ + 1 = #(insert s ∅)
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
hs : s ∉ ∅
h𝒜₁ : (insert s ∅).Nonempty
h𝒜₂ : univ ∉ insert s ∅
h𝒜₃ : (insert s ∅).Nontrivial
ih :
  ∀ (𝒜 : Finset (Finset α)), #𝒜 < #∅ + 1 → 𝒜.Nonempty → univ ∉ 𝒜 → supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #∅ + 1 = #(insert s ∅)
⊢ False
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr
β : Type u_2
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : ExistsAddOfLE β
a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β
ha₀ : 0 ≤ a₀
ha₁ : 0 ≤ a₁
hb₀ : 0 ≤ b₀
hb₁ : 0 ≤ b₁
hc₀ : 0 ≤ c₀
hc₁ : 0 ≤ c₁
hd₀ : 0 ≤ d₀
hd₁ : 0 ≤ d₁
h₀₀ : a₀ * b₀ ≤ c₀ * d₀
h₁₀ : a₁ * b₀ ≤ c₀ * d₁
h₀₁ : a₀ * b₁ ≤ c₀ * d₁
h₁₁ : a₁ * b₁ ≤ c₁ * d₁
hcd : 0 < c₀ * d₁
⊢ (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁) ≤ (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁)

Tactic:
calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ {t ∈ 𝒜 | t.erase a = s} ↔
    t ∈ if s ∈ 𝒜 then if insert a s ∈ 𝒜 then {s, insert a s} else {s} else if insert a s ∈ 𝒜 then {insert a s} else ∅