harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem interior_extChartAt_target_nonempty (x : M) :
    (interior (extChartAt I x).target).Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ (interior (extChartAt I x).target).Nonempty

Tactic:
by_contra! H

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H✝ : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H✝
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H✝ : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H✝
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
this : ↑(extChartAt I x) x ∈ closure (interior (extChartAt I x).target)
⊢ False

Tactic:
simp only [H, closure_empty, mem_empty_iff_false] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H✝ : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H✝
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
⊢ False

Tactic:
have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H✝ : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H✝
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H✝
inst✝ : ChartedSpace H✝ M
x : M
H : interior (extChartAt I x).target = ∅
this : ↑(extChartAt I x) x ∈ closure (interior (extChartAt I x).target)
⊢ False
-- Mathlib/SetTheory/Game/Nim.lean
theorem exists_grundyValue_moveRight_of_lt {G : PGame} [G.Impartial] {o : Nimber}
    (h : o < grundyValue G) : ∃ i, grundyValue (G.moveRight i) = o

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
⊢ ∃ i, (G.moveRight i).grundyValue = o

Tactic:
obtain ⟨i, hi⟩ := exists_grundyValue_moveLeft_of_lt h

Result:
case intro
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
i : (-G).LeftMoves
hi : ((-G).moveLeft i).grundyValue = o
⊢ ∃ i, (G.moveRight i).grundyValue = o

Proof state:
case h
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
i : (-G).LeftMoves
hi : ((-G).moveLeft i).grundyValue = o
⊢ (G.moveRight (toLeftMovesNeg.symm i)).grundyValue = o

Tactic:
rwa [← grundyValue_neg, ← moveLeft_neg]

Result:
no goals

Proof state:
case intro
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
i : (-G).LeftMoves
hi : ((-G).moveLeft i).grundyValue = o
⊢ ∃ i, (G.moveRight i).grundyValue = o

Tactic:
use toLeftMovesNeg.symm i

Result:
case h
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
i : (-G).LeftMoves
hi : ((-G).moveLeft i).grundyValue = o
⊢ (G.moveRight (toLeftMovesNeg.symm i)).grundyValue = o

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveRight i).grundyValue = o

Tactic:
rw [← grundyValue_neg] at h

Result:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < (-G).grundyValue
⊢ ∃ i, (G.moveRight i).grundyValue = o
-- Mathlib/Data/Set/Function.lean
theorem SurjOn.congr (h : SurjOn f₁ s t) (H : EqOn f₁ f₂ s) : SurjOn f₂ s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t

Tactic:
rwa [SurjOn, ← H.image_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_eq_of_nat {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*}
    [∀ i, SeminormedAddCommGroup (β i)] (n : ℕ) (h : p = n) (f : PiLp p β) :
    ‖f‖ = (∑ i, ‖f i‖ ^ n) ^ (1 / (n : ℝ))

Proof state:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)

Tactic:
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n)

Result:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < p.toReal
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)

Proof state:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < p.toReal
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)

Tactic:
simp only [one_div, h, Real.rpow_natCast, ENNReal.toReal_natCast, eq_self_iff_true,
  Finset.sum_congr, norm_eq_sum this]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_mul_I : tan (x * I) = tanh x * I

Proof state:
x : ℂ
⊢ tan (x * I) = tanh x * I

Tactic:
rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem disjoint_insert_right : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t

Proof state:
α : Type u
s t : Set α
a : α
⊢ Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t

Tactic:
rw [disjoint_comm, disjoint_insert_left, disjoint_comm]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_simple_mul (w : W) (i : B) :
    ℓ (s i * w) = ℓ w + 1 ∨ ℓ (s i * w) + 1 = ℓ w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
have := cs.length_mul_simple w⁻¹ i

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ w⁻¹ * cs.simple i = (cs.simple i * w)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
theorem AnalyticAt.cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x)
    (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (fun z => f z ^ g z) x

Tactic:
rw [← analyticWithinAt_univ] at fa ga ⊢

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z => f z ^ g z) univ x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (fun z => f z ^ g z) univ x

Tactic:
exact fa.cpow ga m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.not_neg (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(-x) = x + -1#w

Tactic:
rw [_root_.BitVec.not_neg]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(~~~x + 1#w) = x + -1#w

Tactic:
rw [← BitVec.neg_eq_not_add x]

Result:
w : Nat
x : BitVec w
⊢ ~~~(-x) = x + -1#w
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)]
lemma inv_pi (s : Set ι) (t : ∀ i, Set (α i)) : (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Proof state:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t)⁻¹ = s.pi fun i => (t i)⁻¹

Tactic:
ext x

Result:
case h
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i => (t i)⁻¹

Proof state:
case h
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (s.pi t)⁻¹ ↔ x ∈ s.pi fun i => (t i)⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toList_eq_singleton_iff {a : α} {s : Finset α} : s.toList = [a] ↔ s = {a}

Proof state:
α : Type u_1
a : α
s : Finset α
⊢ s.toList = [a] ↔ s = {a}

Tactic:
rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem char_tensor (V W : FDRep k G) : (V ⊗ W).character = V.character * W.character

Proof state:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g

Tactic:
convert trace_tensorProduct' (V.ρ g) (W.ρ g)

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
⊢ (V ⊗ W).character = V.character * W.character

Tactic:
ext g

Result:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem eq_of_forall_apply_eq (μ ν : ProbabilityMeasure Ω)
    (h : ∀ s : Set Ω, MeasurableSet s → μ s = ν s) : μ = ν

Proof state:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
simpa [ennreal_coeFn_eq_coeFn_toMeasure] using congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (h s s_mble)

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
⊢ μ = ν

Tactic:
ext1 s s_mble

Result:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
    l.contains a ↔ ∃ a' ∈ l, a == a'

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ l.contains a = true ↔ ∃ a', a' ∈ l ∧ (a == a') = true

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsUpperSet.le_card_inter_finset (h𝒜 : IsUpperSet (𝒜 : Set (Finset α)))
    (hℬ : IsUpperSet (ℬ : Set (Finset α))) :
    #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Proof state:
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
exact mul_le_mul_left' (card_le_card inter_subset_right) _

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
rw [← Fintype.card_finset]

Result:
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ Fintype.card (Finset α) * #ℬ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
  card_sdiff inter_subset_right, sdiff_inter_self_right, sdiff_compl,
  _root_.inf_comm] at this

Result:
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
have := h𝒜.card_inter_le_finset hℬ

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ #𝒜ᶜ * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Proof state:
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ Fintype.card (Finset α) * #ℬ

Tactic:
exact mul_le_mul_right' (card_le_univ _) _

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem iff_orderOf [hp : Fact p.Prime] : IsPGroup p G ↔ ∀ g : G, ∃ k : ℕ, orderOf g = p ^ k :=
  forall_congr' fun g =>
    ⟨fun ⟨_, hk⟩ =>
      Exists.imp (fun _ h => h.right)
        ((Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hk)),
      Exists.imp fun k hk => by rw [← hk, pow_orderOf_eq_one]⟩

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
hp : Fact (Nat.Prime p)
g : G
k : ℕ
hk : orderOf g = p ^ k
⊢ g ^ p ^ k = 1

Tactic:
rw [← hk, pow_orderOf_eq_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) : HasDerivAt negMulLog (- log x - 1) x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_

Result:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt negMulLog (-log x - 1) x

Tactic:
rw [← deriv_negMulLog hx, hasDerivAt_deriv_iff]

Result:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x

Proof state:
x : ℝ
hx : x ≠ 0
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_le_smul {p q : Seminorm 𝕜 E} {a b : ℝ≥0} (hpq : p ≤ q) (hab : a ≤ b) :
    a • p ≤ b • q

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
⊢ a • p ≤ b • q

Tactic:
simp_rw [le_def]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
⊢ ∀ (x : E), (a • p) x ≤ (b • q) x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
x : E
⊢ (a • p) x ≤ (b • q) x

Tactic:
exact mul_le_mul hab (hpq x) (apply_nonneg p x) (NNReal.coe_nonneg b)

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
⊢ ∀ (x : E), (a • p) x ≤ (b • q) x

Tactic:
intro x

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
a b : ℝ≥0
hpq : p ≤ q
hab : a ≤ b
x : E
⊢ (a • p) x ≤ (b • q) x
-- Mathlib/Data/Real/EReal.lean
theorem exists_rat_btwn_of_lt :
    ∀ {a b : EReal}, a < b → ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b
  | ⊤, _, h => (not_top_lt h).elim
  | (a : ℝ), ⊥, h => (lt_irrefl _ ((bot_lt_coe a).trans h)).elim
  | (a : ℝ), (b : ℝ), h => by simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]
  | (a : ℝ), ⊤, _ =>
    let ⟨b, hab⟩ := exists_rat_gt a
    ⟨b, by simpa using hab, coe_lt_top _⟩
  | ⊥, ⊥, h => (lt_irrefl _ h).elim
  | ⊥, (a : ℝ), _ =>
    let ⟨b, hab⟩ := exists_rat_lt a
    ⟨b, bot_lt_coe _, by simpa using hab⟩
  | ⊥, ⊤, _ => ⟨0, bot_lt_coe _, coe_lt_top _⟩

Proof state:
a : ℝ
x✝ : ⊥ < ↑a
b : ℚ
hab : ↑b < a
⊢ ↑↑b < ↑a

Tactic:
simpa using hab

Result:
no goals

Proof state:
a b : ℝ
h : ↑a < ↑b
⊢ ∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b

Tactic:
simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]

Result:
no goals

Proof state:
a : ℝ
x✝ : ↑a < ⊤
b : ℚ
hab : a < ↑b
⊢ ↑a < ↑↑b

Tactic:
simpa using hab

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_div_const_uIcc (a b c : α) : (fun x => x / a) '' [[b, c]] = [[b / a, c / a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
⊢ (fun x => x / a) '' [[b, c]] = [[b / a, c / a]]

Tactic:
simp only [div_eq_mul_inv, image_mul_const_uIcc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma nndist_pi_eq_iff {f g : ∀ b, π b} {r : ℝ≥0} (hr : 0 < r) :
    nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ b, nndist (f b) (g b) ≤ r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ (∀ (b : β), nndist (f b) (g b) ≤ r) →
    ((∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i))

Tactic:
intro h

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
⊢ (∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i)

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ (∀ (b : β), nndist (f b) (g b) ≤ r) →
    ((∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i))

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
⊢ (∃ x, r ≤ nndist (f x) (g x)) ↔ ∃ i, nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i)

Tactic:
refine exists_congr fun b => ?_

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
b : β
⊢ r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
b : β
⊢ r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)

Tactic:
apply (and_iff_right <| h _).symm

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_le_iff_le_toReal {a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ∞) :
    ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b

Proof state:
case intro
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ (↑b).toReal

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe

Result:
no goals

Proof state:
a : ℝ
b : ℝ≥0∞
hb : b ≠ ⊤
⊢ ENNReal.ofReal a ≤ b ↔ a ≤ b.toReal

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro
a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ (↑b).toReal
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
    {f : Option β → Option β} (h : m.WF) :
    Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
fallback : β
f : Option β → Option β
h : m.WF
⊢ getD (alter m k f) k fallback = (f (get? m k)).getD fallback

Tactic:
simp [getD_alter h]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem map_noncommProd [MonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm) (g : F) :
    g (s.noncommProd f comm) =
      s.noncommProd (fun i => g (f i)) fun _ hx _ hy _ => (comm.of_refl hx hy).map g

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Monoid β
inst✝² : Monoid γ
inst✝¹ : FunLike F β γ
inst✝ : MonoidHomClass F β γ
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
g : F
⊢ g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) ⋯

Tactic:
simp [noncommProd, Multiset.map_noncommProd]

Result:
no goals
-- Mathlib/Data/Fintype/Quotient.lean
theorem listChoice_mk {l : List ι} (a : ∀ i ∈ l, α i) : listChoice (S := S) (⟦a · ·⟧) = ⟦a⟧ :=
  match l with
  |     [] => Quotient.sound nofun
  | i :: l => by
    unfold listChoice List.Pi.tail
    rw [listChoice_mk]
    exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (listChoice fun x1 x2 => ⟦a x1 x2⟧) = ⟦a⟧

Tactic:
unfold listChoice List.Pi.tail

Result:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 => ⟦a x1 x2⟧).liftOn₂ (listChoice fun j hj => (fun x1 x2 => ⟦a x1 x2⟧) j ⋯)
      (fun x1 x2 => ⟦List.Pi.cons i l x1 x2⟧) ⋯ =
    ⟦a⟧

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 => ⟦a x1 x2⟧).liftOn₂ (listChoice fun j hj => (fun x1 x2 => ⟦a x1 x2⟧) j ⋯)
      (fun x1 x2 => ⟦List.Pi.cons i l x1 x2⟧) ⋯ =
    ⟦a⟧

Tactic:
rw [listChoice_mk]

Result:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 => ⟦a x1 x2⟧).liftOn₂ ⟦fun j hj => a j ⋯⟧ (fun x1 x2 => ⟦List.Pi.cons i l x1 x2⟧) ⋯ = ⟦a⟧