harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem biSup_adjoin_simple : ⨆ x ∈ S, F⟮x⟯ = adjoin F S

Proof state:
case e_S
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ ⨆ t ∈ S, {t} = S

Tactic:
exact S.biUnion_of_singleton

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ ⨆ x ∈ S, F⟮x⟯ = adjoin F S

Tactic:
rw [← iSup_subtype'', ← gc.l_iSup, iSup_subtype'']

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ adjoin F (⨆ t ∈ S, {t}) = adjoin F S

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ adjoin F (⨆ t ∈ S, {t}) = adjoin F S

Tactic:
congr

Result:
case e_S
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ ⨆ t ∈ S, {t} = S
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_pow_natAbs (a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖

Tactic:
rw [← zpow_natCast, ← Int.abs_eq_natAbs, norm_zpow_abs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem cons_lt_cons_self [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] {l₁ l₂ : List α} :
    (a :: l₁) < (a :: l₂) ↔ l₁ < l₂

Proof state:
α : Type u_1
a : α
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : List α
⊢ a :: l₁ < a :: l₂ ↔ l₁ < l₂

Tactic:
simp [cons_lt_cons_iff, i₀.irrefl]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Multiset.measurable_prod' (l : Multiset (α → M)) (hl : ∀ f ∈ l, Measurable f) :
    Measurable l.prod

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod

Tactic:
rcases l with ⟨l⟩

Result:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ Measurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l))

Proof state:
case mk
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ Measurable (prod (Quot.mk (⇑(List.isSetoid (α → M))) l))

Tactic:
simpa using l.measurable_prod' (by simpa using hl)

Result:
no goals

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
l✝ : Multiset (α → M)
l : List (α → M)
hl : ∀ f ∈ Quot.mk (⇑(List.isSetoid (α → M))) l, Measurable f
⊢ ∀ f ∈ l, Measurable f

Tactic:
simpa using hl

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_id : trace R M id = (finrank R M : R)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) id = ↑(finrank R M)

Tactic:
rw [← one_eq_id, trace_one]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem seminorm_le_bound' (k n : ℕ) (f : 𝓢(ℝ, F)) {M : ℝ} (hMp : 0 ≤ M)
    (hM : ∀ x, |x| ^ k * ‖iteratedDeriv n f x‖ ≤ M) : SchwartzMap.seminorm 𝕜 k n f ≤ M

Proof state:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M

Tactic:
simpa only [Real.norm_eq_abs, norm_iteratedFDeriv_eq_norm_iteratedDeriv]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ (SchwartzMap.seminorm 𝕜 k n) f ≤ M

Tactic:
refine seminorm_le_bound 𝕜 k n f hMp ?_

Result:
𝕜 : Type u_1
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M
-- Mathlib/Analysis/Analytic/Basic.lean
@[simp] lemma hasFPowerSeriesWithinOnBall_insert_self :
    HasFPowerSeriesWithinOnBall f p (insert x s) x r ↔ HasFPowerSeriesWithinOnBall f p s x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
⊢ x + y ∈ insert x (insert x s) → y ∈ EMetric.ball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
simpa only [insert_idem] using h.hasSum (y := y)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
⊢ HasFPowerSeriesWithinOnBall f p (insert x s) x r ↔ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩  <;>
exact ⟨h.r_le, h.r_pos, fun {y} ↦ by simpa only [insert_idem] using h.hasSum (y := y)⟩

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem tail_ofSeq (s : Seq α) : tail (ofSeq s) = ofSeq s.tail

Proof state:
α : Type u
s : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a => (a, ↑s.tail)) s.head) = ↑s.tail

Tactic:
induction' s using Seq.recOn with x s <;> simp only [ofSeq, Seq.tail_nil, Seq.head_nil,
  Option.map_none', Seq.tail_cons, Seq.head_cons, Option.map_some']

Result:
case nil
α : Type u
⊢ nil = some <$> Seq.nil

Proof state:
case nil
α : Type u
⊢ nil = some <$> Seq.nil

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s : Seq α
⊢ (↑s).tail = ↑s.tail

Tactic:
simp only [tail, destruct_ofSeq, map_pure', flatten_pure]

Result:
α : Type u
s : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a => (a, ↑s.tail)) s.head) = ↑s.tail
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem eigenspace_le_genEigenspace {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) :
    f.eigenspace μ ≤ f.genEigenspace μ k :=
  (f.genEigenspace _).monotone <| by simpa using Nat.succ_le_of_lt hk

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ 1 ≤ ↑k

Tactic:
simpa using Nat.succ_le_of_lt hk

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isShortNF : W.b₈ = -W.a₄ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.b₈ = -W.a₄ ^ 2

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem abs_rpow_le_abs_rpow (x y : ℝ) : |x ^ y| ≤ |x| ^ y

Proof state:
case inr
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)

Tactic:
exact mul_le_of_le_one_right (exp_pos _).le (abs_cos_le_one _)

Result:
no goals

Proof state:
x y : ℝ
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rcases le_or_lt 0 x with hx | hx

Result:
case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y

case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Proof state:
case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
  abs_of_pos (exp_pos _)]

Result:
case inr
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)

Proof state:
case inl
x y : ℝ
hx : 0 ≤ x
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_rpow_of_nonneg hx]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algEquivOfAssociated_toAlgHom {p q : K[X]} (hp : p ≠ 0) (hpq : Associated p q) :
    (algEquivOfAssociated hp hpq).toAlgHom =
      liftHom p (root q) (by simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]) :=
  rfl

Proof state:
K : Type ?u.379036
L : Type ?u.379039
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p q : K[X]
hp : p ≠ 0
hpq : Associated p q
⊢ (aeval (root q)) p = 0

Tactic:
simp only [aeval_eq, mk_eq_zero, hpq.symm.dvd]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_id {n : ℤ} (z₁ : Cochain F G n) :
    z₁.comp (Cochain.ofHom (𝟙 G)) (add_zero n) = z₁

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (z₁.comp (ofHom (𝟙 G)) ⋯).v p q hpq = z₁.v p q hpq

Tactic:
simp only [comp_zero_cochain_v, ofHom_v, HomologicalComplex.id_f, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
⊢ z₁.comp (ofHom (𝟙 G)) ⋯ = z₁

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ (z₁.comp (ofHom (𝟙 G)) ⋯).v p q hpq = z₁.v p q hpq
-- Mathlib/RingTheory/Generators.lean
lemma aeval_val_eq_zero {x} (hx : x ∈ P.ker) : aeval P.val x = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x : P.Ring
hx : x ∈ P.ker
⊢ (aeval P.val) x = 0

Tactic:
rwa [← algebraMap_apply]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem fromPadicInt_comp_toPadicInt :
    (fromPadicInt p).comp (toPadicInt p) = RingHom.id (𝕎 (ZMod p))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fromPadicInt p).comp (toPadicInt p) = RingHom.id (𝕎 (ZMod p))

Tactic:
apply WittVector.hom_ext

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (k : ℕ), (truncate k).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate k).comp (RingHom.id (𝕎 (ZMod p)))

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (zmodEquivTrunc p n).toRingHom.comp ((PadicInt.toZModPow n).comp (toPadicInt p)) =
    (truncate n).comp (RingHom.id (𝕎 (ZMod p)))

Tactic:
simp only [toPadicInt, toZModPow, RingHom.comp_id, PadicInt.lift_spec, RingHom.id_comp, ←
  RingHom.comp_assoc, RingEquiv.toRingHom_comp_symm_toRingHom]

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (k : ℕ), (truncate k).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate k).comp (RingHom.id (𝕎 (ZMod p)))

Tactic:
intro n

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (truncate n).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate n).comp (RingHom.id (𝕎 (ZMod p)))

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (truncate n).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate n).comp (RingHom.id (𝕎 (ZMod p)))

Tactic:
rw [fromPadicInt, ← RingHom.comp_assoc, truncate_comp_lift, RingHom.comp_assoc]

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (zmodEquivTrunc p n).toRingHom.comp ((PadicInt.toZModPow n).comp (toPadicInt p)) =
    (truncate n).comp (RingHom.id (𝕎 (ZMod p)))
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- In a space with an inner regular measure, any measurable set coincides almost everywhere with
its everywhere positive subset. -/
lemma everywherePosSubset_ae_eq [OpensMeasurableSpace α] [InnerRegular μ] (hs : MeasurableSet s) :
    μ.everywherePosSubset s =ᵐ[μ] s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
⊢ μ.everywherePosSubset s =ᶠ[ae μ] s

Tactic:
simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty,
  true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
⊢ ∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
⊢ ∀ i ⊆ s \ μ.everywherePosSubset s, IsCompact i → μ i = 0

Tactic:
intro k hk h'k

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Tactic:
exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} {h₁} :
    get (m.insert k v) a h₁ =
      if h₂ : k == a then v
      else get m a (contains_of_contains_insert _ h h₁ (Bool.eq_false_iff.2 h₂))

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β
h₁ : (m.insert k v).contains a = true
⊢ get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else get m a ⋯

Tactic:
simp_to_model [insert] using List.getValue_insertEntry

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem range_coe (h : X ≃ₜ Y) : range h = univ

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ range ⇑h = univ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem uset_toArray (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) :
    l.toArray.uset i a h = (l.set i.toNat a).toArray

Proof state:
α : Type u_1
l : List α
i : USize
a : α
h : i.toNat < l.toArray.size
⊢ l.toArray.uset i a h = (l.set i.toNat a).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem closedBall_sub_closedBall [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
    closedBall a ε - closedBall b δ = closedBall (a - b) (ε + δ)

Proof state:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)

Tactic:
rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem le_mul_left {a b : Cardinal} (h : b ≠ 0) : a ≤ b * a

Proof state:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
convert mul_le_mul_right' (one_le_iff_ne_zero.mpr h) a

Result:
case h.e'_3
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = 1 * a

Proof state:
case h.e'_3
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a = 1 * a

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
    {s : AffineSubspace ℝ P} [Nonempty s] [HasOrthogonalProjection s.direction] {p₁ : P} (p₂ : P)
    (hp₁ : p₁ ∈ s) :
    dist p₁ p₂ * dist p₁ p₂ =
      dist p₁ (orthogonalProjection s p₂) * dist p₁ (orthogonalProjection s p₂) +
        dist p₂ (orthogonalProjection s p₂) * dist p₂ (orthogonalProjection s p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ inner (p₁ -ᵥ ↑((orthogonalProjection s) p₂)) (↑((orthogonalProjection s) p₂) -ᵥ p₂) = 0

Tactic:
exact Submodule.inner_right_of_mem_orthogonal (vsub_orthogonalProjection_mem_direction p₂ hp₁)
  (orthogonalProjection_vsub_mem_direction_orthogonal s 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
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ ↑((orthogonalProjection s) p₂) * dist p₁ ↑((orthogonalProjection s) p₂) +
      dist p₂ ↑((orthogonalProjection s) p₂) * dist p₂ ↑((orthogonalProjection s) p₂)

Tactic:
rw [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₁ (orthogonalProjection s 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
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ inner (p₁ -ᵥ ↑((orthogonalProjection s) p₂)) (↑((orthogonalProjection s) p₂) -ᵥ p₂) = 0
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem SeminormedAddCommGroup.cauchySeq_of_le_geometric {C : ℝ} {r : ℝ} (hr : r < 1)
    {u : ℕ → α} (h : ∀ n, ‖u n - u (n + 1)‖ ≤ C * r ^ n) : CauchySeq u :=
  cauchySeq_of_le_geometric r C hr (by simpa [dist_eq_norm] using h)

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C r : ℝ
hr : r < 1
u : ℕ → α
h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n
⊢ ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ C * r ^ n

Tactic:
simpa [dist_eq_norm] using h

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem commute_subtype_of_commute
    (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y) (i j : ι)
    (hne : i ≠ j) :
    ∀ (x : H i) (y : H j), Commute ((H i).subtype x) ((H j).subtype y)

Proof state:
case mk.mk
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute ((H i).subtype ⟨x, hx⟩) ((H j).subtype ⟨y, hy⟩)

Tactic:
exact hcomm hne x y hx hy

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
⊢ ∀ (x : ↥(H i)) (y : ↥(H j)), Commute ((H i).subtype x) ((H j).subtype y)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩

Result:
case mk.mk
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute ((H i).subtype ⟨x, hx⟩) ((H j).subtype ⟨y, hy⟩)
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ fract (a - ↑m) = fract a

Tactic:
rw [fract]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem IsFundamentalDomain.measurePreserving_quotient_mk
    {𝓕 : Set α} (h𝓕 : IsFundamentalDomain G 𝓕 ν)
    (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ] :
    MeasurePreserving π (ν.restrict 𝓕) μ where
  measurable := measurable_quotient_mk' (s := α_mod_G)
  map_eq

Proof state:
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
this : HasFundamentalDomain G α ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ

Tactic:
rw [h𝓕.projection_respects_measure (μ := μ)]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ

Tactic:
haveI : HasFundamentalDomain G α ν := ⟨𝓕, h𝓕⟩

Result:
G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
ν : Measure α
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
this : HasFundamentalDomain G α ν
⊢ Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem exists_mem_normalizedFactors {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :
    ∃ p, p ∈ normalizedFactors x

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ normalizedFactors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ normalizedFactors x

Tactic:
exact ⟨p, hp⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ normalizedFactors x

Tactic:
obtain ⟨p, hp, _⟩ := exists_mem_normalizedFactors_of_dvd hx hp' hp'x

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
p : α
hp : p ∈ normalizedFactors x
right✝ : p' ~ᵤ p
⊢ ∃ p, p ∈ normalizedFactors x

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ p, p ∈ normalizedFactors x

Tactic:
obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx

Result:
case intro.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p' : α
hp' : Irreducible p'
hp'x : p' ∣ x
⊢ ∃ p, p ∈ normalizedFactors x
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
@[deprecated ENNReal.tsum_const (since := "2025-02-06")]
lemma _root_.ENNReal.tsum_const_eq (c : ℝ≥0∞) : ∑' _ : α, c = c * count (univ : Set α)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
c : ℝ≥0∞
⊢ ∑' (x : α), c = c * count univ

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_eq_top_iff_of_pos {x : ℝ≥0∞} {y : ℝ} (hy : 0 < y) : x ^ y = ⊤ ↔ x = ⊤

Proof state:
x : ℝ≥0∞
y : ℝ
hy : 0 < y
⊢ x ^ y = ⊤ ↔ x = ⊤

Tactic:
simp [rpow_eq_top_iff, hy, asymm hy]

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem one_lt_card_iff_nontrivial [Finite α] : 1 < Nat.card α ↔ Nontrivial α

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α