harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is a prime if
`p ≠ 2`. -/
lemma prime_norm_toInteger_sub_one_of_prime_ne_two' [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑p) (hodd : p ≠ 2) :
    Prime (Algebra.norm ℤ (hζ.toInteger - 1))

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa using hcycl

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ Prime ((Algebra.norm ℤ) (hζ✝.toInteger - 1))

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ Prime ((Algebra.norm ℤ) (hζ✝.toInteger - 1))

Tactic:
exact hζ.prime_norm_toInteger_sub_one_of_prime_ne_two hodd

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_eLpNorm_one_densityProcess_limitProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    Tendsto (fun n ↦ eLpNorm ((fun x ↦ densityProcess κ ν n a x s)
      - (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a))
      1 (ν a)) atTop (𝓝 0)

Proof state:
case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ eLpNorm ({x | 2 ≤ ‖κ.densityProcess ν n a x s‖₊}.indicator fun x => κ.densityProcess ν n a x s) 1 (ν a) = 0

Tactic:
suffices {x | 2 ≤ ‖densityProcess κ ν n a x s‖₊} = ∅ by simp [this]

Result:
case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ {x | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} = ∅

Proof state:
case refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ C,
        ∀ (i : ℕ),
          eLpNorm ({x | C ≤ ‖κ.densityProcess ν i a x s‖₊}.indicator fun x => κ.densityProcess ν i a x s) 1 (ν a) ≤
            ENNReal.ofReal ε

Tactic:
refine fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩

Result:
case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ eLpNorm ({x | 2 ≤ ‖κ.densityProcess ν n a x s‖₊}.indicator fun x => κ.densityProcess ν n a x s) 1 (ν a) = 0

case refine_2.refine_2.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
⊢ 0 ≤ ENNReal.ofReal ε

Proof state:
case refine_2.refine_2.refine_1.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
x : γ
⊢ ⟨κ.densityProcess ν n a x s, ⋯⟩ ≤ 1

Tactic:
exact mod_cast (densityProcess_le_one hκν _ _ _ _)

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_one : seminormFromConst' hf1 hc hpm 1 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ seminormFromConst_seq c f 1 =ᶠ[atTop] fun x => 1

Tactic:
simp only [EventuallyEq, eventually_atTop, ge_iff_le]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f 1 b = 1

Tactic:
exact ⟨1, seminormFromConst_seq_one hc hpm⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ seminormFromConst' hf1 hc hpm 1 = 1

Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (seminormFromConst_isLimit hf1 hc hpm 1)
  tendsto_const_nhds

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ seminormFromConst_seq c f 1 =ᶠ[atTop] fun x => 1
-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem nodup_antidiagonalTuple (k n : ℕ) : List.Nodup (antidiagonalTuple k n)

Proof state:
case succ.right.succ.refine_2.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : Fin.cons (b.1 + 1) x₂ = Fin.cons (a.1 + 1) x₁
⊢ False

Tactic:
rw [Fin.cons_inj, Nat.succ_inj'] at h₁₂

Result:
case succ.right.succ.refine_2.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False

Proof state:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ ∀ x ∈ antidiagonal n, (map (fun x_1 => Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup

Tactic:
intro i _

Result:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ (map (fun x => Fin.cons i.1 x) (antidiagonalTuple k i.2)).Nodup
-- Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
theorem isSheaf_iff_isSheafPreservesLimitPairwiseIntersections :
    F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPreservesLimitPairwiseIntersections → F.IsSheafPairwiseIntersections

Tactic:
intro h ι U

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPairwiseIntersections ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPairwiseIntersections → F.IsSheafPreservesLimitPairwiseIntersections

case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPreservesLimitPairwiseIntersections → F.IsSheafPairwiseIntersections

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
rw [isSheaf_iff_isSheafPairwiseIntersections]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPairwiseIntersections ↔ F.IsSheafPreservesLimitPairwiseIntersections

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheafPairwiseIntersections → F.IsSheafPreservesLimitPairwiseIntersections

Tactic:
intro h ι U

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ PreservesLimit (Pairwise.diagram U).op F

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ PreservesLimit (Pairwise.diagram U).op F

Tactic:
exact preservesLimit_of_preserves_limit_cone (Pairwise.coconeIsColimit U).op (h U).some

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Pairwise.diagram U).op F
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))

Tactic:
exact ⟨isLimitOfPreserves _ (Pairwise.coconeIsColimit U).op⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))

Tactic:
haveI := h U

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
h : F.IsSheafPreservesLimitPairwiseIntersections
ι : Type w
U : ι → Opens ↑X
this : PreservesLimit (Pairwise.diagram U).op F
⊢ Nonempty (IsLimit (Functor.mapCone F (Pairwise.cocone U).op))
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt (f : C(E, ℝ))
    {K : Set E} (hK : MeasurableSet K) (hε : 0 < ε) (hKP : P Kᶜ < ε.toNNReal) :
    |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| < sqrt ε

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ (P Kᶜ).toReal < ε

Tactic:
exact toReal_lt_of_lt_ofReal hKP

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ (P Kᶜ).toReal * (√ε)⁻¹ < √ε

Tactic:
rw [mul_inv_lt_iff₀ (sqrt_pos_of_pos hε), mul_self_sqrt (le_of_lt hε)]

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ (P Kᶜ).toReal < ε

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε

Tactic:
apply lt_of_le_of_lt (norm_integral_sub_setIntegral_le
  (Eventually.of_forall (fun _ => abs_mulExpNegMulSq_le hε)) hK
  (integrable_mulExpNegMulSq_comp f hε))

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ (P Kᶜ).toReal * (√ε)⁻¹ < √ε
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem isCokernelEpiComp_desc {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g]
    {h : W ⟶ Y} (hh : h = g ≫ f) (s : CokernelCofork h) :
    (isCokernelEpiComp i g hh).desc s =
      i.desc
        (Cofork.ofπ s.π
          (by
            rw [← cancel_epi g, ← Category.assoc, ← hh]
            simp)) :=
  rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
rw [← cancel_epi g, ← Category.assoc, ← hh]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_coe_mem_lie (x : I) (m : N) : ⁅(x : L), (m : M)⁆ ∈ ⁅I, N⁆

Proof state:
case a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
use x, m

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ ⁅I, N⁆

Tactic:
rw [lieIdeal_oper_eq_span]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ lieSpan R L {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}

Tactic:
apply subset_lieSpan

Result:
case a
R : Type u
L : Type v
M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ ⁅↑x, ↑m⁆ ∈ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
-- Mathlib/Analysis/Convolution.lean
theorem contDiffOn_convolution_left_with_param [μ.IsAddLeftInvariant] [μ.IsNegInvariant]
    (L : E' →L[𝕜] E →L[𝕜] F) {f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {k : Set G}
    (hs : IsOpen s) (hk : IsCompact k) (hgs : ∀ p, ∀ x, p ∈ s → x ∉ k → g p x = 0)
    (hf : LocallyIntegrable f μ) (hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)) :
    ContDiffOn 𝕜 n (fun q : P × G => (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : NormedSpace 𝕜 E'
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup P
inst✝² : NormedSpace 𝕜 P
μ : Measure G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
f : G → E
n : ℕ∞
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
⊢ ContDiffOn 𝕜 (↑n) (fun q => (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ)

Tactic:
simpa only [convolution_flip] using contDiffOn_convolution_right_with_param L.flip hs hk hgs hf hg

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_self_center (z : ℍ) (r : ℝ) :
    dist (z : ℂ) (z.center r) = z.im * (Real.cosh r - 1)

Proof state:
z : ℍ
r : ℝ
⊢ |(↑(z.center r)).im - (↑z).im| = z.im * Real.cosh r - z.im

Tactic:
exact abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))

Result:
no goals

Proof state:
z : ℍ
r : ℝ
⊢ dist ↑z ↑(z.center r) = z.im * (Real.cosh r - 1)

Tactic:
rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]

Result:
z : ℍ
r : ℝ
⊢ |(↑(z.center r)).im - (↑z).im| = z.im * Real.cosh r - z.im
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y

Proof state:
w : Nat
x y : BitVec w
⊢ -x * y = x * -y

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem eventually_filterAt_measurableSet (x : X) : ∀ᶠ t in v.filterAt x, MeasurableSet t

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t

Tactic:
filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation_map_complex (f : E ≃ₗᵢ[ℝ] ℂ)
    (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x : E) :
    f (J x) = I * f x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : E
⊢ f (o.rightAngleRotation x) = I * f x

Tactic:
rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map (hF := _),
  LinearIsometryEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
lemma exists_eq_one {x : V} (hx : x ≠ 0) :
    ∃ f : V →L[R] R, f x = 1

Proof state:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
hx : x ≠ 0
f : V →L[R] R
hf : f x ≠ 0
⊢ ∃ f, f x = 1

Tactic:
exact ⟨(f x)⁻¹ • f, inv_mul_cancel₀ hf⟩

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
hx : x ≠ 0
⊢ ∃ f, f x = 1

Tactic:
rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩

Result:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x : V
hx : x ≠ 0
f : V →L[R] R
hf : f x ≠ 0
⊢ ∃ f, f x = 1
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
lemma extendScalarsComp_hom_app_one_tmul (M : ModuleCat R₁) (m : M) :
    (extendScalarsComp f₁₂ f₂₃).hom.app M ((1 : R₃) ⊗ₜ m) =
      (1 : R₃) ⊗ₜ[R₂,f₂₃] ((1 : R₂) ⊗ₜ[R₁,f₁₂] m)

Proof state:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m

Tactic:
rw [← extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp]

Result:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        ((extendRestrictScalarsAdj f₁₂).unit.app M ≫
          (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
            (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))))
      m =
    1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m

Proof state:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        ((extendRestrictScalarsAdj f₁₂).unit.app M ≫
          (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
            (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))))
      m =
    1 ⊗ₜ[R₂] 1 ⊗ₜ[R₁] m

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Ioi (hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) :
    (Ioi a).map (Embedding.subtype p) = (Ioi a : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ioi a) = Ioi ↑a

Tactic:
rw [subtype_Ioi_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi ↑a)) = Ioi ↑a

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi ↑a)) = Ioi ↑a

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop

Result:
no goals