harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_emod_of_dvd (n : Int) {m k : Int}
    (h : m ∣ k) : (n % k) % m = n % m

Proof state:
n m k : Int
h : m ∣ k
⊢ n % k % m = n % m

Tactic:
conv => rhs; rw [← emod_add_ediv n k]

Result:
n m k : Int
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m

Proof state:
n m k : Int
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m

Tactic:
match k, h with
| _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]

Result:
no goals

Proof state:
n m k : Int
h : m ∣ k
t : Int
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m

Tactic:
rw [Int.mul_assoc, add_mul_emod_self_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
/-- A hamiltonian path visits every vertex. -/
@[simp] lemma IsHamiltonian.mem_support (hp : p.IsHamiltonian) (c : α) : c ∈ p.support

Proof state:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
hp : p.IsHamiltonian
c : α
⊢ c ∈ p.support

Tactic:
simp only [← List.count_pos_iff, hp _, Nat.zero_lt_one]

Result:
no goals
-- Mathlib/Data/Fintype/Sigma.lean
lemma Set.biUnion_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
    ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩

Proof state:
ι : Type u_1
α : Type u_2
κ : ι → Type u_3
inst✝ : (i : ι) → Fintype (κ i)
s : Finset ι
f : Sigma κ → Set α
⊢ ⋃ ij ∈ s.sigma fun x => Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/List/Pairwise.lean
theorem Pairwise.rel_head_of_rel_head_head (h₁ : l.Pairwise R) (ha : a ∈ l)
    (hhead : R (l.head <| ne_nil_of_mem ha) (l.head <| ne_nil_of_mem ha)) :
    R (l.head <| ne_nil_of_mem ha) a

Proof state:
case nil
α : Type u_1
R : α → α → Prop
a : α
h₁ : Pairwise R []
ha : a ∈ []
hhead : R ([].head ⋯) ([].head ⋯)
⊢ R ([].head ⋯) a

Tactic:
simp at ha

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ne_one_of_mem_sphere (hr : r ≠ 0) (x : sphere (1 : E) r) : (x : E) ≠ 1 :=
  ne_one_of_norm_ne_zero <| by rwa [norm_eq_of_mem_sphere' x]

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hr : r ≠ 0
x : ↑(sphere 1 r)
⊢ ‖↑x‖ ≠ 0

Tactic:
rwa [norm_eq_of_mem_sphere' x]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma IsComplement.nonempty_left (hst : IsComplement S T) : S.Nonempty

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : IsComplement S T
⊢ S.Nonempty

Tactic:
contrapose! hst

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hst : S = ∅
⊢ ¬IsComplement S T

Tactic:
simp [hst]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem im_smul_eq_div_normSq : (g • z).im = z.im / Complex.normSq (denom g z)

Proof state:
g : SL(2, ℤ)
z : ℍ
⊢ (g • z).im = z.im / Complex.normSq (denom (↑g) z)

Tactic:
simpa only [coe, coe_GLPos_coe_GL_coe_matrix, (g : SL(2, ℝ)).prop, one_mul] using
  z.im_smul_eq_div_normSq g

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_ennreal_eq_one {x : ℝ≥0∞} : (x : EReal) = 1 ↔ x = 1

Proof state:
x : ℝ≥0∞
⊢ ↑x = 1 ↔ x = 1

Tactic:
rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.union {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁)
    (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∪ s₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Result:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ b, bif b then s₁ else s₂)

Proof state:
α : Type u_1
m : MeasurableSpace α
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
h₂ : MeasurableSet s₂
⊢ MeasurableSet (⋃ b, bif b then s₁ else s₂)

Tactic:
exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_neg_eq_zero {x : α} : fract (-x) = 0 ↔ fract x = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ fract (-x) = 0 ↔ fract x = 0

Tactic:
simp only [fract_eq_iff, le_refl, zero_lt_one, tsub_zero, true_and]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (∃ z, -x = ↑z) ↔ ∃ z, x = ↑z

Tactic:
constructor <;> rintro ⟨z, hz⟩ <;> use -z <;> simp [← hz]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma oneLePart_inf_leOnePart_eq_one (a : α) : a⁺ᵐ ⊓ a⁻ᵐ = 1

Proof state:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1

Tactic:
rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
  oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_singleton (a : α) : 𝓝[{a}] a = pure a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}] a = pure a

Tactic:
rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toLeft_inter : (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft
-- Mathlib/Order/WithBot.lean
lemma WithTop.toDual_lt_iff {x : WithTop α} {y : WithBot αᵒᵈ} :
    WithTop.toDual x < y ↔ WithBot.ofDual y < x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ WithTop.toDual x < y ↔ WithBot.ofDual y < x

Tactic:
cases x <;> cases y <;> simp [toDual_lt]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma injective_inclusionSpan :
    Injective (p.inclusionSpan S)

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : ↑((inclusionSpan S p) x) = ↑((inclusionSpan S p) y)
⊢ x = y

Tactic:
simpa using hxy

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
⊢ Injective ⇑(inclusionSpan S p)

Tactic:
intro x y hxy

Result:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : (inclusionSpan S p) x = (inclusionSpan S p) y
⊢ x = y

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : (inclusionSpan S p) x = (inclusionSpan S p) y
⊢ x = y

Tactic:
rw [Subtype.ext_iff] at hxy

Result:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
p : Submodule R M
x y : ↥p
hxy : ↑((inclusionSpan S p) x) = ↑((inclusionSpan S p) y)
⊢ x = y
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem cons_diff_of_mem {a : α} {l₂ : List α} (h : a ∈ l₂) (l₁ : List α) :
    (a :: l₁).diff l₂ = l₁.diff (l₂.erase a)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : List α
h : a ∈ l₂
l₁ : List α
⊢ (a :: l₁).diff l₂ = l₁.diff (l₂.erase a)

Tactic:
rw [cons_diff, if_pos h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_dite_of_false {p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, ¬ p i)
    (f : ∀ i, p i → β) (g : ∀ i, ¬ p i → β) :
    ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, g i.1 (h _ i.2)

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
x✝ : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : α) → p i → β
g : (i : α) → ¬p i → β
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, g ↑i ⋯

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_cot_ofReal_re (x : ℝ) : ((cot x).re : ℂ) = cot x :=
  conj_eq_iff_re.1 <| by rw [← cot_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (↑x).cot = (↑x).cot

Tactic:
rw [← cot_conj, conj_ofReal]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem exists_next_right {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) :
    ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z :=
  have Hne : (s.filter (x < ·)).Nonempty := h.imp fun y hy => mem_filter.2 (by simpa)
  have aux := mem_filter.1 (min'_mem _ Hne)
  ⟨min' _ Hne, aux.1, by simp, fun z hzs hz => min'_le _ _ <| mem_filter.2 ⟨hzs, by simpa⟩⟩

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ x < y

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : (filter (fun x_1 => x < x_1) s).Nonempty
aux : (filter (fun x_1 => x < x_1) s).min' Hne ∈ s ∧ x < (filter (fun x_1 => x < x_1) s).min' Hne
z : α
hzs : z ∈ s
hz : x < z
⊢ x < z

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : (filter (fun x_1 => x < x_1) s).Nonempty
aux : (filter (fun x_1 => x < x_1) s).min' Hne ∈ s ∧ x < (filter (fun x_1 => x < x_1) s).min' Hne
⊢ x < (filter (fun x_1 => x < x_1) s).min' Hne

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_concat (x : BitVec w) (b : Bool) :
    (concat x b).toNat = x.toNat * 2 + b.toNat

Proof state:
case pred.false
w : Nat
x : BitVec w
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || false.toNat.testBit i) = (x.toNat * 2 + false.toNat).testBit i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ (x.concat b).toNat = x.toNat * 2 + b.toNat

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
w : Nat
x : BitVec w
b : Bool
⊢ ∀ (i : Nat), (x.concat b).toNat.testBit i = (x.toNat * 2 + b.toNat).testBit i

Proof state:
case pred.true
w : Nat
x : BitVec w
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || true.toNat.testBit i) = (x.toNat * 2 + true.toNat).testBit i

Tactic:
rintro (_ | i)
<;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right, Nat.testBit_add_one]

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
b : Bool
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || b.toNat.testBit i) = (x.toNat * 2 + b.toNat).testBit i

Tactic:
cases b

Result:
case pred.false
w : Nat
x : BitVec w
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || false.toNat.testBit i) = (x.toNat * 2 + false.toNat).testBit i

case pred.true
w : Nat
x : BitVec w
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || true.toNat.testBit i) = (x.toNat * 2 + true.toNat).testBit i

Proof state:
case pred
w : Nat
x : BitVec w
b : Bool
⊢ ∀ (i : Nat), (x.concat b).toNat.testBit i = (x.toNat * 2 + b.toNat).testBit i

Tactic:
simp only [concat, toNat_append, Nat.shiftLeft_eq, Nat.pow_one, toNat_ofBool, Nat.testBit_or]

Result:
case pred
w : Nat
x : BitVec w
b : Bool
⊢ ∀ (i : Nat), ((x.toNat * 2).testBit i || b.toNat.testBit i) = (x.toNat * 2 + b.toNat).testBit i
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem injective_of_iterate_injective {n : ℕ} (hn : n ≠ 0) (h : Injective (f' ^ n)) :
    Injective f'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Injective (⇑(f' ^ n.pred) ∘ ⇑f')
⊢ Injective ⇑f'

Tactic:
exact h.of_comp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ Injective ⇑f'

Tactic:
rw [← Nat.succ_pred_eq_of_pos (show 0 < n by omega), iterate_succ, coe_comp] at h

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Injective (⇑(f' ^ n.pred) ∘ ⇑f')
⊢ Injective ⇑f'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Injective ⇑(f' ^ n)
⊢ 0 < n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
    (h' : EqOn g f (s ∩ EMetric.ball x r)) (h'' : g x = f x) :
    HasFPowerSeriesWithinOnBall g p s x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ EMetric.ball x r)
h'' : g x = f x
⊢ ∀ {y : E}, x + y ∈ insert x s → y ∈ EMetric.ball 0 r → HasSum (fun n => (p n) fun x => y) (g (x + y))

Tactic:
intro y hy h'y

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ EMetric.ball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : y ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (p n) fun x => y) (g (x + y))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_reverse (l : Vector α n) : countP p l.reverse = countP p l

Proof state:
case mk
α : Type u_1
p : α → Bool
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
l : Vector α n
⊢ countP p l.reverse = countP p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ioo_succ_right_eq_insert_of_not_isMax (h₁ : a < b) (h₂ : ¬IsMax b) :
    Ioo a (succ b) = insert b (Ioo a b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
lemma Pi.isCompact_closure_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
    IsCompact (closure s) ↔ ∀ i, IsCompact (closure <| eval i '' s)

Proof state:
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
⊢ IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (eval i '' s))

Tactic:
simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem mul_inv_cancel : IsUnit a → a * a⁻¹ = 1

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
⊢ IsUnit a → a * a⁻¹ = 1

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * (↑u)⁻¹ = 1

Proof state:
case intro
α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ ↑u * (↑u)⁻¹ = 1

Tactic:
rw [← Units.val_inv_eq_inv_val, Units.mul_inv]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem typein_lt_self {o : Ordinal} (i : o.toType) : typein (α := o.toType) (· < ·) i < o

Proof state:
o : Ordinal.{u_1}
i : o.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding i < type fun x1 x2 => x1 < x2

Tactic:
apply typein_lt_type

Result:
no goals

Proof state:
o : Ordinal.{u_1}
i : o.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
simp_rw [← type_toType o]

Result:
o : Ordinal.{u_1}
i : o.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding i < type fun x1 x2 => x1 < x2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_right_eq_self {a b : Nat} : a + b = a ↔ b = 0

Proof state:
a b : Nat
⊢ a + b = a ↔ b = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_atTop_curry [Preorder α] [Preorder β] {p : α × β → Prop}
    (hp : ∀ᶠ x : α × β in Filter.atTop, p x) : ∀ᶠ k in atTop, ∀ᶠ l in atTop, p (k, l)

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
exact hp.curry

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
rw [← prod_atTop_atTop_eq] at hp

Result:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
-- Mathlib/GroupTheory/Sylow.lean
theorem prime_dvd_card_quotient_normalizer [Finite G] {p : ℕ} {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ (n + 1) ∣ Nat.card G) {H : Subgroup G} (hH : Nat.card H = p ^ n) :
    p ∣ Nat.card (normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
  let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
  have hcard : Nat.card (G ⧸ H) = s * p :=
    (mul_left_inj' (show Nat.card H ≠ 0 from Nat.card_pos.ne')).1
      (by
        rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
  have hm :
    s * p % p =
      Nat.card (normalizer H ⧸ Subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) % p :=
    hcard ▸ (card_quotient_normalizer_modEq_card_quotient hH).symm
  Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card (G ⧸ H) * Nat.card ↥H = s * p * Nat.card ↥H

Tactic:
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]

Result:
no goals

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ comap H.normalizer.subtype H) % p
⊢ Nat.card (↥H.normalizer ⧸ comap H.normalizer.subtype H) % p = 0

Tactic:
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
/-- A functor reflecting larger filtered colimits also reflects smaller filtered colimits. -/
lemma reflectsFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
    [UnivLE.{w₂, w₂'}] [ReflectsFilteredColimitsOfSize.{w', w₂'} F] :
      ReflectsFilteredColimitsOfSize.{w, w₂} F where
  reflects_filtered_colimits J _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsFiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsColimitsOfShape J F

Tactic:
exact reflectsColimitsOfShape_of_equiv e F

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsColimitsOfShape J F

Tactic:
haveI := IsFiltered.of_equivalence e.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsFiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsColimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ ReflectsColimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsColimitsOfShape J F
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub (a b : α) : toIocDiv hp a (b - p) = toIocDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (b - p) = toIocDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIocDiv_sub_zsmul hp a b 1

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
/-- See `uniformOn_eq_zero'` for a version assuming `MeasurableSet s` instead of
`MeasurableSingletonClass Ω`. -/
@[simp] lemma uniformOn_eq_zero [MeasurableSingletonClass Ω] :
    uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
s : Set Ω
inst✝ : MeasurableSingletonClass Ω
⊢ uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Tactic:
simp [uniformOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem drop_mk (a : Array α) (h : a.size = n) (m) :
    (Vector.mk a h).drop m = Vector.mk (a.extract m a.size) (by simp [h]) := rfl

Proof state:
α : Type ?u.6591
n : Nat
a : Array α
h : a.size = n
m : Nat
⊢ (a.extract m).size = n - m

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
@[simp] lemma logDeriv_inv (x : 𝕜) : logDeriv (·⁻¹) x = -1 / x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ logDeriv (fun x => x⁻¹) x = -1 / x

Tactic:
simpa using logDeriv_zpow x (-1)

Result:
no goals