harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet_iff_iIndepSets_singleton {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω}
    {μ : Measure α} {f : ι → Set Ω} (hf : ∀ i, MeasurableSet (f i)) :
    iIndepSet f κ μ ↔ iIndepSets (fun i ↦ {f i}) κ μ :=
  ⟨iIndep.iIndepSets fun _ ↦ rfl,
    iIndepSets.iIndep _ (fun i ↦ generateFrom_le <| by rintro t (rfl : t = _); exact hf _) _
      (fun _ ↦ IsPiSystem.singleton _) fun _ ↦ rfl⟩

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ ∀ t ∈ {f i}, MeasurableSet t

Tactic:
rintro t (rfl : t = _)

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ MeasurableSet (f i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
i : ι
⊢ MeasurableSet (f i)

Tactic:
exact hf _

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp] lemma add_eq_bot : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Proof state:
α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem compLinearMap_injective (f : ∀ i, M₁ i →ₗ[R] M₁' i) (hf : ∀ i, Surjective (f i)) :
    Injective fun g : MultilinearMap R M₁' M₂ => g.compLinearMap f := fun g₁ g₂ h =>
  ext fun x => by
    simpa [fun i => surjInv_eq (hf i)]
      using MultilinearMap.ext_iff.mp h fun i => surjInv (hf i) (x i)

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
M₁' : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ⇑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g => g.compLinearMap f) g₁ = (fun g => g.compLinearMap f) g₂
x : (i : ι) → M₁' i
⊢ g₁ x = g₂ x

Tactic:
simpa [fun i => surjInv_eq (hf i)]
  using MultilinearMap.ext_iff.mp h fun i => surjInv (hf i) (x i)

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem irreducible_aux (f g : Polynomial (FixedPoints.subfield G F)) (hf : f.Monic) (hg : g.Monic)
    (hfg : f * g = minpoly G F x) : f = 1 ∨ g = 1

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
⊢ f ∣ f * g

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ f = 1 ∨ g = 1

Tactic:
have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
⊢ f = 1 ∨ g = 1

Proof state:
case inl
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ f = 1 ∨ g = 1

Tactic:
right

Result:
case inl.h
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
f g : Polynomial ↥(subfield G F)
hf : f.Monic
hg : g.Monic
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (subfield G F).subtype x f = 0
⊢ g = 1
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_deleteEdges (s : Set (Sym2 V)) : (G.deleteEdges s).edgeSet = G.edgeSet \ s

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ (G.deleteEdges s).edgeSet = G.edgeSet \ s

Tactic:
simp [deleteEdges]

Result:
no goals
-- Mathlib/RingTheory/CotangentLocalizationAway.lean
@[simp]
lemma compLocalizationAwayAlgHom_toAlgHom_toComp (x : P.Ring) :
    compLocalizationAwayAlgHom T g P (((localizationAway g (S := T)).toComp P).toAlgHom x) =
      algebraMap P.Ring _ x

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S
x : P.Ring
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway g).toComp P).toAlgHom x) =
    (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) x

Tactic:
simp only [toComp_toAlgHom, Ideal.mem_comap, RingHom.mem_ker, compLocalizationAwayAlgHom, comp,
  localizationAway, AlgHom.toRingHom_eq_coe, aeval_rename,
  Sum.elim_comp_inr, ← IsScalarTower.toAlgHom_apply (R := R), ← comp_aeval_apply,
  aeval_X_left_apply]

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem strictConvex_closedBall [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) :
    StrictConvex 𝕜 (closedBall x r)

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
rw [← vadd_closedBall_zero]

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (x +ᵥ closedBall 0 r)

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
exact (subsingleton_closedBall x hr).strictConvex

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (x +ᵥ closedBall 0 r)

Tactic:
exact (StrictConvexSpace.strictConvex_closedBall r hr).vadd _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
rcases le_or_lt r 0 with hr | hr

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem bot_rel_eq_leftRel (H : Subgroup G) :
    ⇑(setoid ↑(⊥ : Subgroup G) ↑H) = ⇑(QuotientGroup.leftRel H)

Proof state:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H

Tactic:
constructor

Result:
case h.h.a.mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H

case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2 ∈ ⊥, ∃ b_1 ∈ H, b = a_2 * a * b_1

Proof state:
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H

Tactic:
rwa [one_mul, inv_mul_cancel_left]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = 1 * a * (a⁻¹ * b)

Tactic:
rw [one_mul, mul_inv_cancel_left]

Result:
no goals

Proof state:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑⊥ ↑H) a b ↔ (QuotientGroup.leftRel H) a b

Tactic:
rw [rel_iff, QuotientGroup.leftRel_apply]

Result:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H

Proof state:
case h.h.a.mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H

Tactic:
rintro ⟨a, rfl : a = 1, b, hb, rfl⟩

Result:
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⇑(setoid ↑⊥ ↑H) = ⇑(QuotientGroup.leftRel H)

Tactic:
ext a b

Result:
case h.h.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (setoid ↑⊥ ↑H) a b ↔ (QuotientGroup.leftRel H) a b

Proof state:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1

Tactic:
exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩

Result:
no goals

Proof state:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2 ∈ ⊥, ∃ b_1 ∈ H, b = a_2 * a * b_1

Tactic:
rintro (h : a⁻¹ * b ∈ H)

Result:
case h.h.a.mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1
-- Mathlib/NumberTheory/Pell.lean
theorem d_nonsquare_of_one_lt_x {a : Solution₁ d} (ha : 1 < a.x) : ¬IsSquare d

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ ¬IsSquare d

Tactic:
have hp := a.prop

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hp : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ ¬IsSquare d

Proof state:
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x ^ 2 - b * b * a.y ^ 2 = 1
⊢ False

Tactic:
simp_rw [← sq, ← mul_pow, sq_sub_sq, Int.mul_eq_one_iff_eq_one_or_neg_one] at hp

Result:
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1
⊢ False

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hp : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ ¬IsSquare d

Tactic:
rintro ⟨b, rfl⟩

Result:
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x ^ 2 - b * b * a.y ^ 2 = 1
⊢ False

Proof state:
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1
⊢ False

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_reverse (a : α) (l : List α) : count a l.reverse = count a l

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ count a l.reverse = count a l

Tactic:
simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
@[simp]
lemma IsLittleOTVS.zero (g : α → F) (l : Filter α) : (0 : α → E) =o[𝕜;l] g

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
g : α → F
l : Filter α
⊢ 0 =o[𝕜;l] g

Tactic:
intros U hU

Result:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
g : α → F
l : Filter α
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (0 x) ≤ ↑ε * egauge 𝕜 V (g x)

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
g : α → F
l : Filter α
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (0 x) ≤ ↑ε * egauge 𝕜 V (g x)

Tactic:
simpa [egauge_zero_right _ (Filter.nonempty_of_mem hU)] using ⟨univ, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
g : α → F
l : Filter α
U : Set E
hU : U ∈ 𝓝 0
⊢ univ ∈ 𝓝 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_pow {p a : α} (hp : Prime p) {k : ℕ} :
    emultiplicity p (a ^ k) = k * emultiplicity p a

Proof state:
case succ
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
k : ℕ
hk : emultiplicity p (a ^ k) = ↑k * emultiplicity p a
⊢ emultiplicity p (a ^ (k + 1)) = ↑(k + 1) * emultiplicity p a

Tactic:
simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
⊢ emultiplicity p (a ^ 0) = ↑0 * emultiplicity p a

Tactic:
simp [emultiplicity_of_one_right hp.not_unit]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
k : ℕ
⊢ emultiplicity p (a ^ k) = ↑k * emultiplicity p a

Tactic:
induction' k with k hk

Result:
case zero
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
⊢ emultiplicity p (a ^ 0) = ↑0 * emultiplicity p a

case succ
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
k : ℕ
hk : emultiplicity p (a ^ k) = ↑k * emultiplicity p a
⊢ emultiplicity p (a ^ (k + 1)) = ↑(k + 1) * emultiplicity p a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevInTwo'_snd (l : { l : List α // l.length = n }) :
    (splitRevInTwo' l).2 = ⟨(splitInTwo ⟨l.1.reverse, by simpa using l.2⟩).1.1.reverse, by simp; omega⟩

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ ⟨drop (n / 2) l.val, ⋯⟩ = ⟨drop (l.val.reverse.length - (n + 1) / 2) l.val, ⋯⟩

Tactic:
congr 2

Result:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ n / 2 = l.val.reverse.length - (n + 1) / 2

Proof state:
α : Type ?u.41771
n : Nat
l : { l // l.length = n }
⊢ (splitInTwo ⟨l.val.reverse, ⋯⟩).fst.val.reverse.length = (n + 1) / 2

Tactic:
simp

Result:
α : Type ?u.41771
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) l.val.length = (n + 1) / 2

Proof state:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ (splitRevInTwo' l).snd = ⟨(splitInTwo ⟨l.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩

Tactic:
simp only [splitRevInTwo', splitRevAt_eq, reverse_take, splitInTwo_fst, reverse_reverse]

Result:
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ ⟨drop (n / 2) l.val, ⋯⟩ = ⟨drop (l.val.reverse.length - (n + 1) / 2) l.val, ⋯⟩

Proof state:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ n / 2 = l.val.reverse.length - (n + 1) / 2

Tactic:
simp

Result:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ n / 2 = l.val.length - (n + 1) / 2

Proof state:
α : Type ?u.41771
n : Nat
l : { l // l.length = n }
⊢ min ((n + 1) / 2) l.val.length = (n + 1) / 2

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.41771
n : Nat
l : { l // l.length = n }
⊢ l.val.reverse.length = ?m.41820

Tactic:
simpa using l.2

Result:
no goals

Proof state:
case e_val.e_a
α : Type u_1
n : Nat
l : { l // l.length = n }
⊢ n / 2 = l.val.length - (n + 1) / 2

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    k ∈ m.keys ↔ k ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ k ∈ m.keys ↔ k ∈ m

Tactic:
rw [mem_iff_contains]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ k ∈ m.keys ↔ m.contains k = true

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ k ∈ m.keys ↔ m.contains k = true

Tactic:
simp_to_raw using Raw₀.mem_keys ⟨m, _⟩ h

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem ext_of_direction_eq {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction)
    (hn : ((s₁ : Set P) ∩ s₂).Nonempty) : s₁ = s₂

Proof state:
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₁.direction

Tactic:
rw [hd]

Result:
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₂.direction

Proof state:
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₁
⊢ (p -ᵥ hn.some) +ᵥ hn.some ∈ s₂

Tactic:
refine vadd_mem_of_mem_direction ?_ hq2

Result:
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₁
⊢ p -ᵥ hn.some ∈ s₂.direction
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_fn_integral_sub ⦃f g : α × β → E⦄ (F : E → E') (hf : Integrable f (μ.prod ν))
    (hg : Integrable g (μ.prod ν)) :
    (∫ x, F (∫ y, f (x, y) - g (x, y) ∂ν) ∂μ) =
      ∫ x, F ((∫ y, f (x, y) ∂ν) - ∫ y, g (x, y) ∂ν) ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ =
    ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ

Tactic:
refine integral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν)

Proof state:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν - ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
simp [integral_sub h2f h2g]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem pullbackZeroZeroIso_inv_fst (X Y : C) [HasBinaryProduct X Y] :
    (pullbackZeroZeroIso X Y).inv ≫ pullback.fst 0 0 = prod.fst

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.fst 0 0 = prod.fst

Tactic:
dsimp [pullbackZeroZeroIso]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.fst 0 0 =
    prod.fst

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd ⋯,
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.fst 0 0 =
    prod.fst

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
    (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
    ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
      ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n

Tactic:
simpa using hf.uniform_geometric_approx' h

Result:
no goals