harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem intervalIntegrable_deriv_of_nonneg (hcont : ContinuousOn g (uIcc a b))
    (hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x)
    (hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x) : IntervalIntegrable g' volume a b

Proof state:
case inr
g' g : ℝ → ℝ
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x
⊢ IntegrableOn g' (Ioc b a) volume

Tactic:
exact integrableOn_deriv_of_nonneg hcont hderiv hpos

Result:
no goals

Proof state:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), 0 ≤ g' x
⊢ IntervalIntegrable g' volume a b

Tactic:
rcases le_total a b with hab | hab

Result:
case inl
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), 0 ≤ g' x
hab : a ≤ b
⊢ IntervalIntegrable g' volume a b

case inr
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b

Proof state:
case inr
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), 0 ≤ g' x
hab : b ≤ a
⊢ IntervalIntegrable g' volume a b

Tactic:
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le,
  integrableOn_empty, true_and] at hcont hderiv hpos ⊢

Result:
case inr
g' g : ℝ → ℝ
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x
⊢ IntegrableOn g' (Ioc b a) volume

Proof state:
case inl
g' g : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x
⊢ IntegrableOn g' (Ioc a b) volume

Tactic:
exact integrableOn_deriv_of_nonneg hcont hderiv hpos

Result:
no goals

Proof state:
case inl
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), 0 ≤ g' x
hab : a ≤ b
⊢ IntervalIntegrable g' volume a b

Tactic:
simp only [uIcc_of_le, min_eq_left, max_eq_right, hab, IntervalIntegrable, hab,
  Ioc_eq_empty_of_le, integrableOn_empty, and_true] at hcont hderiv hpos ⊢

Result:
case inl
g' g : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x
⊢ IntegrableOn g' (Ioc a b) volume
-- Mathlib/Data/Set/Prod.lean
theorem image_swap_prod (s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s

Tactic:
rw [image_swap_eq_preimage_swap, preimage_swap_prod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n - C a) = n

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n - C a).degree = ↑n

Tactic:
rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_eq_one_of_char_two (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) :
    quadraticCharFun F a = 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → -1 = 1

Tactic:
exact fun h ↦ (h (FiniteField.isSquare_of_char_two hF a)).elim

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = 1

Tactic:
simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F = 2
a : F
ha : a ≠ 0
⊢ ¬IsSquare a → -1 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_neg_add_le {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c

Proof state:
a b c : Int
h : -b + a ≤ c
⊢ a ≤ b + c

Tactic:
have h := Int.add_le_add_left h b

Result:
a b c : Int
h✝ : -b + a ≤ c
h : b + (-b + a) ≤ b + c
⊢ a ≤ b + c

Proof state:
a b c : Int
h✝ : -b + a ≤ c
h : b + (-b + a) ≤ b + c
⊢ a ≤ b + c

Tactic:
rwa [Int.add_neg_cancel_left] at h

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasStrictFDerivAt.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasStrictFDerivAt f f' x) (hx : f x = x) (n : ℕ) :
    HasStrictFDerivAt f^[n] (f' ^ n) x

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
ihn : HasStrictFDerivAt f^[n] (f' ^ n) x
⊢ HasStrictFDerivAt (f^[n] ∘ f) (f' ^ n * f') x

Tactic:
rw [← hx] at ihn

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
ihn : HasStrictFDerivAt f^[n] (f' ^ n) (f x)
⊢ HasStrictFDerivAt (f^[n] ∘ f) (f' ^ n * f') x

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
ihn : HasStrictFDerivAt f^[n] (f' ^ n) (f x)
⊢ HasStrictFDerivAt (f^[n] ∘ f) (f' ^ n * f') x

Tactic:
exact ihn.comp x hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasStrictFDerivAt f^[n] (f' ^ n) x

Tactic:
induction n with
| zero => exact hasStrictFDerivAt_id x
| succ n ihn =>
  rw [Function.iterate_succ, pow_succ]
  rw [← hx] at ihn
  exact ihn.comp x hf

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
ihn : HasStrictFDerivAt f^[n] (f' ^ n) x
⊢ HasStrictFDerivAt f^[n + 1] (f' ^ (n + 1)) x

Tactic:
rw [Function.iterate_succ, pow_succ]

Result:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
n : ℕ
ihn : HasStrictFDerivAt f^[n] (f' ^ n) x
⊢ HasStrictFDerivAt (f^[n] ∘ f) (f' ^ n * f') x

Proof state:
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasStrictFDerivAt f f' x
hx : f x = x
⊢ HasStrictFDerivAt f^[0] (f' ^ 0) x

Tactic:
exact hasStrictFDerivAt_id x

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma Δ_of_char_two : W.Δ = W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 2 * W.b₈ - 8 * (W.a₁ * W.a₃) ^ 3 - 27 * (W.a₃ ^ 2) ^ 2 + 9 * W.a₁ ^ 2 * (W.a₁ * W.a₃) * W.a₃ ^ 2 =
    W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

Tactic:
linear_combination (-W.a₁ ^ 4 * W.b₈ - 14 * W.a₃ ^ 4) * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.Δ = W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3

Tactic:
rw [Δ, b₂_of_char_two, b₄_of_char_two, b₆_of_char_two]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ -(W.a₁ ^ 2) ^ 2 * W.b₈ - 8 * (W.a₁ * W.a₃) ^ 3 - 27 * (W.a₃ ^ 2) ^ 2 + 9 * W.a₁ ^ 2 * (W.a₁ * W.a₃) * W.a₃ ^ 2 =
    W.a₁ ^ 4 * W.b₈ + W.a₃ ^ 4 + W.a₁ ^ 3 * W.a₃ ^ 3
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem mul_mul_mul_comm (hbc : Commute b c) (a d : S) :
    a * b * (c * d) = a * c * (b * d)

Proof state:
S : Type u_3
inst✝ : Semigroup S
b c : S
hbc : Commute b c
a d : S
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
simp only [hbc.left_comm, mul_assoc]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_nontrivial_iff :
    (Finset.univ : Finset α).Nontrivial ↔ Nontrivial α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ univ.Nontrivial ↔ Nontrivial α

Tactic:
rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem LipschitzWith.comp_memLp {α E F} {K} [MeasurableSpace α] {μ : Measure α}
    [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g)
    (g0 : g 0 = 0) (hL : MemLp f p μ) : MemLp (g ∘ f) p μ :=
  have : ∀ x, ‖g (f x)‖ ≤ K * ‖f x‖ := fun x ↦ by
    -- TODO: add `LipschitzWith.nnnorm_sub_le` and `LipschitzWith.nnnorm_le`
    simpa [g0] using hg.norm_sub_le (f x) 0
  hL.of_le_mul (hg.continuous.comp_aestronglyMeasurable hL.1) (Eventually.of_forall this)

Proof state:
p : ℝ≥0∞
α : Type u_7
E : Type u_8
F : Type u_9
K : ℝ≥0
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : E → F
hg : LipschitzWith K g
g0 : g 0 = 0
hL : MemLp f p μ
x : α
⊢ ‖g (f x)‖ ≤ ↑K * ‖f x‖

Tactic:
simpa [g0] using hg.norm_sub_le (f x) 0

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Linear.lean
@[simp] lemma coe_toLinear_eq_zero_iff : (χ : L →ₗ[R] R) = 0 ↔ χ.IsZero :=
  ⟨fun h ↦ funext fun x ↦ LinearMap.congr_fun h x, fun h ↦ by ext; simp [h.eq]⟩

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : LinearWeights R L M
χ : Weight R L M
h : χ.IsZero
x✝ : L
⊢ (toLinear R L M χ) x✝ = 0 x✝

Tactic:
simp [h.eq]

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : LinearWeights R L M
χ : Weight R L M
h : χ.IsZero
⊢ toLinear R L M χ = 0

Tactic:
ext

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : LinearWeights R L M
χ : Weight R L M
h : χ.IsZero
x✝ : L
⊢ (toLinear R L M χ) x✝ = 0 x✝
-- Mathlib/Order/Chain.lean
theorem ChainClosure.succ_fixpoint (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂)
    (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂

Proof state:
case succ
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set α
hc₁ : ChainClosure r s✝
h : s✝ ⊆ c₂
⊢ SuccChain r s✝ ⊆ c₂

Tactic:
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id

Result:
no goals

Proof state:
case union
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, a ⊆ c₂
⊢ ⋃₀ s✝ ⊆ c₂

Tactic:
exact sUnion_subset ih

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂

Tactic:
induction hc₁ with
| succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
| union _ ih => exact sUnion_subset ih

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc (attr := simp)]
lemma inl_v_triangle_mor₃_f (p q : ℤ) (hpq : p + (-1) = q) :
    (inl φ).v p q hpq ≫ (triangle φ).mor₃.f q =
      -(K.shiftFunctorObjXIso 1 q p (by rw [← hpq, neg_add_cancel_right])).inv

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ q + 1 = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ (inl φ).v p q hpq ≫ ((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v q q ⋯ = -(HomologicalComplex.XIsoOfEq K ⋯).inv

Tactic:
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
  Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by omega), shiftFunctor_obj_X,
  shiftFunctorObjXIso, Preadditive.comp_neg, inl_v_fst_v_assoc]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.1909, u_1} C
inst✝⁴ : Category.{?u.1913, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ p = q + 1

Tactic:
rw [← hpq, neg_add_cancel_right]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ (inl φ).v p q hpq ≫ (triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv

Tactic:
dsimp [triangle]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ (inl φ).v p q hpq ≫ ((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v q q ⋯ = -(HomologicalComplex.XIsoOfEq K ⋯).inv
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem testAgainstNN_eq_mass_mul (f : Ω →ᵇ ℝ≥0) :
    μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
nth_rw 1 [μ.self_eq_mass_smul_normalize]

Result:
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ (μ.mass • μ.normalize.toFiniteMeasure).testAgainstNN f = μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f

Tactic:
rw [μ.normalize.toFiniteMeasure.smul_testAgainstNN_apply μ.mass f, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp] lemma rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0∞) : (x ^ y⁻¹) ^ y = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y⁻¹) ^ y = x

Tactic:
rw [← rpow_mul, inv_mul_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma degreeOf_t_neq_of_neq (hv : v ∈ f.support) (hw : w ∈ f.support) (neq : v ≠ w) :
    (T f <| monomial v <| coeff v f).degreeOf 0 ≠
    (T f <| monomial w <| coeff w f).degreeOf 0

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
neq : v ≠ w
⊢ ∑ i : Fin (n + 1), r i * v i ≠ ∑ i : Fin (n + 1), r i * w i

Tactic:
refine sum_r_mul_neq f v w (fun i ↦ ?_) (fun i ↦ ?_) neq <;>
exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i)) (by omega)

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
neq : v ≠ w
⊢ degreeOf 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠
    degreeOf 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))

Tactic:
rw [degreeOf_zero_t _ _ <| mem_support_iff.mp hv, degreeOf_zero_t _ _ <| mem_support_iff.mp hw]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
neq : v ≠ w
⊢ ∑ i : Fin (n + 1), r i * v i ≠ ∑ i : Fin (n + 1), r i * w i

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
neq : v ≠ w
i : Fin (n + 1)
⊢ f.totalDegree < up

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Norm/Defs.lean
theorem norm_eq_matrix_det [Fintype ι] [DecidableEq ι] (b : Basis ι R S) (s : S) :
    norm R s = Matrix.det (Algebra.leftMulMatrix b s)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ (norm R) s = ((leftMulMatrix b) s).det

Tactic:
rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Field.lean
lemma nnqsmul_nonneg (q : ℚ≥0) (ha : 0 ≤ a) : 0 ≤ q • a

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
exact mul_nonneg q.cast_nonneg ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
rw [NNRat.smul_def]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a
-- Mathlib/Algebra/Homology/ImageToKernel.lean
@[simp]
lemma imageToKernel_arrow_apply {FV : V → V → Type*} {CV : V → Type*}
    [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV] (w : f ≫ g = 0)
    (x : ToType (Subobject.underlying.obj (imageSubobject f))) :
    (kernelSubobject g).arrow (imageToKernel f g w x) =
      (imageSubobject f).arrow x

Proof state:
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝³ : HasImage f
g : B ⟶ C
inst✝² : HasKernel g
FV : V → V → Type u_2
CV : V → Type u_3
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
w : f ≫ g = 0
x : ToType (Subobject.underlying.obj (imageSubobject f))
⊢ (ConcreteCategory.hom (kernelSubobject g).arrow) ((ConcreteCategory.hom (imageToKernel f g w)) x) =
    (ConcreteCategory.hom (imageSubobject f).arrow) x

Tactic:
rw [← ConcreteCategory.comp_apply, imageToKernel_arrow]

Result:
no goals
-- Mathlib/Data/Subtype.lean
theorem coind_injective {α β} {f : α → β} {p : β → Prop} (h : ∀ a, p (f a)) (hf : Injective f) :
    Injective (coind f h) := fun x y hxy ↦ hf <| by apply congr_arg Subtype.val hxy

Proof state:
α : Sort u_4
β : Sort u_5
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
hf : Injective f
x y : α
hxy : coind f h x = coind f h y
⊢ f x = f y

Tactic:
apply congr_arg Subtype.val hxy

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_lt_re (a : ℝ) : frontier { z : ℂ | a < z.re } = { z | z.re = a }

Proof state:
a : ℝ
⊢ frontier {z | a < z.re} = {z | z.re = a}

Tactic:
simpa only [frontier_Ioi] using frontier_preimage_re (Ioi a)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_pow (b x : ℝ) (k : ℕ) : logb b (x ^ k) = k * logb b x

Proof state:
b x : ℝ
k : ℕ
⊢ logb b (x ^ k) = ↑k * logb b x

Tactic:
rw [logb, logb, log_pow, mul_div_assoc]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.insert_dep (hB : M.IsBase B) (h : e ∈ M.E \ B) : M.Dep (insert e B)

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ ¬M.Indep (insert e B)

Tactic:
exact h.2 ∘ (fun hi ↦ insert_eq_self.mp (hB.eq_of_subset_indep hi (subset_insert e B)).symm)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ M.Dep (insert e B)

Tactic:
rw [← not_indep_iff (insert_subset h.1 hB.subset_ground)]

Result:
α : Type u_1
M : Matroid α
B : Set α
e : α
hB : M.IsBase B
h : e ∈ M.E \ B
⊢ ¬M.Indep (insert e B)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem finrank :
    finrank ℝ (euclidean.mixedSpace K) = finrank ℚ K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ (euclidean.mixedSpace K) = finrank ℚ K

Tactic:
rw [LinearEquiv.finrank_eq (toMixed K).toLinearEquiv, mixedEmbedding.finrank]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_add_one_sq_lt_ack_add_four (m n : ℕ) : ack m ((n + 1) ^ 2) < ack (m + 4) n :=
  calc
    ack m ((n + 1) ^ 2) < ack m ((ack m n + 1) ^ 2) :=
      ack_strictMono_right m <| Nat.pow_lt_pow_left (succ_lt_succ <| lt_ack_right m n) two_ne_zero
    _ ≤ ack m (ack (m + 3) n) := ack_mono_right m <| ack_add_one_sq_lt_ack_add_three m n
    _ ≤ ack (m + 2) (ack (m + 3) n) := ack_mono_left _ <| by omega
    _ = ack (m + 3) (n + 1) := (ack_succ_succ _ n).symm
    _ ≤ ack (m + 4) n := ack_succ_right_le_ack_succ_left _ n

Proof state:
m n : ℕ
⊢ m ≤ m + 2

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.const_add [AddSemigroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (a + x)) c := fun x => by simpa [add_assoc] using h (a + x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddSemigroup α
h : Periodic f c
a x : α
⊢ (fun x => f (a + x)) (x + c) = (fun x => f (a + x)) x

Tactic:
simpa [add_assoc] using h (a + x)

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_insert_inl : (insert (inl a) u).toRight = u.toRight

Proof state:
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inl a) u).toRight = u.toRight

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
a : α
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_neg_natCast (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹

Proof state:
case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n✝ : ℕ
⊢ A ^ (-↑(n✝ + 1)) = (A ^ (n✝ + 1))⁻¹

Tactic:
exact DivInvMonoid.zpow_neg' _ _

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℕ
⊢ A ^ (-↑n) = (A ^ n)⁻¹

Tactic:
cases n

Result:
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-↑0) = (A ^ 0)⁻¹

case succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n✝ : ℕ
⊢ A ^ (-↑(n✝ + 1)) = (A ^ (n✝ + 1))⁻¹

Proof state:
case zero
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
⊢ A ^ (-↑0) = (A ^ 0)⁻¹

Tactic:
simp

Result:
no goals