harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem const_lintegral (c : ℝ≥0∞) : (const α c).lintegral μ = c * μ univ

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ ((fun x => c) ⁻¹' {c}) = c * μ univ

Tactic:
rw [preimage_const_of_mem (mem_singleton c)]

Result:
no goals

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : IsEmpty α
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Tactic:
simp [μ.eq_zero_of_isEmpty]

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ (Function.const α c ⁻¹' {c}) = c * μ univ

Tactic:
unfold Function.const

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ ((fun x => c) ⁻¹' {c}) = c * μ univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : IsEmpty α
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Tactic:
simp only [range_const, coe_const, Finset.sum_singleton]

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ (Function.const α c ⁻¹' {c}) = c * μ univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ (const α c).lintegral μ = c * μ univ

Tactic:
rw [lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ
-- Mathlib/Data/List/Zip.lean
theorem unzip_swap (l : List (α × β)) : unzip (l.map Prod.swap) = (unzip l).swap

Proof state:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map Prod.swap l).unzip = l.unzip.swap

Tactic:
simp only [unzip_eq_map, map_map]

Result:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nat_tsum (f : ℕ → ℝ≥0∞) :
    Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' n, f n))

Proof state:
f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)

Tactic:
exact ENNReal.summable.hasSum

Result:
no goals

Proof state:
f : ℕ → ℝ≥0∞
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
rw [← hasSum_iff_tendsto_nat]

Result:
f : ℕ → ℝ≥0∞
⊢ HasSum f (∑' (n : ℕ), f n)
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_intCast (n : ℤ) : norm (n : ℤ√d) = n * n

Proof state:
d n : ℤ
⊢ (↑n).norm = n * n

Tactic:
simp [norm]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem fourierIntegral_fderiv
    (hf : Integrable f) (h'f : Differentiable ℝ f) (hf' : Integrable (fderiv ℝ f)) :
    𝓕 (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) volume
⊢ 𝓕 (fderiv ℝ f) = fourierSMulRight (-(innerSL ℝ).flip) (𝓕 f)

Tactic:
exact VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) volume
⊢ 𝓕 (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)

Tactic:
rw [← innerSL_real_flip V]

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
hf : Integrable f volume
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) volume
⊢ 𝓕 (fderiv ℝ f) = fourierSMulRight (-(innerSL ℝ).flip) (𝓕 f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem size_ne_zero_of_mem {a : α} {l : Vector α n} (h : a ∈ l) : n ≠ 0

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ?m.107286 ∈ l

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : a ∈ l
⊢ n ≠ 0

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ l.size ≠ 0

Proof state:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ l.size ≠ 0

Tactic:
simpa using Array.ne_empty_of_mem (by simpa using h)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
lemma degree_X_add_C [Nontrivial R]
    {ι : Type*} (m : MonomialOrder ι) (i : ι) (r : R) :
    m.degree (X i + C r) = single i 1

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (single i 1) ≠ m.toSyn 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ 0 < m.toSyn (single i 1)

Tactic:
rw [← bot_eq_zero, bot_lt_iff_ne_bot, bot_eq_zero, ← map_zero m.toSyn]

Result:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (single i 1) ≠ m.toSyn 0

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.degree (X i + C r) = single i 1

Tactic:
rw [degree_add_of_lt, degree_X]

Result:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Tactic:
simp only [degree_C, map_zero, degree_X]

Result:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ 0 < m.toSyn (single i 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_append {p : α → Prop} {l₁ : Vector α n} {l₂ : Vector α m} :
    (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x)

Proof state:
α : Type u_1
n m : Nat
p : α → Prop
l₁ : Vector α n
l₂ : Vector α m
⊢ (∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
simp only [mem_append, or_imp, forall_and]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem _root_.ZFSet.isOrdinal_iff_isTrichotomous :
    x.IsOrdinal ↔ x.IsTransitive ∧ IsTrichotomous _ (Subrel (· ∈ ·) (· ∈ x)) where
  mp h := ⟨h.isTransitive, h.isTrichotomous⟩
  mpr

Proof state:
case intro.inr.inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
y z : { x_1 // x_1 ∈ x }
hyz : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) z y
⊢ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y y

Tactic:
cases asymm hyz hzw

Result:
no goals

Proof state:
x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsOrdinal

Proof state:
case intro.inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
y z w : { x_1 // x_1 ∈ x }
hyz : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) z w
hyw : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y w
⊢ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y w

Tactic:
exact hyw

Result:
no goals

Proof state:
case intro.inr.inr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
y z w : { x_1 // x_1 ∈ x }
hyz : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) z w
hwy : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) w y
⊢ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y w

Tactic:
cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

Result:
no goals

Proof state:
case intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsOrdinal

Tactic:
rw [isOrdinal_iff_isTrans]

Result:
case intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)

Proof state:
case intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)

Tactic:
refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩

Result:
case intro
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsTrichotomous { x_1 // x_1 ∈ x } (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
y z w : { x_1 // x_1 ∈ x }
hyz : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) z w
⊢ Subrel (fun x1 x2 => x1 ∈ x2) (fun x_1 => x_1 ∈ x) y w
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
theorem prod_map_le_prod_map₀ {ι : Type*} {s : Multiset ι} (f : ι → R) (g : ι → R)
    (h0 : ∀ i ∈ s, 0 ≤ f i) (h : ∀ i ∈ s, f i ≤ g i) :
    (map f s).prod ≤ (map g s).prod

Proof state:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
s : Multiset ι
f g : ι → R
h0 : ∀ i ∈ s, 0 ≤ f i
h : ∀ i ∈ s, f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
cases s using Quotient.ind

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ i ∈ ⟦a✝⟧, 0 ≤ f i
h : ∀ i ∈ ⟦a✝⟧, f i ≤ g i
⊢ (map f ⟦a✝⟧).prod ≤ (map g ⟦a✝⟧).prod

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ i ∈ ⟦a✝⟧, 0 ≤ f i
h : ∀ i ∈ ⟦a✝⟧, f i ≤ g i
⊢ (map f ⟦a✝⟧).prod ≤ (map g ⟦a✝⟧).prod

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ i ∈ a✝, 0 ≤ f i
h : ∀ i ∈ a✝, f i ≤ g i
⊢ (List.map f a✝).prod ≤ (List.map g a✝).prod

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a✝ : List ι
h0 : ∀ i ∈ a✝, 0 ≤ f i
h : ∀ i ∈ a✝, f i ≤ g i
⊢ (List.map f a✝).prod ≤ (List.map g a✝).prod

Tactic:
apply List.prod_map_le_prod_map₀ f g h0 h

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedCommAux_comp_gradedCommAux :
    gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id

Proof state:
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
⊢ gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜 = LinearMap.id

Tactic:
ext i a b

Result:
case H.a.h.h.w
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (((AlgebraTensorModule.curry
            ((gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜) ∘ₗ lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i))
          a)
        b)
      i✝ =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i)) a) b) i✝

Proof state:
case H.a.h.h.w
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ ((gradedCommAux R 𝒜 ℬ) ((gradedCommAux R ℬ 𝒜) ((lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)))) i✝ =
    ((lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)) i✝

Tactic:
rw [gradedCommAux_lof_tmul, LinearMap.map_smul_of_tower, gradedCommAux_lof_tmul, smul_smul,
  mul_comm i.2 i.1, Int.units_mul_self, one_smul]

Result:
no goals

Proof state:
case H.a.h.h.w
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ (((AlgebraTensorModule.curry
            ((gradedCommAux R 𝒜 ℬ ∘ₗ gradedCommAux R ℬ 𝒜) ∘ₗ lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i))
          a)
        b)
      i✝ =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i)) a) b) i✝

Tactic:
dsimp

Result:
case H.a.h.h.w
R : Type u_1
ι : Type u_2
inst✝⁷ : CommSemiring ι
inst✝⁶ : Module ι (Additive ℤˣ)
inst✝⁵ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁴ : CommRing R
inst✝³ : (i : ι) → AddCommGroup (𝒜 i)
inst✝² : (i : ι) → AddCommGroup (ℬ i)
inst✝¹ : (i : ι) → Module R (𝒜 i)
inst✝ : (i : ι) → Module R (ℬ i)
i : ι × ι
a : ℬ i.1
b : 𝒜 i.2
i✝ : ι × ι
⊢ ((gradedCommAux R 𝒜 ℬ) ((gradedCommAux R ℬ 𝒜) ((lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)))) i✝ =
    ((lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)) i✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_eq_mkVector_iff {l₁ : Vector α n} {l₂ : Vector α m} {a : α} :
    l₁ ++ l₂ = mkVector (n + m) a ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

Proof state:
α : Type u_1
n m : Nat
l₁ : Vector α n
l₂ : Vector α m
a : α
⊢ l₁ ++ l₂ = mkVector (n + m) a ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

Tactic:
simp [← toArray_inj, Array.append_eq_mkArray_iff]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_zsmul_sub_self (a b : α) : toIcoDiv hp a b • p - b = -toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b

Tactic:
rw [toIcoMod, neg_sub]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem zero_mul (b : R) : 0 * b = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 * b = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/RetractArgument.lean
lemma llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts
    [HasFactorization W₁ W₂] [W₁.IsStableUnderRetracts] (h₁ : W₁ ≤ W₂.llp) :
    W₂.llp = W₁ :=
  le_antisymm (fun A B i hi ↦ by
    have h := factorizationData W₁ W₂ i
    have := hi _ h.hp
    simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi) h₁

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
this : HasLiftingProperty i h.p
⊢ W₁ i

Tactic:
simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
⊢ W₁ i

Tactic:
have h := factorizationData W₁ W₂ i

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
⊢ W₁ i

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
⊢ W₁ i

Tactic:
have := hi _ h.hp

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
h : W₁.MapFactorizationData W₂ i
this : HasLiftingProperty i h.p
⊢ W₁ i
-- Mathlib/Tactic/CategoryTheory/Reassoc.lean
theorem eq_whisker' {X Y : C} {f g : X ⟶ Y} (w : f = g) {Z : C} (h : Y ⟶ Z) :
    f ≫ h = g ≫ h

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=
  Complex.ext_iff.2 <| by simp [two_mul, ofReal]

Proof state:
z : ℂ
⊢ (z + (starRingEnd ℂ) z).re = (↑(2 * z.re)).re ∧ (z + (starRingEnd ℂ) z).im = (↑(2 * z.re)).im

Tactic:
simp [two_mul, ofReal]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_irrefl {f : CauSeq α abs} : ¬f < f
  | h => not_limZero_of_pos h (by simp [zero_limZero])

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f : CauSeq α abs
x✝ : f < f
h : f < f := x✝
⊢ (f - f).LimZero

Tactic:
simp [zero_limZero]

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem unshift_shift {p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F} :
    (p.unshift z).shift = p

Proof state:
case h
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (p n)).curryRight = p n

Tactic:
exact LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

Result:
no goals

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
⊢ (p.unshift z).shift = p

Tactic:
ext1 n

Result:
case h
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ (p.unshift z).shift n = p n

Proof state:
case h
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ (p.unshift z).shift n = p n

Tactic:
simp [shift, unshift]

Result:
case h
𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
n : ℕ
⊢ ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (p n)).curryRight = p n
-- Mathlib/Computability/Tape.lean
theorem ListBlank.append_mk {Γ} [Inhabited Γ] (l₁ l₂ : List Γ) :
    ListBlank.append l₁ (ListBlank.mk l₂) = ListBlank.mk (l₁ ++ l₂)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l₁ l₂ : List Γ
⊢ append l₁ (mk l₂) = mk (l₁ ++ l₂)

Tactic:
induction l₁ <;>
  simp only [*, ListBlank.append, List.nil_append, List.cons_append, ListBlank.cons_mk]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem remainder_lt' (n : ℕ) {m : ℝ} (m1 : 1 < m) :
    remainder m n < (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) :=
  -- two useful inequalities
  have m0 : 0 < m := zero_lt_one.trans m1
  have mi : 1 / m < 1 := (div_lt_one m0).mpr m1
  -- to show the strict inequality between these series, we prove that:
  calc
    (∑' i, 1 / m ^ (i + (n + 1))!) < ∑' i, 1 / m ^ (i + (n + 1)!) :=
        -- 1. the second series dominates the first
        tsum_lt_tsum (fun b => one_div_pow_le_one_div_pow_of_le m1.le
          (b.add_factorial_succ_le_factorial_add_succ n))
        -- 2. the term with index `i = 2` of the first series is strictly smaller than
        -- the corresponding term of the second series
        (one_div_pow_strictAnti m1 (n.add_factorial_succ_lt_factorial_add_succ (i := 2) le_rfl))
        -- 3. the first series is summable
        (remainder_summable m1 n)
        -- 4. the second series is summable, since its terms grow quickly
        (summable_one_div_pow_of_le m1 fun _ => le_self_add)
    -- split the sum in the exponent and massage
    _ = ∑' i : ℕ, (1 / m) ^ i * (1 / m ^ (n + 1)!)

Proof state:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ ∑' (i : ℕ), 1 / m ^ (i + (n + 1)!) = ∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!)

Tactic:
simp only [pow_add, one_div, mul_inv, inv_pow]

Result:
no goals

Proof state:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ 0 ≤ 1 / m

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)

Tactic:
rw [tsum_geometric_of_lt_one (by positivity) mi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ k = 0 ∨ l = []

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ take k l = [] ↔ k = 0 ∨ l = []

Tactic:
cases l <;> cases k <;> simp [Nat.succ_ne_zero]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem kerLift_injective : Function.Injective (kerLift f) :=
  lift_injective_of_ker_le_ideal (ker f) (fun a => by simp only [mem_ker, imp_self]) le_rfl

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
a : R
⊢ a ∈ ker f → f a = 0

Tactic:
simp only [mem_ker, imp_self]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuation_of_algebraMap (r : R) : v.valuation K r = v.intValuation r

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ (valuation K v) ↑r = v.intValuation r

Tactic:
rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]

Result:
no goals