harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_const_smul (c : R) (hf : DifferentiableWithinAt 𝕜 f s x) :
    derivWithin (fun y => c • f y) s x = c • derivWithin f s x

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c • f y) s x = c • derivWithin f s x

Tactic:
exact (hf.hasDerivWithinAt.const_smul c).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c • f y) s x = c • derivWithin f s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun y => c • f y) s x = c • derivWithin f s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c • f y) s x = c • derivWithin f s x

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R F
inst✝¹ : SMulCommClass 𝕜 R F
inst✝ : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c • f y) s x = c • derivWithin f s x
-- Mathlib/Algebra/Quandle.lean
theorem self_invAct_act_eq {x y : R} : (x ◃⁻¹ x) ◃ y = x ◃ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y

Tactic:
have h := @self_act_invAct_eq _ _ (op x) (op y)

Result:
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃⁻¹ op y = op x ◃⁻¹ op y
⊢ (x ◃⁻¹ x) ◃ y = x ◃ y
-- Mathlib/Algebra/Algebra/Unitization.lean
@[simp high]
lemma starMap_inl (φ : A →⋆ₙₐ[R] B) (r : R) :
    starMap φ (inl r) = algebraMap R (Unitization R B) r

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
r : R
⊢ (starMap φ) (inl r) = (algebraMap R (Unitization R B)) r

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem polyOfInterest_vars_eq (n : ℕ) : (polyOfInterest p n).vars =
    ((p : 𝕄) ^ (n + 1) * (wittMul p (n + 1) + (p : 𝕄) ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
      X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) -
      X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)))).vars

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Proof state:
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ≠ 0

Tactic:
exact mod_cast hp.out.ne_zero

Result:
no goals

Proof state:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) ≠ 0

Tactic:
apply pow_ne_zero

Result:
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
rw [polyOfInterest, this, vars_C_mul]

Result:
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) = C (↑p ^ (n + 1))

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_comm (x y : BitVec w) :
    x ^^^ y = y ^^^ x

Proof state:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ y).getLsbD i = (y ^^^ x).getLsbD i

Tactic:
simp [Bool.xor_comm]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x ^^^ y = y ^^^ x

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ y).getLsbD i = (y ^^^ x).getLsbD i
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem Subsingleton.pi_mulSingle_eq {α : Type*} [DecidableEq I] [Subsingleton I] [One α]
    (i : I) (x : α) : Pi.mulSingle i x = fun _ => x :=
  funext fun j => by rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

Proof state:
I : Type u
α : Type u_4
inst✝² : DecidableEq I
inst✝¹ : Subsingleton I
inst✝ : One α
i : I
x : α
j : I
⊢ Pi.mulSingle i x j = x

Tactic:
rw [Subsingleton.elim j i, Pi.mulSingle_eq_same]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_monomial_mul' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff m (monomial s r * p) = if s ≤ m then r * coeff (m - s) p else 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m ((monomial s) r * p) = if s ≤ m then r * coeff (m - s) p else 0

Tactic:
rw [mul_comm, mul_comm r]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0

Tactic:
exact coeff_mul_monomial' _ _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
  (nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
    rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H

Proof state:
a b : Int
H : (-(b - a)).NonNeg
⊢ -(b - a) = a - b

Tactic:
simp [Int.add_comm, Int.sub_eq_add_neg]

Result:
no goals

Proof state:
a b : Int
H : (-(b - a)).NonNeg
⊢ b ≤ a

Tactic:
rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_pos' {a : R} (ha : 0 < a) {c : R} (hc : IsRegular c) : 0 < c * a * star c

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 < a
c : R
hc : IsRegular c
⊢ 0 < c * a * star c

Tactic:
simpa only [star_star] using conjugate_pos ha hc.star

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Units.lean
lemma not_isUnit_of_degree_pos (p : R[X]) (hpl : 0 < p.degree) : ¬ IsUnit p

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Subsingleton R
⊢ ¬IsUnit p

Tactic:
simp [Subsingleton.elim p 0] at hpl

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
⊢ ¬IsUnit p

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Subsingleton R
⊢ ¬IsUnit p

case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Nontrivial R
⊢ ¬IsUnit p

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Nontrivial R
h : IsUnit p
⊢ False

Tactic:
simp [degree_eq_zero_of_isUnit h] at hpl

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Nontrivial R
⊢ ¬IsUnit p

Tactic:
intro h

Result:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Nontrivial R
h : IsUnit p
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasFDerivWithinAt.rpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x)
    (h : 0 < f x) : HasFDerivWithinAt (fun x => f x ^ g x)
      ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h : 0 < f x
⊢ HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x

Tactic:
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp_hasFDerivWithinAt x
  (hf.prod hg)

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem id_tensor_rightUnitor_inv (X Y : C) : 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ _).inv ≫ (α_ _ _ _).hom

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invUnitsSub_mul_sub (u : Rˣ) : invUnitsSub u * (C R u - X) = 1

Proof state:
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ invUnitsSub u * ((C R) ↑u - X) = 1

Tactic:
simp [mul_sub, sub_sub_cancel]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.iUnion {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} (hyp : ∀ n, IndepSets (s n) s' κ μ) :
    IndepSets (⋃ n, s n) s' κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋃ n, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rw [Set.mem_iUnion] at ht1

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : ∃ i, t1 ∈ s i
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : ∃ i, t1 ∈ s i
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
obtain ⟨n, ht1⟩ := ht1

Result:
case intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
case intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht2 : t2 ∈ s'
n : ι
ht1 : t1 ∈ s n
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact hyp n t1 t2 ht1 ht2

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
⊢ IndepSets (⋃ n, s n) s' κ μ

Tactic:
intro t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋃ n, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : ℕ) (s : Finset (Fin (k + l)))
    (hs : s.card = l) (x y : E) :
    ‖p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y‖₊ ≤
      ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤
    (‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊

Tactic:
apply ContinuousMultilinearMap.le_of_opNNNorm_le

Result:
case h
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖(p.changeOriginSeriesTerm k l s hs) fun x_1 => x‖₊ ≤ ‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k

Tactic:
rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]

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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤
    (‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊

Proof state:
case h
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ ‖(p.changeOriginSeriesTerm k l s hs) fun x_1 => x‖₊ ≤ ‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊

Tactic:
apply ContinuousMultilinearMap.le_opNNNorm

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
@[simp]
lemma TensorProduct.equivFinsuppOfBasisRight_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) =
    (𝒞.repr n).mapRange (· • m) (zero_smul _ _)

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
⊢ (equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n) = Finsupp.mapRange (fun x => x • m) ⋯ (𝒞.repr n)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
a✝ : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x => x • m) ⋯ (𝒞.repr n)) a✝

Proof state:
case h
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
a✝ : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x => x • m) ⋯ (𝒞.repr n)) a✝

Tactic:
simp [equivFinsuppOfBasisRight]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_redundant_pair (f : α → β → (σ × σ) → (σ × σ) × γ)
    (h : ∀ x y s, let s' := (f x y (s, s)).fst; s'.fst = s'.snd) :
    (mapAccumr₂ f xs ys (s, s)).snd = (mapAccumr₂ (fun x y (s : σ) =>
      (f x y (s, s) |>.fst.fst, f x y (s, s) |>.snd)
    ) xs ys s).snd :=
  mapAccumr₂_bisim_tail <| by
    use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
    simp_all

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ (fun x s =>
        match x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s)
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (fun x s =>
            match x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s)
          s q →
        (fun x s =>
              match x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s)
            (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
          (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ ∃ R,
    R (s, s) s ∧
      ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
        R s q →
          R (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
            (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2

Tactic:
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ × σ → (σ × σ) × γ
h :
  ∀ (x : α) (y : β) (s : σ),
    let s' := (f x y (s, s)).1;
    s'.1 = s'.2
⊢ (fun x s =>
        match x with
        | (s₁, s₂) => s₂ = s ∧ s₁ = s)
      (s, s) s ∧
    ∀ {s : σ × σ} {q : σ} (a : α) (b : β),
      (fun x s =>
            match x with
            | (s₁, s₂) => s₂ = s ∧ s₁ = s)
          s q →
        (fun x s =>
              match x with
              | (s₁, s₂) => s₂ = s ∧ s₁ = s)
            (f a b s).1 ((f a b (q, q)).1.1, (f a b (q, q)).2).1 ∧
          (f a b s).2 = ((f a b (q, q)).1.1, (f a b (q, q)).2).2
-- Mathlib/Order/Filter/Lift.lean
theorem lift_iInf_of_directed [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β}
    (hf : Directed (· ≥ ·) f) (hg : Monotone g) : (iInf f).lift g = ⨅ i, (f i).lift g :=
  lift_iInf_le.antisymm fun s => by
    simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]
    exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 => x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g

Tactic:
simp only [mem_lift_sets hg, exists_imp, and_imp, mem_iInf_of_directed hf]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 => x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ i, (f i).lift g

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hf : Directed (fun x1 x2 => x1 ≥ x2) f
hg : Monotone g
s : Set β
⊢ ∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ i, (f i).lift g

Tactic:
exact fun t i ht hs => mem_iInf_of_mem i <| mem_lift ht hs

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma exists_mem_toTriangle {x y : α ⊕ β ⊕ γ} (hxy : (graph t).Adj x y) :
    ∃ z ∈ t, x ∈ toTriangle z ∧ y ∈ toTriangle z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
⊢ ∃ z ∈ t, x ∈ toTriangle z ∧ y ∈ toTriangle z

Tactic:
cases hxy <;> exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝¹ : α
b✝ : β
c✝ : γ
a✝ : (a✝¹, b✝, c✝) ∈ t
⊢ in₂ c✝ ∈ toTriangle (a✝¹, b✝, c✝) ∧ in₁ b✝ ∈ toTriangle (a✝¹, b✝, c✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ZMod/QuotientGroup.lean
lemma quotientEquivSigmaZMod_apply (q : orbitRel.Quotient (zpowers g) (G ⧸ H)) (k : ℤ) :
    quotientEquivSigmaZMod H g (g ^ k • q.out) = ⟨q, k⟩

Proof state:
G : Type u_3
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ℤ
⊢ (H.quotientEquivSigmaZMod g) (g ^ k • Quotient.out q) = ⟨q, ↑k⟩

Tactic:
rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_intCast,
  zpow_smul_mod_minimalPeriod]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_inter_distrib (s t : Finset α) : (s ∩ t).filter p = s.filter p ∩ t.filter p

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t

Tactic:
ext

Result:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p (s ∩ t) ↔ a✝ ∈ filter p s ∩ filter p t

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p (s ∩ t) ↔ a✝ ∈ filter p s ∩ filter p t

Tactic:
simp [mem_filter, mem_inter, and_assoc]

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem hasBasis_nhds_of_ne_zero {x : Γ₀} (h : x ≠ 0) :
    HasBasis (𝓝 x) (fun _ : Unit => True) fun _ => {x}

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (pure x).HasBasis (fun x => True) fun x_1 => {x}

Tactic:
exact hasBasis_pure _

Result:
no goals

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (𝓝 x).HasBasis (fun x => True) fun x_1 => {x}

Tactic:
rw [nhds_of_ne_zero h]

Result:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (pure x).HasBasis (fun x => True) fun x_1 => {x}