harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Smooth/Kaehler.lean
@[simp]
lemma tensorKaehlerQuotKerSqEquiv_symm_tmul_D (s t) :
    (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ .D _ _ t) =
      s ⊗ₜ .D _ _ (Ideal.Quotient.mk _ t)

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (D R P) t) =
    s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
      (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)

Tactic:
apply (tensorKaehlerQuotKerSqEquiv R P S).injective

Result:
case a
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S) ((tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (D R P) t)) =
    (tensorKaehlerQuotKerSqEquiv R P S)
      (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
        (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t))

Proof state:
case a
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S) ((tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (D R P) t)) =
    (tensorKaehlerQuotKerSqEquiv R P S)
      (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
        (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Proof state:
x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))

Tactic:
exact sinh_add_aux

Result:
no goals

Proof state:
x y : ℂ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
  mul_assoc, two_sinh, mul_left_comm, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
  mul_left_comm, two_cosh, ← mul_assoc, two_cosh]

Result:
x y : ℂ
⊢ (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y - cexp (-x) * cexp (-y))
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem map_liftQ [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h) (q : Submodule R (M ⧸ p)) :
    q.map (p.liftQ f h) = (q.comap p.mkQ).map f :=
  le_antisymm (by rintro _ ⟨⟨x⟩, hxq, rfl⟩; exact ⟨x, hxq, rfl⟩)
    (by rintro _ ⟨x, hxq, rfl⟩; exact ⟨Quotient.mk x, hxq, rfl⟩)

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
q : Submodule R (M ⧸ p)
⊢ map (p.liftQ f h) q ≤ map f (comap p.mkQ q)

Tactic:
rintro _ ⟨⟨x⟩, hxq, rfl⟩

Result:
case intro.mk.intro
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
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel) x ∈ ↑q
⊢ (p.liftQ f h) (Quot.mk (⇑p.quotientRel) x) ∈ map f (comap p.mkQ q)

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
q : Submodule R (M ⧸ p)
⊢ map f (comap p.mkQ q) ≤ map (p.liftQ f h) q

Tactic:
rintro _ ⟨x, hxq, rfl⟩

Result:
case intro.intro
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
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap p.mkQ q)
⊢ f x ∈ map (p.liftQ f h) q

Proof state:
case intro.mk.intro
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
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel) x ∈ ↑q
⊢ (p.liftQ f h) (Quot.mk (⇑p.quotientRel) x) ∈ map f (comap p.mkQ q)

Tactic:
exact ⟨x, hxq, rfl⟩

Result:
no goals

Proof state:
case intro.intro
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
q : Submodule R (M ⧸ p)
x : M
hxq : x ∈ ↑(comap p.mkQ q)
⊢ f x ∈ map (p.liftQ f h) q

Tactic:
exact ⟨Quotient.mk x, hxq, rfl⟩

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_subtype (p : α → Prop) [DecidablePred p] (s : Finset α) :
    #(s.subtype p) = #(s.filter p)

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ #(Finset.subtype p s) = #(filter p s)

Tactic:
simp [Finset.subtype]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem powerset_card_biUnion [DecidableEq (Finset α)] (s : Finset α) :
    Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetCard i s

Proof state:
α : Type u_1
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ s.powerset = (range (#s + 1)).biUnion fun i => powersetCard i s

Tactic:
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_compl_self :
    ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x

Tactic:
rw [compl_eq_univ_diff, continuousWithinAt_diff_self, continuousWithinAt_univ]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.tan (o.oangle y (y - x)) * ‖y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).tan * ‖y‖ = ‖x‖
-- Mathlib/Order/WithBot.lean
lemma lt_iff_exists_coe : x < y ↔ ∃ b : α, y = b ∧ x < b

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithBot α
⊢ x < y ↔ ∃ b, y = ↑b ∧ x < ↑b

Tactic:
cases y <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma isValuedIn_iff_mem_range :
    P.IsValuedIn S ↔ ∀ i j, P.pairing i j ∈ range (algebraMap S R)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra S R
⊢ P.IsValuedIn S ↔ ∀ (i j : ι), P.pairing i j ∈ range ⇑(algebraMap S R)

Tactic:
simp only [isValuedIn_iff, mem_range]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem of_subsingleton [Subsingleton α] {K : ℝ≥0} : AntilipschitzWith K f := fun x y => by
  simp only [Subsingleton.elim x y, edist_self, zero_le]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
K : ℝ≥0
x y : α
⊢ edist x y ≤ ↑K * edist (f x) (f y)

Tactic:
simp only [Subsingleton.elim x y, edist_self, zero_le]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem root_mul_right_of_isRoot {p : R[X]} (q : R[X]) : IsRoot p a → IsRoot (p * q) a := fun H =>
  by rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]

Proof state:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Filter.lift'_closure_eq_bot {l : Filter X} : l.lift' closure = ⊥ ↔ l = ⊥ :=
  ⟨fun h => bot_unique <| h ▸ l.le_lift'_closure, fun h =>
    h.symm ▸ by rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ ⊥.lift' closure = ⊥

Tactic:
rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_comp_lift {T : Submonoid M} (hST : S ≤ T) {Q : Type*} [CommMonoid Q]
    (k : LocalizationMap T Q) {A : Type*} [CommMonoid A] {l : M →* A}
    (hl : ∀ w : T, IsUnit (l w)) :
    (k.lift hl).comp (f.lift (map_units k ⟨_, hST ·.2⟩)) =
    f.lift (hl ⟨_, hST ·.2⟩) := .symm <|
  lift_unique _ _ fun x ↦ by rw [← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp (f.lift ⋯)) (f.toMap x) = l x

Tactic:
rw [← MonoidHom.comp_apply,
MonoidHom.comp_assoc, lift_comp, lift_comp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_map_filter_mul_prod_map_filter_not (p : α → Prop) [DecidablePred p] (f : α → M)
    (l : List α) :
    ((l.filter p).map f).prod * ((l.filter fun x => ¬p x).map f).prod = (l.map f).prod

Proof state:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun b => decide (p b)) l)).prod * (map f (filter (fun x => decide ¬p x) l)).prod = (map f l).prod

Tactic:
rw [← prod_map_ite]

Result:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map (fun a => if p a then f a else f a) l).prod = (map f l).prod

Proof state:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map (fun a => if p a then f a else f a) l).prod = (map f l).prod

Tactic:
simp only [ite_self]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
/--
If `s ≠ 0`, then the `if .. then .. else` construction in `LSeries.term` isn't needed, since
`0 ^ s = 0`.
-/
lemma term_of_ne_zero' {s : ℂ} (hs : s ≠ 0) (f : ℕ → ℂ) (n : ℕ) :
    term f s n = f n / n ^ s

Proof state:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ term f s 0 = f 0 / ↑0 ^ s

Tactic:
rw [term_zero, Nat.cast_zero, zero_cpow hs, div_zero]

Result:
no goals

Proof state:
case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s

Tactic:
rw [term_of_ne_zero hn]

Result:
no goals

Proof state:
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
⊢ term f s n = f n / ↑n ^ s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ term f s 0 = f 0 / ↑0 ^ s

case inr
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = f n / ↑n ^ s
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) {a} :
    a < bsup.{_, v} o f ↔ ∃ i hi, a < f i hi

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi

Tactic:
simpa only [not_forall, not_le] using not_congr (@bsup_le_iff.{_, v} _ f a)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean
lemma norm_sqrt (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖sqrt a‖ = √‖a‖

Tactic:
simpa using congr(NNReal.toReal $(nnnorm_sqrt a ha))

Result:
no goals
-- Mathlib/Probability/Kernel/Proper.lean
lemma IsProper.setLIntegral_eq_indicator_mul_lintegral (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧)
    (hf : Measurable[𝓧] f) (hB : MeasurableSet[𝓑] B) (x₀ : X) :
    ∫⁻ x in B, f x ∂(π x₀) = B.indicator 1 x₀ * ∫⁻ x, f x ∂(π x₀)

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
x₀ : X
⊢ ∫⁻ (x : X) in B, f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
simp [← hπ.lintegral_indicator_mul h𝓑𝓧 hf hB, ← indicator_mul_left,
  lintegral_indicator (h𝓑𝓧 _ hB)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem right_mem_perpBisector : p₂ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₂ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂

Tactic:
simpa [mem_perpBisector_iff_inner_eq_inner] using eq_comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_expand [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α]
    {buckets : {d : Array (AssocList α β) // 0 < d.size}} : IsHashSelf (expand buckets).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulHashable α
inst✝ : EquivBEq α
buckets : { d // 0 < d.size }
⊢ IsHashSelf (expand buckets).val

Tactic:
simpa [expand, expand.go_eq] using isHashSelf_foldl_reinsertAux _ _ (by simp)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulHashable α
inst✝ : EquivBEq α
buckets : { d // 0 < d.size }
⊢ IsHashSelf ⟨mkArray (buckets.val.size * 2) AssocList.nil, ⋯⟩.val

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem map_comp_coe {α β} (h : α → β) :
    Functor.map h ∘ ofList = (ofList ∘ Functor.map h : List α → Multiset β)

Proof state:
case h
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝

Tactic:
simp only [Function.comp_apply, fmap_def, map_coe, List.map_eq_map]

Result:
no goals

Proof state:
α β : Type u_1
h : α → β
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h

Tactic:
funext

Result:
case h
α β : Type u_1
h : α → β
x✝ : List α
⊢ (Functor.map h ∘ ofList) x✝ = (ofList ∘ Functor.map h) x✝
-- Mathlib/Data/Rat/Defs.lean
lemma mul_eq_mkRat (q r : ℚ) : q * r = mkRat (q.num * r.num) (q.den * r.den)

Proof state:
q r : ℚ
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
rw [mul_def, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem totalVariation_zero : (0 : SignedMeasure α).totalVariation = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ totalVariation 0 = 0

Tactic:
simp [totalVariation, toJordanDecomposition_zero]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_image (hf : LeftInvOn f' f s) : f' '' (f '' s) = s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' '' (f '' s) = s

Tactic:
rw [Set.image_image, image_congr hf, image_id']

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedFDerivWithin_eq_equiv_comp :
    iteratedFDerivWithin 𝕜 n f s =
      ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDerivWithin n f s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s

Tactic:
rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
  Function.id_comp]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem binomial_eq_choose [DecidableEq α] (h : a ≠ b) :
    multinomial {a, b} f = (f a + f b).choose (f a)

Proof state:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} f = (f a + f b).choose (f a)

Tactic:
simp [binomial_eq h, choose_eq_factorial_div_factorial (Nat.le_add_right _ _)]

Result:
no goals
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem extend_mul [Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
    Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
classical
funext x
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x

Tactic:
simp only [not_exists, extend_def, Pi.mul_apply, apply_dite₂, dite_eq_ite, ite_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
⊢ extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Mul γ
f : α → β
g₁ g₂ : α → γ
e₁ e₂ : β → γ
x : β
⊢ extend f (g₁ * g₂) (e₁ * e₂) x = (extend f g₁ e₁ * extend f g₂ e₂) x
-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_sub (x y : FreeRing α) : ↑(x - y) = (x : FreeCommRing α) - y

Proof state:
α : Type u
x y : FreeRing α
⊢ ↑(x - y) = ↑x - ↑y

Tactic:
rw [castFreeCommRing, map_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃)

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ (l₂ ++ l₃)

Tactic:
rw [← List.append_assoc]

Result:
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ l₂ ++ l₃

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ l₂ ++ l₃

Tactic:
apply infix_append

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem isLimit_iff_bijective_sectionOfCone (c : Cone F) :
    Nonempty (IsLimit c) ↔ (Types.sectionOfCone c).Bijective

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)

Tactic:
simp_rw [isLimit_iff, Function.bijective_iff_existsUnique, Subtype.forall, F.sections_ext_iff,
  sectionOfCone]

Result:
no goals
-- Mathlib/Topology/Homotopy/HSpaces.lean
theorem delayReflLeft_zero (γ : Path x y) : delayReflLeft 0 γ = (Path.refl x).trans γ

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 0 γ = (refl x).trans γ

Tactic:
simp only [delayReflLeft, delayReflRight_zero, trans_symm, refl_symm, Path.symm_symm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma dist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 < r) :
    dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ b, dist (f b) (g b) ≤ r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ
hr : 0 < r
⊢ dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr.le

Result:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Proof state:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < ↑r
⊢ dist f g = ↑r ↔ (∃ i, dist (f i) (g i) = ↑r) ∧ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Tactic:
simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_coe_Finset (s : Finset α) : (s : Set α).ncard = s.card

Proof state:
α : Type u_1
s : Finset α
⊢ (↑s).ncard = s.card

Tactic:
rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_add_lt_sub (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m + k) < n - m

Proof state:
m k n : Nat
h₁ : m + k ≤ n
h₂ : 0 < k
⊢ n - (m + k) < n - m

Tactic:
rw [← Nat.sub_sub]

Result:
m k n : Nat
h₁ : m + k ≤ n
h₂ : 0 < k
⊢ n - m - k < n - m

Proof state:
m k n : Nat
h₁ : m + k ≤ n
h₂ : 0 < k
⊢ n - m - k < n - m

Tactic:
exact Nat.sub_lt_of_pos_le h₂ (Nat.le_sub_of_add_le' h₁)

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
lemma mem_functorObj_iff {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X)
    {x : X} : f x ∈ hf.functorObj U ↔ x ∈ U

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ (Opens.map f).obj (hf.functorObj U)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ U

Tactic:
conv_rhs => rw [← hf.map_functorObj U]

Result:
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ (Opens.map f).obj (hf.functorObj U)
-- Mathlib/RingTheory/Flat/Basic.lean
theorem tensorProduct_mapIncl_injective_of_right
    [Flat R M] [Flat R q] : Function.Injective (mapIncl p q)

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R M
inst✝ : Flat R ↥q
⊢ Function.Injective ⇑(lTensor M q.subtype ∘ₗ rTensor (↥q) p.subtype)

Tactic:
exact (lTensor_preserves_injective_linearMap _ q.injective_subtype).comp
  (rTensor_preserves_injective_linearMap _ p.injective_subtype)

Result:
no goals

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R M
inst✝ : Flat R ↥q
⊢ Function.Injective ⇑(mapIncl p q)

Tactic:
rw [mapIncl, ← lTensor_comp_rTensor]

Result:
R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R M
inst✝ : Flat R ↥q
⊢ Function.Injective ⇑(lTensor M q.subtype ∘ₗ rTensor (↥q) p.subtype)