harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_image_eq (hf : ∀ t, Tendsto (· + t) f f) (t : τ) : ω f ϕ (ϕ t '' s) = ω f ϕ s :=
  Subset.antisymm (omegaLimit_image_subset _ _ _ _ (hf t)) <|
    calc
      ω f ϕ s = ω f ϕ (ϕ (-t) '' (ϕ t '' s))

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => x + t) f f
t : τ
⊢ ω f ϕ.toFun s = ω f ϕ.toFun (ϕ.toFun (-t) '' (ϕ.toFun t '' s))

Tactic:
simp [image_image, ← map_add]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma inv_pow (a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
  | 0 => by rw [pow_zero, pow_zero, inv_one]
  | n + 1 => by rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a⁻¹ ^ 0 = (a ^ 0)⁻¹

Tactic:
rw [pow_zero, pow_zero, inv_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹

Tactic:
rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem coeff_eq_zero {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (d : σ →₀ ℕ)
    (hd : weight w d ≠ n) : coeff d φ = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ coeff d φ = 0

Tactic:
have aux := mt (@hφ d) hd

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0

Tactic:
rwa [Classical.not_not] at aux

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ofNat_mul_im (n : ℕ) [n.AtLeastTwo] (z : K) :
    im (ofNat(n) * z) = ofNat(n) * im z

Proof state:
K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ im (OfNat.ofNat n * z) = OfNat.ofNat n * im z

Tactic:
rw [← ofReal_ofNat, im_ofReal_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem toExterior_ι (m : M) :
    TensorAlgebra.toExterior (TensorAlgebra.ι R m) = ExteriorAlgebra.ι R m

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ toExterior ((ι R) m) = (ExteriorAlgebra.ι R) m

Tactic:
simp [toExterior]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
    (l.push a).unattach = l.unattach.push a.1

Proof state:
α : Type u_1
p : α → Prop
a : { x // p x }
l : Array { x // p x }
⊢ (l.push a).unattach = l.unattach.push a.val

Tactic:
simp only [unattach, Array.map_push]

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csInf_of_not_bdd_below {s : Set ℤ} (h : ¬BddBelow s) : sInf s = 0 :=
  dif_neg (by simp [h])

Proof state:
s : Set ℤ
h : ¬BddBelow s
⊢ ¬(s.Nonempty ∧ BddBelow s)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_of (η : f ⟶ g) :
    η = (Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem le_update_self_iff : x ≤ update x i a ↔ x i ≤ a

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x ≤ update x i a ↔ x i ≤ a

Tactic:
simp [le_update_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_zero : arccos 0 = π / 2

Proof state:
⊢ arccos 0 = π / 2

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.toFinset_insert [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) :
    hs.toFinset = insert a (hs.subset <| subset_insert _ _).toFinset :=
  Finset.ext <| by simp

Proof state:
α : Type u
inst✝ : DecidableEq α
s : Set α
a : α
hs : (insert a s).Finite
⊢ ∀ (a_1 : α), a_1 ∈ hs.toFinset ↔ a_1 ∈ insert a ⋯.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_wordProd_le (ω : List B) : ℓ (π ω) ≤ ω.length :=
  Nat.find_min' (cs.exists_word_with_prod (π ω)) ⟨ω, by tauto⟩

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ω.length = ω.length ∧ cs.wordProd ω = cs.wordProd ω

Tactic:
tauto

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_ae_eq_condExp
    (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun ω ↦ (condExpKernel μ m ω s).toReal) =ᵐ[μ] μ⟦s | m⟧ :=
  (condExpKernel_ae_eq_condExp' hs).trans (by rw [inf_of_le_left hm])

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[s.indicator fun ω => 1|m ⊓ mΩ] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m]

Tactic:
rw [inf_of_le_left hm]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
@[simp] lemma min_self (a : α) : min a a = a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ min a a = a

Tactic:
simp [min_def]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
    divisors (p ^ k) = (Finset.range (k + 1)).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
rw [mem_divisors_prime_pow pp]

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))

Proof state:
p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).divisors = map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
ext a

Result:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))

Proof state:
case h
p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
simp [Nat.lt_succ, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_yield_eq_foldl
    (l : List α) (f : α → β → β) (init : β) :
    forIn (m := Id) l init (fun a b => .yield (f a b)) =
      l.foldl (fun b a => f a b) init

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f a b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    foldl (fun b a => f a b) init l

Tactic:
induction l generalizing init <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
init : β
⊢ (forIn l init fun a b => ForInStep.yield (f a b)) = foldl (fun b a => f a b) init l

Tactic:
simp only [forIn_eq_foldlM]

Result:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => ForInStep.yield (f a b)
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    foldl (fun b a => f a b) init l
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_ne_zero_iff {θ : Angle} : θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← sign_eq_zero_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_Δ' : (W.variableChange C).Δ' = C.u⁻¹ ^ 12 * W.Δ'

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (W.variableChange C).Δ' = C.u⁻¹ ^ 12 * W.Δ'

Tactic:
simp_rw [Units.ext_iff, Units.val_mul, coe_Δ', variableChange_Δ, Units.val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma insertNth_mem_Icc {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)}
    {q₁ q₂ : ∀ j, α j} :
    i.insertNth x p ∈ Icc q₁ q₂ ↔
      x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
q₁ q₂ : (j : Fin (n + 1)) → α j
⊢ i.insertNth x p ∈ Icc q₁ q₂ ↔
    x ∈ Icc (q₁ i) (q₂ i) ∧ p ∈ Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)

Tactic:
simp only [mem_Icc, insertNth_le_iff, le_insertNth_iff, and_assoc, @and_left_comm (x ≤ q₂ i)]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem coeff_mul_single_zero [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} :
    (x * single 0 r).coeff a = x.coeff a * r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
⊢ (x * (single 0) r).coeff a = x.coeff a * r

Tactic:
rw [← add_zero a, coeff_mul_single_add, add_zero]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- `x * y` and `y * x` have the same moves. -/
protected lemma mul_comm (x y : PGame) : x * y ≡ y * x :=
  match x, y with
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ => by
    refine Identical.of_equiv ((Equiv.prodComm _ _).sumCongr (Equiv.prodComm _ _))
      ((Equiv.sumComm _ _).trans ((Equiv.prodComm _ _).sumCongr (Equiv.prodComm _ _))) ?_ ?_ <;>
    · rintro (⟨_, _⟩ | ⟨_, _⟩) <;>
      exact ((((PGame.mul_comm _ (mk _ _ _ _)).add (PGame.mul_comm (mk _ _ _ _) _)).trans
        (PGame.add_comm _ _)).sub (PGame.mul_comm _ _))
  termination_by (x, y)

Proof state:
case refine_2
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ ∀ (i : (mk xl xr xL xR * mk yl yr yL yR).RightMoves),
    (mk xl xr xL xR * mk yl yr yL yR).moveRight i ≡
      (mk yl yr yL yR * mk xl xr xL xR).moveRight
        (((Equiv.sumComm (xl × yr) (xr × yl)).trans ((Equiv.prodComm xr yl).sumCongr (Equiv.prodComm xl yr))) i)

Tactic:
rintro (⟨_, _⟩ | ⟨_, _⟩) <;>
exact ((((PGame.mul_comm _ (mk _ _ _ _)).add (PGame.mul_comm (mk _ _ _ _) _)).trans
  (PGame.add_comm _ _)).sub (PGame.mul_comm _ _))

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_one_iff_of_monic (q : ℕ) [ExpChar F q] (hm : f.Monic)
    (hi : Irreducible f) : f.natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), f = X ^ q ^ n - C y

Proof state:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
⊢ f.natSepDegree = 1 ↔ ∃ n y, f = X ^ q ^ n - C y

Tactic:
simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp] lemma bot_wcovBy_coe : ⊥ ⩿ (a : WithBot α) ↔ IsMin a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊥ ⩿ ↑a ↔ IsMin a

Tactic:
simp only [wcovBy_iff_Ioo_eq, ← image_coe_Iio, bot_le, image_eq_empty, true_and, Iio_eq_empty_iff]

Result:
no goals
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma antivary_iff_exists_monotone_antitone :
    Antivary f g ↔ ∃ (_ : LinearOrder ι), Monotone f ∧ Antitone g

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Antivary f g ↔ ∃ x, Monotone f ∧ Antitone g

Tactic:
simp [← antivaryOn_univ, antivaryOn_iff_exists_monotoneOn_antitoneOn]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_triangle_left (x y z : α) : dist x y ≤ dist z x + dist z y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y

Tactic:
apply dist_triangle

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist z x + dist z y

Tactic:
rw [dist_comm z]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_toMatrix_eq_det_toMatrix [DecidableEq κ] (b : Basis ι A M) (c : Basis κ A M)
    (f : M →ₗ[A] M) : det (LinearMap.toMatrix b b f) = det (LinearMap.toMatrix c c f)

Proof state:
M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ ((toMatrix b b) f).det = ((toMatrix c c) f).det

Tactic:
rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
    Matrix.det_conj_of_mul_eq_one] <;>
  rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftProp_iff {P : (H → H') → Set H → H → Prop} {f : M → M'} :
    LiftProp P f ↔
      Continuous f ∧ ∀ x, P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) univ (chartAt H x x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
⊢ LiftProp P f ↔ Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_le_middle_of_le_half_left {n r : ℕ} (hr : r ≤ n / 2) :
    choose n r ≤ choose n (n / 2)

Proof state:
case of_succ
n r k : ℕ
hk : k < n / 2
ih : n.choose (k + 1) ≤ n.choose (n / 2)
⊢ n.choose k ≤ n.choose (n / 2)

Tactic:
exact (choose_le_succ_of_lt_half_left hk).trans ih

Result:
no goals

Proof state:
case self
n r : ℕ
⊢ n.choose (n / 2) ≤ n.choose (n / 2)

Tactic:
rfl

Result:
no goals

Proof state:
n r : ℕ
hr : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
induction hr using decreasingInduction with
| self => rfl
| of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem darts_takeUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.takeUntil u h).darts ⊆ p.darts := fun x hx => by
  rw [← take_spec p h, darts_append, List.mem_append]
  exact Or.inl hx

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
exact Or.inl hx

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
⊢ x ∈ p.darts

Tactic:
rw [← take_spec p h, darts_append, List.mem_append]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.takeUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_δ_μ (X Y : C) (T : D) : T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 _

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.Monoidal
X Y : C
T : D
⊢ T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 (T ⊗ F.obj (X ⊗ Y))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem self_eq_add_right {a b : Nat} : a = a + b ↔ b = 0

Proof state:
a b : Nat
⊢ a = a + b ↔ b = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem isCompact_Ioo_iff {a b : α} : IsCompact (Set.Ioo a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ioo_iff.mp h.isClosed, by simp_all⟩

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ b ≤ a → IsCompact (Ioo a b)

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem cancel_left {g : FrameHom β γ} {f₁ f₂ : FrameHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : CompleteLattice γ
g : FrameHom β γ
f₁ f₂ : FrameHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
    {f : Option β → Option β} (h : m.WF) :
    (Const.alter m k f).getKeyD k fallback = if (f (Const.get? m k)).isSome then k else fallback

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k fallback : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).getKeyD k fallback = if (f (get? m k)).isSome = true then k else fallback

Tactic:
simp [getKeyD_alter h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotation_self (x : E) : ⟪J x, x⟫ = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ inner (o.rightAngleRotation x) x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma smul_pos_iff_of_pos_right [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
    0 < a • b ↔ 0 < a

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : SMulPosStrictMono α β
inst✝ : SMulPosReflectLT α β
hb : 0 < b
⊢ 0 < a • b ↔ 0 < a

Tactic:
simpa only [zero_smul] using smul_lt_smul_iff_of_pos_right hb (a₁ := 0) (a₂ := a)

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem cancel_left (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => BiheytingHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : BiheytingAlgebra α
inst✝¹ : BiheytingAlgebra β
inst✝ : BiheytingAlgebra γ
f₁ f₂ : BiheytingHom α β
g : BiheytingHom β γ
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem lift_comp_conePointsIsoOfNatIso_hom {F G : J ⥤ C} {r s : Cone F} {t : Cone G}
    (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) :
    P.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom :=
  Q.hom_ext (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F G : J ⥤ C
r s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointsIsoOfNatIso Q w).hom) ≫ t.π.app j = map r Q w.hom ≫ t.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_one_X : coeff R 1 (X : R⟦X⟧) = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ (coeff R 1) X = 1

Tactic:
rw [coeff_X, if_pos rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst)
    {h'} :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
h' : (insertMany empty l).val.contains k' = true
⊢ (insertMany empty l).val.getKey k' h' = k

Tactic:
rw [getKey_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableOn_univ : DifferentiableOn 𝕜 f univ ↔ Differentiable 𝕜 f

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
⊢ DifferentiableOn 𝕜 f univ ↔ Differentiable 𝕜 f

Tactic:
simp only [DifferentiableOn, Differentiable, differentiableWithinAt_univ, mem_univ,
  forall_true_left]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioi_pred_eq_Ici (a : α) : Ioi (pred a) = Ici a := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : α
⊢ ↑(Ioi (pred a)) = ↑(Ici a)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem ContDiffWithinAt.rpow (hf : ContDiffWithinAt ℝ n f s x) (hg : ContDiffWithinAt ℝ n g s x)
    (h : f x ≠ 0) : ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
s : Set E
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
h : f x ≠ 0
⊢ ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x

Tactic:
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prod hg)

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem int_add_iff : LiouvilleWith p (m + x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_int_iff]

Result:
no goals
-- Mathlib/Logic/Unique.lean
theorem forall_iff {p : α → Prop} : (∀ a, p a) ↔ p default :=
  ⟨fun h ↦ h _, fun h x ↦ by rwa [Unique.eq_default x]⟩

Proof state:
α : Sort u_1
inst✝ : Unique α
p : α → Prop
h : p default
x : α
⊢ p x

Tactic:
rwa [Unique.eq_default x]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem cg_of_countable [Countable M] : CG L M

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ CG L M

Tactic:
simp only [cg_def, Substructure.cg_of_countable, topEquiv.toEquiv.countable_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_eq_nhdsWithin' {a : α} {s t u : Set α} (hs : s ∈ 𝓝 a) (h₂ : t ∩ s = u ∩ s) :
    𝓝[t] a = 𝓝[u] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_2 : (coordinate 2).eval (.ofList (a0 :: a1 :: a2 :: t)) = a2

Proof state:
a0 a1 a2 : Int
t : List Int
⊢ (coordinate 2).eval (Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem one_minus_nonneg (x : I) : 0 ≤ 1 - (x : ℝ)

Proof state:
x : ↑I
⊢ 0 ≤ 1 - ↑x

Tactic:
simpa using x.2.2

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem continuous_mulExpNegMulSq : Continuous (fun x => mulExpNegMulSq ε x) :=
  Continuous.mul continuous_id (by fun_prop)

Proof state:
ε : ℝ
⊢ Continuous fun x => rexp (-(ε * x * x))

Tactic:
fun_prop

Result:
no goals