harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq {n : ℕ}
    (s : Simplex ℝ P n) {p₁ : P} (p₂ : P) (hp₁ : p₁ ∈ affineSpan ℝ (Set.range s.points)) :
    dist p₁ p₂ * dist p₁ p₂ =
      dist p₁ (s.orthogonalProjectionSpan p₂) * dist p₁ (s.orthogonalProjectionSpan p₂) +
        dist p₂ (s.orthogonalProjectionSpan p₂) * dist p₂ (s.orthogonalProjectionSpan p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p₁ p₂ : P
hp₁ : p₁ ∈ affineSpan ℝ (Set.range s.points)
⊢ inner (p₁ -ᵥ ↑(s.orthogonalProjectionSpan p₂)) (↑(s.orthogonalProjectionSpan p₂) -ᵥ p₂) = 0

Tactic:
exact
  Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
    (orthogonalProjection_vsub_mem_direction_orthogonal _ p₂)

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p₁ p₂ : P
hp₁ : p₁ ∈ affineSpan ℝ (Set.range s.points)
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ ↑(s.orthogonalProjectionSpan p₂) * dist p₁ ↑(s.orthogonalProjectionSpan p₂) +
      dist p₂ ↑(s.orthogonalProjectionSpan p₂) * dist p₂ ↑(s.orthogonalProjectionSpan p₂)

Tactic:
rw [PseudoMetricSpace.dist_comm p₂ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V p₁ _,
  dist_eq_norm_vsub V _ p₂, ← vsub_add_vsub_cancel p₁ (s.orthogonalProjectionSpan p₂) p₂,
  norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p₁ p₂ : P
hp₁ : p₁ ∈ affineSpan ℝ (Set.range s.points)
⊢ inner (p₁ -ᵥ ↑(s.orthogonalProjectionSpan p₂)) (↑(s.orthogonalProjectionSpan p₂) -ᵥ p₂) = 0
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_of_injective_of_subset_range (f : α → β) (s : Set β) (h : Injective f)
    (h2 : s ⊆ range f) : #(f ⁻¹' s) = #s

Proof state:
α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑s

Tactic:
convert mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1 <;> rw [lift_id]

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toMultiset_le_toMultiset : toMultiset f ≤ toMultiset g ↔ f ≤ g

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f ≤ toMultiset g ↔ f ≤ g

Tactic:
simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_map (p : β → Bool) (f : α → β) (l : Array α) :
    countP p (map f l) = countP (p ∘ f) l

Proof state:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
toList✝ : List α
⊢ countP p (map f { toList := toList✝ }) = countP (p ∘ f) { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
l : Array α
⊢ countP p (map f l) = countP (p ∘ f) l

Tactic:
cases l

Result:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
toList✝ : List α
⊢ countP p (map f { toList := toList✝ }) = countP (p ∘ f) { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_negOfNat (n : Nat) : natAbs (negOfNat n) = n

Proof state:
n : Nat
⊢ (negOfNat n).natAbs = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_empty [LawfulBEq α] {a : α} [Inhabited (β a)] {c} :
    (empty c : Raw₀ α β).get! a = default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
c : Nat
⊢ (empty c).get! a = default

Tactic:
simp [get!, empty]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_add_cancel_left {a : EReal} {b : Real} : b - (b + a) = -a

Proof state:
a : EReal
b : ℝ
⊢ ↑b - (↑b + a) = -a

Tactic:
rw [add_comm, sub_add_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem units_smul_eq_neg_iff {u : Rˣ} {v : Module.Ray R M} : u • v = -v ↔ u.1 < 0

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
u : Rˣ
v : Module.Ray R M
⊢ u • v = -v ↔ ↑u < 0

Tactic:
rw [← neg_inj, neg_neg, ← Module.Ray.neg_units_smul, units_smul_eq_self_iff, Units.val_neg,
  neg_pos]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Indization/ParallelPair.lean
theorem hg : g = IsColimit.map (isColimit₁ f g P₁ P₂)
    (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ψ f g P₁ P₂) yoneda)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ g =
    { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ g =
    { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)

Tactic:
rw [IsColimit.ι_map]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ g =
    (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ g =
    (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
simpa using i.hom.2.w.symm

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquiv_mk' (x : R) (y : M) : algEquiv M S Q (mk' S x y) = mk' Q x y

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
x : R
y : ↥M
⊢ (algEquiv M S Q) (mk' S x y) = mk' Q x y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_disjUnion (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) {π₁ π₂ : TaggedPrepartition I}
    (h : Disjoint π₁.iUnion π₂.iUnion) :
    integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂

Proof state:
case refine_1
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₁.boxes
⊢ (vol J) (f ((π₁.disjUnion π₂ h).tag J)) = (vol J) (f (π₁.tag J))

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Result:
no goals

Proof state:
case refine_2
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ : J ∈ π₂.boxes
⊢ (vol J) (f ((π₁.disjUnion π₂ h).tag J)) = (vol J) (f (π₂.tag J))

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_one_right (hx : x ≠ 0) : angle x 1 = |x.arg|

Proof state:
x : ℂ
hx : x ≠ 0
⊢ angle x 1 = |x.arg|

Tactic:
simp [angle_eq_abs_arg, hx]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_triple_of_mem_affineSpan_pair {p₁ p₂ p₃ p₄ p₅ : P} (h₁ : p₁ ∈ line[k, p₄, p₅])
    (h₂ : p₂ ∈ line[k, p₄, p₅]) (h₃ : p₃ ∈ line[k, p₄, p₅]) :
    Collinear k ({p₁, p₂, p₃} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ Collinear k {p₁, p₂, p₃}

Tactic:
refine (collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃} ⊆ {p₁, p₂, p₃, p₄}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ p₅ : P
h₁ : p₁ ∈ affineSpan k {p₄, p₅}
h₂ : p₂ ∈ affineSpan k {p₄, p₅}
h₃ : p₃ ∈ affineSpan k {p₄, p₅}
⊢ {p₁, p₂, p₃} ⊆ {p₁, p₂, p₃, p₄}

Tactic:
simp [Set.insert_subset_insert]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem terminatedAt_ofList (l : List α) :
    (ofList l).TerminatedAt l.length

Proof state:
α : Type u
l : List α
⊢ (↑l).TerminatedAt l.length

Tactic:
simp [ofList, TerminatedAt]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma inv_add_inv_conj_ennreal : (p⁻¹ + q⁻¹ : ℝ≥0∞) = 1

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
exact h.inv_add_inv_conj

Result:
no goals

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ ↑p⁻¹ + ↑q⁻¹ = 1

Tactic:
norm_cast

Result:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ p⁻¹ + q⁻¹ = 1
-- Mathlib/Algebra/Group/Commute/Basic.lean
@[to_additive]
protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * b * a = b

Tactic:
rw [h.inv_left.eq, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.eq_of_length : l₁ <+ l₂ → length l₁ = length l₂ → l₁ = l₂
  | .slnil, _ => rfl
  | .cons a s, h => nomatch Nat.not_lt.2 s.length_le (h ▸ lt_succ_self _)
  | .cons₂ a s, h => by rw [s.eq_of_length (succ.inj h)]

Proof state:
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : (a :: l₁✝).length = (a :: l₂✝).length
⊢ a :: l₁✝ = a :: l₂✝

Tactic:
rw [s.eq_of_length (succ.inj h)]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_right_Ico (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) '' Ico a b = Ico (a * c) (b * c) :=
  ((Units.mk0 c h.ne').mulRight.image_eq_preimage _).trans (by simp [h, division_def])

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ ⇑(Equiv.symm (Units.mk0 c ⋯).mulRight) ⁻¹' Ico a b = Ico (a * c) (b * c)

Tactic:
simp [h, division_def]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem diff_subset_closure_iff : s \ t ⊆ closure t ↔ s ⊆ closure t

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t

Tactic:
rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_self {a : Int} (H : a ≠ 0) : a / a = 1

Proof state:
a : Int
H : a ≠ 0
⊢ a / a = 1

Tactic:
have := Int.mul_ediv_cancel 1 H

Result:
a : Int
H : a ≠ 0
this : 1 * a / a = 1
⊢ a / a = 1

Proof state:
a : Int
H : a ≠ 0
this : 1 * a / a = 1
⊢ a / a = 1

Tactic:
rwa [Int.one_mul] at this

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_mono : Monotone (comap f) := fun J₁ J₂ h ↦ by
  rw [← SetLike.coe_subset_coe] at h ⊢
  dsimp only [SetLike.coe]
  exact Set.preimage_mono h

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ (↑(comap f J₁)).carrier ⊆ (↑(comap f J₂)).carrier

Tactic:
exact Set.preimage_mono h

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ ↑(comap f J₁) ⊆ ↑(comap f J₂)

Tactic:
dsimp only [SetLike.coe]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ (↑(comap f J₁)).carrier ⊆ (↑(comap f J₂)).carrier

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : J₁ ≤ J₂
⊢ comap f J₁ ≤ comap f J₂

Tactic:
rw [← SetLike.coe_subset_coe] at h ⊢

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ ↑(comap f J₁) ⊆ ↑(comap f J₂)
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_one_eq_diagonal [DecidableEq m] (a : α) :
    a • (1 : Matrix m m α) = diagonal fun _ => a

Proof state:
m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ a • 1 = diagonal fun x => a

Tactic:
simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem UpperSemicontinuousAt.comp_continuousAt_of_eq {f : α → β} {g : ι → α} {y : α} {x : ι}
    (hf : UpperSemicontinuousAt f y) (hg : ContinuousAt g x) (hy : g x = y) :
    UpperSemicontinuousAt (fun x ↦ f (g x)) x

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : UpperSemicontinuousAt f y
hg : ContinuousAt g x
hy : g x = y
⊢ UpperSemicontinuousAt (fun x => f (g x)) x

Tactic:
rw [← hy] at hf

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : UpperSemicontinuousAt f (g x)
hg : ContinuousAt g x
hy : g x = y
⊢ UpperSemicontinuousAt (fun x => f (g x)) x

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
ι : Type u_5
inst✝ : TopologicalSpace ι
f : α → β
g : ι → α
y : α
x : ι
hf : UpperSemicontinuousAt f (g x)
hg : ContinuousAt g x
hy : g x = y
⊢ UpperSemicontinuousAt (fun x => f (g x)) x

Tactic:
exact comp_continuousAt hf hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.Const.getThenInsertIfNew? {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)}
    {a : α} {b : β} (h : m.WF) : (Const.getThenInsertIfNew? m a b).2.WF

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
a : α
b : β
h : m.WF
⊢ (Raw.Const.getThenInsertIfNew? m a b).snd.WF

Tactic:
simpa [Raw.Const.getThenInsertIfNew?, h.size_buckets_pos] using .constGetThenInsertIfNew?₀ h

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem TopologicalSpace.IsTopologicalBasis.inseparable_iff {b : Set (Set X)}
    (hb : IsTopologicalBasis b) {x y : X} : Inseparable x y ↔ ∀ s ∈ b, (x ∈ s ↔ y ∈ s) :=
  ⟨fun h _ hs ↦ inseparable_iff_forall_isOpen.1 h _ (hb.isOpen hs),
    fun h ↦ hb.nhds_hasBasis.eq_of_same_basis <| by
      convert hb.nhds_hasBasis using 2
      exact and_congr_right (h _)⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
⊢ (𝓝 y).HasBasis (fun t => t ∈ b ∧ x ∈ t) fun t => t

Tactic:
convert hb.nhds_hasBasis using 2

Result:
case h.e'_4.h.a
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
x✝ : Set X
⊢ x✝ ∈ b ∧ x ∈ x✝ ↔ x✝ ∈ b ∧ y ∈ x✝

Proof state:
case h.e'_4.h.a
X : Type u_1
inst✝ : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
x✝ : Set X
⊢ x✝ ∈ b ∧ x ∈ x✝ ↔ x✝ ∈ b ∧ y ∈ x✝

Tactic:
exact and_congr_right (h _)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem alternatingProd_cons (a : α) (l : List α) :
    alternatingProd (a :: l) = a / alternatingProd l

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
l : List α
⊢ (a :: l).alternatingProd = a / l.alternatingProd

Tactic:
rw [div_eq_mul_inv, alternatingProd_cons']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
  | [] => ⟨nil, by rw [dropLast, List.append_nil]⟩
  | a :: l => ⟨_, dropLast_concat_getLast (cons_ne_nil a l)⟩

Proof state:
α : Type u_1
⊢ [].dropLast ++ [] = []

Tactic:
rw [dropLast, List.append_nil]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem I_sq : I ^ 2 = -1

Proof state:
⊢ I ^ 2 = -1

Tactic:
rw [sq, I_mul_I]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_coe_coe (a b : ℝ) :
    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, b)

Proof state:
a b : ℝ
⊢ ContinuousAt (fun p => p.1 + p.2) (↑a, ↑b)

Tactic:
simp only [ContinuousAt, nhds_coe_coe, ← coe_add, tendsto_map'_iff, Function.comp_def,
  tendsto_coe, tendsto_add]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma top_mul_of_neg {x : EReal} (h : x < 0) : ⊤ * x = ⊥

Proof state:
x : EReal
h : x < 0
⊢ x * ⊤ = ⊥

Tactic:
exact mul_top_of_neg h

Result:
no goals

Proof state:
x : EReal
h : x < 0
⊢ ⊤ * x = ⊥

Tactic:
rw [EReal.mul_comm]

Result:
x : EReal
h : x < 0
⊢ x * ⊤ = ⊥
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem coe_inv_of_nonzero {J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) :
    (↑J⁻¹ : Submodule R₁ K) = IsLocalization.coeSubmodule K ⊤ / (J : Submodule R₁ K)

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
J : FractionalIdeal R₁⁰ K
h : J ≠ 0
⊢ ↑J⁻¹ = IsLocalization.coeSubmodule K ⊤ / ↑J

Tactic:
simp_rw [inv_nonzero _ h, coe_one, coe_mk, IsLocalization.coeSubmodule_top]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Multiset.aemeasurable_prod (s : Multiset (α → M)) (hs : ∀ f ∈ s, AEMeasurable f μ) :
    AEMeasurable (fun x => (s.map fun f : α → M => f x).prod) μ

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
s : Multiset (α → M)
hs : ∀ f ∈ s, AEMeasurable f μ
⊢ AEMeasurable (fun x => (map (fun f => f x) s).prod) μ

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.aemeasurable_prod' hs

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_mul (x y : R) (p q : R[X][Y]) :
    (p * q).evalEval x y = p.evalEval x y * q.evalEval x y

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p * q) = evalEval x y p * evalEval x y q

Tactic:
simp only [evalEval, eval_mul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_swap {x y : α} (hxy : x ≠ y) : #(swap x y).support = 2 :=
  show #(swap x y).support = #⟨x ::ₘ y ::ₘ 0, by simp [hxy]⟩ from
    congr_arg card <| by simp [support_swap hxy, *, Finset.ext_iff]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (swap x y).support = { val := x ::ₘ y ::ₘ 0, nodup := ⋯ }

Tactic:
simp [support_swap hxy, *, Finset.ext_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (x ::ₘ y ::ₘ 0).Nodup

Tactic:
simp [hxy]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem is3Clique_triple_iff : G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Proof state:
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ (((↑{c}).Pairwise G.Adj ∧ ∀ b_1 ∈ ↑{c}, b ≠ b_1 → G.Adj b b_1) ∧ ∀ b_1 ∈ insert b ↑{c}, a ≠ b_1 → G.Adj a b_1) ∧
      #{a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
by_cases hab : a = b <;> by_cases hbc : b = c <;> by_cases hac : a = c <;> subst_vars <;>
  simp [G.ne_of_adj, and_rotate, *]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

Tactic:
simp only [isNClique_iff, isClique_iff, Set.pairwise_insert_of_symmetric G.symm, coe_insert]

Result:
α : Type u_1
G : SimpleGraph α
a b c : α
inst✝ : DecidableEq α
⊢ (((↑{c}).Pairwise G.Adj ∧ ∀ b_1 ∈ ↑{c}, b ≠ b_1 → G.Adj b b_1) ∧ ∀ b_1 ∈ insert b ↑{c}, a ≠ b_1 → G.Adj a b_1) ∧
      #{a, b, c} = 3 ↔
    G.Adj a b ∧ G.Adj a c ∧ G.Adj b c
-- Mathlib/Analysis/Calculus/FDeriv/Linear.lean
theorem ContinuousLinearMap.hasFDerivAtFilter : HasFDerivAtFilter e e x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by
    simp only [e.map_sub, sub_self, Pi.zero_apply]

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E →L[𝕜] F
x✝ : E
L : Filter E
x : E
⊢ 0 x = e x - e x✝ - e (x - x✝)

Tactic:
simp only [e.map_sub, sub_self, Pi.zero_apply]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₅_app_two :
    (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨2, by valid⟩ = app₂ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.360109, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯
⊢ 2 < 5 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem apply_le_one (μ : ProbabilityMeasure Ω) (s : Set Ω) : μ s ≤ 1

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
⊢ μ s ≤ 1

Tactic:
simpa using apply_mono μ (subset_univ s)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_zero_left (d : ℕ) : hilbertPoly (0 : F[X]) d = 0

Proof state:
case zero
F : Type u_1
inst✝ : Field F
⊢ (match 0 with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0

Tactic:
simp only

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
d : ℕ
⊢ (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0

Tactic:
induction d with
| zero => simp only
| succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

Result:
no goals

Proof state:
case succ
F : Type u_1
inst✝ : Field F
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0
⊢ (match d + 1 with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0

Tactic:
simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
d : ℕ
⊢ hilbertPoly 0 d = 0

Tactic:
delta hilbertPoly

Result:
F : Type u_1
inst✝ : Field F
d : ℕ
⊢ (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ support 0, coeff 0 i • preHilbertPoly F d i) =
    0
-- Mathlib/Data/List/Map2.lean
theorem map₂Right_eq_map₂Right' : map₂Right f as bs = (map₂Right' f as bs).fst

Proof state:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
⊢ map₂Right f as bs = (map₂Right' f as bs).fst

Tactic:
simp only [map₂Right, map₂Right', map₂Left_eq_map₂Left']

Result:
no goals