harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Fold.lean
theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
dsimp only [fold]

Result:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
rw [cons_val, Multiset.map_cons, fold_cons_left]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul (1 ⊗ₜ[R] 1)) x = x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem convs'_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) :
    g.convs' m = g.convs' n

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.convs' m = g.convs' n

Tactic:
simp only [convs', convs'Aux_stable_of_terminated n_le_m terminatedAt_n]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_imp_distrib_right {f : Filter α} [NeBot f] {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x → q) ↔ (∀ᶠ x in f, p x) → q

Proof state:
α : Type u
f : Filter α
inst✝ : f.NeBot
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q

Tactic:
simp only [frequently_imp_distrib, frequently_const]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
lemma star_le_iff {x y : R} : star x ≤ y ↔ x ≤ star y

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ star x ≤ y ↔ x ≤ star y

Tactic:
rw [← star_le_star_iff, star_star]

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem mem_nhds {s : Set R} {x : R} : s ∈ 𝓝 x ↔ ∃ γ : Γ₀ˣ, { y | (v (y - x) : Γ₀) < γ } ⊆ s

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {y | v (y - x) < ↑γ} ⊆ s

Tactic:
simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
  ((hasBasis_nhds_zero R Γ₀).comap fun y => y - x).mem_iff]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma add_sub_sub_cancel (h : c ≤ a) : a + b - (a - c) = b + c

Proof state:
a b c : ℕ
h : c ≤ a
⊢ a + b - (a - c) = b + c

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_three_mul : cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Proof state:
x : ℝ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)

Proof state:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)

Tactic:
simp [cosh_three_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem _root_.Matrix.mem_range_scalar_of_commute_transvectionStruct {M : Matrix n n R}
    (hM : ∀ t : TransvectionStruct n R, Commute t.toMatrix M) :
    M ∈ Set.range (Matrix.scalar n)

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
i j : n
hij : i ≠ j
⊢ Commute (stdBasisMatrix i j 1) M

Tactic:
simpa [transvection, mul_add, add_mul] using (hM ⟨i, j, hij, 1⟩).eq

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Pairwise fun i j => Commute (stdBasisMatrix i j 1) M

Tactic:
intro i j hij

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
i j : n
hij : i ≠ j
⊢ Commute (stdBasisMatrix i j 1) M

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
refine mem_range_scalar_of_commute_stdBasisMatrix ?_

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Pairwise fun i j => Commute (stdBasisMatrix i j 1) M
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_sqrt_two (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a ^ 2 = a

Tactic:
simp only [nnrpow_sqrt, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]

Result:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a

Tactic:
rw [nnrpow_one a]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
/-- "Functoriality of `MakesOverArrow η s` in `s`. -/
lemma map₂ {F : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {X Y : C} (f : X ⟶ Y)
    {s : yoneda.obj X ⟶ A} {t : yoneda.obj Y ⟶ A} (hst : yoneda.map f ≫ t = s)
    {u : F.obj (op Y)} (h : MakesOverArrow η t u) : MakesOverArrow η s (F.map f.op u) :=
  ⟨by rw [elementwise_of% η.naturality, h.app, yonedaEquiv_naturality, hst]⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X Y : C
f : X ⟶ Y
s : yoneda.obj X ⟶ A
t : yoneda.obj Y ⟶ A
hst : yoneda.map f ≫ t = s
u : F.obj (op Y)
h : MakesOverArrow η t u
⊢ η.app (op X) (F.map f.op u) = yonedaEquiv s

Tactic:
rw [elementwise_of% η.naturality, h.app, yonedaEquiv_naturality, hst]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_comap_inr : (prod p q).comap (inr R M M₂) = q

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M₂
⊢ x✝ ∈ comap (inr R M M₂) (p.prod q) ↔ x✝ ∈ q

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ comap (inr R M M₂) (p.prod q) = q

Tactic:
ext

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x✝ : M₂
⊢ x✝ ∈ comap (inr R M M₂) (p.prod q) ↔ x✝ ∈ q
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuous_zpow : ∀ n : ℤ, Continuous (· ^ n : ℝ≥0∞ → ℝ≥0∞)
  | (n : ℕ) => mod_cast ENNReal.continuous_pow n
  | .negSucc n => by simpa using (ENNReal.continuous_pow _).inv

Proof state:
n : ℕ
⊢ Continuous fun x => x ^ Int.negSucc n

Tactic:
simpa using (ENNReal.continuous_pow _).inv

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem inverses_right (h : Semiconj f ga gb) (ha : RightInverse ga' ga) (hb : LeftInverse gb' gb) :
    Semiconj f ga' gb' := fun x ↦ by
  rw [← hb (f (ga' x)), ← h.eq, ha x]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)

Tactic:
rw [← hb (f (ga' x)), ← h.eq, ha x]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableOn_neg_iff : DifferentiableOn 𝕜 (fun y => -f y) s ↔ DifferentiableOn 𝕜 f s :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : DifferentiableOn 𝕜 (fun y => -f y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_succ (n : Nat) : range (succ n) = range n ++ [n]

Proof state:
n : Nat
⊢ range n.succ = range n ++ [n]

Tactic:
simp only [range_eq_range', range'_1_concat, Nat.zero_add]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ioo (a b : α) {c : α} (h : 0 < c) :
    (c * ·) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => c * x) ⁻¹' Ioo a b = Ioo (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iio, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem map_le_map_iff' {f : F} (hf : ker f = ⊥) {p p'} : map f p ≤ map f p' ↔ p ≤ p'

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : ker f = ⊥
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p'

Tactic:
rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Pointed.lean
theorem toConvexCone_pointed (S : PointedCone 𝕜 E) : (S : ConvexCone 𝕜 E).Pointed

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
S : PointedCone 𝕜 E
⊢ (↑S).Pointed

Tactic:
simp [toConvexCone, ConvexCone.Pointed]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma opcyclesOpIso_hom_naturality (φ : S₁ ⟶ S₂)
    [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    opcyclesMap (opMap φ) ≫ (S₁.opcyclesOpIso).hom =
      S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ opcyclesMap (opMap φ) ≫ S₁.opcyclesOpIso.hom = S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op

Tactic:
rw [← cancel_epi S₂.op.pOpcycles, p_opcyclesMap_assoc, opMap_τ₂,
  op_pOpcycles_opcyclesOpIso_hom, op_pOpcycles_opcyclesOpIso_hom_assoc, ← op_comp,
  ← op_comp, cyclesMap_i]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_bin : eval assign (.bin lhs op rhs) = op.eval (lhs.eval assign) (rhs.eval assign)

Proof state:
assign : Assignment
a✝ : Nat
lhs : BVExpr a✝
op : BVBinOp
rhs : BVExpr a✝
⊢ eval assign (lhs.bin op rhs) = op.eval (eval assign lhs) (eval assign rhs)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem finset_image_add_of_nonempty {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
    (g : β → α) {t : Finset β} (ht : t.Nonempty) :
    ∃ b : β, (b ∈ t) ∧ f (t.sum g) ≤ f (g b)

Proof state:
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
ht : t.Nonempty
b : β
hbt : t.Nonempty → b ∈ t
hbf : f (t.sum g) ≤ f (g b)
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Tactic:
exact ⟨b, hbt ht, hbf⟩

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
ht : t.Nonempty
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)

Tactic:
obtain ⟨b, hbt, hbf⟩ := finset_image_add hna g t

Result:
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
t : Finset β
ht : t.Nonempty
b : β
hbt : t.Nonempty → b ∈ t
hbf : f (t.sum g) ≤ f (g b)
⊢ ∃ b ∈ t, f (t.sum g) ≤ f (g b)
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_own_rightCoset (a : α) : a ∈ op a • (s : Set α) :=
  suffices 1 * a ∈ op a • (s : Set α) by simpa
  mem_rightCoset a (one_mem s : 1 ∈ s)

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : 1 * a ∈ op a • ↑s
⊢ a ∈ op a • ↑s

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_pos_right_iff_sameRay_and_ne_zero (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
simp_rw [eq_comm (a := x)]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

Tactic:
rw [SameRay.sameRay_comm]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x ∧ x ≠ 0

Tactic:
exact exists_pos_left_iff_sameRay_and_ne_zero hy

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@[reassoc, simp]
lemma map₂_inv_hom {f g : a ⟶ b} (η : f ≅ g) :
    F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)

Tactic:
rw [← F.map₂_comp, Iso.inv_hom_id, F.map₂_id]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_le_of_compl_le (h : yᶜ ≤ x) : xᶜ ≤ y

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ x
⊢ xᶜ ≤ y

Tactic:
simpa only [compl_compl] using compl_le_compl h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKey! k (modifyKey k f l) = if containsKey k l then k else default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKey! k (modifyKey k f l) = if containsKey k l = true then k else default

Tactic:
simp [getKey!_modifyKey, hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn_eq_elim [Monad m] [LawfulMonad m]
    (o : Option α) (f : (a : α) → β → m (ForInStep β)) (b : β) :
    forIn o b f =
      o.elim (pure b) (fun a => ForInStep.value <$> f a b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : α → β → m (ForInStep β)
b : β
⊢ forIn o b f = o.elim (pure b) fun a => ForInStep.value <$> f a b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_mul_of_ediv_eq_left {a b c : Int}
    (H1 : b ∣ a) (H2 : a / b = c) : a = c * b

Proof state:
a b c : Int
H1 : b ∣ a
H2 : a / b = c
⊢ a = c * b

Tactic:
rw [Int.mul_comm, Int.eq_mul_of_ediv_eq_right H1 H2]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem exists_open_set_nhds' {U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) :
    ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
  exists_open_set_nhds (by simpa using h)

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
U : Set X
h : U ∈ ⨆ x ∈ s, 𝓝 x
⊢ ∀ x ∈ s, U ∈ 𝓝 x

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_inv' : a < b⁻¹ ↔ b < a⁻¹

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
a b : α
inst✝ : MulRightStrictMono α
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

Result:
no goals
-- Mathlib/Topology/QuasiSeparated.lean
theorem IsQuasiSeparated.of_subset {s t : Set α} (ht : IsQuasiSeparated t) (h : s ⊆ t) :
    IsQuasiSeparated s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s

Tactic:
intro U V hU hU' hU'' hV hV' hV''

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_const_sub_iff (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_lt_iff_lt_mul' : c⁻¹ * a < b ↔ a < b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ c⁻¹ * a < b ↔ a < b * c

Tactic:
rw [inv_mul_lt_iff_lt_mul, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem coe_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv {𝕜 E : Type*} [NormedField 𝕜] [Norm E] {a : 𝕜}
    {f : 𝕜 → E} (h : IsBoundedUnder (· ≤ ·) (𝓝[≠] a) (norm ∘ f)) :
    f =o[𝓝[≠] a] fun x => (x - a)⁻¹

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[≠] a) atTop

Tactic:
exact (tendsto_norm_sub_self_nhdsNE a).inv_tendsto_nhdsGT_zero

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[≠] a) atTop

Tactic:
simp only [Function.comp_def, norm_inv]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[≠] a) atTop

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ f =o[𝓝[≠] a] fun x => (x - a)⁻¹

Tactic:
refine (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[≠] a) atTop
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem associativity_inv (X Y Z : C) :
    δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
      F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, Category.assoc, associativity,
  ← Category.assoc, ← F.map_comp, Iso.inv_hom_id, F.map_id, id_comp]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma IsMulFreimanHom.mul_eq_mul (hf : IsMulFreimanHom 2 A B f) {a b c d : α}
    (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) :
    f a * f b = f c * f d

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ {f a, f b}.prod = {f c, f d}.prod

Tactic:
refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h <;> simp [ha, hb, hc, hd]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : a * b = c * d
⊢ f a * f b = f c * f d

Tactic:
simp_rw [← prod_pair] at h ⊢

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : {a, b}.prod = {c, d}.prod
⊢ {f a, f b}.prod = {f c, f d}.prod
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_or : f <$> or o o' = (f <$> o).or (f <$> o')

Proof state:
α✝¹ α✝ : Type u_1
f : α✝¹ → α✝
o o' : Option α✝¹
⊢ f <$> o.or o' = (f <$> o).or (f <$> o')

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m

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

Tactic:
have := Nat.sub_le_sub_right (succ_le_of_lt h) n

Result:
n k m : Nat
H : n ≤ k
h : k < n + m
this : k.succ - n ≤ n + m - n
⊢ k - n < m

Proof state:
n k m : Nat
H : n ≤ k
h : k < n + m
this : k.succ - n ≤ n + m - n
⊢ k - n < m

Tactic:
rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this

Result:
no goals