harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem mk_eq_div (p q : K[X]) : RatFunc.mk p q = algebraMap _ _ p / algebraMap _ _ q

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
⊢ RatFunc.mk p q = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q

Tactic:
simp only [mk_eq_div', ofFractionRing_div, ofFractionRing_algebraMap]

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma isAtomistic_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) :
    IsAtomistic α

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ ∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
obtain ⟨s, hs, hs'⟩ := hS.atomistic a (h ▸ le_top)

Result:
case intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
s : Set α
hs : s ⊆ S
hs' : a = sSup s
⊢ ∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ IsAtomistic α

Tactic:
refine ⟨fun a ↦ ?_⟩

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ ∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
s : Set α
hs : s ⊆ S
hs' : a = sSup s
⊢ ∃ s, a = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
exact ⟨s, hs', fun I hI ↦ hS.isAtom I (hs hI)⟩

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finAddFlip_apply_mk_left {k : ℕ} (h : k < m) (hk : k < m + n := Nat.lt_add_right n h)
    (hnk : n + k < n + m := Nat.add_lt_add_left h n) :
    finAddFlip (⟨k, hk⟩ : Fin (m + n)) = ⟨n + k, hnk⟩

Proof state:
m n k : ℕ
h : k < m
hk : optParam (k < m + n) ⋯
hnk : optParam (n + k < n + m) ⋯
⊢ finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩

Tactic:
convert finAddFlip_apply_castAdd ⟨k, h⟩ n

Result:
no goals
-- Mathlib/CategoryTheory/Action/Monoidal.lean
theorem leftDual_ρ [LeftRigidCategory V] (h : H) : (ᘁX).ρ h = ᘁX.ρ (h⁻¹ : H)

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

case x
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

Tactic:
rfl

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ h⁻¹

Tactic:
rw [← SingleObj.inv_as_inv]

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

case x
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.union [DecidableEq α] (l₁ : List α) (h : Nodup l₂) : (l₁ ∪ l₂).Nodup

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₂.Nodup → (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup

Tactic:
exact (ih h).insert

Result:
no goals

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
l₂ : List α
inst✝ : DecidableEq α
l₁ : List α
h : l₂.Nodup
⊢ (l₁ ∪ l₂).Nodup

Tactic:
induction' l₁ with a l₁ ih generalizing l₂

Result:
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

case cons
α : Type u
inst✝ : DecidableEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₂.Nodup → (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_mkArray [LawfulBEq α] (n : Nat) (a b : α) :
    (mkArray n a).erase b = if b == a then mkArray (n - 1) a else mkArray n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ (mkArray n a).erase b = if (b == a) = true then mkArray (n - 1) a else mkArray n a

Tactic:
simp only [← List.toArray_replicate, List.erase_toArray]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ ((List.replicate n a).erase b).toArray =
    if (b == a) = true then (List.replicate (n - 1) a).toArray else (List.replicate n a).toArray

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ ((List.replicate n a).erase b).toArray =
    if (b == a) = true then (List.replicate (n - 1) a).toArray else (List.replicate n a).toArray

Tactic:
simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ (if (b == a) = true then List.replicate (n - 1) a else List.replicate n a).toArray =
    if (b == a) = true then mkArray (n - 1) a else mkArray n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a b : α
⊢ (if (b == a) = true then List.replicate (n - 1) a else List.replicate n a).toArray =
    if (b == a) = true then mkArray (n - 1) a else mkArray n a

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Data/Int/CharZero.lean
theorem cast_div_charZero {k : Type*} [DivisionRing k] [CharZero k] {m n : ℤ} (n_dvd : n ∣ m) :
    ((m / n : ℤ) : k) = m / n

Proof state:
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

case inr
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Proof state:
case inl
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m : ℤ
n_dvd : 0 ∣ m
⊢ ↑(m / 0) = ↑m / ↑0

Tactic:
simp [Int.ediv_zero]

Result:
no goals

Proof state:
case inr
k : Type u_3
inst✝¹ : DivisionRing k
inst✝ : CharZero k
m n : ℤ
n_dvd : n ∣ m
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
exact cast_div n_dvd (cast_ne_zero.mpr hn)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma isProbabilityMeasure_tilted [NeZero μ] (hf : Integrable (fun x ↦ exp (f x)) μ) :
    IsProbabilityMeasure (μ.tilted f)

Proof state:
case measure_univ.h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 < ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact integral_exp_pos hf

Result:
no goals

Proof state:
case measure_univ.h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]

Result:
case measure_univ.h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 < ∫ (x : α), rexp (f x) ∂μ

Proof state:
case measure_univ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) Set.univ = 1

Tactic:
simp_rw [tilted_apply' _ _ MeasurableSet.univ, setLIntegral_univ,
  ENNReal.ofReal_div_of_pos (integral_exp_pos hf), div_eq_mul_inv]

Result:
case measure_univ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1

Proof state:
case measure_univ.ht
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ IsProbabilityMeasure (μ.tilted f)

Tactic:
constructor

Result:
case measure_univ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) Set.univ = 1

Proof state:
case measure_univ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const'' _ hf.1.aemeasurable.ennreal_ofReal,
  ← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le),
  ENNReal.mul_inv_cancel]

Result:
case measure_univ.h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0

case measure_univ.ht
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c

Proof state:
case zero
c b : Nat
⊢ max (0 * c) (b * c) = max 0 b * c

Tactic:
simp

Result:
no goals

Proof state:
case succ
c i : Nat
ind : ∀ (b : Nat), max (i * c) (b * c) = max i b * c
b : Nat
⊢ max ((i + 1) * c) (b * c) = max (i + 1) b * c

Tactic:
cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_max_add_right, ind]

Result:
no goals

Proof state:
a b c : Nat
⊢ max (a * c) (b * c) = max a b * c

Tactic:
induction a generalizing b with
| zero => simp
| succ i ind =>
  cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_max_add_right, ind]

Result:
no goals
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
to the multiplicative integers, or is densely ordered. -/
@[to_additive existing]
lemma LinearOrderedCommGroup.discrete_or_denselyOrdered :
    Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
⊢ Nonempty (Additive G ≃+o ℤ) → Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
rintro ⟨f, hf⟩

Result:
case intro.mk
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
f : Additive G ≃+ ℤ
hf : ∀ {a b : Additive G}, f.toFun a ≤ f.toFun b ↔ a ≤ b
⊢ Nonempty (G ≃*o Multiplicative ℤ)

Proof state:
case intro.mk
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
f : Additive G ≃+ ℤ
hf : ∀ {a b : Additive G}, f.toFun a ≤ f.toFun b ↔ a ≤ b
⊢ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
exact ⟨AddEquiv.toMultiplicative' f, hf⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Tactic:
refine (LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)).imp ?_ id

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
⊢ Nonempty (Additive G ≃+o ℤ) → Nonempty (G ≃*o Multiplicative ℤ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_eq_size {p} : countP p l = l.size ↔ ∀ a ∈ l, p a

Proof state:
α✝ : Type u_1
n✝ : Nat
l : Vector α✝ n✝
p : α✝ → Bool
⊢ countP p l = l.size ↔ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.size ↔
    ∀ (a : α✝), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a = true

Proof state:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } =
      { toArray := toArray✝, size_toArray := size_toArray✝ }.size ↔
    ∀ (a : α✝), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem zero : mapFun f (0 : 𝕎 R) = 0

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
⊢ mapFun (⇑f) 0 = 0

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getCast!_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} [Inhabited (β a)] :
    l.getCast! a = getValueCast! a l.toList

Proof state:
case nil
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
⊢ getCast! a nil = getValueCast! a nil.toList

Tactic:
simp [getCast!, List.getValueCast!]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : AssocList α β
a : α
inst✝ : Inhabited (β a)
⊢ getCast! a l = getValueCast! a l.toList

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
⊢ getCast! a nil = getValueCast! a nil.toList

case cons
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getCast! a tail✝ = getValueCast! a tail✝.toList
⊢ getCast! a (cons key✝ value✝ tail✝) = getValueCast! a (cons key✝ value✝ tail✝).toList

Proof state:
case cons
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getCast! a tail✝ = getValueCast! a tail✝.toList
⊢ getCast! a (cons key✝ value✝ tail✝) = getValueCast! a (cons key✝ value✝ tail✝).toList

Tactic:
simp_all [getCast!, List.getValueCast!, List.getValueCast!, List.getValueCast?_cons,
  apply_dite Option.get!]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_compl (f : α → ℝ≥0∞) {A : Set α} (hA : MeasurableSet A) :
    ∫⁻ x in A, f x ∂μ + ∫⁻ x in Aᶜ, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [← lintegral_add_measure, Measure.restrict_add_restrict_compl hA]

Result:
no goals
-- Mathlib/Algebra/AlgebraicCard.lean
theorem cardinalMk_le_max : #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀

Proof state:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ #{ x // IsAlgebraic R x } ≤ #R ⊔ ℵ₀

Tactic:
rw [← lift_id #_, ← lift_id #R]

Result:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R ⊔ ℵ₀

Proof state:
R A : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ lift.{u, u} #{ x // IsAlgebraic R x } ≤ lift.{u, u} #R ⊔ ℵ₀

Tactic:
exact cardinalMk_lift_le_max R A

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next_stop : ∀ {s}, ValidFor l m r s → s.next ⟨utf8Len m⟩ = ⟨utf8Len m⟩
  | _, ⟨⟩ => by simp [Substring.next, Pos.add_eq]

Proof state:
l m r : List Char
⊢ { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.next
      { byteIdx := utf8Len m } =
    { byteIdx := utf8Len m }

Tactic:
simp [Substring.next, Pos.add_eq]

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem mulLeft_eq_zero_iff (a : A) : mulLeft R a = 0 ↔ a = 0

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : mulLeft R a = 0
⊢ a = 0

Tactic:
rw [← mul_one a, ← mulLeft_apply R a 1, h, LinearMap.zero_apply]

Result:
no goals

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : a = 0
⊢ mulLeft R 0 = 0

Tactic:
exact mulLeft_zero_eq_zero _ _

Result:
no goals

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : a = 0
⊢ mulLeft R a = 0

Tactic:
rw [h]

Result:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : a = 0
⊢ mulLeft R 0 = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
⊢ mulLeft R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : mulLeft R a = 0
⊢ a = 0

case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
h : a = 0
⊢ mulLeft R a = 0
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalCompAux'_of_whisker {f f' g g' h : C} {η : g ⟶ h} {θ : f' ⟶ g'}
    {η₁ : g ⊗ f ⟶ h ⊗ f} {ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'}
    {ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ (f ⊗ g')}
    {ηθ₂ : g ⊗ (f ⊗ f') ⟶ h ⊗ (f ⊗ g')}
    (e_η₁ : η ▷ f = η₁) (e_ηθ : η₁ ⊗ ((Iso.refl _).hom ≫ θ ≫ (Iso.refl _).hom) = ηθ)
    (e_ηθ₁ : ηθ ≫ (α_ _ _ _).hom = ηθ₁) (e_ηθ₂ : (α_ _ _ _).inv ≫ ηθ₁ = ηθ₂) :
    η ⊗ (f ◁ θ) = ηθ₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ f ◁ θ = (α_ g f f').inv ≫ (η ▷ f ⊗ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom) ≫ (α_ h f g').hom

Tactic:
simp [MonoidalCategory.tensorHom_def]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ f ◁ θ = ηθ₂

Tactic:
simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : g ⊗ f ⟶ h ⊗ f
ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'
ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ f ⊗ g'
ηθ₂ : g ⊗ f ⊗ f' ⟶ h ⊗ f ⊗ g'
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom = ηθ
e_ηθ₁ : ηθ ≫ (α_ h f g').hom = ηθ₁
e_ηθ₂ : (α_ g f f').inv ≫ ηθ₁ = ηθ₂
⊢ η ⊗ f ◁ θ = (α_ g f f').inv ≫ (η ▷ f ⊗ (Iso.refl f').hom ≫ θ ≫ (Iso.refl g').hom) ≫ (α_ h f g').hom
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ univ) :
    ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ infDist x sᶜ = dist y x

Tactic:
rwa [dist_comm]

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|
  Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ infDist x sᶜ = dist y x

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure sᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
rw [closure_compl] at hys

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ (interior s)ᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure sᶜ
hyd : infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_left_mono]
lemma zpow_right_mono (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [zpow_add_one]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 ≤ a
⊢ Monotone fun n => a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a : α
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
exact le_mul_of_one_le_right' ha

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_inf_distrib_right (f : ι → α) (a : α) :
    s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup' hs fun i => a ⊓ f i) = s.sup' hs fun i => f i ⊓ a

Tactic:
simp_rw [inf_comm]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a

Tactic:
rw [inf_comm, sup'_inf_distrib_left]

Result:
α : Type u_2
ι : Type u_5
inst✝ : DistribLattice α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.sup' hs fun i => a ⊓ f i) = s.sup' hs fun i => f i ⊓ a
-- Mathlib/Combinatorics/Digraph/Orientation.lean
@[simp]
lemma toSimpleGraphStrict_top : (⊤ : Digraph V).toSimpleGraphStrict = ⊤

Proof state:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝

Tactic:
exact ⟨And.left, fun h ↦ ⟨h.ne, trivial, trivial⟩⟩

Result:
no goals

Proof state:
V : Type u_1
⊢ ⊤.toSimpleGraphStrict = ⊤

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊤.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊤.Adj x✝¹ x✝