harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_flatten_eq_none_iff {xs : Vector (Vector α m) n} {p : α → Bool} :
    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x

Proof state:
α : Type
m n : Nat
xs : Vector (Vector α m) n
p : α → Bool
⊢ find? p xs.flatten = none ↔ ∀ (ys : Vector α m), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma Colorable.chromaticNumber_eq_sInf {G : SimpleGraph V} {n} (h : G.Colorable n) :
    G.chromaticNumber = sInf {n' : ℕ | G.Colorable n'}

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})

Tactic:
rw [ENat.coe_sInf, chromaticNumber]

Result:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ {n' | G.Colorable n'}.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
exact ⟨_, h⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem sup [SemilatticeSup β] [ContinuousSup β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f ⊔ g) μ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n ⊔ hg.approx n) n)) < ⊤

Tactic:
refine (measure_mono (support_sup _ _)).trans_lt ?_

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑(hf.approx n) ∪ support ⇑(hg.approx n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊔ g) μ

Tactic:
refine
  ⟨fun n => hf.approx n ⊔ hg.approx n, fun n => ?_, fun x =>
    (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n ⊔ hg.approx n) n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑(hf.approx n) ∪ support ⇑(hg.approx n)) < ⊤

Tactic:
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma integral_le_sum_Ico_of_le
    (hab : a ≤ b) (h : ∀ i ∈ Ico a b, ∀ x ∈ Ico (i : ℝ) (i + 1 : ℕ), g x ≤ f i)
    (hg : IntegrableOn g (Set.Ico a b)) :
    ∫ x in a..b, g x ≤ ∑ i ∈ Finset.Ico a b, f i

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), g x ≤ f ↑i
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∫ (x : ℝ) in ↑a..↑b, g x ≤ ∑ i ∈ Finset.Ico a b, f ↑i

Tactic:
convert neg_le_neg (sum_Ico_le_integral_of_le (f := -f) (g := -g) hab
  (fun i hi x hx ↦ neg_le_neg (h i hi x hx)) hg.neg) <;> simp

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zmodEquivZPowers_apply_coe_nat (i : ℕ) :
    h.zmodEquivZPowers i = Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ)

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

Tactic:
have : (i : ZMod k) = (i : ℤ) := by norm_cast

Result:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
this : ↑i = ↑↑i
⊢ h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ↑i = ↑↑i

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
this : ↑i = ↑↑i
⊢ h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

Tactic:
simp only [this, zmodEquivZPowers_apply_coe_int, zpow_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).size = if k ∈ m then m.size else m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).size = if k ∈ m then m.size else m.size + 1

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).size = if m.contains k = true then m.size else m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).size = if m.contains k = true then m.size else m.size + 1

Tactic:
simp_to_raw using Raw₀.size_insert

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable
    [FiniteDimensional F E] [Algebra.IsSeparable F E]
    (h : LinearIndependent F v) : LinearIndependent F (v · ^ q ^ n)

Proof state:
case h.e'_4.h
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') => b x ^ q ^ n
f : ι → ↑ι' := fun i => ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = ((fun x => b x ^ q ^ n) ∘ f) x✝

Tactic:
simp_rw [Function.comp_apply, b]

Result:
case h.e'_4.h
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') => b x ^ q ^ n
f : ι → ↑ι' := fun i => ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = (Basis.extend h') (f x✝) ^ q ^ n
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma disjoint_fromEdgeSet : Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (s ∩ {e | e.IsDiag})

Tactic:
exact Set.disjoint_left.2 fun e he he' ↦ not_isDiag_of_mem_edgeSet _ he he'.2

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ {e | e.IsDiag} ∪ s ∩ {e | e.IsDiag})

Tactic:
rw [← disjoint_edgeSet,  edgeSet_fromEdgeSet, Set.disjoint_union_right, and_iff_left]

Result:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G.edgeSet (s ∩ {e | e.IsDiag})

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s

Tactic:
conv_rhs => rw [← Set.diff_union_inter s {e : Sym2 V | e.IsDiag}]

Result:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ {e | e.IsDiag} ∪ s ∩ {e | e.IsDiag})
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffine_smul (P : Fin 3 → F) {u : F} (hu : IsUnit u) :
    toAffine W (u • P) = toAffine W P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
  toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]

Result:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z = P x / P z ∧ (u • P) y / (u • P) z = P y / P z

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hPz : P z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (u • P) = toAffine W P

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
⊢ toAffine W (u • P) = toAffine W P

Tactic:
by_cases hP : W.Nonsingular P

Result:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z = P x / P z ∧ (u • P) y / (u • P) z = P y / P z

Tactic:
simp only [smul_fin3_ext, mul_div_mul_left _ _ hu.ne_zero, and_self]

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (u • P) = toAffine W P

Tactic:
rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_some [@TransCmp α cmp] {t : RBMap α β cmp} :
    t.find? x = some v ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq

Proof state:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ t.toList ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

Tactic:
exact ⟨_, h, rfl⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

Tactic:
rintro ⟨b, h⟩

Result:
case mpr.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
b : α
h : (b, v) ∈ t.toList ∧ cmp x b = Ordering.eq
⊢ ∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

Proof state:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
rintro ⟨_, h, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ t.toList ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ t.toList ∧ cmp x y = Ordering.eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ t.find? x = some v ↔ ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
simp only [find?, findEntry?_some, Option.map_eq_some']

Result:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) ↔ ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
constructor

Result:
case mp
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v) → ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq

case mpr
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ (∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq) → ∃ a, (a ∈ t.toList ∧ cmp x a.fst = Ordering.eq) ∧ a.snd = v

Proof state:
case mp.intro.intro
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
x : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
w✝ : α × β
h : w✝ ∈ t.toList ∧ cmp x w✝.fst = Ordering.eq
⊢ ∃ y, (y, w✝.snd) ∈ t.toList ∧ cmp x y = Ordering.eq

Tactic:
exact ⟨_, h⟩

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem toMatrix_rotation (a : Circle) :
    LinearMap.toMatrix basisOneI basisOneI (rotation a).toLinearEquiv =
      Matrix.planeConformalMatrix (re a) (im a) (by simp [pow_two, ← normSq_apply])

Proof state:
a : Circle
⊢ (LinearMap.toMatrix basisOneI basisOneI) ↑(rotation a).toLinearEquiv =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯)

Tactic:
ext i j

Result:
case a
a : Circle
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑(rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) i j

Proof state:
a : Circle
⊢ (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0

Tactic:
simp [pow_two, ← normSq_apply]

Result:
no goals

Proof state:
case a
a : Circle
i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑(rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im ⋯) i j

Tactic:
simp only [LinearMap.toMatrix_apply, coe_basisOneI, LinearEquiv.coe_coe,
  LinearIsometryEquiv.coe_toLinearEquiv, rotation_apply, coe_basisOneI_repr, mul_re, mul_im,
  Matrix.val_planeConformalMatrix, Matrix.of_apply, Matrix.cons_val', Matrix.empty_val',
  Matrix.cons_val_fin_one]

Result:
case a
a : Circle
i j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re] i =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i => ![(↑a).im, (↑a).re] j) i

Proof state:
case a
a : Circle
i j : Fin 2
⊢ ![(↑a).re * (![1, I] j).re - (↑a).im * (![1, I] j).im, (↑a).re * (![1, I] j).im + (↑a).im * (![1, I] j).re] i =
    Matrix.vecCons (![(↑a).re, -(↑a).im] j) (fun i => ![(↑a).im, (↑a).re] j) i

Tactic:
fin_cases i <;> fin_cases j <;> simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) :
    prev ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs + c.utf8Size⟩ = ⟨utf8Len cs⟩

Proof state:
cs : List Char
c : Char
cs' : List Char
⊢ (if { byteIdx := utf8Len cs + c.utf8Size } = 0 then 0
    else utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size }) =
    { byteIdx := utf8Len cs }

Tactic:
refine (if_neg (Pos.ne_of_gt add_utf8Size_pos)).trans ?_

Result:
cs : List Char
c : Char
cs' : List Char
⊢ utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size } = { byteIdx := utf8Len cs }

Proof state:
cs : List Char
c : Char
cs' : List Char
⊢ utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size } = { byteIdx := utf8Len cs }

Tactic:
rw [utf8PrevAux_of_valid] <;> simp

Result:
no goals

Proof state:
cs : List Char
c : Char
cs' : List Char
⊢ { data := cs ++ c :: cs' }.prev { byteIdx := utf8Len cs + c.utf8Size } = { byteIdx := utf8Len cs }

Tactic:
simp only [prev]

Result:
cs : List Char
c : Char
cs' : List Char
⊢ (if { byteIdx := utf8Len cs + c.utf8Size } = 0 then 0
    else utf8PrevAux (cs ++ c :: cs') 0 { byteIdx := utf8Len cs + c.utf8Size }) =
    { byteIdx := utf8Len cs }
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem size_eraseIdxIfInBounds (a : Array α) (i : Nat) :
    (a.eraseIdxIfInBounds i).size = if i < a.size then a.size-1 else a.size

Proof state:
case isTrue
α : Type u_1
a : Array α
i : Nat
h✝ : i < a.size
⊢ (a.eraseIdx i h✝).size = a.size - 1

case isFalse
α : Type u_1
a : Array α
i : Nat
h✝ : ¬i < a.size
⊢ a.size = a.size

Tactic:
simp

Result:
case isFalse
α : Type u_1
a : Array α
i : Nat
h✝ : ¬i < a.size
⊢ a.size = a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ (a.eraseIdxIfInBounds i).size = if i < a.size then a.size - 1 else a.size

Tactic:
simp only [eraseIdxIfInBounds]

Result:
α : Type u_1
a : Array α
i : Nat
⊢ (if h : i < a.size then a.eraseIdx i h else a).size = if i < a.size then a.size - 1 else a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ (if h : i < a.size then a.eraseIdx i h else a).size = if i < a.size then a.size - 1 else a.size

Tactic:
split

Result:
case isTrue
α : Type u_1
a : Array α
i : Nat
h✝ : i < a.size
⊢ (a.eraseIdx i h✝).size = a.size - 1

case isFalse
α : Type u_1
a : Array α
i : Nat
h✝ : ¬i < a.size
⊢ a.size = a.size

Proof state:
case isFalse
α : Type u_1
a : Array α
i : Nat
h✝ : ¬i < a.size
⊢ a.size = a.size

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem mk_one (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) :
    LipschitzOnWith 1 f s :=
  of_dist_le_mul <| by simpa only [NNReal.coe_one, one_mul] using h

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑1 * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem Fintype.univ_Prop : (Finset.univ : Finset Prop) = {True, False} :=
  Finset.eq_of_veq <| by simp; rfl

Proof state:
⊢ univ.val = True ::ₘ {False}

Tactic:
rfl

Result:
no goals

Proof state:
⊢ univ.val = {True, False}.val

Tactic:
simp

Result:
⊢ univ.val = True ::ₘ {False}
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem condExp_zero_or_one_of_measurableSet_limsup [StandardBorelSpace Ω]
    (hm : m ≤ m0) [IsFiniteMeasure μ]
    (h_le : ∀ n, s n ≤ m0) (h_indep : iCondIndep m hm s μ)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a))
    (hns_univ : ∀ n, ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) :
    ∀ᵐ ω ∂μ, (μ⟦t | m⟧) ω = 0 ∨ (μ⟦t | m⟧) ω = 1

Proof state:
case h
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ (((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = ⊤) ∨ ((condExpKernel μ m) ω) t = 1

Tactic:
cases hω with
| inl h => exact Or.inl (Or.inl h)
| inr h => exact Or.inr h

Result:
no goals

Proof state:
case h.inl
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
inst✝¹ : StandardBorelSpace Ω
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h✝ : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
h : ((condExpKernel μ m) ω) t = 0
⊢ (((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = ⊤) ∨ ((condExpKernel μ m) ω) t = 1

Tactic:
exact Or.inl (Or.inl h)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
lemma weightedVSub_smul {G : Type*} [Group G] [DistribMulAction G V] [SMulCommClass G k V]
    {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → V) (a : G) :
    s.weightedVSub (a • p) w = a • s.weightedVSub p w

Proof state:
k : Type u_1
V : Type u_2
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ι : Type u_4
G : Type u_6
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → V
a : G
⊢ (s.weightedVSub (a • p)) w = a • (s.weightedVSub p) w

Tactic:
rw [weightedVSub, weightedVSubOfPoint_smul,
  weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Basic.lean
theorem zero_add (x : X[S⁻¹]) : 0 + x = x

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝

Tactic:
rw [← zero_oreDiv, add_oreDiv]

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ (0 + r✝) /ₒ s✝ = r✝ /ₒ s✝

Proof state:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ (0 + r✝) /ₒ s✝ = r✝ /ₒ s✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ 0 + x = x

Tactic:
induction x

Result:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝