harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_neg_of_lt_neg {a b : Int} (h : a < -b) : b < -a

Proof state:
a b : Int
h✝ : a < -b
h : - -b < -a
⊢ b < -a

Tactic:
rwa [Int.neg_neg] at h

Result:
no goals

Proof state:
a b : Int
h : a < -b
⊢ b < -a

Tactic:
have h := Int.neg_lt_neg h

Result:
a b : Int
h✝ : a < -b
h : - -b < -a
⊢ b < -a
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.neg (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (-x) (-s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) ((fun x => -x) '' s)

Tactic:
exact hs.is_linear_image IsLinearMap.isLinearMap_neg

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) (-s)

Tactic:
rw [← image_neg_eq_neg]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) ((fun x => -x) '' s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n :=
  match m, le.dest h with
  | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le

Proof state:
n m k a : Nat
h : n ≤ n + a
⊢ k - (n + a) ≤ k - n

Tactic:
rw [← Nat.sub_sub]

Result:
n m k a : Nat
h : n ≤ n + a
⊢ k - n - a ≤ k - n

Proof state:
n m k a : Nat
h : n ≤ n + a
⊢ k - n - a ≤ k - n

Tactic:
apply sub_le

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isIndepSet_compl : Gᶜ.IsIndepSet s ↔ G.IsClique s

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ s.Pairwise G.Adj

Tactic:
rw [Set.Pairwise]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w => ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj

Tactic:
repeat rw [Set.Pairwise]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → G.Adj x y

Tactic:
simp_all [compl_adj]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsIndepSet s ↔ G.IsClique s

Tactic:
rw [isIndepSet_iff, isClique_iff]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (s.Pairwise fun v w => ¬Gᶜ.Adj v w) ↔ s.Pairwise G.Adj
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_nilpotencyClass :
    lowerCentralSeries G (Group.nilpotencyClass G) = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass G) = ⊥

Tactic:
classical
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass G) = ⊥

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ lowerCentralSeries G (Nat.find ⋯) = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ lowerCentralSeries G (Nat.find ⋯) = ⊥

Tactic:
exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertEntry [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} {h} : getKey a (insertEntry k v l) h =
    if h' : k == a then k
    else getKey a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h'))

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ getKey a (insertEntry k v l) h = if h' : (k == a) = true then k else getKey a l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, apply_dite Option.some, getKey?_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ (if (k == a) = true then some k else getKey? a l) = if h : (k == a) = true then some k else some (getKey a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ (if (k == a) = true then some k else getKey? a l) = if h : (k == a) = true then some k else some (getKey a l ⋯)

Tactic:
simp only [← getKey?_eq_some_getKey, dite_eq_ite]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Function.lean
theorem PreErgodic.ae_eq_const_of_ae_eq_comp (h : PreErgodic f μ) (hgm : Measurable g)
    (hg_eq : g ∘ f = g) : ∃ c, g =ᵐ[μ] const α c :=
  exists_eventuallyEq_const_of_forall_separating MeasurableSet fun U hU ↦
    h.ae_mem_or_ae_nmem (s := g ⁻¹' U) (hgm hU) <| by rw [← preimage_comp, hg_eq]

Proof state:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.CountablySeparated X
f : α → α
g : α → X
h : PreErgodic f μ
hgm : Measurable g
hg_eq : g ∘ f = g
U : Set X
hU : MeasurableSet U
⊢ f ⁻¹' (g ⁻¹' U) = g ⁻¹' U

Tactic:
rw [← preimage_comp, hg_eq]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_one : IsPell (⟨a, 1⟩ : ℤ√(d a1)) :=
  show az a * az a - d a1 * 1 * 1 = 1 by simp [dz_val]

Proof state:
a : ℕ
a1 : 1 < a
⊢ az a * az a - ↑(Pell.d a1) * 1 * 1 = 1

Tactic:
simp [dz_val]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_of_locally_continuousOn
    (h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) : ContinuousOn f s

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
⊢ ContinuousWithinAt f s x

Tactic:
rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
rcases h x xs with ⟨t, open_t, xt, ct⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s

Tactic:
intro x xs

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x

Tactic:
have := ct x ⟨xs, xt⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
⊢ ContinuousWithinAt f s x
-- Mathlib/RingTheory/LocalRing/Module.lean
theorem subsingleton_tensorProduct [Module.Finite R M] :
    Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Tactic:
rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
  ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
  ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]

Result:
no goals
-- Mathlib/NumberTheory/GaussSum.lean
theorem gaussSum_mulShift (χ : MulChar R R') (ψ : AddChar R R') (a : Rˣ) :
    χ a * gaussSum χ (mulShift ψ a) = gaussSum χ ψ

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ i : R, χ ↑a * (χ i * ψ (↑a * i)) = ∑ a : R, χ a * ψ a

Tactic:
simp_rw [← mul_assoc, ← map_mul]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x : R, χ (↑a * x) * ψ (↑a * x) = ∑ a : R, χ a * ψ a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ

Tactic:
simp only [gaussSum, mulShift_apply, Finset.mul_sum]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ i : R, χ ↑a * (χ i * ψ (↑a * i)) = ∑ a : R, χ a * ψ a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ ∑ x : R, χ (↑a * x) * ψ (↑a * x) = ∑ a : R, χ a * ψ a

Tactic:
exact Fintype.sum_bijective _ a.mulLeft_bijective _ _ fun x ↦ rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem mapRange_single {f : M → N} {hf : f 0 = 0} {a : α} {b : M} :
    mapRange f hf (single a b) = single a (f b) :=
  ext fun a' => by
    classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ (mapRange f hf (single a b)) a' = (single a (f b)) a'

Tactic:
classical simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
a : α
b : M
a' : α
⊢ (mapRange f hf (single a b)) a' = (single a (f b)) a'

Tactic:
simpa only [single_eq_pi_single] using Pi.apply_single _ (fun _ => hf) a _ a'

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_eq_empty_iff : Ioi a = ∅ ↔ IsMax a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
simp only [isMax_iff_forall_not_lt, eq_empty_iff_forall_not_mem, mem_Ioi]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_le_add_left : ∀ (a b : ZNum), a ≤ b → ∀ (c : ZNum), c + a ≤ c + b

Proof state:
⊢ ∀ (a b : ZNum), a ≤ b → ∀ (c : ZNum), c + a ≤ c + b

Tactic:
intro a b h c

Result:
a b : ZNum
h : a ≤ b
c : ZNum
⊢ c + a ≤ c + b

Proof state:
a b : ZNum
h : a ≤ b
c : ZNum
⊢ c + a ≤ c + b

Tactic:
revert h

Result:
a b c : ZNum
⊢ a ≤ b → c + a ≤ c + b

Proof state:
a b c : ZNum
⊢ a ≤ b → c + a ≤ c + b

Tactic:
transfer_rw

Result:
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑c + ↑a ≤ ↑c + ↑b

Proof state:
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑c + ↑a ≤ ↑c + ↑b

Tactic:
exact fun h => _root_.add_le_add_left h c

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pullback_inter {f : Y ⟶ X} (S R : Sieve X) :
    (S ⊓ R).pullback f = S.pullback f ⊓ R.pullback f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S R : Sieve X
⊢ pullback f (S ⊓ R) = pullback f S ⊓ pullback f R

Tactic:
simp [Sieve.ext_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_nonneg (K₀ : PositiveCompacts G) {U : Set G} (K : Compacts G) :
    0 ≤ prehaar (K₀ : Set G) U K

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : TopologicalSpace G
K₀ : PositiveCompacts G
U : Set G
K : Compacts G
⊢ 0 ≤ prehaar (↑K₀) U K

Tactic:
apply div_nonneg <;> norm_cast <;> apply zero_le

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin {n : WithTop ℕ∞} {m : ℕ}
    (h : ContDiffWithinAt 𝕜 n f s x) (hmn : m < n) (hs : UniqueDiffOn 𝕜 (insert x s)) :
    DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
n : WithTop ℕ∞
m : ℕ
h : ContDiffWithinAt 𝕜 n f s x
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 (insert x s)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x

Tactic:
simpa only [iteratedDerivWithin_eq_equiv_comp,
  LinearIsometryEquiv.comp_differentiableWithinAt_iff] using
  h.differentiableWithinAt_iteratedFDerivWithin hmn hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' || rhs') = (lhs || rhs)

Proof state:
lhs rhs lhs' rhs' : Bool
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ (lhs' || rhs') = (lhs || rhs)

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem exists_of_mem_mapIdx {b : β} {l : List α}
    (h : b ∈ mapIdx f l) : ∃ (i : Nat) (h : i < l.length), f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
h : b ∈ mapIdx f l
⊢ ∃ i h, f i l[i] = b

Tactic:
rw [mapIdx_eq_mapFinIdx] at h

Result:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b

Proof state:
β : Type u_1
α : Type u_2
f : Nat → α → β
b : β
l : List α
h : b ∈ l.mapFinIdx fun i a x => f i a
⊢ ∃ i h, f i l[i] = b

Tactic:
simpa [Fin.exists_iff] using exists_of_mem_mapFinIdx h

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_sum {ι} (s : Finset ι) (f : ι → 𝔸) : exp 𝕂 (∑ i ∈ s, f i) = ∏ i ∈ s, exp 𝕂 (f i)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ exp 𝕂 (∑ i ∈ s, f i) = ∏ i ∈ s, exp 𝕂 (f i)

Tactic:
rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]

Result:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ (↑s).Pairwise (Function.onFun Commute f)

Proof state:
case h
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
ι : Type u_3
s : Finset ι
f : ι → 𝔸
⊢ (↑s).Pairwise (Function.onFun Commute f)

Tactic:
exact fun i _hi j _hj _ => Commute.all _ _

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_ne_eq_erase (f : Π₀ i, β i) (i : ι) : f.filter (· ≠ i) = f.erase i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x => x ≠ i) f = erase i f

Tactic:
ext1 j

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (filter (fun x => x ≠ i) f) j = (erase i f) j

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (filter (fun x => x ≠ i) f) j = (erase i f) j

Tactic:
simp only [DFinsupp.filter_apply, DFinsupp.erase_apply, ite_not]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_add_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂)

Proof state:
n₁ n₂ d₁ d₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ + n₂ /. d₂ = (n₁ * d₂ + n₂ * d₁) /. (d₁ * d₂)

Tactic:
rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
simp_all [-Int.natCast_mul, Int.ofNat_eq_zero, Int.neg_eq_zero, divInt_neg', Int.mul_neg,
  Int.ofNat_mul_ofNat, Int.neg_add, Int.neg_mul, mkRat_add_mkRat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → m.getKey? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → m.getKey? a = none

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKey? a (toListModel m.val.buckets) = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → List.getKey? a (toListModel m.val.buckets) = none

Tactic:
empty

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem smul_map_inv_sub_map_inv_of_isTwoCocycle {f : G × G → A} (hf : IsTwoCocycle f) (g : G) :
    g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isTwoCocycle hf g] at this

Result:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
exact sub_eq_sub_iff_add_eq_add.2 this.symm

Result:
no goals

Proof state:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
have := hf g g⁻¹ g

Result:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsTwoCocycle f
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
-- Mathlib/Order/Lattice.lean
theorem SemilatticeSup.ext_sup {α} {A B : SemilatticeSup α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y)
    (x y : α) :
    (haveI := A; x ⊔ y) = x ⊔ y :=
  eq_of_forall_ge_iff fun c => by simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]

Proof state:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c

Tactic:
simp only [sup_le_iff]

Result:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Proof state:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
rw [← H, @sup_le_iff α A, H, H]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem MeasurableSet.pi {s : Set δ} {t : ∀ i : δ, Set (π i)} (hs : s.Countable)
    (ht : ∀ i ∈ s, MeasurableSet (t i)) : MeasurableSet (s.pi t)

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (⋂ a ∈ s, eval a ⁻¹' t a)

Tactic:
exact MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)

Result:
no goals

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (s.pi t)

Tactic:
rw [pi_def]

Result:
δ : Type u_4
π : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (π a)
s : Set δ
t : (i : δ) → Set (π i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (⋂ a ∈ s, eval a ⁻¹' t a)
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_list_prod :
    ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
  | [] => by rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]
  | p::ps => by
    rw [List.prod_cons, List.map, List.sum_cons]
    exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ (p * ps.prod).totalDegree ≤ p.totalDegree + (List.map totalDegree ps).sum

Tactic:
exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ (p :: ps).prod.totalDegree ≤ (List.map totalDegree (p :: ps)).sum

Tactic:
rw [List.prod_cons, List.map, List.sum_cons]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
ps : List (MvPolynomial σ R)
⊢ (p * ps.prod).totalDegree ≤ p.totalDegree + (List.map totalDegree ps).sum

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ [].prod.totalDegree ≤ (List.map totalDegree []).sum

Tactic:
rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma compls_sups (s t : Finset α) : (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ

Tactic:
simp_rw [← image_compl]

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

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

Tactic:
exact image_image₂_distrib fun _ _ ↦ compl_sup

Result:
no goals