harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul (hp : Prime p) {a b : M} {k l : ℕ} :
    p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩ =>
  have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z

Tactic:
rwa [mul_right_inj' hp0] at h

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ x
d : M
hd : x = p * d
⊢ a = p ^ (k + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)

Tactic:
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : M
hx : a = p ^ k * x
y : M
hy : b = p ^ l * y
z : M
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ y
d : M
hd : y = p * d
⊢ b = p ^ (l + 1) * d

Tactic:
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.inr_map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y)
    (g : X ⟶ Z) : biprod.inr ≫ biprod.map f g = g ≫ biprod.inr

Proof state:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr

Tactic:
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩

Result:
no goals

Proof state:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map f g = g ≫ inr

Tactic:
rw [biprod.map_eq_map']

Result:
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inr ≫ map' f g = g ≫ inr
-- Mathlib/Topology/Separation/Basic.lean
theorem compl_singleton_mem_nhdsSet_iff [T1Space X] {x : X} {s : Set X} : {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
⊢ {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s

Tactic:
rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]

Result:
no goals
-- Mathlib/Algebra/Module/BigOperators.lean
theorem Multiset.sum_smul_sum {s : Multiset R} {t : Multiset M} :
    s.sum • t.sum = ((s ×ˢ t).map fun p : R × M ↦ p.fst • p.snd).sum

Proof state:
case cons
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
a : R
s : Multiset R
ih : s.sum • t.sum = (map (fun p => p.1 • p.2) (s ×ˢ t)).sum
⊢ (a ::ₘ s).sum • t.sum = (map (fun p => p.1 • p.2) ((a ::ₘ s) ×ˢ t)).sum

Tactic:
simp [add_smul, ih, ← Multiset.smul_sum]

Result:
no goals

Proof state:
case empty
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
⊢ sum 0 • t.sum = (map (fun p => p.1 • p.2) (0 ×ˢ t)).sum

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Multiset R
t : Multiset M
⊢ s.sum • t.sum = (map (fun p => p.1 • p.2) (s ×ˢ t)).sum

Tactic:
induction' s using Multiset.induction with a s ih

Result:
case empty
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
⊢ sum 0 • t.sum = (map (fun p => p.1 • p.2) (0 ×ˢ t)).sum

case cons
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Multiset M
a : R
s : Multiset R
ih : s.sum • t.sum = (map (fun p => p.1 • p.2) (s ×ˢ t)).sum
⊢ (a ::ₘ s).sum • t.sum = (map (fun p => p.1 • p.2) ((a ::ₘ s) ×ˢ t)).sum
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`. -/
lemma HasUnifEigenvalue.le {f : End R M} {μ : R} {k m : ℕ∞}
    (hm : k ≤ m) (hk : f.HasUnifEigenvalue μ k) :
    f.HasUnifEigenvalue μ m

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
rw [← le_bot_iff, ← hk]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) m

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) k ≠ ⊥
⊢ (f.genEigenspace μ) m ≠ ⊥

Tactic:
contrapose! hk

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
unfold HasUnifEigenvalue at *

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) k ≠ ⊥
⊢ (f.genEigenspace μ) m ≠ ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) m

Tactic:
exact (f.genEigenspace _).monotone hm

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem mul_inv : ∀ {z : ℤ_[p]}, ‖z‖ = 1 → z * z.inv = 1
  | ⟨k, _⟩, h => by
    have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)
    unfold PadicInt.inv
    rw [norm_eq_padic_norm] at h
    dsimp only
    rw [dif_pos h]
    apply Subtype.ext_iff_val.2
    simp [mul_inv_cancel₀ hk]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩ = 1

Tactic:
apply Subtype.ext_iff_val.2

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ↑(⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩) = ↑1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1

Tactic:
have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ↑(⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩) = ↑1

Tactic:
simp [mul_inv_cancel₀ hk]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ *
      match ⟨k, property✝⟩ with
      | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) =
    1

Tactic:
dsimp only

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ * if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
h' : k = 0
⊢ 0 = 1

Tactic:
simp [h'] at h

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ *
      match ⟨k, property✝⟩ with
      | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) =
    1

Tactic:
rw [norm_eq_padic_norm] at h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ *
      match ⟨k, property✝⟩ with
      | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) =
    1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ * if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) = 1

Tactic:
rw [dif_pos h]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * ⟨k⁻¹, ⋯⟩ = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
hk : k ≠ 0
⊢ ⟨k, property✝⟩ * inv ⟨k, property✝⟩ = 1

Tactic:
unfold PadicInt.inv

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property✝ : ‖k‖ ≤ 1
h : ‖⟨k, property✝⟩‖ = 1
hk : k ≠ 0
⊢ (⟨k, property✝⟩ *
      match ⟨k, property✝⟩ with
      | ⟨k, property⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, ⋯⟩ else 0) =
    1
-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.eq_ite [DecidableEq ι] {i j : ι} (v : G i) (w : G j) :
    ⟪V i v, V j w⟫ = ite (i = j) ⟪V i v, V j w⟫ 0

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i j : ι
v : G i
w : G j
h : i = j
⊢ inner ((V i) v) ((V j) w) = inner ((V i) v) ((V j) w)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i j : ι
v : G i
w : G j
⊢ inner ((V i) v) ((V j) w) = if i = j then inner ((V i) v) ((V j) w) else 0

Tactic:
split_ifs with h

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i j : ι
v : G i
w : G j
h : i = j
⊢ inner ((V i) v) ((V j) w) = inner ((V i) v) ((V j) w)

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner ((V i) v) ((V j) w) = 0

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner ((V i) v) ((V j) w) = 0

Tactic:
exact hV h v w

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem units_smul_of_neg (u : Rˣ) (hu : u.1 < 0) (v : Module.Ray R M) : u • v = -v

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ u • v = -v

Tactic:
rw [← neg_inj, neg_neg, ← neg_units_smul, units_smul_of_pos]

Result:
case hu
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ 0 < ↑(-u)

Proof state:
case hu
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
hu : ↑u < 0
v : Ray R M
⊢ 0 < ↑(-u)

Tactic:
rwa [Units.val_neg, Right.neg_pos_iff]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
@[simp] lemma ringEquivCongr_refl (a : ℕ) : ringEquivCongr (rfl : a = a) = .refl _

Proof state:
a : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod a)

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
/-- See `Real.one_sub_inv_le_log_of_pos` for the stronger version when `x ≠ 0`. -/
lemma neg_inv_le_log (hx : 0 ≤ x) : -x⁻¹ ≤ log x

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹

Tactic:
exact log_le_self <| inv_nonneg.2 hx

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ -x⁻¹ ≤ log x

Tactic:
rw [neg_le, ← log_inv]

Result:
x : ℝ
hx : 0 ≤ x
⊢ log x⁻¹ ≤ x⁻¹
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_recursion (n m k : ℕ) :
    hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

Proof state:
n m k : ℕ
⊢ hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)

Tactic:
rw [hyperoperation]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (x : G)
    (i : ℕ) : ‖iteratedFDeriv 𝕜 i (f ∘ g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ (g x)‖

Tactic:
apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ ‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ (g x)‖
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem epi_of_epi_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Epi h]
    (w : f ≫ g = h) : Epi g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g

Tactic:
exact epi_of_epi f g

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_range_add_one_eq_factorial : ∀ n : ℕ, (∏ x ∈ range n, (x + 1)) = n !
  | 0 => rfl
  | n + 1 => by simp [factorial, Finset.range_succ, prod_range_add_one_eq_factorial n]

Proof state:
n : ℕ
⊢ ∏ x ∈ range (n + 1), (x + 1) = (n + 1)!

Tactic:
simp [factorial, Finset.range_succ, prod_range_add_one_eq_factorial n]

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_ne {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a')
    (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) :
    (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Proof state:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
rw [eq_iff_iff, not_iff_not, cancel_factors_eq ha hb had hbd hgcd]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Tactic:
classical
rw [eq_iff_iff, not_iff_not, cancel_factors_eq ha hb had hbd hgcd]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_monomial_single {i : σ} {n : ℕ} : pderiv i (monomial (single i n) a) =
    monomial (single i (n - 1)) (a * n)

Proof state:
R : Type u
σ : Type v
a : R
inst✝ : CommSemiring R
i : σ
n : ℕ
⊢ (pderiv i) ((monomial (single i n)) a) = (monomial (single i (n - 1))) (a * ↑n)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_iff' :
    M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
rw [IsBasis, maximal_subset_iff]

Result:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zpow_one_add₀ (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i

Tactic:
rw [zpow_add₀ h, zpow_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@[simp]
lemma Pi.map_id {f : α → C} [HasProduct f] : Pi.map (fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Proof state:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map fun a => 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map fun a => 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Proof state:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map fun a => 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem map_apply_ιMulti {n : ℕ} (f : M →ₗ[R] N) (m : Fin n → M) :
    map f (ιMulti R n m) = ιMulti R n (f ∘ m)

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ (map f) ((ιMulti R n) m) = (ιMulti R n) (⇑f ∘ m)

Tactic:
rw [ιMulti_apply, ιMulti_apply, map_list_prod]

Result:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ (List.map (⇑(map f)) (List.ofFn fun i => (ι R) (m i))).prod = (List.ofFn fun i => (ι R) ((⇑f ∘ m) i)).prod

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ (List.map (⇑(map f)) (List.ofFn fun i => (ι R) (m i))).prod = (List.ofFn fun i => (ι R) ((⇑f ∘ m) i)).prod

Tactic:
simp only [List.map_ofFn, Function.comp_def, map_apply_ι]

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Algebra.lean
theorem algebra_iso_of_iso {A B : Algebra T} (f : A ⟶ B) [IsIso f.f] : IsIso f :=
  ⟨⟨{   f := inv f.f
        h

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ A.a = B.a ≫ inv f.f

Tactic:
rw [IsIso.eq_comp_inv f.f, Category.assoc, ← f.h]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ T.map f.f ≫ B.a = B.a

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ T.map (inv f.f) ≫ T.map f.f ≫ B.a = B.a

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
A B : T.Algebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ f ≫ { f := inv f.f, h := ⋯ } = 𝟙 A ∧ { f := inv f.f, h := ⋯ } ≫ f = 𝟙 B

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_eq_finprod (hf : (mulSupport f).Finite) :
    ∏' b, f b = ∏ᶠ b, f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf : (mulSupport f).Finite
⊢ ∏' (b : β), f b = ∏ᶠ (b : β), f b

Tactic:
simp [tprod_def, multipliable_of_finite_mulSupport hf, hf]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem totalVariation_neg (s : SignedMeasure α) : (-s).totalVariation = s.totalVariation

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).totalVariation = s.totalVariation

Tactic:
simp [totalVariation, toJordanDecomposition_neg, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_whiskerRight (f : a ⟶ b) (g : b ⟶ c) :
    (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
    cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
    comp_whiskerRight_assoc, triangle, associator_naturality_left]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_of_not_integrable (hf : ¬ Integrable (fun x ↦ exp (f x)) μ) : μ.tilted f = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.withDensity fun x => ENNReal.ofReal (rexp (f x) / 0)) = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ μ.tilted f = 0

Tactic:
rw [Measure.tilted, integral_undef hf]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.withDensity fun x => ENNReal.ofReal (rexp (f x) / 0)) = 0
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem iterate (hf : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f^[m] n x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x

Tactic:
exact hf.isFixedPt.iterate m

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x

Tactic:
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]

Result:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt f^[n]^[m] x
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma oddKernel_def' (a x : ℝ) : ↑(oddKernel ↑a x) = cexp (-π * a ^ 2 * x) *
    (jacobiTheta₂' (a * I * x) (I * x) / (2 * π * I) + a * jacobiTheta₂ (a * I * x) (I * x))

Proof state:
a x : ℝ
⊢ ↑(oddKernel (↑a) x) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
  (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]

Result:
no goals

Proof state:
a x : ℝ
⊢ ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * ↑x

Tactic:
ring

Result:
no goals