harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem fst_unzip (as : Array (α × β)) : (Array.unzip as).fst = as.map Prod.fst

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) { toList := as }).fst =
    map Prod.fst { toList := as }

Tactic:
simp only [List.foldl_toArray']

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (List.foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).fst = map Prod.fst { toList := as }

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ List.foldl push (#[], #[]).fst (List.map Prod.fst as) = map Prod.fst { toList := as }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (List.foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).fst = map Prod.fst { toList := as }

Tactic:
rw [← List.foldl_hom (f := Prod.fst) (g₂ := fun bs x => bs.push x.1) (H := by simp), ← List.foldl_map]

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ List.foldl push (#[], #[]).fst (List.map Prod.fst as) = map Prod.fst { toList := as }

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ as.unzip.fst = map Prod.fst as

Tactic:
simp only [unzip]

Result:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).fst = map Prod.fst as

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) as).fst = map Prod.fst as

Tactic:
rcases as with ⟨as⟩

Result:
case mk
α : Type u_1
β : Type u_2
as : List (α × β)
⊢ (foldl (fun x x_1 => (x.fst.push x_1.fst, x.snd.push x_1.snd)) (#[], #[]) { toList := as }).fst =
    map Prod.fst { toList := as }

Proof state:
α : Type u_1
β : Type u_2
as : List (α × β)
l : List (α × β)
init : Array α × Array β
⊢ ∀ (x : Array α × Array β) (y : α × β), (fun bs x => bs.push x.fst) x.fst y = (x.fst.push y.fst, x.snd.push y.snd).fst

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma int_div_self_pos {a : ℤ} (ha : 0 < a) : 0 < a / a

Proof state:
a : ℤ
ha : 0 < a
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
a : ℤ
ha : 0 < a
⊢ 0 < a / a

Tactic:
rw [Int.ediv_self ha.ne']

Result:
a : ℤ
ha : 0 < a
⊢ 0 < 1
-- Mathlib/Data/Stream/Init.lean
theorem iterate_eq (f : α → α) (a : α) : iterate f a = a::iterate f (f a)

Proof state:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)

Tactic:
rw [tail_iterate]

Result:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)

Proof state:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: iterate f (f a) = a :: iterate f (f a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)

Tactic:
rw [← Stream'.eta (iterate f a)]

Result:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.reverse {t : RBNode α} : t.reverse.All p ↔ t.All p

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
⊢ All p t.reverse ↔ All p t

Tactic:
induction t <;> simp [*, and_comm]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem Disjoint.sdiff_unique (hd : Disjoint x z) (hz : z ≤ y) (hs : y ≤ x ⊔ z) :
    y \ x = z :=
  sdiff_unique
    (by
      rw [← inf_eq_right] at hs
      rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
        hs, sup_eq_left])
    (by rw [inf_assoc, hd.eq_bot, inf_bot_eq])

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y

Tactic:
rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
  hs, sup_eq_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [inf_assoc, hd.eq_bot, inf_bot_eq]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : y ≤ x ⊔ z
⊢ y ⊓ x ⊔ z = y

Tactic:
rw [← inf_eq_right] at hs

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ x ⊔ z = y
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem biInf_apply {ι} {I : Set ι} (hI : I.Nonempty) (m : ι → OuterMeasure α) (s : Set α) :
    (⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ i ∈ I, m i (t n)

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
simp only [← iInf_subtype'', iInf_apply]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
haveI := hI.to_subtype

Result:
α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem Orientation.measure_eq_volume (o : Orientation ℝ F (Fin n)) :
    o.volumeForm.measure = volume

Proof state:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
⊢ o.volumeForm.measure = volume

Tactic:
have A : o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1 :=
  Orientation.measure_orthonormalBasis o (stdOrthonormalBasis ℝ F)

Result:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ o.volumeForm.measure = volume

Proof state:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ o.volumeForm.measure = volume

Tactic:
rw [addHaarMeasure_unique o.volumeForm.measure
  (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]

Result:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ addHaarMeasure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = volume

Proof state:
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A : o.volumeForm.measure ↑(stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1
⊢ addHaarMeasure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = volume

Tactic:
simp only [volume, Basis.addHaar]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_comp_castSucc {α : Sort*} {a : α} {f : Fin n → α} :
    (snoc f a : Fin (n + 1) → α) ∘ castSucc = f :=
  funext fun i ↦ by rw [Function.comp_apply, snoc_castSucc]

Proof state:
n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ (snoc f a ∘ castSucc) i = f i

Tactic:
rw [Function.comp_apply, snoc_castSucc]

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem mem_acceptsFrom {s : σ} {x : List α} :
    x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept

Proof state:
α : Type u
σ : Type v
M : DFA α σ
s : σ
x : List α
⊢ x ∈ M.acceptsFrom s ↔ M.evalFrom s x ∈ M.accept

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem hom.congr_right {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.right = φ₂.right

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.right = φ₂.right

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1

Proof state:
n : Nat
⊢ 0 ≠ n + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem uniformEquicontinuous_finite [Finite ι] {F : ι → β → α} :
    UniformEquicontinuous F ↔ ∀ i, UniformContinuous (F i)

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ (∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β, (F y x_2.1, F y x_2.2) ∈ x) ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)

Tactic:
simp only [UniformEquicontinuous, eventually_all, @forall_swap _ ι]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
inst✝ : Finite ι
F : ι → β → α
⊢ (∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β, (F y x_2.1, F y x_2.2) ∈ x) ↔ ∀ (i : ι), UniformContinuous (F i)
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f` is convex on `S` and differentiable at all points of `S`, then its derivative is monotone
on `S`. -/
lemma strictMonoOn_deriv (hfc : StrictConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
    StrictMonoOn (deriv f) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ deriv f x < deriv f y

Tactic:
exact (hfc.deriv_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_deriv hx hy hxy (hfd y hy))

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictMonoOn (deriv f) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ deriv f x < deriv f y
-- Mathlib/Order/Bounded.lean
theorem bounded_le_inter_le [LinearOrder α] (a : α) :
    Bounded (· ≤ ·) (s ∩ { b | a ≤ b }) ↔ Bounded (· ≤ ·) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
refine ⟨?_, Bounded.mono Set.inter_subset_left⟩

Result:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) → Bounded (fun x1 x2 => x1 ≤ x2) s

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) → Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
rw [← @bounded_le_inter_lt _ s _ a]

Result:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) → Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b})

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a ≤ b}) → Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b})

Tactic:
exact Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@[reassoc]
lemma fromLeftDerivedZero'_naturality {C} [Category C] [Abelian C] {X Y : C} (f : X ⟶ Y)
    (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f)
    (F : C ⥤ D) [F.Additive] :
    HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex _).map φ) 0 ≫
        Q.fromLeftDerivedZero' F = P.fromLeftDerivedZero' F ≫ F.map f

Proof state:
D : Type u_1
inst✝⁴ : Category.{u_4, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0 ≫ Q.fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F ≫ F.map f

Tactic:
simp only [← cancel_epi (HomologicalComplex.pOpcycles _ _), ← F.map_comp, comm,
  HomologicalComplex.p_opcyclesMap_assoc, Functor.mapHomologicalComplex_map_f,
  pOpcycles_comp_fromLeftDerivedZero', pOpcycles_comp_fromLeftDerivedZero'_assoc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Closeds.lean
theorem lipschitz_infDist_set (x : α) : LipschitzWith 1 fun s : NonemptyCompacts α => infDist x s :=
  LipschitzWith.of_le_add fun s t => by
    rw [dist_comm]
    exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

Proof state:
α : Type u
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist s t

Tactic:
rw [dist_comm]

Result:
α : Type u
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s

Proof state:
α : Type u
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s

Tactic:
exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
@[simp, norm_cast]
lemma cast_pow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n) = (m ^ n : α)
  | 0 => by simp
  | n + 1 => by rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

Proof state:
α : Type u_1
inst✝ : Semiring α
m n : ℕ
⊢ ↑(m ^ (n + 1)) = ↑m ^ (n + 1)

Tactic:
rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem countable_meas_level_set_pos₀ {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    [SFinite μ] [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β}
    (g_mble : NullMeasurable g μ) : Set.Countable { t : β | 0 < μ { a : α | g a = t } }

Proof state:
α : Type u_5
β : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
level_sets_disjoint : Pairwise (Disjoint on fun t => {a | g a = t})
⊢ {t | 0 < μ {a | g a = t}}.Countable

Tactic:
exact Measure.countable_meas_pos_of_disjoint_iUnion₀
  (fun b => g_mble (‹MeasurableSingletonClass β›.measurableSet_singleton b))
  ((fun _ _ h ↦ Disjoint.aedisjoint (level_sets_disjoint h)))

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
⊢ {t | 0 < μ {a | g a = t}}.Countable

Tactic:
have level_sets_disjoint : Pairwise (Disjoint on fun t : β => { a : α | g a = t }) :=
  fun s t hst => Disjoint.preimage g (disjoint_singleton.mpr hst)

Result:
α : Type u_5
β : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : SFinite μ
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
level_sets_disjoint : Pairwise (Disjoint on fun t => {a | g a = t})
⊢ {t | 0 < μ {a | g a = t}}.Countable
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma filter_piFinset_eq_map_snocEquiv (P : (∀ i, α (castSucc i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (init r)} =
      (S (last _) ×ˢ {r ∈ piFinset (init S) | P r}).map (snocEquiv α).toEmbedding

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ filter (fun r => P (init r)) (piFinset S) =
    map (snocEquiv α).toEmbedding (S (last n) ×ˢ filter (fun r => P r) (piFinset (init S)))

Tactic:
simp [← map_snocEquiv_filter_piFinset, map_map]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma re_mul_ofReal (z : ℂ) (r : ℝ) : (z * r).re = z.re *  r

Proof state:
z : ℂ
r : ℝ
⊢ (z * ↑r).re = z.re * r

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_sqrt (a : A) (x : ℝ) (h : 0 ∉ spectrum ℝ≥0 a)
    (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
⊢ 2⁻¹ ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ
h : 0 ∉ spectrum ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
rw [sqrt_eq_rpow, div_eq_mul_inv, one_mul,
    rpow_rpow _ _ _ h (by norm_num), inv_mul_eq_div]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
/-- If `X` is an object in a Grothendieck abelian category, then
the functor `coyoneda.obj (op X)` commutes with colimits corresponding
to diagrams of monomorphisms indexed by `κ`-filtered categories
for a big enough regular cardinal `κ`. -/
lemma preservesColimit_coyoneda_obj_of_mono
    (Y : J ⥤ C) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
    [IsCardinalFiltered J κ] (hXκ : HasCardinalLT (Subobject X) κ)
    [∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)] :
    PreservesColimit Y ((coyoneda.obj (op X))) where
  preserves {c} hc := ⟨by
    have := isFiltered_of_isCardinalDirected J κ
    exact Types.FilteredColimit.isColimitOf' _ _
      (surjectivity hc hXκ) (injectivity hc hXκ)⟩

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
have := isFiltered_of_isCardinalDirected J κ

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
this : IsFiltered J
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
this : IsFiltered J
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
exact Types.FilteredColimit.isColimitOf' _ _
  (surjectivity hc hXκ) (injectivity hc hXκ)

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
/-- The **Marica-Schönheim Inequality**. -/
lemma Finset.card_le_card_diffs (s : Finset α) : #s ≤ #(s \\ s) :=
  le_of_pow_le_pow_left₀ two_ne_zero (zero_le _) <| by
    simpa [← sq] using s.le_card_diffs_mul_card_diffs s

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s : Finset α
⊢ #s ^ 2 ≤ #(s \\ s) ^ 2

Tactic:
simpa [← sq] using s.le_card_diffs_mul_card_diffs s

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem surjective_rangeRestrict : Surjective f.rangeRestrict

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f.rangeRestrict

Tactic:
rw [← range_eq_top, range_rangeRestrict]

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
/-- **Vertical line test** for monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some monoid homomorphism `f : H → I`. -/
@[to_additive "**Vertical line test** for additive monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` surjects onto the first
factor and `G` intersects every \"vertical line\" `{(h, i) | i : I}` at most once. Then `G` is the
graph of some monoid homomorphism `f : H → I`."]
lemma Submonoid.exists_eq_mgraph {G : Submonoid (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) :
    ∃ f : H →* I, G = f.mgraph

Proof state:
H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.mgraph

Tactic:
simpa using MonoidHom.exists_mrange_eq_mgraph hG₁.surjective
  fun a b h ↦ congr_arg (Prod.snd ∘ G.subtype) (hG₁.injective h)

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@[simp] lemma eLpNormEssSup_smul_measure (hc : c ≠ 0) (f : α → F) :
    eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
R : Type u_6
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → F
⊢ essSup (fun x => ‖f x‖ₑ) (c • μ) = essSup (fun x => ‖f x‖ₑ) μ

Tactic:
exact essSup_smul_measure hc _

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
R : Type u_6
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → F
⊢ eLpNormEssSup f (c • μ) = eLpNormEssSup f μ

Tactic:
simp_rw [eLpNormEssSup]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
R : Type u_6
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → F
⊢ essSup (fun x => ‖f x‖ₑ) (c • μ) = essSup (fun x => ‖f x‖ₑ) μ
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem im_pos_of_dist_center_le {z : ℍ} {r : ℝ} {w : ℂ}
    (h : dist w (center z r) ≤ z.im * Real.sinh r) : 0 < w.im :=
  calc
    0 < z.im * (Real.cosh r - Real.sinh r) := mul_pos z.im_pos (sub_pos.2 <| sinh_lt_cosh _)
    _ = (z.center r).im - z.im * Real.sinh r := mul_sub _ _ _
    _ ≤ (z.center r).im - dist (z.center r : ℂ) w := sub_le_sub_left (by rwa [dist_comm]) _
    _ ≤ w.im := sub_le_comm.1 <| (le_abs_self _).trans (abs_im_le_norm <| z.center r - w)

Proof state:
z : ℍ
r : ℝ
w : ℂ
h : dist w ↑(z.center r) ≤ z.im * Real.sinh r
⊢ dist (↑(z.center r)) w ≤ z.im * Real.sinh r

Tactic:
rwa [dist_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[simp, norm_cast] lemma odd_coe_nat (n : ℕ) : Odd (n : ℤ) ↔ Odd n

Proof state:
n : ℕ
⊢ Odd ↑n ↔ Odd n

Tactic:
rw [← not_even_iff_odd, ← Nat.not_even_iff_odd, even_coe_nat]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} : exp x = exp y ↔ exp (x - y) = 1

Proof state:
x y : ℂ
⊢ cexp x = cexp y ↔ cexp (x - y) = 1

Tactic:
rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]

Result:
no goals