harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
    ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖g‖₊ ≠ 0

Tactic:
simpa only [hg'] using one_ne_zero

Result:
no goals

Proof state:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
have hg' : ‖g‖₊ = 1 := NNReal.eq hg

Result:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ MapsTo (⇑g) (ball (f c) R₂) (ball ((⇑g ∘ f) c) R₂)

Tactic:
simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_update_of_ne (f : α →₀ M) {a a' : α} (ha : a ≠ a') (b : M) :
    erase a (update f a' b) = update (erase a f) a' b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a a' : α
ha : a ≠ a'
b : M
⊢ erase a (f.update a' b) = (erase a f).update a' b

Tactic:
rw [erase_eq_update_zero, erase_eq_update_zero, update_comm _ ha]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval₂_C_X : eval₂ C X p = p :=
  Polynomial.induction_on' p (fun p q hp hq => by simp [hp, hq]) fun n x => by
    rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

Proof state:
R : Type u
inst✝ : Semiring R
p✝ p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ eval₂ C X ((monomial n) x) = (monomial n) x

Tactic:
rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
theorem iff_op : HasLift sq ↔ HasLift sq.op

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct

Tactic:
exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
rw [iff, iff]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem Dart.edge_fiber [DecidableEq V] (d : G.Dart) :
    ({d' : G.Dart | d'.edge = d.edge} : Finset _) = {d, d.symm} :=
  Finset.ext fun d' => by simpa using dart_edge_eq_iff d' d

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
d d' : G.Dart
⊢ d' ∈ filter (fun d' => d'.edge = d.edge) univ ↔ d' ∈ {d, d.symm}

Tactic:
simpa using dart_edge_eq_iff d' d

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s

Proof state:
α : Type u_1
s : Set (α × α)
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s

Tactic:
rw [← range_diag, range_subset_iff]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem coeff_select (x : 𝕎 R) (n : ℕ) :
    (select P x).coeff n = aeval x.coeff (selectPoly P n)

Proof state:
case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ { coeff := fun n => if P n then x.coeff n else 0 }.coeff n = x.coeff n

Tactic:
simp only [hi, if_true]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) (if P n then X n else 0)

Tactic:
split_ifs with hi

Result:
case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) (X n)

case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) 0

Proof state:
case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) 0

Tactic:
rw [map_zero, mk]

Result:
case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ { coeff := fun n => if P n then x.coeff n else 0 }.coeff n = 0

Proof state:
case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ { coeff := fun n => if P n then x.coeff n else 0 }.coeff n = 0

Tactic:
simp only [hi, if_false]

Result:
no goals

Proof state:
case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) (X n)

Tactic:
rw [aeval_X, mk]

Result:
case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ { coeff := fun n => if P n then x.coeff n else 0 }.coeff n = x.coeff n

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (select P x).coeff n = (aeval x.coeff) (selectPoly P n)

Tactic:
dsimp [select, selectPoly]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
⊢ (mk p fun n => if P n then x.coeff n else 0).coeff n = (aeval x.coeff) (if P n then X n else 0)
-- Mathlib/NumberTheory/LSeries/Deriv.lean
private lemma LSeries.LSeriesSummable_logMul_and_hasDerivAt {f : ℕ → ℂ} {s : ℂ}
    (h : abscissaOfAbsConv f < s.re) :
    LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Proof state:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₂ : IsOpen S := isOpen_lt continuous_const continuous_re

Result:
case intro.intro.intro.intro
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n => ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x => term f x n) S
h₂ : IsOpen S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma inf_apply {s : Set α} (hs : MeasurableSet s) :
    (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)

Tactic:
conv in ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) => rw [← tsum_univ, ← heq]

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (x : ↑({k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)})), μ (t' ↑x) ⊓ ν (t' ↑x)

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
⊢ ∃ i, ∃ (_ : i ∈ {k | ν (t' k) < μ (t' k)}), x ∈ t' i

Tactic:
refine ⟨i, ?_, hi⟩

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
x : α
x✝ : x ∈ (⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ) ∩ s
hx₁ : x ∈ ⋂ i ∈ {k | μ (t' k) ≤ ν (t' k)}, (t' i)ᶜ
hx₂ : x ∈ s
i : ℕ
hi : x ∈ t' i
⊢ i ∈ {k | ν (t' k) < μ (t' k)}
-- Mathlib/Data/ZMod/Basic.lean
theorem val_mul_iff_lt {n : ℕ} [NeZero n] (a b : ZMod n) :
    (a * b).val = a.val * b.val ↔ a.val * b.val < n

Proof state:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n

Tactic:
apply ZMod.val_lt

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ (a * b).val = a.val * b.val ↔ a.val * b.val < n

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Proof state:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

Tactic:
rw [← h]

Result:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n

Proof state:
case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
apply ZMod.val_mul_of_lt h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation_symm :
    LinearIsometryEquiv.symm J = LinearIsometryEquiv.trans J (LinearIsometryEquiv.neg ℝ)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)

Tactic:
rw [rightAngleRotation]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).symm =
    (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).trans
      (LinearIsometryEquiv.neg ℝ)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).symm =
    (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).trans
      (LinearIsometryEquiv.neg ℝ)

Tactic:
exact LinearIsometryEquiv.toLinearIsometry_injective rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
    (∀ (i) (_ : i ∈ l.map f), P i) ↔ ∀ (j) (_ : j ∈ l), P (f j)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
P : β → Prop
⊢ (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tight.lean
/-- Inner regular finite measures on T2 spaces are tight. -/
lemma isTightMeasureSet_singleton_of_innerRegular [T2Space α] [OpensMeasurableSpace α]
    [IsFiniteMeasure μ] [h : μ.InnerRegular] :
    IsTightMeasureSet {μ}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
⊢ μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
intro s hs r hr

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
obtain ⟨K, hKs, hK_compact, hμK⟩ := h.innerRegular hs r hr

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
K : Set α
hKs : K ⊆ s
hK_compact : IsCompact K
hμK : r < μ K
⊢ ∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s
K : Set α
hKs : K ⊆ s
hK_compact : IsCompact K
hμK : r < μ K
⊢ ∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K

Tactic:
exact ⟨K, hKs, ⟨hK_compact, hK_compact.isClosed⟩, hμK⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
⊢ IsTightMeasureSet {μ}

Tactic:
refine isTightMeasureSet_singleton_of_innerRegularWRT ?_

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝² : T2Space α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
⊢ μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem bijective_iff_injective_and_card [Finite β] (f : α → β) :
    Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofFinite β

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
this : Fintype β
⊢ Surjective f ↔ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
⊢ Surjective f ↔ Nat.card α = Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)

Tactic:
rw [← and_congr_right_iff, ← Bijective,
  card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
rw [Bijective, and_congr_right_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
this✝ : Fintype β
this : Fintype α
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
revert h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
this✝ : Fintype β
this : Fintype α
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
this : Fintype β
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofInjective f h

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
h : Injective f
this✝ : Fintype β
this : Fintype α
⊢ Surjective f ↔ Nat.card α = Nat.card β
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem mul_right_le_iff [IsDedekindDomain A] {J : FractionalIdeal A⁰ K} (hJ : J ≠ 0) :
    ∀ {I I'}, I * J ≤ I' * J ↔ I ≤ I'

Proof state:
case mp
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I * J ≤ I' * J → I ≤ I'

Tactic:
intro h

Result:
case mp
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
h : I * J ≤ I' * J
⊢ I ≤ I'

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I * J ≤ I' * J ↔ I ≤ I'

Tactic:
constructor

Result:
case mp
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I * J ≤ I' * J → I ≤ I'

case mpr
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I ≤ I' → I * J ≤ I' * J

Proof state:
case mpr
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I ≤ I' → I * J ≤ I' * J

Tactic:
exact fun h => mul_right_mono J h

Result:
no goals

Proof state:
case mp
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
h : I * J ≤ I' * J
⊢ I ≤ I'

Tactic:
convert mul_right_mono J⁻¹ h <;> dsimp only <;>
rw [mul_assoc, FractionalIdeal.mul_inv_cancel hJ, mul_one]

Result:
no goals

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ ∀ {I I' : FractionalIdeal A⁰ K}, I * J ≤ I' * J ↔ I ≤ I'

Tactic:
intro I I'

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ I * J ≤ I' * J ↔ I ≤ I'
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_top [Fintype V] : (⊤ : SimpleGraph V).chromaticNumber = Fintype.card V

Proof state:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
⊢ C v = C w → v = w

Tactic:
contrapose

Result:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
⊢ ¬v = w → ¬C v = C w

Proof state:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
⊢ ¬v = w → ¬C v = C w

Tactic:
intro h

Result:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
h : ¬v = w
⊢ ¬C v = C w

Proof state:
V : Type u
inst✝ : Fintype V
⊢ ⊤.chromaticNumber = ↑(card V)

Tactic:
rw [chromaticNumber_eq_card_iff_forall_surjective (selfColoring _).colorable]

Result:
V : Type u
inst✝ : Fintype V
⊢ ∀ (C : ⊤.Coloring V), Surjective ⇑C

Proof state:
V : Type u
inst✝ : Fintype V
⊢ ∀ (C : ⊤.Coloring V), Surjective ⇑C

Tactic:
intro C

Result:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Surjective ⇑C

Proof state:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Injective ⇑C

Tactic:
intro v w

Result:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
⊢ C v = C w → v = w

Proof state:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Surjective ⇑C

Tactic:
rw [← Finite.injective_iff_surjective]

Result:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
⊢ Injective ⇑C

Proof state:
V : Type u
inst✝ : Fintype V
C : ⊤.Coloring V
v w : V
h : ¬v = w
⊢ ¬C v = C w

Tactic:
exact C.valid h

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
@[to_additive]
lemma preimage_image_coe (s : Set G) : ((↑) : G → Q) ⁻¹' ((↑) '' s) = N * s

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
⊢ mk ⁻¹' (mk '' s) = ↑N * s

Tactic:
ext a

Result:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' (mk '' s) ↔ a ∈ ↑N * s

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ ↑N
b : G
hb : b ∈ s
⊢ ↑b = ↑((fun x1 x2 => x1 * x2) a b)

Tactic:
simpa only [QuotientGroup.mk_mul, self_eq_mul_left, QuotientGroup.eq_one_iff]

Result:
no goals

Proof state:
case h.mp
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' (mk '' s) → a ∈ ↑N * s

Tactic:
rintro ⟨b, hb, h⟩

Result:
case h.mp.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ a ∈ ↑N * s

Proof state:
case h.mp.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ a ∈ ↑N * s

Tactic:
refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩

Result:
case h.mp.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ ↑(a / b) = 1

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ ↑N
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ mk ⁻¹' (mk '' s)

Tactic:
refine ⟨b, hb, ?_⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ ↑N
b : G
hb : b ∈ s
⊢ ↑b = ↑((fun x1 x2 => x1 * x2) a b)

Proof state:
case h
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' (mk '' s) ↔ a ∈ ↑N * s

Tactic:
constructor

Result:
case h.mp
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ mk ⁻¹' (mk '' s) → a ∈ ↑N * s

case h.mpr
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' (mk '' s)

Proof state:
case h.mp.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : ↑b = ↑a
⊢ ↑(a / b) = 1

Tactic:
simp only [h, QuotientGroup.mk_div, div_self']

Result:
no goals

Proof state:
case h.mpr
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ ↑N * s → a ∈ mk ⁻¹' (mk '' s)

Tactic:
rintro ⟨a, ha, b, hb, rfl⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ ↑N
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ mk ⁻¹' (mk '' s)