harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma IsMulFreimanIso.subset (hA : A₁ ⊆ A₂) (hf : IsMulFreimanIso n A₂ B₂ f)
    (hf' : BijOn f A₁ B₁) : IsMulFreimanIso n A₁ B₁ f where
  bijOn := hf'
  map_prod_eq_map_prod s t hsA htA hs ht

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A₁ A₂ : Set α
B₁ B₂ : Set β
f : α → β
n : ℕ
hA : A₁ ⊆ A₂
hf : IsMulFreimanIso n A₂ B₂ f
hf' : BijOn f A₁ B₁
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

Tactic:
refine hf.map_prod_eq_map_prod (fun a ha ↦ hA (hsA ha)) (fun a ha ↦ hA (htA ha)) hs ht

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma inl_comp_binaryCoproductIso_hom :
    Limits.coprod.inl ≫ (binaryCoproductIso F G).hom = coprod.inl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (colimit.isoColimitCocone (binaryCoproductColimitCocone F G)).hom = coprod.inl

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (binaryCoproductIso F G).hom = coprod.inl

Tactic:
simp only [binaryCoproductIso]

Result:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (colimit.isoColimitCocone (binaryCoproductColimitCocone F G)).hom = coprod.inl
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_uniformity_iff_dist_tendsto_zero {f : ι → α × α} {p : Filter ι} :
    Tendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0)

Proof state:
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : ι → α × α
p : Filter ι
⊢ Tendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0)

Tactic:
rw [Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq'_antitone : Antitone (Real.log ∘ stirlingSeq ∘ succ) :=
  antitone_nat_of_succ_le fun n =>
    sub_nonneg.mp <| (log_stirlingSeq_diff_hasSum n).nonneg fun m => by positivity

Proof state:
n m : ℕ
⊢ 0 ≤ 1 / (2 * ↑(m + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (m + 1)

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
lemma nsmul_cons {s : Multiset α} (n : ℕ) (a : α) :
    n • (a ::ₘ s) = n • ({a} : Multiset α) + n • s

Proof state:
α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = n • {a} + n • s

Tactic:
rw [← singleton_add, nsmul_add]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem neg {x : R} (hx : IsSelfAdjoint x) : IsSelfAdjoint (-x)

Proof state:
R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)

Tactic:
simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem add_mul_left_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + y * z) y :=
  @of_add_mul_left_left R _ _ _ (-z) <| by simpa only [mul_neg, add_neg_cancel_right] using h

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z + y * -z) y

Tactic:
simpa only [mul_neg, add_neg_cancel_right] using h

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_le_neg_iff {x : PGame} : 0 ≤ -x ↔ x ≤ 0

Proof state:
x : PGame
⊢ 0 ≤ -x ↔ x ≤ 0

Tactic:
rw [le_neg_iff, neg_zero]

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map
in a universe that `R` fits in. -/
lemma iff_lTensor_preserves_injective_linearMapₛ [Small.{v'} R] : Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [AddCommMonoid N] [AddCommMonoid N'] [Module R N] [Module R N']
      (f : N →ₗ[R] N'), Function.Injective f → Function.Injective (f.lTensor M)

Proof state:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(lTensor M f)

Tactic:
simp_rw [iff_rTensor_preserves_injective_linearMapₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma groupCohomologyπ_comp_isoH0_hom  :
    groupCohomologyπ A 0 ≫ (isoH0 A).hom = (isoZeroCocycles A).hom

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ groupCohomologyπ A 0 ≫ (isoH0 A).hom = (isoZeroCocycles A).hom

Tactic:
simp [isoH0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_eraseKey_self [BEq α] [PartialEquivBEq α] [Inhabited α]  {l : List ((a : α) × β a)}
    {k : α} (hl : DistinctKeys l) : getKey! k (eraseKey k l) = default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k : α
hl : DistinctKeys l
⊢ getKey! k (eraseKey k l) = default

Tactic:
simp [getKey!_eq_getKey?, getKey?_eraseKey_self hl]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma netEntropyEntourage_univ (T : X → X) {F : Set X} (h : F.Nonempty) :
    netEntropyEntourage T F univ = 0

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyEntourage T F univ = 0

Tactic:
simp [netEntropyEntourage, netMaxcard_univ T h]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformGroup_iInf {ι : Sort*} {us' : ι → UniformSpace β}
    (h' : ∀ i, @UniformGroup β (us' i) _) : @UniformGroup β (⨅ i, us' i) _

Proof state:
β : Type u_2
inst✝ : Group β
ι : Sort u_3
us' : ι → UniformSpace β
h' : ∀ (i : ι), UniformGroup β
⊢ UniformGroup β

Tactic:
exact uniformGroup_sInf (Set.forall_mem_range.mpr h')

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem mem_uniformity' {s : Set (CauchyFilter α × CauchyFilter α)} :
    s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ f g : CauchyFilter α, t ∈ f.1 ×ˢ g.1 → (f, g) ∈ s

Proof state:
α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

Tactic:
exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
⊢ s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

Tactic:
refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))

Result:
α : Type u
inst✝ : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.of_cons {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
    (cons h p).IsTrail → p.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsTrail → p.IsTrail

Tactic:
simp [isTrail_def]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem pow {q : ℚ} (hq : q ≠ 0) {k : ℕ} :
    padicValRat p (q ^ k) = k * padicValRat p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
⊢ padicValRat p (q ^ k) = ↑k * padicValRat p q

Tactic:
induction k <;>
  simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ', add_mul, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
    (if c then x else y).val = if c then x.val else y.val

Proof state:
n : Nat
c : Prop
inst✝ : Decidable c
x y : Fin n
⊢ ↑(if c then x else y) = if c then ↑x else ↑y

Tactic:
by_cases c <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Adjunction.lean
/--
The left adjoint of a triangulated functor is triangulated.
-/
lemma isTriangulated_leftAdjoint [G.IsTriangulated] : F.IsTriangulated

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{u_4, u_1} C
inst✝¹⁴ : Category.{u_3, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : G.IsTriangulated
this : F.op.IsTriangulated
⊢ F.IsTriangulated

Tactic:
exact F.isTriangulated_of_op

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{u_4, u_1} C
inst✝¹⁴ : Category.{u_3, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : G.IsTriangulated
⊢ F.IsTriangulated

Tactic:
have := isTriangulated_rightAdjoint adj.op

Result:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{u_4, u_1} C
inst✝¹⁴ : Category.{u_3, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : G.IsTriangulated
this : F.op.IsTriangulated
⊢ F.IsTriangulated
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_succ_eval {S : Type*} [Semiring S] (n : ℕ) (k : S) :
    (ascPochhammer S (n + 1)).eval k = (ascPochhammer S n).eval k * (k + n)

Proof state:
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
rw [ascPochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
  eval_C_mul, Nat.cast_comm, ← mul_add]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem iInf_const_zero {α : Sort*} : ⨅ _ : α, (0 : ℝ≥0) = 0

Proof state:
α : Sort u_2
⊢ ⨅ i, ↑0 = ↑0

Tactic:
exact Real.iInf_const_zero

Result:
no goals

Proof state:
α : Sort u_2
⊢ ⨅ x, 0 = 0

Tactic:
rw [← coe_inj, coe_iInf]

Result:
α : Sort u_2
⊢ ⨅ i, ↑0 = ↑0
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem degreeLTEquiv_eq_zero_iff_eq_zero {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) :
    degreeLTEquiv _ _ ⟨p, hp⟩ = 0 ↔ p = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ (degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_one_div_of_neg (ha : a < 0) (hb : b < 0) :
    ∫ x : ℝ in a..b, 1 / x = log (b / a)

Proof state:
a b : ℝ
ha : a < 0
hb : b < 0
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv_of_neg ha hb]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousWithinAt_finite [Finite ι] {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAt F S x₀ ↔ ∀ i, ContinuousWithinAt (F i) S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (i : ι), ContinuousWithinAt (F i) S x₀

Tactic:
simp [EquicontinuousWithinAt, ContinuousWithinAt,
  (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball,
  @forall_swap _ ι]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem CovBy.Ioc_eq (h : a ⋖ b) : Ioc a b = {b}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⋖ b
⊢ Ioc a b = {b}

Tactic:
rw [← Ioo_union_right h.lt, h.Ioo_eq, empty_union]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma smul_basis_mul_C (y : R[X]) (p q : R[X]) :
    (p • (1 : W.CoordinateRing) + q • mk W Y) * mk W (C y) =
      (p * y) • (1 : W.CoordinateRing) + (q * y) • mk W Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
y p q : R[X]
⊢ ((mk W) (C p) * 1 + (mk W) (C q) * (mk W) Y) * (mk W) (C y) =
    (mk W) (C p) * (mk W) (C y) * 1 + (mk W) (C q) * (mk W) (C y) * (mk W) Y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
y p q : R[X]
⊢ (p • 1 + q • (mk W) Y) * (mk W) (C y) = (p * y) • 1 + (q * y) • (mk W) Y

Tactic:
simp only [smul, _root_.map_mul]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
y p q : R[X]
⊢ ((mk W) (C p) * 1 + (mk W) (C q) * (mk W) Y) * (mk W) (C y) =
    (mk W) (C p) * (mk W) (C y) * 1 + (mk W) (C q) * (mk W) (C y) * (mk W) Y
-- Mathlib/Data/Finset/Insert.lean
theorem eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ s.Nontrivial

Proof state:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial

Tactic:
exact Set.eq_singleton_or_nontrivial ha

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← coe_eq_singleton]

Result:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_map {l : Vector α n} (f : α → β) :
    (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
⊢ (map f l).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma toNNReal_le_natCast {r : ℝ} {n : ℕ} : r.toNNReal ≤ n ↔ r ≤ n

Proof state:
r : ℝ
n : ℕ
⊢ r.toNNReal ≤ ↑n ↔ r ≤ ↑n

Tactic:
simpa using toNNReal_le_toNNReal_iff n.cast_nonneg

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_self (a : Prop) : Xor' a a = False

Proof state:
a : Prop
⊢ Xor' a a = False

Tactic:
simp [Xor']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x

Proof state:
case cons
α✝ : Type u_1
p : α✝ → Bool
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : find? p tail✝ = none ↔ ∀ (x : α✝), x ∈ tail✝ → ¬p x = true
⊢ (match p head✝ with
      | true => some head✝
      | false => find? p tail✝) =
      none ↔
    p head✝ = false ∧ ∀ (a : α✝), a ∈ tail✝ → p a = false

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

Tactic:
induction l <;> simp [find?_cons]

Result:
case cons
α✝ : Type u_1
p : α✝ → Bool
head✝ : α✝
tail✝ : List α✝
tail_ih✝ : find? p tail✝ = none ↔ ∀ (x : α✝), x ∈ tail✝ → ¬p x = true
⊢ (match p head✝ with
      | true => some head✝
      | false => find? p tail✝) =
      none ↔
    p head✝ = false ∧ ∀ (a : α✝), a ∈ tail✝ → p a = false
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_div_distrib [DivisionCommMonoid G] (f g : α → G) (hs : s.Finite) :
    ∏ᶠ i ∈ s, f i / g i = (∏ᶠ i ∈ s, f i) / ∏ᶠ i ∈ s, g i

Proof state:
α : Type u_1
G : Type u_4
s : Set α
inst✝ : DivisionCommMonoid G
f g : α → G
hs : s.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
simp only [div_eq_mul_inv, finprod_mem_mul_distrib hs, finprod_mem_inv_distrib g hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
    List.lookup k l₁ = some b → List.lookup k l₂ = some b

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : l₁ <+: l₂
⊢ lookup k l₁ = some b → lookup k l₂ = some b

Tactic:
simp only [lookup_eq_findSome?]

Result:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : l₁ <+: l₂
⊢ findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁ = some b →
    findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂ = some b

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
b : β
l₁ l₂ : List (α × β)
h : l₁ <+: l₂
⊢ findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₁ = some b →
    findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l₂ = some b

Tactic:
exact h.findSome?_eq_some

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem add_mul [Fintype m] (L M : Matrix l m α) (N : Matrix m n α) :
    (L + M) * N = L * N + M * N

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
i✝ : l
j✝ : n
⊢ ((L + M) * N) i✝ j✝ = (L * N + M * N) i✝ j✝

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
i✝ : l
j✝ : n
⊢ ((L + M) * N) i✝ j✝ = (L * N + M * N) i✝ j✝

Tactic:
apply add_dotProduct

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
lemma nnreal_smul_lt_top_iff {x : ℝ≥0} {y : ℝ≥0∞} (hx : x ≠ 0) : x • y < ⊤ ↔ y < ⊤

Proof state:
x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y < ⊤ ↔ y < ⊤

Tactic:
rw [lt_top_iff_ne_top, lt_top_iff_ne_top, nnreal_smul_ne_top_iff hx]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) :
    degree (p * C (leadingCoeff q)⁻¹) = degree p

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
rw [degree_mul_C h₁]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)

Result:
K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}
    (h₁ : p₁ = p₂)
    (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a)
    : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a)

Proof state:
p₁ p₂ : Prop
q₁ : p₁ → Prop
q₂ : p₂ → Prop
h₁ : p₁ = p₂
h₂ : ∀ (a : p₂), q₁ ⋯ = q₂ a
⊢ (∀ (a : p₁), q₁ a) = ∀ (a : p₂), q₂ a

Tactic:
subst h₁

Result:
p₁ : Prop
q₁ q₂ : p₁ → Prop
h₂ : ∀ (a : p₁), q₁ ⋯ = q₂ a
⊢ (∀ (a : p₁), q₁ a) = ∀ (a : p₁), q₂ a

Proof state:
p₁ : Prop
q₁ q₂ : p₁ → Prop
h₂ : ∀ (a : p₁), q₁ ⋯ = q₂ a
⊢ (∀ (a : p₁), q₁ a) = ∀ (a : p₁), q₂ a

Tactic:
simp [← h₂]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem norm_qParam_lt_iff (hh : 0 < h) (A : ℝ) (z : ℂ) :
    ‖qParam h z‖ < Real.exp (-2 * π * A / h) ↔ A < im z

Proof state:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π < 0

Tactic:
simpa using Real.pi_pos

Result:
no goals

Proof state:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ ‖𝕢 h z‖ < rexp (-2 * π * A / h) ↔ A < z.im

Tactic:
rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]

Result:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π < 0
-- Mathlib/Topology/Algebra/Support.lean
theorem not_mem_mulTSupport_iff_eventuallyEq : x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
x : α
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1

Tactic:
simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
  ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem inv_inv : inv (inv r) = r

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
x : α
y : β
⊢ r.inv.inv x y ↔ r x y

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.inv.inv = r

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
x : α
y : β
⊢ r.inv.inv x y ↔ r x y
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp]
lemma le_mul_iff_one_le_left [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : a ≤ b * a ↔ 1 ≤ b :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_right a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : MulPosMono α
inst✝ : MulPosReflectLE α
a0 : 0 < a
⊢ a ≤ b * a ↔ 1 * a ≤ b * a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys :=
  ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩

Proof state:
α : Type u_1
a : α
xs ys : Array α
h : xs = ys
⊢ xs.push a = ys.push a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
lemma isLocallyInjective_presheafToSheaf_map_iff :
    Sheaf.IsLocallyInjective ((presheafToSheaf J A).map φ) ↔ IsLocallyInjective J φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallyInjective ((presheafToSheaf J A).map φ) ↔ IsLocallyInjective J φ

Tactic:
rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
  ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
  ← comp_isLocallyInjective_iff J (toSheafify J P),
  toSheafify_naturality, sheafToPresheaf_map]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem HeapNode.realSize_toHeap (s : HeapNode α) : s.toHeap.realSize = s.realSize := go s where
  go {n res} : ∀ s : HeapNode α, (toHeap.go s n res).realSize = s.realSize + res.realSize
  | .nil => (Nat.zero_add _).symm
  | .node a c s => by simp [toHeap.go, go, Nat.add_assoc, Nat.add_left_comm]

Proof state:
α : Type u_1
s✝ : HeapNode α
n : Nat
res : Heap α
a : α
c s : HeapNode α
⊢ (toHeap.go (node a c s) n res).realSize = (node a c s).realSize + res.realSize

Tactic:
simp [toHeap.go, go, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem mul_left_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
    c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Proof state:
a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]

Result:
a b c m : ℕ
hc : c ≠ 0
⊢ ↑c * ↑m ∣ ↑c * (↑b - ↑a) → ↑m ∣ ↑b - ↑a

Proof state:
a b c m : ℕ
hc : c ≠ 0
⊢ ↑c * ↑m ∣ ↑c * (↑b - ↑a) → ↑m ∣ ↑b - ↑a

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_right_inj {x y : BitVec w} (z : BitVec w) : (z - x = z - y) ↔ x = y

Proof state:
w : Nat
x y z : BitVec w
⊢ z - x = z - y ↔ x = y

Tactic:
simp [sub_toAdd]

Result:
no goals