harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem add_left' (f f' g : α →₂[μ] E) : ⟪f + f', g⟫ = inner f g + inner f' g

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
⊢ ∫ (a : α), inner (↑↑(f + f') a) (↑↑g a) ∂μ = ∫ (a : α), inner (↑↑f a + ↑↑f' a) (↑↑g a) ∂μ

Tactic:
refine integral_congr_ae ((coeFn_add f f').mono fun x hx => ?_)

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ (fun a => inner (↑↑(f + f') a) (↑↑g a)) x = (fun a => inner (↑↑f a + ↑↑f' a) (↑↑g a)) x

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
⊢ inner (f + f') g = inner f g + inner f' g

Tactic:
simp_rw [inner_def, ← integral_add (integrable_inner (𝕜 := 𝕜) f g) (integrable_inner f' g),
  ← inner_add_left]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
⊢ ∫ (a : α), inner (↑↑(f + f') a) (↑↑g a) ∂μ = ∫ (a : α), inner (↑↑f a + ↑↑f' a) (↑↑g a) ∂μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ (fun a => inner (↑↑(f + f') a) (↑↑g a)) x = (fun a => inner (↑↑f a + ↑↑f' a) (↑↑g a)) x

Tactic:
simp only [hx, Pi.add_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
lemma cPolynomialAt : CPolynomialAt 𝕜 f x :=
  f.hasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
    (by simp only [Metric.emetric_ball_top, Set.mem_univ])

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
x : (i : ι) → E i
⊢ x ∈ EMetric.ball 0 ⊤

Tactic:
simp only [Metric.emetric_ball_top, Set.mem_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem IsHermitian.fromBlocks₂₂ [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜)
    {D : Matrix n n 𝕜} (hD : D.IsHermitian) :
    (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
convert IsHermitian.fromBlocks₁₁ _ _ hD <;> simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian

Tactic:
rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
  fromBlocks_submatrix_sum_swap_sum_swap]

Result:
m : Type u_2
n : Type u_3
𝕜 : Type u_5
inst✝³ : CommRing 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m m 𝕜
B : Matrix m n 𝕜
D : Matrix n n 𝕜
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_uIcc : #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))

Tactic:
exact card_Icc _ _

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ f.support ∪ g.support, #(uIcc (f i) (g i))

Tactic:
rw [← support_inf_union_support_sup]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_inl_inl (i j : Q.rels) :
    aeval (Sum.elim X (MvPolynomial.C ∘ P.val))
      ((Q.comp P).jacobiMatrix (Sum.inl j) (Sum.inl i)) = Q.jacobiMatrix j i

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).jacobiMatrix (Sum.inl j) (Sum.inl i)) = Q.jacobiMatrix j i

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply, comp_map, Sum.elim_inl,
  ← Q.comp_aeval_relation_inl P.toPresentation]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((pderiv (Sum.inl (Q.map j))) ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P.toPresentation).relation (Sum.inl i)))

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : DecidableEq Q.rels
inst✝ : Fintype Q.rels
i j : Q.rels
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((pderiv (Sum.inl (Q.map j))) ((Q.comp P).relation (Sum.inl i))) =
    (pderiv (Q.map j)) ((aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P.toPresentation).relation (Sum.inl i)))

Tactic:
apply aeval_sumElim_pderiv_inl

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma Monotone.frequently_ge_map_of_frequently_ge {f : R → S} (f_incr : Monotone f)
    {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) :
    ∃ᶠ x' in F.map f, f l ≤ x'

Proof state:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
⊢ z < l

Tactic:
by_contra con

Result:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
con : ¬z < l
⊢ False

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, ¬(fun x' => f l ≤ x') x
⊢ ∀ᶠ (x : R) in F, ¬(fun x => l ≤ x) x

Tactic:
simp only [not_le, not_lt] at ev freq_ge ⊢

Result:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
⊢ ∀ᶠ (x : R) in F, x < l

Proof state:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
con : ¬z < l
⊢ False

Tactic:
exact lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
⊢ ∀ᶠ (x : R) in F, x < l

Tactic:
filter_upwards [ev] with z hz

Result:
case h
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
⊢ z < l

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
⊢ ∃ᶠ (x' : S) in map f F, f l ≤ x'

Tactic:
refine fun ev ↦ freq_ge ?_

Result:
R : Type u_6
S : Type u_7
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, ¬(fun x' => f l ≤ x') x
⊢ ∀ᶠ (x : R) in F, ¬(fun x => l ≤ x) x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) :
    Option.map (cast h) x = cast (congrArg Option h) x

Proof state:
γ γ' : Type u
h : γ = γ'
x : Option γ
⊢ Option.map (cast h) x = cast ⋯ x

Tactic:
cases h

Result:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x

Proof state:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma not_top_le_coe (a : α) : ¬ ⊤ ≤ (a : WithTop α)

Proof state:
α : Type u_1
inst✝ : LE α
a : α
⊢ ¬⊤ ≤ ↑a

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f.toBasis.orientation) :
    e.toBasis.det = -f.toBasis.det

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = -f.toBasis.det

Tactic:
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h,
  neg_one_smul ℝ (M := E [⋀^ι]→ₗ[ℝ] ℝ)]

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det = -f.toBasis.det

Tactic:
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f.toBasis • f.toBasis.det = -f.toBasis.det
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_mulVec_assoc [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α]
    (a : R) (A : Matrix m n α) (b : n → α) : (a • A) *ᵥ b = a • A *ᵥ b

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
A : Matrix m n α
b : n → α
x✝ : m
⊢ ((a • A) *ᵥ b) x✝ = (a • A *ᵥ b) x✝

Tactic:
apply smul_dotProduct

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
A : Matrix m n α
b : n → α
⊢ (a • A) *ᵥ b = a • A *ᵥ b

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
A : Matrix m n α
b : n → α
x✝ : m
⊢ ((a • A) *ᵥ b) x✝ = (a • A *ᵥ b) x✝
-- Mathlib/Data/Set/Insert.lean
theorem pair_eq_pair_iff {x y z w : α} :
    ({x, y} : Set α) = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Proof state:
α : Type u
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
x y z w : α
⊢ {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp [subset_antisymm_iff, insert_subset_iff]

Result:
α : Type u
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
lemma sumComm_inr : (Diffeomorph.sumComm I M n M') ∘ Sum.inr = Sum.inl

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x✝ : M'
⊢ (⇑(sumComm I M n M') ∘ Sum.inr) x✝ = Sum.inl x✝

Tactic:
exact Sum.swap_inr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
⊢ ⇑(sumComm I M n M') ∘ Sum.inr = Sum.inl

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x✝ : M'
⊢ (⇑(sumComm I M n M') ∘ Sum.inr) x✝ = Sum.inl x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
    zip l₁ l₂ = zip (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
  | [], _ => by simp
  | _, [] => by simp
  | a :: l₁, b :: l₂ => by simp [succ_min_succ, zip_eq_zip_take_min l₁ l₂]

Proof state:
α : Type u_1
β : Type u_2
x✝ : List β
⊢ [].zip x✝ = (take (min [].length x✝.length) []).zip (take (min [].length x✝.length) x✝)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
l₁ : List α
b : β
l₂ : List β
⊢ (a :: l₁).zip (b :: l₂) =
    (take (min (a :: l₁).length (b :: l₂).length) (a :: l₁)).zip
      (take (min (a :: l₁).length (b :: l₂).length) (b :: l₂))

Tactic:
simp [succ_min_succ, zip_eq_zip_take_min l₁ l₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : List α
⊢ x✝.zip [] = (take (min x✝.length [].length) x✝).zip (take (min x✝.length [].length) [])

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_sdiv {x y : BitVec w} : (x.sdiv y).toNat =
    match x.msb, y.msb with
    | false, false => (udiv x y).toNat
    | false, true  =>  (- (x.udiv (- y))).toNat
    | true,  false => (- ((- x).udiv y)).toNat
    | true,  true  => ((- x).udiv (- y)).toNat

Proof state:
w : Nat
x y : BitVec w
⊢ (x.sdiv y).toNat =
    match x.msb, y.msb with
    | false, false => (x.udiv y).toNat
    | false, true => (-x.udiv (-y)).toNat
    | true, false => (-(-x).udiv y).toNat
    | true, true => ((-x).udiv (-y)).toNat

Tactic:
simp only [sdiv_eq, toNat_udiv]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
      | false, false => x.udiv y
      | false, true => -x.udiv (-y)
      | true, false => -(-x).udiv y
      | true, true => (-x).udiv (-y)).toNat =
    match x.msb, y.msb with
    | false, false => (x.udiv y).toNat
    | false, true => (-x.udiv (-y)).toNat
    | true, false => (-(-x).udiv y).toNat
    | true, true => ((-x).udiv (-y)).toNat

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
      | false, false => x.udiv y
      | false, true => -x.udiv (-y)
      | true, false => -(-x).udiv y
      | true, true => (-x).udiv (-y)).toNat =
    match x.msb, y.msb with
    | false, false => (x.udiv y).toNat
    | false, true => (-x.udiv (-y)).toNat
    | true, false => (-(-x).udiv y).toNat
    | true, true => ((-x).udiv (-y)).toNat

Tactic:
by_cases h : x.msb <;> by_cases h' : y.msb <;> simp [h, h']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
/-- If the coproduct comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
lemma PreservesColimitPair.of_iso_coprod_comparison [i : IsIso (coprodComparison G X Y)] :
    PreservesColimit (pair X Y) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))

Tactic:
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsIso ((colimit.isColimit (pair (G.obj X) (G.obj Y))).desc (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsIso ((colimit.isColimit (pair (G.obj X) (G.obj Y))).desc (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)))

Tactic:
apply i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))

Tactic:
apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem Filter.HasBasis.uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop}
    {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)}
    (hb : (𝓤 β).HasBasis q t) {f : α → β} :
    UniformContinuous f ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i :=
  (ha.tendsto_iff hb).trans <| by simp only [Prod.forall]

Proof state:
α : Type ua
β : Type ub
ι : Sort u_1
inst✝¹ : UniformSpace α
ι' : Sort u_2
inst✝ : UniformSpace β
p : ι → Prop
s : ι → Set (α × α)
ha : (𝓤 α).HasBasis p s
q : ι' → Prop
t : ι' → Set (β × β)
hb : (𝓤 β).HasBasis q t
f : α → β
⊢ (∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ x ∈ s ia, (f x.1, f x.2) ∈ t ib) ↔
    ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i

Tactic:
simp only [Prod.forall]

Result:
no goals
-- Mathlib/Algebra/Order/Group/OrderIso.lean
theorem OrderIso.mulRight_symm (a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹

Proof state:
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a x : α
⊢ (mulRight a).symm x = (mulRight a⁻¹) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ (mulRight a).symm = mulRight a⁻¹

Tactic:
ext x

Result:
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a x : α
⊢ (mulRight a).symm x = (mulRight a⁻¹) x
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_neg (p : R[X]) : trailingDegree (-p) = trailingDegree p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).trailingDegree = p.trailingDegree

Tactic:
unfold trailingDegree

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.min = p.support.min

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).support.min = p.support.min

Tactic:
rw [support_neg]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_le [LinearOrderedSemiring α] {m n : Num} : (m : α) ≤ n ↔ m ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr cast_lt

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : Num
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : Num
⊢ ¬↑n < ↑m ↔ m ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_self (n : Nat) : n % n = 0

Proof state:
n : Nat
⊢ n % n = 0

Tactic:
rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive add_one_zsmul]
lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
  | .negSucc 0 => by simp [Int.negSucc_eq', Int.add_left_neg]
  | .negSucc (n + 1) => by
    rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]
    rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]
    exact zpow_negSucc _ _

Proof state:
G : Type u_3
inst✝ : Group G
a : G
⊢ a ^ (Int.negSucc 0 + 1) = a ^ Int.negSucc 0 * a

Tactic:
simp [Int.negSucc_eq', Int.add_left_neg]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹

Tactic:
exact zpow_negSucc _ _

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]

Result:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = (a ^ (n + 1))⁻¹

Tactic:
rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]

Result:
G : Type u_3
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (-↑(n + 1)) = (a ^ (n + 1))⁻¹