harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma leftHomologyMap'_add :
    leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ +
      leftHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
simp only [γ.leftHomologyMap'_eq, γ'.leftHomologyMap'_eq,
  (γ.add γ').leftHomologyMap'_eq, LeftHomologyMapData.add_φH]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
-- Mathlib/Order/Compare.lean
theorem cmp_eq_cmp_symm : cmp x y = cmp x' y' ↔ cmp y x = cmp y' x' :=
  ⟨fun h => by rwa [← cmp_swap x', ← cmp_swap, swap_inj],
   fun h => by rwa [← cmp_swap y', ← cmp_swap, swap_inj]⟩

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'

Tactic:
rwa [← cmp_swap y', ← cmp_swap, swap_inj]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
rwa [← cmp_swap x', ← cmp_swap, swap_inj]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `mul_inv_le_iff₀` for a version with multiplication on the other side. -/
lemma mul_inv_le_iff₀' (hc : 0 < c) : b * c⁻¹ ≤ a ↔ b ≤ c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ b * c⁻¹ ≤ a ↔ b ≤ c * a

Tactic:
rw [mul_inv_le_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_zero : cos 0 = 1

Proof state:
⊢ cos 0 = 1

Tactic:
simp [cos]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem factorThruImageSubobject_comp_self {W : C} (k : W ⟶ X) (h) :
    (imageSubobject f).factorThru (k ≫ f) h = k ≫ factorThruImageSubobject f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ f) h = k ≫ factorThruImageSubobject f

Tactic:
ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : (imageSubobject f).Factors (k ≫ f)
⊢ (imageSubobject f).factorThru (k ≫ f) h ≫ (imageSubobject f).arrow =
    (k ≫ factorThruImageSubobject f) ≫ (imageSubobject f).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_apply (F : Multiplicative G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F (Multiplicative.ofAdd a)

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : AddMonoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : Multiplicative G →* A
f : MonoidAlgebra k G
⊢ ((lift k G A) F) f = sum f fun a b => b • F (Multiplicative.ofAdd a)

Tactic:
simp only [lift_apply', Algebra.smul_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_or_eq_of_mem_setIfInBounds
    {as : Array α} {i : Nat} {a b : α} (h : a ∈ as.setIfInBounds i b) : a ∈ as ∨ a = b

Proof state:
case mk
α : Type u_1
i : Nat
a b : α
toList✝ : List α
h : a ∈ { toList := toList✝ }.setIfInBounds i b
⊢ a ∈ { toList := toList✝ } ∨ a = b

Tactic:
simpa using List.mem_or_eq_of_mem_set (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
a b : α
h : a ∈ as.setIfInBounds i b
⊢ a ∈ as ∨ a = b

Tactic:
cases as

Result:
case mk
α : Type u_1
i : Nat
a b : α
toList✝ : List α
h : a ∈ { toList := toList✝ }.setIfInBounds i b
⊢ a ∈ { toList := toList✝ } ∨ a = b

Proof state:
α : Type u_1
i : Nat
a b : α
toList✝ : List α
h : a ∈ { toList := toList✝ }.setIfInBounds i b
⊢ a ∈ toList✝.set ?m.141212 b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem isOpen : IsOpen { x : R | IsUnit x }

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}

Tactic:
rw [mem_ball_iff_norm] at hy

Result:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
⊢ IsOpen {x | IsUnit x}

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}

Tactic:
rw [Metric.isOpen_iff]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ ∀ x ∈ {x | IsUnit x}, ∃ ε > 0, Metric.ball x ε ⊆ {x | IsUnit x}

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
⊢ ∀ x ∈ {x | IsUnit x}, ∃ ε > 0, Metric.ball x ε ⊆ {x | IsUnit x}

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε > 0, Metric.ball (↑x) ε ⊆ {x | IsUnit x}

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε > 0, Metric.ball (↑x) ε ⊆ {x | IsUnit x}

Tactic:
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩

Result:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}

Proof state:
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
a✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}

Tactic:
exact (x.ofNearby y hy).isUnit

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_neg_swap (a b : α) :
    variationOnFromTo f s a b = -variationOnFromTo f s b a

Proof state:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
simp only [variationOnFromTo, if_pos ab.le, if_neg ab.not_le, neg_neg]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a

Tactic:
simp only [variationOnFromTo.self, neg_zero]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
simp only [variationOnFromTo, if_pos ba.le, if_neg ba.not_le, neg_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
rcases lt_trichotomy a b with (ab | rfl | ba)

Result:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a

case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_mul_left_iff (h : a ≠ 0) : (Summable fun i ↦ a * f i) ↔ Summable f :=
  ⟨fun H ↦ by simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹, fun H ↦ H.mul_left _⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
H : Summable fun i => a * f i
⊢ Summable f

Tactic:
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpToOn_zero_iff :
    HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
hm : ↑0 ≤ 0
this : EqOn (fun x => p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
⊢ ContinuousOn f s

Tactic:
exact H.1

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
m : ℕ
hm : ↑m ≤ 0
⊢ ContinuousOn (fun x => p x m) s

Tactic:
obtain rfl : m = 0 := mod_cast hm.antisymm (zero_le _)

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
hm : ↑0 ≤ 0
⊢ ContinuousOn (fun x => p x 0) s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
⊢ HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x

Tactic:
refine ⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H =>
    ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun m hm ↦ ?_⟩⟩

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
m : ℕ
hm : ↑m ≤ 0
⊢ ContinuousOn (fun x => p x m) s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
hm : ↑0 ≤ 0
this : EqOn (fun x => p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
⊢ ContinuousOn (fun x => p x 0) s

Tactic:
rw [continuousOn_congr this, LinearIsometryEquiv.comp_continuousOn_iff]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
H : ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
hm : ↑0 ≤ 0
this : EqOn (fun x => p x 0) (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s
⊢ ContinuousOn f s
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_mul_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
a₁ a₂ : G
b₁ b₂ : k
⊢ single (a₁ * a₂) (b₁ * 0) = 0

Tactic:
rw [mul_zero, single_zero]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
a₁ a₂ : G
b₁ b₂ : k
⊢ (sum (single a₁ b₁) fun a₁ b₁ => sum (single a₂ b₂) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)) =
    single (a₁ * a₂) (b₁ * b₂)

Tactic:
exact (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
  (sum_single_index (by rw [mul_zero, single_zero]))

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
a₁ a₂ : G
b₁ b₂ : k
⊢ (sum (single a₂ b₂) fun a₂ b₂ => single (a₁ * a₂) (0 * b₂)) = 0

Tactic:
simp only [zero_mul, single_zero, sum_zero]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
a₁ a₂ : G
b₁ b₂ : k
⊢ single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂)

Tactic:
rw [mul_def]

Result:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Mul G
a₁ a₂ : G
b₁ b₂ : k
⊢ (sum (single a₁ b₁) fun a₁ b₁ => sum (single a₂ b₂) fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)) =
    single (a₁ * a₂) (b₁ * b₂)
-- Mathlib/Data/Nat/Digits.lean
theorem eleven_dvd_iff :
    11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum

Proof state:
n : ℕ
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum

Tactic:
have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by norm_num) n

Result:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum

Proof state:
n : ℕ
⊢ ↑11 ∣ ↑10 - -1

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum

Tactic:
exact t

Result:
no goals

Proof state:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum

Tactic:
rw [ofDigits_neg_one] at t

Result:
n : ℕ
t : 11 ∣ n ↔ ↑11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
⊢ 11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
-- Mathlib/Order/Nucleus.lean
theorem iInf_apply {ι : Type*} (f : ι → (Nucleus X)) (x : X) : iInf f x = ⨅ j, f j x

Proof state:
X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ (iInf f) x = ⨅ j, (f j) x

Tactic:
rw [iInf, sInf_apply, iInf_range]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem lintegral_edist_lt_top {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
    (∫⁻ a, edist (f a) (g a) ∂μ) < ∞ :=
  lt_of_le_of_lt (lintegral_edist_triangle hf.aestronglyMeasurable aestronglyMeasurable_zero)
    (ENNReal.add_lt_top.2 <| by
      simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]
      exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ

Tactic:
exact ⟨hf.hasFiniteIntegral, hg.hasFiniteIntegral⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫⁻ (a : α), edist (f a) (0 a) ∂μ < ⊤ ∧ ∫⁻ (a : α), edist (g a) (0 a) ∂μ < ⊤

Tactic:
simp_rw [Pi.zero_apply, ← hasFiniteIntegral_iff_edist]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ HasFiniteIntegral f μ ∧ HasFiniteIntegral g μ
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Iio (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iio a).map (Embedding.subtype p) = (Iio a : Finset α)

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

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

Result:
no goals

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

Tactic:
rw [subtype_Iio_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Iio ↑a)) = Iio ↑a
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_monomial [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (ha : a ≠ 0) (n : ℕ) :
    (monomial n a).aroots S = n • ({0} : Multiset S)

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).aroots S = n • {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
theorem isInt_dvd_false : {a b : ℤ} → {a' b' : ℤ} →
    IsInt a a' → IsInt b b' → Int.emod b' a' != 0 → ¬a ∣ b
  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, e => mt Int.emod_eq_zero_of_dvd (by simpa using e)

Proof state:
n✝¹ n✝ : ℤ
e : (n✝.emod n✝¹ != 0) = true
⊢ ¬↑n✝ % ↑n✝¹ = 0

Tactic:
simpa using e

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem nhds_zero : 𝓝 (0 : Γ₀) = ⨅ γ ≠ 0, 𝓟 (Iio γ)

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 0 = ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)

Tactic:
rw [nhds_eq_update, update_self]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
lemma obj_eq_of_cons_eq_cons {p : Path a b} {p' : Path a c}
    {e : b ⟶ d} {e' : c ⟶ d} (h : p.cons e = p'.cons e') : b = c

Proof state:
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a b
p' : Path a c
e : b ⟶ d
e' : c ⟶ d
h : p.cons e = p'.cons e'
⊢ b = c

Tactic:
injection h

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem mem_nhds_discrete {x : α} {s : Set α} :
    s ∈ 𝓝 x ↔ x ∈ s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
rw [nhds_discrete, mem_pure]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_two : sin (π / 2) = 1 :=
  have : sin (π / 2) = 1 ∨ sin (π / 2) = -1

Proof state:
⊢ sin (π / 2) = 1 ∨ sin (π / 2) = -1

Tactic:
simpa [sq, mul_self_eq_one_iff] using sin_sq_add_cos_sq (π / 2)

Result:
no goals

Proof state:
this : sin (π / 2) = 1 ∨ sin (π / 2) = -1
h : sin (π / 2) = -1
⊢ ¬0 < -1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Int.lean
theorem nnnorm_coe_units (e : ℤˣ) : ‖(e : ℤ)‖₊ = 1

Proof state:
e : ℤˣ
⊢ ‖↑e‖₊ = 1

Tactic:
obtain rfl | rfl := units_eq_one_or e <;>
  simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swapCore_swapCore (r a b : α) : swapCore a b (swapCore a b r) = r

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r

Tactic:
split_ifs <;> cc

Result:
no goals

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ swapCore a b (swapCore a b r) = r

Tactic:
unfold swapCore

Result:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem modEq_mersenne (n k : ℕ) : k ≡ k / 2 ^ n + k % 2 ^ n [MOD 2 ^ n - 1] :=
  -- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
  calc
    k = 2 ^ n * (k / 2 ^ n) + k % 2 ^ n := (Nat.div_add_mod k (2 ^ n)).symm
    _ ≡ 1 * (k / 2 ^ n) + k % 2 ^ n [MOD 2 ^ n - 1] :=
      ((Nat.modEq_sub <| Nat.succ_le_of_lt <| pow_pos zero_lt_two _).mul_right _).add_right _
    _ = k / 2 ^ n + k % 2 ^ n

Proof state:
n k : ℕ
⊢ 1 * (k / 2 ^ n) + k % 2 ^ n = k / 2 ^ n + k % 2 ^ n

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem subset_toMeasurable (μ : Measure α) (s : Set α) : s ⊆ toMeasurable μ s

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ s ⊆ hs.choose

case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ h's.choose

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ ⋯.choose

Tactic:
exacts [hs.choose_spec.1, h's.choose_spec.1, (exists_measurable_superset μ s).choose_spec.1]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose

Tactic:
split_ifs with hs h's

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ s ⊆ hs.choose

case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ h's.choose

case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's : ¬∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u)
⊢ s ⊆ ⋯.choose

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆ toMeasurable μ s

Tactic:
rw [toMeasurable_def]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ s ⊆
    if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then h.choose
    else
      if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → μ (t ∩ u) = μ (s ∩ u) then h'.choose
      else ⋯.choose