harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem lt_iff' : μ < ν ↔ μ ≤ ν ∧ ∃ s, μ s < ν s :=
  lt_iff_le_not_le.trans <| and_congr Iff.rfl <| by simp only [le_iff', not_forall, not_le]

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ¬ν ≤ μ ↔ ∃ s, μ s < ν s

Tactic:
simp only [le_iff', not_forall, not_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_one : permanent (1 : Matrix n n R) = 1

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ permanent 1 = 1

Tactic:
rw [← diagonal_one]

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x => 1).permanent = 1

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x => 1).permanent = 1

Tactic:
simp [-diagonal_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (ofList l).getKey! k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ (ofList l).getKey! k = default

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_dblZ (P : Fin 3 → A) : (W'.baseChange B).toProjective.dblZ (f ∘ P) =
    f ((W'.baseChange A).toProjective.dblZ P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.dblZ (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblZ P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblZ, map_baseChange]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem lift_algebraMap (h : IsAdjoinRoot S f) (a : R) :
    h.lift i x hx (algebraMap R S a) = i a

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
a : R
⊢ (lift i x h hx) ((algebraMap R S) a) = i a

Tactic:
rw [h.algebraMap_apply, lift_map, eval₂_C]

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem Continuous.connectedComponentsLift_continuous (h : Continuous f) :
    Continuous h.connectedComponentsLift :=
  h.quotient_liftOn' <| by convert h.image_eq_of_connectedComponent_eq

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TotallyDisconnectedSpace β
f : α → β
h : Continuous f
⊢ ∀ (a b : α), (connectedComponentSetoid α) a b → f a = f b

Tactic:
convert h.image_eq_of_connectedComponent_eq

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem map_injective {f : α → β} (Hf : Function.Injective f) : Function.Injective (Option.map f)
  | none, none, _ => rfl
  | some a₁, some a₂, H => by rw [Hf (Option.some.inj H)]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
Hf : Function.Injective f
a₁ a₂ : α
H : Option.map f (some a₁) = Option.map f (some a₂)
⊢ some a₁ = some a₂

Tactic:
rw [Hf (Option.some.inj H)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi_div_two : tan (π / 2) = 0

Proof state:
⊢ tan (π / 2) = 0

Tactic:
simp [tan_eq_sin_div_cos]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_μ_inv_app (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] :
    (F.obj m₃).map ((δ F m₁ m₂).app X) =
      (μ F (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫
          (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
rw [map_associator]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      (δ F (m₁ ⊗ m₂) m₃ ≫
              δ F m₁ m₂ ▷ F.obj m₃ ≫
                (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app
          X ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      ((δ F (m₁ ⊗ m₂) m₃).app X ≫
          (F.obj m₃).map ((δ F m₁ m₂).app X) ≫
            𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
              (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X) ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app_assoc, μ_δ_app,
  endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      (δ F (m₁ ⊗ m₂) m₃ ≫
              δ F m₁ m₂ ▷ F.obj m₃ ≫
                (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app
          X ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((δ F m₁ m₂).app X) =
    (μ F (m₁ ⊗ m₂) m₃).app X ≫
      ((δ F (m₁ ⊗ m₂) m₃).app X ≫
          (F.obj m₃).map ((δ F m₁ m₂).app X) ≫
            𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
              (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X) ≫
        (δ F m₁ (m₂ ⊗ m₃)).app X ≫ (δ F m₂ m₃).app ((F.obj m₁).obj X)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsertIfNew_snd_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α}
    {b : β a} : (m.containsThenInsertIfNew a b).2 =
      (Raw₀.containsThenInsertIfNew ⟨m, h.size_buckets_pos⟩ a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.containsThenInsertIfNew a b).snd = (Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).snd.val

Tactic:
simp [Raw.containsThenInsertIfNew, h.size_buckets_pos]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem finrank_bot_mul_relfinrank (h : A ≤ B) : finrank F A * relfinrank A B = finrank F B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ finrank F ↥A * A.relfinrank B = finrank F ↥B

Tactic:
simpa using congr(toNat $(rank_bot_mul_relrank h))

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp)]
lemma finite_powers : (powers a : Set G).Finite ↔ IsOfFinOrder a

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
⊢ IsOfFinOrder a

Tactic:
obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
  (fun n ↦ by simp [mem_powers_iff])

Result:
case intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ IsOfFinOrder a

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) = 1

Tactic:
rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
n : ℕ
⊢ (fun n => a ^ n) n ∈ ↑(powers a)

Tactic:
simp [mem_powers_iff]

Result:
no goals

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ IsOfFinOrder a

Tactic:
refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
m n : ℕ
hmn : m < n
ha : a ^ m = a ^ n
⊢ a ^ (n - m) = 1

Proof state:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ (↑(powers a)).Finite ↔ IsOfFinOrder a

Tactic:
refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩

Result:
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
h : (↑(powers a)).Finite
⊢ IsOfFinOrder a
-- Mathlib/Data/List/MinMax.lean
theorem not_maximum_lt_of_mem' (ha : a ∈ l) : ¬maximum l < (a : WithBot α)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
l : List α
a : α
ha : a ∈ l
⊢ ¬l.maximum < ↑a

Tactic:
cases h : l.maximum <;> simp_all [not_maximum_lt_of_mem ha]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
theorem lt_or_lt_of_mul_lt_mul [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂

Tactic:
contrapose!

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ ≤ a₁ ∧ b₂ ≤ b₁ → a₂ * b₂ ≤ a₁ * b₁

Tactic:
exact fun h => mul_le_mul' h.1 h.2

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_eq_iff {ψ θ : Angle} : (2 : ℕ) • ψ = (2 : ℕ) • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Proof state:
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
simp_rw [← natCast_zsmul, Nat.cast_ofNat, two_zsmul_eq_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem left_eq_midpoint_iff {x y : P} : x = midpoint R x y ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ x = midpoint R x y ↔ x = y

Tactic:
rw [eq_comm, midpoint_eq_left_iff]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem factors_lemma {k} : (k + 2) / minFac (k + 2) < k + 2 :=
  div_lt_self (Nat.zero_lt_succ _) (minFac_prime (by
      apply Nat.ne_of_gt
      apply Nat.succ_lt_succ
      apply Nat.zero_lt_succ
      )).one_lt

Proof state:
k : ℕ
⊢ k + 2 ≠ 1

Tactic:
apply Nat.ne_of_gt

Result:
case h
k : ℕ
⊢ 1 < k + 2

Proof state:
case h.a
k : ℕ
⊢ 0 < k + 1

Tactic:
apply Nat.zero_lt_succ

Result:
no goals

Proof state:
case h
k : ℕ
⊢ 1 < k + 2

Tactic:
apply Nat.succ_lt_succ

Result:
case h.a
k : ℕ
⊢ 0 < k + 1
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma interior_sInter (S : Set (Set α)) : interior (⋂₀ S) = ⋂ s ∈ S, interior s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
S : Set (Set α)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
simp_rw [sInter_eq_biInter, interior_iInter]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma mem_uIoc : a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negY P / P z = W.toAffine.negY (P x / P z) (P y / P z)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z + -W.a₃ * 1 - ((toAffine W).negY (P x / P z) (P y / P z) + -W.a₃ * (P z / P z)) = 0

Tactic:
rw [negY, Affine.negY]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
      (-(P y / P z) - (toAffine W).a₁ * (P x / P z) - (toAffine W).a₃ + -W.a₃ * (P z / P z)) =
    0

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
      (-(P y / P z) - (toAffine W).a₁ * (P x / P z) - (toAffine W).a₃ + -W.a₃ * (P z / P z)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negY P / P z = (toAffine W).negY (P x / P z) (P y / P z)

Tactic:
linear_combination (norm := (rw [negY, Affine.negY]; ring1)) -W.a₃ * div_self hPz

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_pos : 0 < ⌈a⌉ ↔ 0 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma nnreal_lt_iff [Algebra ℝ A] {a : A}
    (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ spectrum ℝ≥0 a, r < x) ↔ ∀ x ∈ spectrum ℝ a, r < x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, r < x) ↔ ∀ x ∈ spectrum ℝ a, ↑r < x

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasDerivWithinAt.inner {f g : ℝ → E} {f' g' : E} {s : Set ℝ} {x : ℝ}
    (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (fun t => ⟪f t, g t⟫) (⟪f x, g'⟫ + ⟪f', g x⟫) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
f' g' : E
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (fun t => Inner.inner (f t) (g t)) (Inner.inner (f x) g' + Inner.inner f' (g x)) s x

Tactic:
simpa using (hf.hasFDerivWithinAt.inner 𝕜 hg.hasFDerivWithinAt).hasDerivWithinAt

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic.roots_eq_primitiveRoots_val [NeZero (n : R)] :
    (cyclotomic n R).roots = (primitiveRoots n R).val

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ (cyclotomic n R).roots = (primitiveRoots n R).val

Tactic:
rw [← cyclotomic.roots_to_finset_eq_primitiveRoots]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_xor {x y : BitVec v} :
    (x ^^^ y).getLsbD i = ((x.getLsbD i) ^^ (y.getLsbD i))

Proof state:
v i : Nat
x y : BitVec v
⊢ (x ^^^ y).getLsbD i = (x.getLsbD i ^^ y.getLsbD i)

Tactic:
rw [← testBit_toNat, getLsbD, getLsbD]

Result:
v i : Nat
x y : BitVec v
⊢ (x ^^^ y).toNat.testBit i = (x.toNat.testBit i ^^ y.toNat.testBit i)

Proof state:
v i : Nat
x y : BitVec v
⊢ (x ^^^ y).toNat.testBit i = (x.toNat.testBit i ^^ y.toNat.testBit i)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_pos_eq (hab : a < b) :
    upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N ω = upcrossingsBefore a b f N ω

Tactic:
simp_rw [upcrossingsBefore, (crossing_pos_eq hab).1]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.length_lt [Fintype V] {u v : V} {p : G.Walk u v} (hp : p.IsPath) :
    p.length < Fintype.card V

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V

Tactic:
exact hp.support_nodup.length_le_card

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.length < Fintype.card V

Tactic:
rw [Nat.lt_iff_add_one_le, ← length_support]

Result:
V : Type u
G : SimpleGraph V
inst✝ : Fintype V
u v : V
p : G.Walk u v
hp : p.IsPath
⊢ p.support.length ≤ Fintype.card V
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_mem_of_ne_empty (l : Array α) (h : l ≠ #[]) : ∃ x, x ∈ l

Proof state:
α : Type u_1
l : Array α
h : l ≠ #[]
⊢ ∃ x, x ∈ l

Tactic:
simpa using List.exists_mem_of_ne_nil l.toList (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
l : Array α
h : l ≠ #[]
⊢ l.toList ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem mrange_eq_iSup {N} [Monoid N] (f : ∀ i, M i →* N) :
    MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
rw [lift, Equiv.coe_fn_mk, Con.lift_range, FreeMonoid.mrange_lift,
  range_sigma_eq_iUnion_range, Submonoid.closure_iUnion]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b => (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ ⨆ i, Submonoid.closure (range fun b => (f ⟨i, b⟩.fst) ⟨i, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
simp only [MonoidHom.mclosure_range]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem row_smul [SMul R α] (x : R) (v : m → α) : row ι (x • v) = x • row ι v

Proof state:
case a
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : ι
j✝ : m
⊢ row ι (x • v) i✝ j✝ = (x • row ι v) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ row ι (x • v) = x • row ι v

Tactic:
ext

Result:
case a
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : ι
j✝ : m
⊢ row ι (x • v) i✝ j✝ = (x • row ι v) i✝ j✝
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_le_div_iff_le_mul' : a⁻¹ ≤ b / c ↔ c ≤ a * b

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ a⁻¹ ≤ b / c ↔ c ≤ a * b

Tactic:
rw [inv_le_div_iff_le_mul, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.ne_nil {x y : List α} (h : x <:+ y) (hx : x ≠ []) : y ≠ []

Proof state:
α : Type u_1
x : List α
hx : x ≠ []
h : x <:+ []
⊢ False

Tactic:
exact hx <| List.suffix_nil.mp h

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
hx : x ≠ []
⊢ y ≠ []

Tactic:
rintro rfl

Result:
α : Type u_1
x : List α
hx : x ≠ []
h : x <:+ []
⊢ False
-- Mathlib/Topology/Separation/Basic.lean
theorem Set.Finite.isClosed [T1Space X] {s : Set X} (hs : Set.Finite s) : IsClosed s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed s

Tactic:
rw [← biUnion_of_singleton s]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed (⋃ x ∈ s, {x})

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed (⋃ x ∈ s, {x})

Tactic:
exact hs.isClosed_biUnion fun i _ => isClosed_singleton

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem sum_of [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) :
    sum I M ((DirectSum.of (fun i ↦ AdicCompletion I (M i)) j) x) =
      map I (lof R ι M j) x

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
j : ι
x : AdicCompletion I (M j)
⊢ (sum I M) ((DirectSum.of (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x

Tactic:
rw [← lof_eq_of R]

Result:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
j : ι
x : AdicCompletion I (M j)
⊢ (sum I M) ((lof R ι (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x

Proof state:
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
j : ι
x : AdicCompletion I (M j)
⊢ (sum I M) ((lof R ι (fun i => AdicCompletion I (M i)) j) x) = (map I (lof R ι M j)) x

Tactic:
apply sum_lof

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem derivWithin_inv' (hc : DifferentiableWithinAt 𝕜 c s x) (hx : c x ≠ 0) :
    derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

Tactic:
exact (hc.hasDerivWithinAt.inv hx).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
⊢ derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2

case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2
-- Mathlib/Order/ScottContinuity.lean
@[simp] lemma ScottContinuous.id : ScottContinuous (id : α → α)

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ ScottContinuous _root_.id

Tactic:
simp [ScottContinuous]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.insertMany_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} :
    Raw.Const.insertMany m l = Raw₀.Const.insertMany ⟨m, h.size_buckets_pos⟩ l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α fun x => β
h : m.WF
ρ : Type w
inst✝ : ForIn Id ρ (α × β)
l : ρ
⊢ Raw.Const.insertMany m l = (Raw₀.Const.insertMany ⟨m, ⋯⟩ l).val.val

Tactic:
simp [Raw.Const.insertMany, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem erase_add_right_pos {a : α} (s) (h : a ∈ t) : (s + t).erase a = s + t.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ (s + t).erase a = s + t.erase a

Tactic:
rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm]

Result:
no goals