harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma dft_comp_unitMul (Φ : ZMod N → E) (u : (ZMod N)ˣ) (k : ZMod N) :
    𝓕 (fun j ↦ Φ (u.val * j)) k = 𝓕 Φ (u⁻¹.val * k)

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k x : ZMod N
⊢ stdAddChar (-(x * k)) • (fun j => Φ (↑u * j)) x = stdAddChar (-(u.mulLeft x * (↑u⁻¹ * k))) • Φ (u.mulLeft x)

Tactic:
simp only [mul_comm u.val, u.mulLeft_apply, ← mul_assoc, u.mul_inv_cancel_right]

Result:
no goals

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k : ZMod N
⊢ 𝓕 (fun j => Φ (↑u * j)) k = 𝓕 Φ (↑u⁻¹ * k)

Tactic:
refine Fintype.sum_equiv u.mulLeft _ _ fun x ↦ ?_

Result:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
u : (ZMod N)ˣ
k x : ZMod N
⊢ stdAddChar (-(x * k)) • (fun j => Φ (↑u * j)) x = stdAddChar (-(u.mulLeft x * (↑u⁻¹ * k))) • Φ (u.mulLeft x)
-- Mathlib/Data/Vector/Basic.lean
theorem toList_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n)
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).toList = v.toList.pmap f hp

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α n
hp : ∀ x ∈ v.toList, p x
⊢ (pmap f v hp).toList = List.pmap f v.toList hp

Tactic:
cases v

Result:
case mk
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
val✝ : List α
property✝ : val✝.length = n
hp : ∀ x ∈ toList ⟨val✝, property✝⟩, p x
⊢ (pmap f ⟨val✝, property✝⟩ hp).toList = List.pmap f (toList ⟨val✝, property✝⟩) hp

Proof state:
case mk
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
val✝ : List α
property✝ : val✝.length = n
hp : ∀ x ∈ toList ⟨val✝, property✝⟩, p x
⊢ (pmap f ⟨val✝, property✝⟩ hp).toList = List.pmap f (toList ⟨val✝, property✝⟩) hp

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem isLUB_csSup' {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s)

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

Tactic:
simp only [csSup_empty, isLUB_empty]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_csSup hne hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
hs : BddAbove ∅
⊢ IsLUB ∅ (sSup ∅)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_insertList [BEq α]
    {l toInsert : List ((a : α) × β a)} :
    (List.insertList l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l toInsert : List ((a : α) × β a)
⊢ (insertList l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Tactic:
induction toInsert generalizing l with
| nil => simp [insertList]
| cons hd tl ih =>
  rw [insertList, List.isEmpty_cons, ih, isEmpty_insertEntry]
  simp

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((a : α) × β a)
⊢ (false && tl.isEmpty) = (l.isEmpty && false)

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
⊢ (insertList l []).isEmpty = (l.isEmpty && [].isEmpty)

Tactic:
simp [insertList]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((a : α) × β a)
⊢ (insertList l (hd :: tl)).isEmpty = (l.isEmpty && (hd :: tl).isEmpty)

Tactic:
rw [insertList, List.isEmpty_cons, ih, isEmpty_insertEntry]

Result:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, (insertList l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((a : α) × β a)
⊢ (false && tl.isEmpty) = (l.isEmpty && false)
-- Mathlib/Data/Finset/Basic.lean
theorem union_erase_of_mem (ha : a ∈ s) (t : Finset α) : s ∪ t.erase a = s ∪ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
t : Finset α
⊢ s ∪ t.erase a = s ∪ t

Tactic:
rw [← insert_erase (mem_union_left t ha), erase_union_distrib, ← insert_union, insert_erase ha]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem prod_list_swap_mem_alternatingGroup_iff_even_length {l : List (Perm α)}
    (hl : ∀ g ∈ l, IsSwap g) : l.prod ∈ alternatingGroup α ↔ Even l.length

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ l.prod ∈ alternatingGroup α ↔ Even l.length

Tactic:
rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ -1 ≠ 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ -1 ≠ 1

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.sUnion {s : Set (Set α)} (hs : s.Countable)
    (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋃₀ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃₀ s)

Tactic:
rw [sUnion_eq_biUnion]

Result:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)

Tactic:
exact .biUnion hs h

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem closure_iUnion_of_finite [Finite ι] (f : ι → Set X) :
    closure (⋃ i, f i) = ⋃ i, closure (f i)

Proof state:
X : Type u
ι : Sort w
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
f : ι → Set X
⊢ closure (⋃ i, f i) = ⋃ i, closure (f i)

Tactic:
rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma coverEntropyEntourage_le_netEntropyEntourage (T : X → X) (F : Set X) {U : Set (X × X)}
    (U_rfl : idRel ⊆ U) (U_symm : SymmetricRel U) :
    coverEntropyEntourage T F (U ○ U) ≤ netEntropyEntourage T F U

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ (fun n => (↑(coverMincard T F (U ○ U) n)).log / ↑n) n ≤ (fun n => (↑(netMaxcard T F U n)).log / ↑n) n

Tactic:
apply div_le_div_right_of_nonneg (Nat.cast_nonneg' n) (log_monotone _)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(coverMincard T F (U ○ U) n) ≤ ↑(netMaxcard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
⊢ coverEntropyEntourage T F (U ○ U) ≤ netEntropyEntourage T F U

Tactic:
refine (limsup_le_limsup) (Eventually.of_forall fun n ↦ ?_)

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ (fun n => (↑(coverMincard T F (U ○ U) n)).log / ↑n) n ≤ (fun n => (↑(netMaxcard T F U n)).log / ↑n) n

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
U_rfl : idRel ⊆ U
U_symm : SymmetricRel U
n : ℕ
⊢ ↑(coverMincard T F (U ○ U) n) ≤ ↑(netMaxcard T F U n)

Tactic:
exact ENat.toENNReal_le.2 (coverMincard_le_netMaxcard T F U_rfl U_symm n)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_orthogonalProjection_eq_zero_iff {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] {p : P} :
    dist p (orthogonalProjection s p) = 0 ↔ p ∈ s

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ dist p ↑((orthogonalProjection s) p) = 0 ↔ p ∈ s

Tactic:
rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem DifferentiableAt.differentiableAt_norm_of_smul (h : DifferentiableAt ℝ (‖·‖) (t • x)) :
    DifferentiableAt ℝ (‖·‖) x

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
exact differentiableAt_norm_smul ht |>.2 h

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : Subsingleton E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
exact (hasFDerivAt_of_subsingleton _ _).differentiableAt

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
hE : Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
exact not_differentiableAt_norm_zero E h |>.elim

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
by_cases hE : Nontrivial E

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : ¬Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
rw [zero_smul] at h

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) 0
hE : Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
obtain rfl | ht := eq_or_ne t 0

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
h : DifferentiableAt ℝ (fun x => ‖x‖) (t • x)
ht : t ≠ 0
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : ¬Nontrivial E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x

Tactic:
rw [not_nontrivial_iff_subsingleton] at hE

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
h : DifferentiableAt ℝ (fun x => ‖x‖) (0 • x)
hE : Subsingleton E
⊢ DifferentiableAt ℝ (fun x => ‖x‖) x
-- Mathlib/Algebra/Ring/Ext.lean
theorem AddCommMonoidWithOne.toAddMonoidWithOne_injective :
    Function.Injective (@AddCommMonoidWithOne.toAddMonoidWithOne R)

Proof state:
case mk.mk
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
add_comm✝¹ : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne✝ : AddMonoidWithOne R
add_comm✝ : ∀ (a b : R), a + b = b + a
a✝ : toAddMonoidWithOne = toAddMonoidWithOne
⊢ mk add_comm✝¹ = mk add_comm✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toAddMonoidWithOne R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toAddMonoidWithOne✝¹ : AddMonoidWithOne R
add_comm✝¹ : ∀ (a b : R), a + b = b + a
toAddMonoidWithOne✝ : AddMonoidWithOne R
add_comm✝ : ∀ (a b : R), a + b = b + a
a✝ : toAddMonoidWithOne = toAddMonoidWithOne
⊢ mk add_comm✝¹ = mk add_comm✝
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem toPushforwardStalk_comp :
    f ≫ StructureSheaf.toPushforwardStalk f p =
      StructureSheaf.toStalk R p ≫
        (TopCat.Presheaf.stalkFunctor _ _).map (Spec.sheafedSpaceMap f).c

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toStalk (↑R) p ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c

Tactic:
rw [StructureSheaf.toStalk, Category.assoc, TopCat.Presheaf.stalkFunctor_map_germ]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toOpen ↑R ⊤ ≫
      (Spec.sheafedSpaceMap f).c.app (op ⊤) ≫
        ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).base).obj
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p True.intro

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toOpen ↑R ⊤ ≫
      (Spec.sheafedSpaceMap f).c.app (op ⊤) ≫
        ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).base).obj
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p True.intro

Tactic:
exact Spec_Γ_naturality_assoc f _

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem one_le_maxVar : 1 ≤ maxVar X Y :=
  calc
    (1 : Real) = 2 * 0 + 1 + 2 * 0

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 2 * 0 + 1 + 2 * 0 ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
gcongr <;> positivity

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 1 = 2 * 0 + 1 + 2 * 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Lex.lean
theorem cons_le_cons [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) :
    a :: l' ≤ a :: l

Proof state:
α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l

Tactic:
exact h.imp .cons (congr_arg _)

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
⊢ a :: l' ≤ a :: l

Tactic:
rw [le_iff_lt_or_eq] at h ⊢

Result:
α : Type u
inst✝ : LinearOrder α
a : α
l l' : List α
h : l' < l ∨ l' = l
⊢ a :: l' < a :: l ∨ a :: l' = a :: l
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
theorem le_prod_of_mem {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod

Proof state:
case cons.inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x = y ∨ x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
rcases h₁ with (rfl | h₁)

Result:
case cons.inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Proof state:
case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ y * ys.prod

Tactic:
exact le_mul_left ih

Result:
no goals

Proof state:
case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
specialize ih h₁

Result:
case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ (y :: ys).prod

Proof state:
case cons
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ y :: ys
⊢ x ≤ (y :: ys).prod

Tactic:
simp only [mem_cons] at h₁

Result:
case cons
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x = y ∨ x ∈ ys
⊢ x ≤ (y :: ys).prod

Proof state:
case nil
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x : M
h₁ : x ∈ []
⊢ x ≤ [].prod

Tactic:
simp at h₁

Result:
no goals

Proof state:
case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ (y :: ys).prod

Tactic:
simp only [List.prod_cons]

Result:
case cons.inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
h₁ : x ∈ ys
ih : x ≤ ys.prod
⊢ x ≤ y * ys.prod
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_im_objs_iff (hφ : Function.Injective φ.obj) (d : D) :
    d ∈ (im φ hφ).objs ↔ ∃ c : C, φ.obj c = d

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ d ∈ (im φ hφ).objs ↔ ∃ c, φ.obj c = d

Tactic:
simp only [im, mem_map_objs_iff, mem_top_objs, true_and]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem le_coe_toReal {x : EReal} (h : x ≠ ⊤) : x ≤ x.toReal

Proof state:
case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
simp only [le_refl, coe_toReal h h']

Result:
no goals

Proof state:
x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑x.toReal

Tactic:
by_cases h' : x = ⊥

Result:
case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal

case neg
x : EReal
h : x ≠ ⊤
h' : ¬x = ⊥
⊢ x ≤ ↑x.toReal

Proof state:
case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
simp only [h', bot_le]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem mem_sup_left {S T : Submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [LE.le] at this

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : Preorder.toLE.1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : Preorder.toLE.1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
exact this

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem Metric.cobounded_eq_cocompact [ProperSpace α] : cobounded α = cocompact α

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ cobounded α = cocompact α

Tactic:
exact cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
  fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact

Result:
no goals

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
⊢ cobounded α = cocompact α

Tactic:
inhabit α

Result:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ cobounded α = cocompact α

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ cobounded α = cocompact α

Tactic:
nontriviality α

Result:
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
a✝ : Nontrivial α
⊢ cobounded α = cocompact α
-- Mathlib/Topology/Algebra/Monoid.lean
theorem IsCompact.mul {s t : Set M} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s * t)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Semigroup M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.1 * x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).image continuous_mul

Result:
no goals

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Semigroup M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s * t)

Tactic:
rw [← image_mul_prod]

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Semigroup M
inst✝ : ContinuousMul M
s t : Set M
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact ((fun x => x.1 * x.2) '' s ×ˢ t)
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Semiring U]
    [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U}
    (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) :
    ψ (aeval a p) = aeval (ψ a) (p.map φ)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = (aeval (ψ a)) (map φ p)

Tactic:
conv_rhs => rw [aeval_def, ← eval_map]

Result:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map (algebraMap T U) (map φ p))

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = eval (ψ a) (map (algebraMap T U) (map φ p))

Tactic:
rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_add_fuzzy_zero_iff {o₁ o₂ : Ordinal} : nim o₁ + nim o₂ ‖ 0 ↔ o₁ ≠ o₂

Proof state:
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ‖ 0 ↔ o₁ ≠ o₂

Tactic:
rw [iff_not_comm, Impartial.not_fuzzy_zero_iff, nim_add_equiv_zero_iff]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem ofReal_exp_ofReal_re (x : ℝ) : ((exp x).re : ℂ) = exp x :=
  conj_eq_iff_re.1 <| by rw [← exp_conj, conj_ofReal]

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

Tactic:
rw [← exp_conj, conj_ofReal]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_nat_mod (s : Finset α) (n : ℕ) (f : α → ℕ) :
    (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n :=
  (Multiset.prod_nat_mod _ _).trans <| by rw [Finset.prod, Multiset.map_map]; rfl

Proof state:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n

Tactic:
rw [Finset.prod, Multiset.map_map]

Result:
α : Type u_3
s : Finset α
n : ℕ
f : α → ℕ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n