harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem pow_mul_m_le_card_part (hP : P.IsEquipartition) (hu : u ∈ P.parts) :
    (4 : ℝ) ^ #P.parts * m ≤ #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * (Fintype.card α / #P.parts / 4 ^ #P.parts) ≤ #u

Tactic:
exact (Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * m ≤ #u

Tactic:
rw [stepBound, ← Nat.div_div_eq_div_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * (Fintype.card α / #P.parts / 4 ^ #P.parts) ≤ #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * ↑m ≤ ↑(#u)

Tactic:
norm_cast

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * m ≤ #u
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.of_cancel_le (ctx : Context) (a b c d : Expr) (h : Poly.cancel a.toNormPoly b.toNormPoly = (c.toPoly, d.toPoly)) : (a.denote ctx ≤ b.denote ctx) = (c.denote ctx ≤ d.denote ctx)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_le ctx (c.toPoly, d.toPoly) = Poly.denote_le ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Tactic:
simp [toNormPoly, Poly.norm,Poly.denote_le, -eq_iff_iff] at this

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : (denote ctx c ≤ denote ctx d) = (denote ctx a ≤ denote ctx b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_le ctx (a.toNormPoly.cancel b.toNormPoly) = Poly.denote_le ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Tactic:
rw [h] at this

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_le ctx (c.toPoly, d.toPoly) = Poly.denote_le ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : (denote ctx c ≤ denote ctx d) = (denote ctx a ≤ denote ctx b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Tactic:
exact this.symm

Result:
no goals

Proof state:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)

Tactic:
have := Poly.denote_le_cancel_eq ctx a.toNormPoly b.toNormPoly

Result:
ctx : Context
a b c d : Expr
h : a.toNormPoly.cancel b.toNormPoly = (c.toPoly, d.toPoly)
this : Poly.denote_le ctx (a.toNormPoly.cancel b.toNormPoly) = Poly.denote_le ctx (a.toNormPoly, b.toNormPoly)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem initialBound_le_bound : initialBound ε l ≤ bound ε l :=
  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right _ <| by positivity

Proof state:
ε : ℝ
l : ℕ
⊢ 0 < 16 ^ stepBound^[⌊4 / ε ^ 5⌋₊] (initialBound ε l)

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem nil_subperm {l : List α} : [] <+~ l := ⟨[], Perm.nil, by simp⟩

Proof state:
α : Type u_1
l : List α
⊢ [] <+ l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_push_ref_eq' (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
    (hidx : idx = len) :
    (s.push ref).get idx (by omega) = ref

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ (s.push ref).get idx ⋯ = ref

Tactic:
have := s.hlen

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.push ref).get idx ⋯ = ref

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx = len
⊢ idx < len + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
idx : Nat
hidx : idx = len
this : s.refs.size = len
⊢ (s.push ref).get idx ⋯ = ref

Tactic:
simp [get, push, ← this, hidx]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_unitInv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
    f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : C
f f' : X ⟶ e.inverse.obj (e.functor.obj Y)
⊢ f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem range_toProd :
    Set.range toProd = { lr : (A →L[𝕜] A) × (A →L[𝕜] A) | ∀ x y, lr.2 x * y = x * lr.1 y } :=
  Set.ext fun x =>
    ⟨by
      rintro ⟨a, rfl⟩
      exact a.central, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

Proof state:
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProd ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}

Tactic:
exact a.central

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)
⊢ x ∈ Set.range toProd → x ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProd ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_and_self : ∀ (x : Bool), (!x && x) = false

Proof state:
⊢ ∀ (x : Bool), (!x && x) = false

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem stdBasisMatrix_add [AddZeroClass α] (i : m) (j : n) (a b : α) :
    stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
⊢ stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
⊢ stdBasisMatrix i j (a + b) i✝ j✝ = (stdBasisMatrix i j a + stdBasisMatrix i j b) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
⊢ (if i = i✝ ∧ j = j✝ then a + b else 0) =
    ((of fun i' j' => if i = i' ∧ j = j' then a else 0) + of fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ j✝

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
⊢ stdBasisMatrix i j (a + b) i✝ j✝ = (stdBasisMatrix i j a + stdBasisMatrix i j b) i✝ j✝

Tactic:
simp only [stdBasisMatrix, of_apply]

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
⊢ (if i = i✝ ∧ j = j✝ then a + b else 0) =
    ((of fun i' j' => if i = i' ∧ j = j' then a else 0) + of fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ j✝
-- Mathlib/Logic/Function/Iterate.lean
theorem comp_iterate (h : Commute f g) (n : ℕ) : (f ∘ g)^[n] = f^[n] ∘ g^[n]

Proof state:
case zero
α : Type u
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[0] = f^[0] ∘ g^[0]

Tactic:
rfl

Result:
no goals

Proof state:
case succ.h
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x

Tactic:
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Result:
no goals

Proof state:
case succ
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
⊢ (f ∘ g)^[n + 1] = f^[n + 1] ∘ g^[n + 1]

Tactic:
funext x

Result:
case succ.h
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x

Proof state:
α : Type u
f g : α → α
h : Commute f g
n : ℕ
⊢ (f ∘ g)^[n] = f^[n] ∘ g^[n]

Tactic:
induction n with
| zero => rfl
| succ n ihn =>
  funext x
  simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Defs.lean
lemma one_sub_le_one_add_mul_one_sub (h : c + b * c ≤ a + b) : 1 - a ≤ (1 + b) * (1 - c)

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + (a + b)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : c + b * c ≤ a + b
⊢ 1 - a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]

Result:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + (a + b)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_one : W.Φ 1 = X

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1 = ↑0 + 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 1 = X

Tactic:
rw [show 1 = ((0 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_one, one_pow, mul_one, if_pos Even.zero,
  mul_one, preΨ'_zero, mul_zero, zero_mul, sub_zero]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem card_pair (a b : α) : card {a, b} = 2

Proof state:
α : Type u_1
a b : α
⊢ {a, b}.card = 2

Tactic:
rw [insert_eq_cons, card_cons, card_singleton]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) :
    star c * a * c ≤ star c * b * c

Proof state:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1

Tactic:
exact ⟨star c * p * c, conjugate_nonneg hp c, by simp only [add_mul, mul_add]⟩

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ star c * (a + p) * c = star c * a * c + star c * p * c

Tactic:
simp only [add_mul, mul_add]

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), b = a + p
c : R
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star c * b * c = star c * a * c + p

Tactic:
obtain ⟨p, hp, rfl⟩ := hab

Result:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), star c * (a + p) * c = star c * a * c + p_1

Proof state:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), star c * (a + p) * c = star c * a * c + p_1

Tactic:
simp_rw [← StarOrderedRing.nonneg_iff] at hp ⊢

Result:
case intro.intro
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a c p : R
hp : 0 ≤ p
⊢ ∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ star c * a * c ≤ star c * b * c

Tactic:
rw [StarOrderedRing.le_iff] at hab ⊢

Result:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), b = a + p
c : R
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star c * b * c = star c * a * c + p
-- Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
theorem isIntegralCurve_eq_of_contMDiff (hγt : ∀ t, I.IsInteriorPoint (γ t))
    (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
    (hγ : IsIntegralCurve γ v) (hγ' : IsIntegralCurve γ' v) (h : γ t₀ = γ' t₀) : γ = γ'

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
hγ : IsIntegralCurve γ v
hγ' : IsIntegralCurve γ' v
h : γ t₀ = γ' t₀
t : ℝ
⊢ ∃ T, t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := exists_abs_lt t

Result:
case intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
hγ : IsIntegralCurve γ v
hγ' : IsIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂ : |t| < T
⊢ ∃ T, t ∈ Ioo (-T) T ∧ t₀ ∈ Ioo (-T) T

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
hγ : IsIntegralCurve γ v
hγ' : IsIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
hT₁ : T > 0
hT₂✝ : |t| < T
hT₂ : -T < t
hT₃ : t < T
S : ℝ
hS₁ : S > 0
hS₂✝ : |t₀| < S
hS₂ : -S < t₀
hS₃ : t₀ < S
⊢ t ∈ Ioo (-(T + S)) (T + S) ∧ t₀ ∈ Ioo (-(T + S)) (T + S)

Tactic:
constructor <;> constructor <;> linarith

Result:
no goals

Proof state:
case h.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }
hγ : IsIntegralCurve γ v
hγ' : IsIntegralCurve γ' v
h : γ t₀ = γ' t₀
t T : ℝ
ht₀ : t ∈ Ioo (-T) T
ht : t₀ ∈ Ioo (-T) T
⊢ γ t = γ' t

Tactic:
exact isIntegralCurveOn_Ioo_eqOn_of_contMDiff ht (fun t _ ↦ hγt t) hv
  ((hγ.isIntegralCurveOn _).mono (subset_univ _))
  ((hγ'.isIntegralCurveOn _).mono (subset_univ _)) h ht₀

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem compl_singleton (a : α) : ({a} : Finset α)ᶜ = univ.erase a

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a}ᶜ = univ.erase a

Tactic:
rw [compl_eq_univ_sdiff, sdiff_singleton_eq_erase]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_iff_ne_rational (x : ℝ) : Irrational x ↔ ∀ a b : ℤ, x ≠ a / b

Proof state:
x : ℝ
⊢ Irrational x ↔ ∀ (a b : ℤ), x ≠ ↑a / ↑b

Tactic:
simp only [Irrational, Rat.forall, cast_mk, not_exists, Set.mem_range, cast_intCast, cast_div,
  eq_comm]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem duplicate_cons_iff {y : α} : x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

Proof state:
α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Proof state:
case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inr hm

Result:
no goals

Proof state:
case refine_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
exact Or.inl ⟨rfl, hm⟩

Result:
no goals

Proof state:
case refine_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l

Tactic:
exact h.cons_duplicate

Result:
no goals

Proof state:
case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
obtain hm | hm := h

Result:
case refine_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l

case refine_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Proof state:
case refine_2.inl.intro.refl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Tactic:
rcases h with (⟨rfl | h⟩ | h)

Result:
case refine_2.inl.intro.refl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l

case refine_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l
-- Mathlib/MeasureTheory/Measure/Dirac.lean
/-- Dirac delta measures at two points are different if and only if there is a measurable set
containing one of the points but not the other. -/
lemma dirac_ne_dirac_iff_exists_measurableSet {x y : α} :
    Measure.dirac x ≠ Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A → y ∈ A

Tactic:
simp only [h A A_mble, imp_self]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1

Tactic:
refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩

Result:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
⊢ x ∈ A ↔ y ∈ A

Tactic:
by_cases x_in_A : x ∈ A

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x ≠ dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Tactic:
apply not_iff_not.mp

Result:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ ¬dirac x ≠ dirac y ↔ ¬∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simp only [x_in_A, h A A_mble x_in_A]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
simpa only [x_in_A, false_iff] using h Aᶜ (MeasurableSet.compl_iff.mpr A_mble) x_in_A

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ ¬dirac x ≠ dirac y ↔ ¬∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A

Tactic:
simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) ↔ ∀ (x_1 : Set α), MeasurableSet x_1 → x ∈ x_1 → y ∈ x_1
-- Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
theorem liftToFinsetColimIso_aux (F : Discrete α ⥤ C) {J : Finset (Discrete α)} (j : J) :
    Sigma.ι (F.obj ·.val) j ≫ colimit.ι (liftToFinsetObj F) J ≫
      (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv
    = colimit.ι F j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ C
J : Finset (Discrete α)
j : { x // x ∈ J }
⊢ Sigma.ι (fun x => F.obj ↑x) j ≫
      colimit.ι (liftToFinsetObj F) J ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone F)).inv =
    colimit.ι F ↑j

Tactic:
simp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Result:
no goals
-- Mathlib/GroupTheory/Solvable.lean
theorem isSolvable_of_comm {G : Type*} [hG : Group G] (h : ∀ a b : G, a * b = b * a) :
    IsSolvable G

Proof state:
case mk
G : Type u_3
toDivInvMonoid✝ : DivInvMonoid G
inv_mul_cancel✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G

Tactic:
exact CommGroup.isSolvable

Result:
no goals

Proof state:
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G

Tactic:
letI hG' : CommGroup G := { hG with mul_comm := h }

Result:
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G

Proof state:
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G

Tactic:
cases hG

Result:
case mk
G : Type u_3
toDivInvMonoid✝ : DivInvMonoid G
inv_mul_cancel✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_getThenInsertIfNew? [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α}
    {b : β a} (h : Raw.WFImp m.1) :
    Perm (toListModel (m.getThenInsertIfNew? a b).2.1.buckets)
      (insertEntryIfNew a b (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertIfNewₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ toListModel (m.getThenInsertIfNew? a b).snd.val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
h : Raw.WFImp m.val
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)