harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem iSup_affineOpens_eq_top (X : Scheme) : ⨆ i : X.affineOpens, (i : X.Opens) = ⊤

Proof state:
case h.self
X : Scheme
⊢ IsTopologicalBasis (Set.range fun i => ↑↑i)

Tactic:
rw [← Set.image_eq_range]

Result:
case h.self
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Proof state:
case h
X : Scheme
⊢ ⋃ i, ↑↑i = ↑⊤

Tactic:
apply IsTopologicalBasis.sUnion_eq

Result:
case h.self
X : Scheme
⊢ IsTopologicalBasis (Set.range fun i => ↑↑i)

Proof state:
X : Scheme
⊢ ⨆ i, ↑i = ⊤

Tactic:
apply Opens.ext

Result:
case h
X : Scheme
⊢ ↑(⨆ i, ↑i) = ↑⊤

Proof state:
case h.self
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Tactic:
exact isBasis_affine_open X

Result:
no goals

Proof state:
case h
X : Scheme
⊢ ↑(⨆ i, ↑i) = ↑⊤

Tactic:
rw [Opens.coe_iSup]

Result:
case h
X : Scheme
⊢ ⋃ i, ↑↑i = ↑⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeftZeroExtend_eq {x : BitVec w} :
    shiftLeftZeroExtend x n = setWidth (w+n) x <<< n

Proof state:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat <<< n < 2 ^ (w + n)

Tactic:
rw [Nat.shiftLeft_eq, Nat.pow_add]

Result:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat * 2 ^ n < 2 ^ w * 2 ^ n

Proof state:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat * 2 ^ n < 2 ^ w * 2 ^ n

Tactic:
exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)

Result:
no goals

Proof state:
case a
w n : Nat
x : BitVec w
⊢ (x.shiftLeftZeroExtend n).toNat = (setWidth (w + n) x <<< n).toNat

Tactic:
rw [shiftLeftZeroExtend, setWidth]

Result:
case a
w n : Nat
x : BitVec w
⊢ ((x.toNat <<< n)#'⋯).toNat = ((if h : w ≤ w + n then setWidth' h x else BitVec.ofNat (w + n) x.toNat) <<< n).toNat

Proof state:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat <<< n = x.toNat <<< n % 2 ^ (w + n)

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat <<< n < 2 ^ (w + n)

Proof state:
w n : Nat
x : BitVec w
⊢ x.shiftLeftZeroExtend n = setWidth (w + n) x <<< n

Tactic:
apply eq_of_toNat_eq

Result:
case a
w n : Nat
x : BitVec w
⊢ (x.shiftLeftZeroExtend n).toNat = (setWidth (w + n) x <<< n).toNat

Proof state:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ ((x.toNat <<< n)#'⋯).toNat = (setWidth' h✝ x <<< n).toNat

Tactic:
simp only [toNat_ofNatLt, toNat_shiftLeft, toNat_setWidth']

Result:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ x.toNat <<< n = x.toNat <<< n % 2 ^ (w + n)

Proof state:
case a.isFalse
w n : Nat
x : BitVec w
h✝ : ¬w ≤ w + n
⊢ ((x.toNat <<< n)#'⋯).toNat = (BitVec.ofNat (w + n) x.toNat <<< n).toNat

Tactic:
omega

Result:
no goals

Proof state:
case a
w n : Nat
x : BitVec w
⊢ ((x.toNat <<< n)#'⋯).toNat = ((if h : w ≤ w + n then setWidth' h x else BitVec.ofNat (w + n) x.toNat) <<< n).toNat

Tactic:
split

Result:
case a.isTrue
w n : Nat
x : BitVec w
h✝ : w ≤ w + n
⊢ ((x.toNat <<< n)#'⋯).toNat = (setWidth' h✝ x <<< n).toNat

case a.isFalse
w n : Nat
x : BitVec w
h✝ : ¬w ≤ w + n
⊢ ((x.toNat <<< n)#'⋯).toNat = (BitVec.ofNat (w + n) x.toNat <<< n).toNat
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive]
lemma disjoint_smul_set_left : Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)

Tactic:
simpa using disjoint_smul_set (a := a) (t := a⁻¹ • t)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_sq (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt (a ^ 2) = a

Tactic:
rw [pow_two, sqrt_mul_self (A := A) a]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma isRightDerivedFunctor_iff_isLeftKanExtension [L.IsLocalization W] :
    RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

Proof state:
case mpr
C : Type u_1
D : Type u_2
H : Type u_5
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_6, u_5} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W

Tactic:
exact fun h => ⟨h⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
D : Type u_2
H : Type u_5
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_6, u_5} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

Tactic:
exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
H : Type u_5
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_6, u_5} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
H : Type u_5
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_6, u_5} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

case mpr
C : Type u_1
D : Type u_2
H : Type u_5
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
inst✝¹ : Category.{u_6, u_5} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W
-- Mathlib/Algebra/Category/Ring/Colimits.lean
theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
    F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Proof state:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
ext

Result:
case hf.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Proof state:
case hf.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Result:
case hf.a.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Proof state:
case hf.a.a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Tactic:
apply Relation.map

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexBetween.lean
theorem Sbtw.dist_lt_max_dist (p : P) {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) :
    dist p₂ p < max (dist p₁ p) (dist p₃ p)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < dist p₁ p ⊔ dist p₃ p

Tactic:
rw [Sbtw, ← wbtw_vsub_const_iff p, Wbtw, affineSegment_eq_segment, ← insert_endpoints_openSegment,
  Set.mem_insert_iff, Set.mem_insert_iff] at h

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
h : (p₂ -ᵥ p = p₁ -ᵥ p ∨ p₂ -ᵥ p = p₃ -ᵥ p ∨ p₂ -ᵥ p ∈ openSegment ℝ (p₁ -ᵥ p) (p₃ -ᵥ p)) ∧ p₂ ≠ p₁ ∧ p₂ ≠ p₃
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
⊢ dist p₂ p < dist p₁ p ⊔ dist p₃ p

Proof state:
case intro.inl.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
h : p₂ = p₁
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₂ p < dist p₁ p ⊔ dist p₃ p

Tactic:
exact False.elim (hp₂p₁ h)

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p p₁ p₂ p₃ : P
hp₁p₃ : p₁ -ᵥ p ≠ p₃ -ᵥ p
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
r : ℝ
hr : (1 - r) • (p₁ -ᵥ p) + r • (p₃ -ᵥ p) = p₂ -ᵥ p
hr0 : 0 < r
hr1 : r < 1
⊢ 1 - r + r = 1

Tactic:
abel

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_sub_sub_self (x y : E) : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x - y, x - y⟫_𝕜 = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
simp only [inner_sub_left, inner_sub_right]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 - ⟪y, x⟫_𝕜 - (⟪x, y⟫_𝕜 - ⟪y, y⟫_𝕜) = ⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_eq_zero_of_lt_natDegree (p : R[X]) (n : ℕ) (h : p.natDegree < n) :
    hasseDeriv n p = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1) = 0

Tactic:
refine Finset.sum_eq_zero fun x hx => ?_

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
x : ℕ
hx : x ∈ p.support
⊢ (monomial (x - n)) (↑(x.choose n) * p.coeff x) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
x : ℕ
hx : x ∈ p.support
⊢ (monomial (x - n)) (↑(x.choose n) * p.coeff x) = 0

Tactic:
simp [Nat.choose_eq_zero_of_lt ((le_natDegree_of_mem_supp _ hx).trans_lt h)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (hasseDeriv n) p = 0

Tactic:
rw [hasseDeriv_apply, sum_def]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ ∑ n_1 ∈ p.support, (monomial (n_1 - n)) (↑(n_1.choose n) * p.coeff n_1) = 0
-- Mathlib/Algebra/Module/Presentation/DirectSum.lean
@[simp]
lemma finsupp_var (i : ι) (g : pres.G) :
    (finsupp pres ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)

Proof state:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (lof A ι (fun x => N) i) (pres.var g) = DFinsupp.single i (pres.var g)

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (pres.finsupp ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)

Tactic:
apply (finsuppLequivDFinsupp A).injective

Result:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (finsuppLequivDFinsupp A) ((pres.finsupp ι).var ⟨i, g⟩) = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))

Proof state:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (directSum fun x => pres).var ⟨i, g⟩ = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))

Tactic:
rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single]

Result:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (lof A ι (fun x => N) i) (pres.var g) = DFinsupp.single i (pres.var g)

Proof state:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (finsuppLequivDFinsupp A) ((pres.finsupp ι).var ⟨i, g⟩) = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))

Tactic:
erw [(finsuppLequivDFinsupp A).apply_symm_apply]

Result:
case a
A : Type u
inst✝⁴ : Ring A
N : Type v
inst✝³ : AddCommGroup N
inst✝² : Module A N
pres : Presentation A N
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq N
i : ι
g : pres.G
⊢ (directSum fun x => pres).var ⟨i, g⟩ = (finsuppLequivDFinsupp A) (Finsupp.single i (pres.var g))
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepSet_zero_right {s t : Set Ω} : IndepSet s t κ 0

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s t : Set Ω
⊢ IndepSet s t κ 0

Tactic:
simp [IndepSet]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
lemma max_le_of_forall_le {α : Type*} [LinearOrder α] [OrderBot α] (l : Multiset α)
    (n : α) (h : ∀ x ∈ l, x ≤ n) : l.fold max ⊥ ≤ n

Proof state:
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : Multiset α
n : α
h : ∀ x ∈ l, x ≤ n
⊢ fold max ⊥ l ≤ n

Tactic:
induction l using Quotient.inductionOn

Result:
case h
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
n : α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x ≤ n
⊢ fold max ⊥ ⟦a✝⟧ ≤ n

Proof state:
case h
α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
n : α
a✝ : List α
h : ∀ x ∈ ⟦a✝⟧, x ≤ n
⊢ fold max ⊥ ⟦a✝⟧ ≤ n

Tactic:
simpa using List.max_le_of_forall_le _ _ h

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma differentiableAt_LFunction (Φ : ZMod N → ℂ) (s : ℂ) (hs : s ≠ 1 ∨ ∑ j, Φ j = 0) :
    DifferentiableAt ℂ (LFunction Φ) s

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
this : DifferentiableAt ℂ (fun y => ∑ i : ZMod N, Φ i * (hurwitzZeta (toAddCircle i) y - 1 / (y - 1) / y.Gammaℝ)) 1
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) 1

Tactic:
simpa only [mul_sub, sum_sub_distrib, ← sum_mul, hs.neg_resolve_left rfl, zero_mul, sub_zero]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun y => ↑N ^ (-y)) s

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (LFunction Φ) s

Tactic:
refine .mul (by fun_prop) ?_

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) s

Proof state:
case inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) s

Tactic:
exact .sum fun j _ ↦ (differentiableAt_hurwitzZeta _ hs').const_mul _

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) s

Tactic:
rcases ne_or_eq s 1 with hs' | rfl

Result:
case inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) s

case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) 1

Proof state:
case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) 1

Tactic:
have := DifferentiableAt.sum (u := univ) fun j _ ↦
  (differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)

Result:
case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hs : 1 ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0
this : DifferentiableAt ℂ (fun y => ∑ i : ZMod N, Φ i * (hurwitzZeta (toAddCircle i) y - 1 / (y - 1) / y.Gammaℝ)) 1
⊢ DifferentiableAt ℂ (fun y => ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) y) 1
-- Mathlib/Algebra/Lie/Matrix.lean
theorem Matrix.lieConj_symm_apply (P A : Matrix n n R) (h : Invertible P) :
    (P.lieConj h).symm A = P⁻¹ * A * P

Proof state:
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ (P.lieConj h).symm A = P⁻¹ * A * P

Tactic:
simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
  LinearMap.toMatrix'_toLin']

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f :=
  prod_nbij (signBijAux f⁻¹) signBijAux_mem signBijAux_injOn signBijAux_surj fun ⟨a, b⟩ hab ↦
    if h : f⁻¹ b < f⁻¹ a then by
      simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self,
        if_neg (mem_finPairsLT.1 hab).not_le]
    else by
      simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
        if_pos (mem_finPairsLT.1 hab).le]

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
h : ¬f⁻¹ b < f⁻¹ a
⊢ (if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) =
    if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
  if_pos (mem_finPairsLT.1 hab).le]

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
h : f⁻¹ b < f⁻¹ a
⊢ (if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) =
    if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self,
  if_neg (mem_finPairsLT.1 hab).not_le]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem MonoidHom.isOfFinOrder [Monoid H] (f : G →* H) {x : G} (h : IsOfFinOrder x) :
    IsOfFinOrder <| f x :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by
    obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
    exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

Proof state:
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Tactic:
exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Tactic:
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one

Result:
case intro.intro
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f x ^ n = 1

Tactic:
rw [← f.map_pow, hn, f.map_one]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem compl_sSup : (sSup s)ᶜ = ⨅ i ∈ s, iᶜ

Proof state:
α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
⊢ (sSup s)ᶜ = ⨅ i ∈ s, iᶜ

Tactic:
simp only [sSup_eq_iSup, compl_iSup]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_inter' (hf : LeftInvOn f' f s) : f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s

Proof state:
case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)

Tactic:
rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩

Result:
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s

case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)

Proof state:
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)

Tactic:
exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁

Tactic:
rwa [← hf h]

Result:
no goals

Proof state:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁ ∩ f '' s

Tactic:
exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁

Tactic:
rwa [mem_preimage, hf h]

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s

Tactic:
rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩

Result:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁ ∩ f '' s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_lt {x : Int} {m : Nat} (h : 0 < m) : bmod x m < (m + 1) / 2

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ x.bmod m < (↑m + 1) / 2

Tactic:
dsimp [bmod]

Result:
x : Int
m : Nat
h : 0 < m
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) < (↑m + 1) / 2

Proof state:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < ?isFalse.b

Tactic:
show _ < 0

Result:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < 0

Proof state:
case isFalse.h₂
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ 0 ≤ (↑m + 1) / 2

Tactic:
exact Int.le.intro_sub _ rfl

Result:
no goals

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) < (↑m + 1) / 2

Tactic:
split

Result:
case isTrue
x : Int
m : Nat
h : 0 < m
h✝ : x % ↑m < (↑m + 1) / 2
⊢ x % ↑m < (↑m + 1) / 2

case isFalse
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < (↑m + 1) / 2

Proof state:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < 0

Tactic:
have : x % m < m := emod_lt_of_pos x (ofNat_pos.mpr h)

Result:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
this : x % ↑m < ↑m
⊢ x % ↑m - ↑m < 0

Proof state:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
this : x % ↑m < ↑m
⊢ x % ↑m - ↑m < 0

Tactic:
exact Int.sub_neg_of_lt this

Result:
no goals

Proof state:
case isTrue
x : Int
m : Nat
h : 0 < m
h✝ : x % ↑m < (↑m + 1) / 2
⊢ x % ↑m < (↑m + 1) / 2

Tactic:
assumption

Result:
no goals

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < (↑m + 1) / 2

Tactic:
apply Int.lt_of_lt_of_le

Result:
case isFalse.h₁
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ x % ↑m - ↑m < ?isFalse.b

case isFalse.h₂
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ?isFalse.b ≤ (↑m + 1) / 2

case isFalse.b
x : Int
m : Nat
h : 0 < m
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ Int