harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem isAddFundamentalDomain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ)
    (μ : Measure ℝ

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! x_1, codRestrict (fun n => n • T) ↑(zmultiples T) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)

Tactic:
simpa only [add_comm x] using existsUnique_add_zsmul_mem_Ioc hT x t

Result:
no goals

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Tactic:
have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
  (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Tactic:
refine this.existsUnique_iff.2 ?_

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! x_1, codRestrict (fun n => n • T) ↑(zmultiples T) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
⊢ IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)
-- Mathlib/Data/Int/LeastGreatest.lean
theorem exists_greatest_of_bdd
    {P : ℤ → Prop}
    (Hbdd : ∃ b : ℤ , ∀ z : ℤ , P z → z ≤ b)
    (Hinh : ∃ z : ℤ , P z) : ∃ ub : ℤ , P ub ∧ ∀ z : ℤ , P z → z ≤ ub

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
let ⟨b, Hb⟩ := Hbdd

Result:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
exact ⟨lb, H⟩

Result:
no goals

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh

Result:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Proof state:
P : ℤ → Prop
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

Tactic:
classical
let ⟨b, Hb⟩ := Hbdd
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
exact ⟨lb, H⟩

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem dot_cross_self (v w : Fin 3 → R) : w ⬝ᵥ v ×₃ w = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ w ⬝ᵥ (crossProduct v) w = 0

Tactic:
rw [← cross_anticomm, dotProduct_neg, dot_self_cross, neg_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem cokernelComparison_map_desc [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z}
    (w : f ≫ h = 0) :
    cokernelComparison f G ≫ G.map (cokernel.desc _ h w) =
      cokernel.desc _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero])

Proof state:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) =
    coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) ⋯

Tactic:
simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ cokernelComparison f G ≫ G.map (cokernel.desc f h w) = cokernel.desc (G.map f) (G.map h) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) =
    coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) ⋯

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem IsOfFinOrder.prod_mk : IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Tactic:
simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem sum_id_lt_of_lt (m n : ι →₀ ℕ) (h : m < n) : (m.sum fun _ => id) < n.sum fun _ => id

Proof state:
case h
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ toMultiset m < toMultiset n

Tactic:
exact toMultiset_strictMono h

Result:
no goals

Proof state:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (m.sum fun x => id) < n.sum fun x => id

Tactic:
rw [← card_toMultiset, ← card_toMultiset]

Result:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (toMultiset m).card < (toMultiset n).card

Proof state:
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (toMultiset m).card < (toMultiset n).card

Tactic:
apply Multiset.card_lt_card

Result:
case h
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ toMultiset m < toMultiset n
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
theorem cfcₙHom_comp [UniqueHom R A] (f : C(σₙ R a, R)₀)
    (f' : C(σₙ R a, σₙ R (cfcₙHom ha f))₀)
    (hff' : ∀ x, f x = f' x) (g : C(σₙ R (cfcₙHom ha f), R)₀) :
    cfcₙHom ha (g.comp f') = cfcₙHom (cfcₙHom_predicate ha f) g

Proof state:
case refine_2
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ (cfcₙHom ha)
      ({ toContinuousMap := ContinuousMap.restrict (σₙ R ((cfcₙHom ha) f)) (ContinuousMap.id R), map_zero' := ⋯ }.comp
        f') =
    (cfcₙHom ha) f

Tactic:
congr

Result:
case refine_2.h.e_6.h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(σₙ R a), R)₀
f' : C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ha) f)))₀
hff' : ∀ (x : ↑(σₙ R a)), f x = ↑(f' x)
g : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀
ψ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] C(↑(σₙ R a), R)₀ :=
  { toFun := fun x => x.comp f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
φ : C(↑(σₙ R ((cfcₙHom ha) f)), R)₀ →⋆ₙₐ[R] A := (cfcₙHom ha).comp ψ
⊢ { toContinuousMap := ContinuousMap.restrict (σₙ R ((cfcₙHom ha) f)) (ContinuousMap.id R), map_zero' := ⋯ }.comp f' = f
-- Mathlib/Order/Interval/Basic.lean
theorem coe_dual (s : Interval α) : (dual s : Set αᵒᵈ) = ofDual ⁻¹' s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Interval α
⊢ ↑(dual s) = ⇑ofDual ⁻¹' ↑s

Tactic:
cases s with
| bot => rfl
| coe s₀ => exact NonemptyInterval.coe_dual s₀

Result:
no goals

Proof state:
case coe
α : Type u_1
inst✝ : PartialOrder α
s₀ : NonemptyInterval α
⊢ ↑(dual ↑s₀) = ⇑ofDual ⁻¹' ↑↑s₀

Tactic:
exact NonemptyInterval.coe_dual s₀

Result:
no goals

Proof state:
case bot
α : Type u_1
inst✝ : PartialOrder α
⊢ ↑(dual ⊥) = ⇑ofDual ⁻¹' ↑⊥

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem nhdsWithin_prod_eq (x : X) (y : Y) (s : Set X) (t : Set Y) :
    𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set X
t : Set Y
⊢ 𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y

Tactic:
simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image₂ f s t = image₂ f' s t :=
  coe_injective <| by
    push_cast
    exact image2_congr h

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f ↑s ↑t = image2 f' ↑s ↑t

Tactic:
exact image2_congr h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ ↑(image₂ f s t) = ↑(image₂ f' s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f f' : α → β → γ
s : Finset α
t : Finset β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f ↑s ↑t = image2 f' ↑s ↑t
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.image_range_card (ha : ∀ x : α, x ∈ zpowers a) :
    Finset.image (fun i => a ^ i) (range (Nat.card α)) = univ

Proof state:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i => a ^ i) (range (Nat.card α)) = univ

Tactic:
rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_subtype {s : Set A} :
    AlgebraicIndependent R ((↑) : s → A) ↔
      ∀ p : MvPolynomial A R, p ∈ MvPolynomial.supported R s → aeval id p = 0 → p = 0

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ supported R s, (aeval _root_.id) p = 0 → p = 0

Tactic:
apply @algebraicIndependent_comp_subtype _ _ _ id

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma oneLePart_eq_ite : a⁺ᵐ = if 1 ≤ a then a else 1

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a ⊔ 1 = (fun x1 x2 => x1 ⊔ x2) 1 a

Tactic:
simp_rw [sup_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 ≤ a then a else 1

Tactic:
rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a ⊔ 1 = (fun x1 x2 => x1 ⊔ x2) 1 a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
      (eq : i = j) (p : j < (a.set i v).size) :
    (a.set i v)[j]'p = v

Proof state:
case mk
α : Type u_1
i : Nat
v : α
j : Nat
eq : i = j
toList✝ : List α
h : i < { toList := toList✝ }.size
p : j < ({ toList := toList✝ }.set i v h).size
⊢ ({ toList := toList✝ }.set i v h)[j] = v

Tactic:
simp

Result:
case mk
α : Type u_1
i : Nat
v : α
j : Nat
eq : i = j
toList✝ : List α
h : i < { toList := toList✝ }.size
p : j < ({ toList := toList✝ }.set i v h).size
⊢ (toList✝.set i v)[j] = v

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
v : α
j : Nat
eq : i = j
p : j < (a.set i v h).size
⊢ (a.set i v h)[j] = v

Tactic:
cases a

Result:
case mk
α : Type u_1
i : Nat
v : α
j : Nat
eq : i = j
toList✝ : List α
h : i < { toList := toList✝ }.size
p : j < ({ toList := toList✝ }.set i v h).size
⊢ ({ toList := toList✝ }.set i v h)[j] = v

Proof state:
case mk
α : Type u_1
i : Nat
v : α
j : Nat
eq : i = j
toList✝ : List α
h : i < { toList := toList✝ }.size
p : j < ({ toList := toList✝ }.set i v h).size
⊢ (toList✝.set i v)[j] = v

Tactic:
simp [set, ← getElem_toList, ←eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_append : eval assign (.append lhs rhs) = (lhs.eval assign) ++ (rhs.eval assign)

Proof state:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.append rhs) = eval assign lhs ++ eval assign rhs

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem Submonoid.fg_iff (P : Submonoid M) :
    Submonoid.FG P ↔ ∃ S : Set M, Submonoid.closure S = P ∧ S.Finite :=
  ⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ =>
    ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
P : Submonoid M
x✝ : ∃ S, closure S = P ∧ S.Finite
S : Set M
hS : closure S = P
hf : S.Finite
⊢ closure ↑hf.toFinset = P

Tactic:
simp [hS]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpFamily_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a}
    (ha : a < c.ord) : nfpFamily f a < c.ord

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ nfpFamily f a < c.ord

Tactic:
apply nfpFamily_lt_ord_lift _ _ hf ha <;> rw [hc.cof_eq]

Result:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c

ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Result:
no goals

Proof state:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c

Tactic:
exact hι

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem minpoly_sub_one_eq_cyclotomic_comp [Algebra K A] [IsDomain A] {ζ : A}
    [IsCyclotomicExtension {n} K A] (hζ : IsPrimitiveRoot ζ n)
    (h : Irreducible (Polynomial.cyclotomic n K)) :
    minpoly K (ζ - 1) = (cyclotomic n K).comp (X + 1)

Proof state:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ (minpoly K ζ).comp (X - C (-1)) = (minpoly K ζ).comp (X + 1)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ ζ - 1 = ζ + (algebraMap K A) (-1)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals

Proof state:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
⊢ minpoly K (ζ - 1) = (cyclotomic (↑n) K).comp (X + 1)

Tactic:
haveI := IsCyclotomicExtension.neZero' n K A

Result:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ minpoly K (ζ - 1) = (cyclotomic (↑n) K).comp (X + 1)

Proof state:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ minpoly K (ζ - 1) = (cyclotomic (↑n) K).comp (X + 1)

Tactic:
rw [show ζ - 1 = ζ + algebraMap K A (-1) by simp [sub_eq_add_neg],
  minpoly.add_algebraMap ζ,
  hζ.minpoly_eq_cyclotomic_of_irreducible h]

Result:
n : ℕ+
A : Type w
K : Type u
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsDomain A
ζ : A
inst✝ : IsCyclotomicExtension {n} K A
hζ : IsPrimitiveRoot ζ ↑n
h : Irreducible (cyclotomic (↑n) K)
this : NeZero ↑↑n
⊢ (minpoly K ζ).comp (X - C (-1)) = (minpoly K ζ).comp (X + 1)
-- Mathlib/Data/List/Sigma.lean
theorem kerase_append_left {a} :
    ∀ {l₁ l₂ : List (Sigma β)}, a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
  | [], _, h => by cases h
  | s :: l₁, l₂, h₁ => by
    if h₂ : a = s.1 then simp [h₂]
    else simp at h₁; rcases h₁ with h₁ | h₁ <;>
      [exact absurd h₁ h₂; simp [h₂, kerase_append_left h₁]]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₂ : ¬a = s.fst
h₁ : a = s.fst ∨ a ∈ l₁.keys
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
rcases h₁ with h₁ | h₁ <;>
[exact absurd h₁ h₂; simp [h₂, kerase_append_left h₁]]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys
h₂ : a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
simp [h₂]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x✝ : List (Sigma β)
h : a ∈ [].keys
⊢ kerase a ([] ++ x✝) = kerase a [] ++ x✝

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
if h₂ : a = s.1 then simp [h₂]
else simp at h₁; rcases h₁ with h₁ | h₁ <;>
  [exact absurd h₁ h₂; simp [h₂, kerase_append_left h₁]]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys
h₂ : ¬a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
simp at h₁

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₂ : ¬a = s.fst
h₁ : a = s.fst ∨ a ∈ l₁.keys
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc]
lemma fromSpecStalk_toSpecΓ (X : Scheme.{u}) (x : X) :
    X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op) ≫
        (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
rw [Scheme.toSpecΓ_naturality, ← SpecMap_ΓSpecIso_hom, ← Spec.map_comp,
  Scheme.fromSpecStalk_appTop]

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op) ≫
        (ΓSpecIso (X.presheaf.stalk x)).hom) =
    Spec.map (X.presheaf.germ ⊤ x trivial)
-- Mathlib/Probability/Kernel/Composition/Comp.lean
lemma comp_sum_right {ι : Type*} [Countable ι] (κ : ι → Kernel α β) (η : Kernel β γ) :
    η ∘ₖ Kernel.sum κ = Kernel.sum fun i ↦ η ∘ₖ (κ i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
⊢ η ∘ₖ Kernel.sum κ = Kernel.sum fun i => η ∘ₖ κ i

Tactic:
ext _ _ hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = ((Kernel.sum fun i => η ∘ₖ κ i) a✝) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = ((Kernel.sum fun i => η ∘ₖ κ i) a✝) s✝

Tactic:
simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply,
  lintegral_sum_measure, comp_apply' _ _ _ hs]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem support_C_mul_T_of_ne_zero {a : R} (a0 : a ≠ 0) (n : ℤ) :
    Finsupp.support (C a * T n) = {n}

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (C a * T n).support = {n}

Tactic:
rw [← single_eq_C_mul_T]

Result:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (Finsupp.single n a).support = {n}

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (Finsupp.single n a).support = {n}

Tactic:
exact support_single_ne_zero _ a0

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
lemma exists_one_half_le_im_and_norm_le (hk : k ≤ 0) (f : F) (τ : ℍ) :
    ∃ ξ : ℍ, 1 / 2 ≤ ξ.im ∧ ‖f τ‖ ≤ ‖f ξ‖ :=
  let ⟨γ, hγ, hdenom⟩ := exists_one_half_le_im_smul_and_norm_denom_le τ
  ⟨γ • τ, hγ, by simpa only [slash_action_eqn'' _ (mem_Gamma_one γ),
    norm_mul, norm_zpow] using le_mul_of_one_le_left (norm_nonneg _) <|
      one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk⟩

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F Γ(1) k
hk : k ≤ 0
f : F
τ : ℍ
γ : Matrix.SpecialLinearGroup (Fin 2) ℤ
hγ : 1 / 2 ≤ (γ • τ).im
hdenom : ‖denom (↑γ) τ‖ ≤ 1
⊢ ‖f τ‖ ≤ ‖f (γ • τ)‖

Tactic:
simpa only [slash_action_eqn'' _ (mem_Gamma_one γ),
norm_mul, norm_zpow] using le_mul_of_one_le_left (norm_nonneg _) <|
one_le_zpow_of_nonpos₀ (norm_pos_iff.2 (denom_ne_zero _ _)) hdenom hk

Result:
no goals