harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_pair {x y z : PSet} : x ∈ ({y, z} : PSet) ↔ Equiv x y ∨ Equiv x z

Proof state:
x y z : PSet.{u_1}
⊢ x ∈ {y, z} ↔ x.Equiv y ∨ x.Equiv z

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem unpair_zero : unpair 0 = 0

Proof state:
⊢ unpair 0 = 0

Tactic:
rw [unpair]

Result:
⊢ (if 0 - sqrt 0 * sqrt 0 < sqrt 0 then (0 - sqrt 0 * sqrt 0, sqrt 0) else (sqrt 0, 0 - sqrt 0 * sqrt 0 - sqrt 0)) = 0

Proof state:
⊢ (if 0 - sqrt 0 * sqrt 0 < sqrt 0 then (0 - sqrt 0 * sqrt 0, sqrt 0) else (sqrt 0, 0 - sqrt 0 * sqrt 0 - sqrt 0)) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_prefix : l.rdropWhile p <+: l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse

Tactic:
exact dropWhile_suffix _

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l <+: l

Tactic:
rw [← reverse_suffix, rdropWhile, reverse_reverse]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p l.reverse <:+ l.reverse
-- Mathlib/Order/Cover.lean
@[simp, norm_cast] lemma coe_covBy_coe : (a : WithBot α) ⋖ b ↔ a ⋖ b :=
  Set.OrdConnected.apply_covBy_apply_iff OrderEmbedding.withBotCoe <| by
    simp [WithBot.range_coe, ordConnected_Ioi]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (range ⇑OrderEmbedding.withBotCoe).OrdConnected

Tactic:
simp [WithBot.range_coe, ordConnected_Ioi]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem card_Iio_eq_card_Iic_sub_one (a : α) : #(Iio a) = #(Iic a) - 1

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iic a) - 1

Tactic:
rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mapIdx_mk (a : Array α) (h : a.size = n) (f : Nat → α → β) :
    (Vector.mk a h).mapIdx f = Vector.mk (a.mapIdx f) (by simp [h]) := rfl

Proof state:
α : Type ?u.10817
n : Nat
β : Type ?u.10843
a : Array α
h : a.size = n
f : Nat → α → β
⊢ (Array.mapIdx f a).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma rightDeriv_klFun_one : derivWithin klFun (Ioi 1) 1 = 0

Proof state:
⊢ derivWithin klFun (Ioi 1) 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem ofReal_rpow_of_pos {x p : ℝ} (hx_pos : 0 < x) :
    ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
x p : ℝ
hx_pos : 0 < x
⊢ ↑x.toNNReal ^ p = ↑(x ^ p).toNNReal

Tactic:
rw [← coe_rpow_of_ne_zero, coe_inj, Real.toNNReal_rpow_of_nonneg hx_pos.le]

Result:
case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0

Proof state:
case h
x p : ℝ
hx_pos : 0 < x
⊢ x.toNNReal ≠ 0

Tactic:
simp [hx_pos]

Result:
no goals

Proof state:
x p : ℝ
hx_pos : 0 < x
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp_rw [ENNReal.ofReal]

Result:
x p : ℝ
hx_pos : 0 < x
⊢ ↑x.toNNReal ^ p = ↑(x ^ p).toNNReal
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_le_iff_forall {x : ℝ} :
    schnirelmannDensity A ≤ x ↔
      ∀ ε : ℝ, 0 < ε → ∃ n : ℕ, 0 < n ∧ #{a ∈ Ioc 0 n | a ∈ A} / n < x + ε

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x + ε

Tactic:
simp only [schnirelmannDensity_lt_iff]

Result:
no goals

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x + ε

Tactic:
rw [le_iff_forall_pos_lt_add]

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < x + ε
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem aeSeq_eq_mk_ae [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ)
    (hp : ∀ᵐ x ∂μ, p x fun n => f n x) : ∀ᵐ a : α ∂μ, ∀ i : ι, aeSeq hf p i a = (hf i).mk (f i) a :=
  have h_ss : aeSeqSet hf p ⊆ { a : α | ∀ i, aeSeq hf p i a = (hf i).mk (f i) a } := fun x hx i =>
    by simp only [aeSeq, hx, if_true]
  (ae_iff.2 (measure_compl_aeSeqSet_eq_zero hf hp)).mono h_ss

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
simp only [aeSeq, hx, if_true]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc (attr := simp)]
lemma pullbackAwayιIso_hom_SpecMap_awayMap_right :
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg (hx.trans (mul_comm _ _)))) =
      Limits.pullback.snd _ _

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯ =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)) =
    Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')

Tactic:
rw [← cancel_mono (awayι 𝒜 g g_deg hm'), ← Limits.pullback.condition,
  ← pullbackAwayιIso_hom_awayι 𝒜 f_deg hm g_deg hm' hx,
  Category.assoc, SpecMap_awayMap_awayι]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯ =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_C_mul_X_pow (ha : a ≠ 0) (n : ℕ) :
    Polynomial.roots (C a * X ^ n) = n • ({0} : Multiset R)

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).roots = n • {0}

Tactic:
rw [roots_C_mul _ ha, roots_X_pow]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem one_of_mem_closedBall (hx : x ∈ closedBall c f.rIn) : f x = 1

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ ↑f x = 1

Tactic:
apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn

Result:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ ‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1

Proof state:
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ ‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1

Tactic:
simpa only [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
  div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
    BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat

Proof state:
w : Nat
x : BitVec w
⊢ x.toInt < 0 ↔ 2 ^ w ≤ 2 * x.toNat

Tactic:
simp [toInt_eq_toNat_cond]

Result:
w : Nat
x : BitVec w
⊢ (if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) < 0 ↔ 2 ^ w ≤ 2 * x.toNat

Proof state:
w : Nat
x : BitVec w
⊢ (if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) < 0 ↔ 2 ^ w ≤ 2 * x.toNat

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem range_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) :
    range (p.liftQ f h) = range f

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ ker f
⊢ range (p.liftQ f h) = range f

Tactic:
simpa only [range_eq_map] using map_liftQ _ _ _ _

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
lemma surjective_of_nonempty_fiber_of_isConnected {X A : C} [Nonempty (F.obj X)]
    [IsConnected A] (f : X ⟶ A) :
    Function.Surjective (F.map f)

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
X A : C
inst✝¹ : Nonempty (F.obj X).carrier
inst✝ : IsConnected A
f : X ⟶ A
this : Epi f
⊢ Function.Surjective (F.map f)

Tactic:
exact surjective_on_fiber_of_epi F f

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
X A : C
inst✝¹ : Nonempty (F.obj X).carrier
inst✝ : IsConnected A
f : X ⟶ A
⊢ Function.Surjective (F.map f)

Tactic:
have : Epi f := epi_of_nonempty_of_isConnected F f

Result:
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
X A : C
inst✝¹ : Nonempty (F.obj X).carrier
inst✝ : IsConnected A
f : X ⟶ A
this : Epi f
⊢ Function.Surjective (F.map f)
-- Mathlib/Data/Finset/Filter.lean
theorem filter_comm (s : Finset α) : (s.filter p).filter q = (s.filter q).filter p

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter q (filter p s) = filter p (filter q s)

Tactic:
simp_rw [filter_filter, and_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
/-- Named in analogy to `Bool.dichotomy`. -/
lemma DyckStep.dichotomy (s : DyckStep) : s = U ∨ s = D

Proof state:
s : DyckStep
⊢ s = U ∨ s = D

Tactic:
cases s <;> tauto

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

Proof state:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)

Tactic:
exact conjugate hx z

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * z)

Tactic:
nth_rewrite 2 [← hz]

Result:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * star z)
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
    (h2s : MapsTo f s (extChartAt I' y).source) :
    MDifferentiableOn I I' f s ↔
        DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Tactic:
rw [extChartAt_source] at hs h2s

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (chartAt H x).source
h2s : MapsTo f s (chartAt H' y).source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (chartAt H x).source
h2s : MapsTo f s (chartAt H' y).source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s)

Tactic:
exact mdifferentiableOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
  (chart_mem_maximalAtlas y) hs h2s

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiff.div₀ (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ x, g x ≠ 0) :
    ContMDiff I' I n (f / g)

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : ContMDiffInv₀ I n G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
h₀ : ∀ (x : M), g x ≠ 0
⊢ ContMDiff I' I n (f / g)

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem denselyOrdered_orderDual [LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α :=
  ⟨by convert @OrderDual.denselyOrdered αᵒᵈ _, @OrderDual.denselyOrdered α _⟩

Proof state:
α : Type u_2
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α

Tactic:
convert @OrderDual.denselyOrdered αᵒᵈ _

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_iff {l l' : List α} {n : ℕ} :
    l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Proof state:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]

Result:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Proof state:
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]

Result:
no goals

Proof state:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rcases l'.length.zero_le.eq_or_lt with hl | hl

Result:
case inl
α : Type u
l l' : List α
n : ℕ
hl : 0 = l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Proof state:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]

Result:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Proof state:
case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 = n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
simp [← hn]

Result:
no goals

Proof state:
case inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn

Result:
case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 = n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Proof state:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ n % l'.length ≤ l'.length

Tactic:
exact (Nat.mod_lt _ hl).le

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_right_iff {X Y : C} (f g : X ⟶ Y) : f ⊗ 𝟙 (𝟙_ C) = g ⊗ 𝟙 (𝟙_ C) ↔ f = g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f g : X ⟶ Y
⊢ f ⊗ 𝟙 (𝟙_ C) = g ⊗ 𝟙 (𝟙_ C) ↔ f = g

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem option_bind {f : α → Option β} {g : α → β → Option σ} (hf : Computable f)
    (hg : Computable₂ g) : Computable fun a => (f a).bind (g a) :=
  (option_casesOn hf (const Option.none) hg).of_eq fun a => by cases f a <;> rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Computable f
hg : Computable₂ g
a : α
⊢ Option.casesOn (f a) Option.none (g a) = (f a).bind (g a)

Tactic:
cases f a <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Idempotent.lean
lemma mul_eq_zero_add_eq_one_ext_left (eq : a.1.1 = b.1.1) : a = b

Proof state:
case refine_1
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 * (↑a).2 = (↑b).2 * (↑a).1

Tactic:
rw [a.2.1, mul_comm, eq, b.2.1]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ a = b

Tactic:
refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 * (↑a).2 = (↑b).2 * (↑a).1

case refine_2
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 + (↑b).2 = 1

Proof state:
case refine_2
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).1 = (↑b).1
⊢ (↑a).1 + (↑b).2 = 1

Tactic:
rw [eq, b.2.2]

Result:
no goals
-- Mathlib/Data/Set/Monotone.lean
theorem strictMono_restrict [Preorder α] [Preorder β] {f : α → β} {s : Set α} :
    StrictMono (s.restrict f) ↔ StrictMonoOn f s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMono (s.restrict f) ↔ StrictMonoOn f s

Tactic:
simp [Set.restrict, StrictMono, StrictMonoOn]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem realPart_I_smul (a : A) : ℜ (I • a) = -ℑ a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ℜ (I • a) = -ℑ a

Tactic:
ext

Result:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ (I • a)) = ↑(-ℑ a)

Proof state:
case a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ (I • a)) = ↑(-ℑ a)

Tactic:
rw [realPart_apply_coe, NegMemClass.coe_neg, imaginaryPart_apply_coe, neg_smul, neg_neg,
  smul_comm I, star_smul, star_def, conj_I, smul_sub, neg_smul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldl_succ_last (f : (i : Fin (n+1)) → α i.castSucc → α i.succ) (x) :
    dfoldl (n+1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (f ·.castSucc ·) x)

Proof state:
case succ
n : Nat
ih :
  ∀ {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0),
    dfoldl n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (f 0 x) =
      f (last n) (dfoldl n (α ∘ castSucc) (fun x1 x2 => f x1.castSucc x2) x)
α : Fin (n + 1 + 1 + 1) → Type u_1
f : (i : Fin (n + 1 + 1)) → α i.castSucc → α i.succ
x : α 0
⊢ f (last n).succ (dfoldl n ((α ∘ succ) ∘ castSucc) (fun x1 x2 => f x1.castSucc.succ x2) (f 0 x)) =
    f (last (n + 1)) (dfoldl n ((α ∘ castSucc) ∘ succ) (fun x1 x2 => f x1.succ.castSucc x2) (f (castSucc 0) x))

Tactic:
congr

Result:
no goals

Proof state:
n : Nat
α : Fin (n + 1 + 1) → Type u_1
f : (i : Fin (n + 1)) → α i.castSucc → α i.succ
x : α 0
⊢ dfoldl (n + 1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (fun x1 x2 => f x1.castSucc x2) x)

Tactic:
rw [dfoldl_succ]

Result:
n : Nat
α : Fin (n + 1 + 1) → Type u_1
f : (i : Fin (n + 1)) → α i.castSucc → α i.succ
x : α 0
⊢ dfoldl n (α ∘ succ) (fun x1 x2 => f x1.succ x2) (f 0 x) =
    f (last n) (dfoldl n (α ∘ castSucc) (fun x1 x2 => f x1.castSucc x2) x)

Proof state:
case zero
α : Fin (0 + 1 + 1) → Type u_1
f : (i : Fin (0 + 1)) → α i.castSucc → α i.succ
x : α 0
⊢ dfoldl 0 (α ∘ succ) (fun x1 x2 => f x1.succ x2) (f 0 x) =
    f (last 0) (dfoldl 0 (α ∘ castSucc) (fun x1 x2 => f x1.castSucc x2) x)

Tactic:
simp [dfoldl_succ, last]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem ne_neg_self [NoZeroSMulDivisors R M] (x : Module.Ray R M) : x ≠ -x

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : Ray R M
⊢ x ≠ -x

Tactic:
induction x using Module.Ray.ind with | h x hx =>
rw [neg_rayOfNeZero, Ne, ray_eq_iff]
exact mt eq_zero_of_sameRay_self_neg hx

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx

Tactic:
rw [neg_rayOfNeZero, Ne, ray_eq_iff]

Result:
case h
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)

Proof state:
case h
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
hx : x ≠ 0
⊢ ¬SameRay R x (-x)

Tactic:
exact mt eq_zero_of_sameRay_self_neg hx

Result:
no goals