harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary strict **rearrangement inequality**. -/
lemma mul_add_mul_lt_mul_add_mul [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddLeftStrictMono α]
    (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d

Proof state:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
b : α
hab : a < a + b
d : α
hd : 0 < d
hcd : c < c + d
⊢ a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)

Tactic:
rw [mul_add, add_right_comm, mul_add, ← add_assoc]

Result:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
b : α
hab : a < a + b
d : α
hd : 0 < d
hcd : c < c + d
⊢ a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d

Proof state:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
b : α
hab : a < a + b
d : α
hd : 0 < d
hcd : c < c + d
⊢ a * c + (a + b) * c + a * d < a * c + (a + b) * c + (a + b) * d

Tactic:
exact add_lt_add_left (mul_lt_mul_of_pos_right hab hd) _

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hcd : c < d
b : α
hab : a < a + b
⊢ a * d + (a + b) * c < a * c + (a + b) * d

Tactic:
obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd

Result:
case intro.intro.intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
b : α
hab : a < a + b
d : α
hd : 0 < d
hcd : c < c + d
⊢ a * (c + d) + (a + b) * c < a * c + (a + b) * (c + d)

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hab : a < b
hcd : c < d
⊢ a * d + b * c < a * c + b * d

Tactic:
obtain ⟨b, rfl⟩ := exists_add_of_le hab.le

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a c d : α
inst✝³ : AddLeftReflectLT α
inst✝² : ExistsAddOfLE α
inst✝¹ : MulPosStrictMono α
inst✝ : AddLeftStrictMono α
hcd : c < d
b : α
hab : a < a + b
⊢ a * d + (a + b) * c < a * c + (a + b) * d
-- Mathlib/Logic/Basic.lean
theorem xor_not_right : Xor' a (¬b) ↔ (a ↔ b)

Proof state:
a b : Prop
⊢ Xor' a ¬b ↔ (a ↔ b)

Tactic:
by_cases a <;> simp [*]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma density_nonneg (hκν : fst κ ≤ ν) (a : α) (x : γ) (s : Set β) :
    0 ≤ density κ ν a x s

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∃ᶠ (x_1 : ℕ) in atTop, 0 ≤ κ.densityProcess ν x_1 a x s

Tactic:
exact Frequently.of_forall (fun n ↦ densityProcess_nonneg _ _ _ _ _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.density ν a x s

Tactic:
refine le_limsup_of_frequently_le ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ ∃ᶠ (x_1 : ℕ) in atTop, 0 ≤ κ.densityProcess ν x_1 a x s

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun n => κ.densityProcess ν n a x s

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_pow {a : ℝ≥0∞} : expGrowthSup (fun n ↦ a ^ n) = log a

Proof state:
a : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
⊢ (a ^ n).log / ↑n = a.log

Tactic:
rw [EReal.div_eq_iff (natCast_ne_bot n) (natCast_ne_top n)
  (zero_lt_one.trans_le (Nat.one_le_cast.2 n_1)).ne.symm, log_pow, mul_comm]

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ (expGrowthSup fun n => a ^ n) = a.log

Tactic:
rw [expGrowthSup, ← limsup_const (f := atTop (α := ℕ)) (log a)]

Result:
a : ℝ≥0∞
⊢ limsup (fun n => (a ^ n).log / ↑n) atTop = limsup (fun x => a.log) atTop

Proof state:
a : ℝ≥0∞
⊢ limsup (fun n => (a ^ n).log / ↑n) atTop = limsup (fun x => a.log) atTop

Tactic:
refine limsup_congr (eventually_atTop.2 ⟨1, fun n n_1 ↦ ?_⟩)

Result:
a : ℝ≥0∞
n : ℕ
n_1 : n ≥ 1
⊢ (a ^ n).log / ↑n = a.log
-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
lemma Complex.norm_eq_one_of_mem_rootsOfUnity {ζ : ℂˣ} {n : ℕ} [NeZero n]
    (hζ : ζ ∈ rootsOfUnity n ℂ) :
    ‖(ζ : ℂ)‖ = 1

Proof state:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑ζ ^ n = 1

Tactic:
norm_cast

Result:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑(ζ ^ n) = 1

Proof state:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ^ n = 1
⊢ ↑(ζ ^ n) = 1

Tactic:
rw [hζ, Units.val_one]

Result:
no goals

Proof state:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ‖↑ζ‖ = 1

Tactic:
refine norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n

Result:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑ζ ^ n = 1

Proof state:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ↑(ζ ^ n) = 1

Tactic:
rw [_root_.mem_rootsOfUnity] at hζ

Result:
ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ^ n = 1
⊢ ↑(ζ ^ n) = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a

Proof state:
case intro
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a x : α✝
h✝ : ∀ (y : α✝), r y x → Acc r y
H : ∀ (y : α✝), r y x → Acc (TransGen r) y
⊢ Acc (TransGen r) x

Tactic:
refine Acc.intro x fun y hy ↦ ?_

Result:
case intro
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a x : α✝
h✝ : ∀ (y : α✝), r y x → Acc r y
H : ∀ (y : α✝), r y x → Acc (TransGen r) y
y : α✝
hy : TransGen r y x
⊢ Acc (TransGen r) y

Proof state:
case intro.single
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a x : α✝
h✝ : ∀ (y : α✝), r y x → Acc r y
H : ∀ (y : α✝), r y x → Acc (TransGen r) y
y : α✝
hyx : r y x
⊢ Acc (TransGen r) y

Tactic:
exact H y hyx

Result:
no goals

Proof state:
case intro.tail
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a x : α✝
h✝ : ∀ (y : α✝), r y x → Acc r y
H : ∀ (y : α✝), r y x → Acc (TransGen r) y
y b✝ : α✝
hyz : TransGen r y b✝
hzx : r b✝ x
⊢ Acc (TransGen r) y

Tactic:
exact (H _ hzx).inv hyz

Result:
no goals

Proof state:
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a : α✝
h : Acc r a
⊢ Acc (TransGen r) a

Tactic:
induction h with
| intro x _ H =>
  refine Acc.intro x fun y hy ↦ ?_
  cases hy with
  | single hyx =>
    exact H y hyx
  | tail hyz hzx =>
    exact (H _ hzx).inv hyz

Result:
no goals

Proof state:
case intro
α✝ : Sort u_1
r : α✝ → α✝ → Prop
a x : α✝
h✝ : ∀ (y : α✝), r y x → Acc r y
H : ∀ (y : α✝), r y x → Acc (TransGen r) y
y : α✝
hy : TransGen r y x
⊢ Acc (TransGen r) y

Tactic:
cases hy with
| single hyx =>
  exact H y hyx
| tail hyz hzx =>
  exact (H _ hzx).inv hyz

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
/-- If `forget C` preserves initials and `X` is initial, then `ToType X` is empty. -/
lemma empty_of_initial_of_preserves [PreservesColimit (Functor.empty.{0} C) (forget C)] (X : C)
    (h : Nonempty (IsInitial X)) : IsEmpty (ToType X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ IsEmpty (ToType X)

Tactic:
rw [← Types.initial_iff_empty]

Result:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ Nonempty (IsInitial (ToType X))

Tactic:
exact Nonempty.map (IsInitial.isInitialObj (forget C) _) h

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by simp)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y : C
T : C ⥤ D
f : S ⟶ T.obj Y
⊢ mkPostcomp f (𝟙 Y) = eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : S ⟶ T.obj Y
⊢ mk f = mk (f ≫ T.map (𝟙 Y))

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
@[simp]
lemma toFinset_Ici (a : α) [Fintype (Ici a)] : (Ici a).toFinset = Finset.Ici a

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
⊢ (Ici a).toFinset = Finset.Ici a

Tactic:
ext

Result:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a

Proof state:
case h
α : Type u_3
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderTop α
a : α
inst✝ : Fintype ↑(Ici a)
a✝ : α
⊢ a✝ ∈ (Ici a).toFinset ↔ a✝ ∈ Finset.Ici a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
Alternative definition of height, with the supremum ranging only over those series that end at `a`.
-/
lemma height_eq_iSup_last_eq (a : α) :
    height a = ⨆ (p : LTSeries α) (_ : p.last = a), ↑(p.length)

Proof state:
case H
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length ≤ n

Tactic:
rw [height_le_iff', iSup₂_le_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length

Tactic:
apply eq_of_forall_ge_iff

Result:
case H
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (c : ℕ∞), height a ≤ c ↔ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length ≤ c

Proof state:
case H
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (c : ℕ∞), height a ≤ c ↔ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length ≤ c

Tactic:
intro n

Result:
case H
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a ≤ n ↔ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length ≤ n
-- Mathlib/Data/List/Lattice.lean
theorem inter_reverse {xs ys : List α} : xs.inter ys.reverse = xs.inter ys

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
⊢ xs.inter ys.reverse = xs.inter ys

Tactic:
simp only [List.inter, elem_eq_mem, mem_reverse]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- `x + y` has exactly the same moves as `y + x`. -/
protected lemma add_comm (x y : PGame) : x + y ≡ y + x :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR => by
    refine Identical.of_equiv (Equiv.sumComm _ _) (Equiv.sumComm _ _) ?_ ?_ <;>
    · rintro (_ | _) <;>
      · dsimp; exact PGame.add_comm _ _
  termination_by (x, y)

Proof state:
case refine_2.inr
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
val✝ : yr
⊢ (mk xl xr xL xR + mk yl yr yL yR).moveRight (Sum.inr val✝) ≡
    (mk yl yr yL yR + mk xl xr xL xR).moveRight ((Equiv.sumComm xr yr) (Sum.inr val✝))

Tactic:
dsimp

Result:
case refine_2.inr
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
val✝ : yr
⊢ mk xl xr xL xR + yR val✝ ≡ (mk yl yr yL yR + mk xl xr xL xR).moveRight ((Equiv.sumComm xr yr) (Sum.inr val✝))

Proof state:
case refine_2.inr
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
val✝ : yr
⊢ mk xl xr xL xR + yR val✝ ≡ (mk yl yr yL yR + mk xl xr xL xR).moveRight ((Equiv.sumComm xr yr) (Sum.inr val✝))

Tactic:
exact PGame.add_comm _ _

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_comm : hausdorffDist s t = hausdorffDist t s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist s t = hausdorffDist t s

Tactic:
simp [hausdorffDist, hausdorffEdist_comm]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma TangentBundle.contMDiffVectorBundle [h : IsManifold I (n + 1) M] :
    haveI : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
    ContMDiffVectorBundle n E (TangentSpace I : M → Type _) I

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I 1 M
⊢ ContMDiffVectorBundle n E (TangentSpace I) I

Tactic:
have : (tangentBundleCore I M).IsContMDiff I n := tangentBundleCore.isContMDiff

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this✝ : IsManifold I 1 M
this : (tangentBundleCore I M).IsContMDiff I n
⊢ ContMDiffVectorBundle n E (TangentSpace I) I

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
⊢ ContMDiffVectorBundle n E (TangentSpace I) I

Tactic:
have : IsManifold I 1 M := .of_le (n := n + 1) le_add_self

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I 1 M
⊢ ContMDiffVectorBundle n E (TangentSpace I) I

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this✝ : IsManifold I 1 M
this : (tangentBundleCore I M).IsContMDiff I n
⊢ ContMDiffVectorBundle n E (TangentSpace I) I

Tactic:
exact (tangentBundleCore I M).instContMDiffVectorBundle

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasStrictFDerivAt.of_nmem_tsupport (h : x ∉ tsupport f) :
    HasStrictFDerivAt f (0 : E →L[𝕜] F) x

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
x : E
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt f 0 x

Tactic:
exact (hasStrictFDerivAt_const (0 : F) x).congr_of_eventuallyEq h.symm

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
x : E
h : x ∉ tsupport f
⊢ HasStrictFDerivAt f 0 x

Tactic:
rw [not_mem_tsupport_iff_eventuallyEq] at h

Result:
𝕜 : 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
x : E
h : f =ᶠ[𝓝 x] 0
⊢ HasStrictFDerivAt f 0 x
-- Mathlib/Data/List/DropRight.lean
theorem rtake_eq_reverse_take_reverse : l.rtake n = reverse (l.reverse.take n)

Proof state:
α : Type u_1
l : List α
n : ℕ
⊢ l.rtake n = (take n l.reverse).reverse

Tactic:
rw [rtake]

Result:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse

Proof state:
case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n✝ : ℕ
⊢ drop ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (take (n✝ + 1) (xs ++ [x]).reverse).reverse

Tactic:
simp [drop_append_eq_append_drop, IH]

Result:
no goals

Proof state:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

Tactic:
exact drop_length _

Result:
no goals

Proof state:
case nil
α : Type u_1
n : ℕ
⊢ drop ([].length - n) [] = (take n [].reverse).reverse

Tactic:
simp

Result:
no goals

Proof state:
case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse

Tactic:
cases n

Result:
case append_singleton.zero
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
⊢ drop ((xs ++ [x]).length - 0) (xs ++ [x]) = (take 0 (xs ++ [x]).reverse).reverse

case append_singleton.succ
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n✝ : ℕ
⊢ drop ((xs ++ [x]).length - (n✝ + 1)) (xs ++ [x]) = (take (n✝ + 1) (xs ++ [x]).reverse).reverse

Proof state:
α : Type u_1
l : List α
n : ℕ
⊢ drop (l.length - n) l = (take n l.reverse).reverse

Tactic:
induction' l using List.reverseRecOn with xs x IH generalizing n

Result:
case nil
α : Type u_1
n : ℕ
⊢ drop ([].length - n) [] = (take n [].reverse).reverse

case append_singleton
α : Type u_1
xs : List α
x : α
IH : ∀ (n : ℕ), drop (xs.length - n) xs = (take n xs.reverse).reverse
n : ℕ
⊢ drop ((xs ++ [x]).length - n) (xs ++ [x]) = (take n (xs ++ [x]).reverse).reverse
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIic_coe (x : Iic b) : projIic b x = x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b : α
x : ↑(Iic b)
⊢ projIic b ↑x = x

Tactic:
cases x

Result:
case mk
α : Type u_1
inst✝ : LinearOrder α
b val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrder α
b val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
apply projIic_of_mem

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
equals the product of their L-series, assuming both L-series converge. -/
lemma LSeriesHasSum.convolution {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a)
    (hg : LSeriesHasSum g s b) :
    LSeriesHasSum (f ⍟ g) s (a * b)

Proof state:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm

Result:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
hsum : Summable fun x => term f s x.1 * term g s x.2
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Proof state:
f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
hsum : Summable fun x => term f s x.1 * term g s x.2
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ioc_eq_Ioi_self_iff {f : ι → α} {a : α} :
    ⋃ i, Ioc a (f i) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
a : α
⊢ ⋃ i, Ioc a (f i) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i

Tactic:
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_id_map (decl : Decl α) : relabel id decl = decl

Proof state:
α : Type
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl

Tactic:
cases decl <;> rfl

Result:
no goals

Proof state:
α : Type
decl : Decl α
⊢ relabel id decl = decl

Tactic:
simp only [relabel, id_eq]

Result:
α : Type
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self (h : I.IsHomogeneous 𝒜) :
    (I.homogeneousCore 𝒜).toIdeal = I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ x ∈ homogeneousCore' 𝒜 I

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 x]

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ homogeneousCore' 𝒜 I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ (homogeneousCore 𝒜 I).toIdeal = I

Tactic:
apply le_antisymm (I.homogeneousCore'_le 𝒜) _

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I ≤ homogeneousCore' 𝒜 I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ homogeneousCore' 𝒜 I

Tactic:
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
⊢ I ≤ homogeneousCore' 𝒜 I

Tactic:
intro x hx

Result:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ x ∈ homogeneousCore' 𝒜 I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : Ideal A
h : IsHomogeneous 𝒜 I
x : A
hx : x ∈ I
⊢ x ∈ homogeneousCore' 𝒜 I

Tactic:
classical
rw [← DirectSum.sum_support_decompose 𝒜 x]
exact Ideal.sum_mem _ fun j _ => Ideal.subset_span ⟨⟨_, isHomogeneousElem_coe _⟩, h _ hx, rfl⟩

Result:
no goals