harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
@[reassoc]
lemma liftCycles_shift_homologyπ
    (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ (K⟦n⟧).X i) (j : ℤ)
    (hj : (up ℤ).next i = j) (hf : f ≫ (K⟦n⟧).d i j = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ)
    (hj' : (up ℤ).next i' = j') :
    (K⟦n⟧).liftCycles f j hj hf ≫ (K⟦n⟧).homologyπ i =
      K.liftCycles (f ≫ (K.shiftFunctorObjXIso n i i' (by omega)).hom) j' hj' (by
        simp only [next] at hj hj'
        obtain rfl : i' = i + n

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
obtain rfl : i' = i + n := by omega

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Tactic:
apply (one_smul (M := ℤˣ) _).symm.trans _

Result:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ 1 • (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Proof state:
C : Type u_1
inst✝² : Category.{?u.81256, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ i' = i + n

Tactic:
omega

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma oneCoboundaries_le_oneCocycles : oneCoboundaries A ≤ oneCocycles A

Proof state:
case intro
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ (dZero A) x ∈ oneCocycles A

Tactic:
exact dZero_apply_mem_oneCocycles x

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ oneCoboundaries A ≤ oneCocycles A

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ (dZero A) x ∈ oneCocycles A
-- Mathlib/RepresentationTheory/Invariants.lean
theorem mul_average_left (g : G) : ↑(Finsupp.single g 1) * average k G = average k G

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (g * x) = ⅟↑(Fintype.card G) • ∑ x : G, f x

Tactic:
rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1

Tactic:
set f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • Finset.univ.sum f

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • Finset.univ.sum f

Tactic:
show ⅟ (Fintype.card G : k) • ∑ x : G, f (g * x) = ⅟ (Fintype.card G : k) • ∑ x : G, f x

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → MonoidAlgebra k G := fun x => Finsupp.single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x : G, f (g * x) = ⅟↑(Fintype.card G) • ∑ x : G, f x

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ Finsupp.single g 1 * average k G = average k G

Tactic:
simp only [mul_one, Finset.mul_sum, Algebra.mul_smul_comm, average, MonoidAlgebra.of_apply,
  Finset.sum_congr, MonoidAlgebra.single_mul_single]

Result:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x : G, single (g * x) 1 = ⅟↑(Fintype.card G) • ∑ x : G, single x 1
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_le_tsub_add : a + b - c ≤ a - c + b

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a - c ≤ b + (a - c)

Tactic:
exact add_tsub_le_assoc

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b - c ≤ a - c + b

Tactic:
rw [add_comm, add_comm _ b]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a - c ≤ b + (a - c)
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_neg_right (x y : F) : ⟪x, -y⟫ = -⟪x, y⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜) (-⟪y, x⟫_𝕜) = -⟪x, y⟫_𝕜

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜) (-⟪y, x⟫_𝕜) = -⟪x, y⟫_𝕜

Tactic:
simp only [RingHom.map_neg, inner_conj_symm]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesOnBall.restrictScalars (hf : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesOnBall f (p.restrictScalars 𝕜) x r :=
  ⟨hf.r_le.trans (FormalMultilinearSeries.radius_le_of_le (fun n ↦ by simp)), hf.r_pos, hf.hasSum⟩

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
n : ℕ
⊢ ‖FormalMultilinearSeries.restrictScalars 𝕜 p n‖ ≤ ‖p n‖

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_over_two_pow_succ (n : ℕ) :
    sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2

Proof state:
case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

Tactic:
refine mul_nonneg (sin_nonneg_of_nonneg_of_le_pi ?_ ?_) zero_le_two

Result:
case hy.refine_1
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2)

case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π

Proof state:
case hy.refine_1
n : ℕ
⊢ 0 ≤ π / 2 ^ (n + 2)

Tactic:
positivity

Result:
no goals

Proof state:
case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
rw [sub_nonneg]

Result:
case hx
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2

Proof state:
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) = √(2 - sqrtTwoAddSeries 0 n) / 2

Tactic:
rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_eq_sq, mul_pow,
  sin_sq_pi_over_two_pow_succ, sub_mul]

Result:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2

case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

case hy
n : ℕ
⊢ 0 ≤ sin (π / 2 ^ (n + 2)) * 2

Proof state:
case hy.refine_2
n : ℕ
⊢ π / 2 ^ (n + 2) ≤ π

Tactic:
exact div_le_self pi_pos.le <| one_le_pow₀ one_le_two

Result:
no goals

Proof state:
n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2

Tactic:
congr <;> norm_num

Result:
no goals

Proof state:
case hx
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2

Tactic:
exact (sqrtTwoAddSeries_lt_two _).le

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_eq_self : toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • p

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b = b + 0 • p

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = b ↔ b ∈ Set.Ioc a (a + p)

Tactic:
rw [toIocMod_eq_iff, and_iff_left]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ z, b = b + z • p
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem eq_mk_iff_exists {X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (x : Meq P S) (y : Meq P T) :
    mk x = mk y ↔ ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine h1 = y.refine h2

Proof state:
case h.e'_3.h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑(y.refine h2.unop) I =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))

Tactic:
dsimp [diagram]

Result:
case h.e'_3.h
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
I : (unop W).Arrow
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ : ToType (P.obj (op I.Y)) = CD (((unop W).index P).left I)
⊢ ↑y { Y := I.Y, f := I.f, hf := ⋯ } =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) I))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((unop W).index P) (multiequalizer (T.index P))
            (fun I => Multiequalizer.ι (T.index P) (I.map h2.unop)) ⋯))
        ((Meq.equiv P T).symm y))
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.ball_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
    Metric.ball (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 < r ^ 2}

Proof state:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i : n, x i ^ 2
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}

Tactic:
simp_rw [mem_setOf, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]

Result:
no goals

Proof state:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}

Tactic:
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _

Result:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i : n, x i ^ 2
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}

Proof state:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.ball 0 r = {x | ∑ i : n, x i ^ 2 < r ^ 2}

Tactic:
ext x

Result:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ x ∈ Metric.ball 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 < r ^ 2}
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem rel_associated_iff_map_eq_map {p q : Multiset α} :
    Multiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q

Tactic:
simp only [mk_eq_mk_iff_associated]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q

Tactic:
rw [← Multiset.rel_eq, Multiset.rel_map]

Result:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
-- Mathlib/Data/Nat/BinaryRec.lean
theorem binaryRec_eq {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)}
    (b n) (h : f false 0 z = z ∨ (n = 0 → b = true)) :
    binaryRec z f (bit b n) = f b n (binaryRec z f n)

Proof state:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
⊢ ⋯ ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Tactic:
generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e

Result:
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
b : Bool
n : Nat
h : f false 0 z = z ∨ (n = 0 → b = true)
h' : ¬bit b n = 0
e : motive (bit ((bit b n).testBit 0) (bit b n >>> 1)) = motive (bit b n)
⊢ e ▸ f ((bit b n).testBit 0) (bit b n >>> 1) (binaryRec z f (bit b n >>> 1)) = f b n (binaryRec z f n)

Proof state:
case intro
motive : Nat → Sort u
z : motive 0
f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)
h' : bit false 0 = 0
h : f false 0 z = z
⊢ (if n0 : bit false 0 = 0 then ⋯ ▸ z
    else
      let x := f (1 &&& bit false 0 != 0) (bit false 0 >>> 1) (binaryRec z f (bit false 0 >>> 1));
      ⋯ ▸ x) =
    f false 0
      (if n0 : 0 = 0 then ⋯ ▸ z
      else
        let x := f (1 &&& 0 != 0) (0 >>> 1) (binaryRec z f (0 >>> 1));
        ⋯ ▸ x)

Tactic:
exact h.symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
lemma sigmaι_eq_iff (i j : ι) (x y) :
    (Sigma.ι f i).base x = (Sigma.ι f j).base y ↔
      (Sigma.mk i x : Σ i, f i) = Sigma.mk j y

Proof state:
case mpr
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
⊢ ⟨i, x⟩ = ⟨j, y⟩ → (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y

Tactic:
rintro ⟨rfl⟩

Result:
case mpr.refl
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f i).base) x

Proof state:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
⊢ (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y → ⟨i, x⟩ = ⟨j, y⟩

Tactic:
intro H

Result:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H : (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y
⊢ ⟨i, x⟩ = ⟨j, y⟩

Proof state:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H : (ConcreteCategory.hom (Sigma.ι f i).base) x = (ConcreteCategory.hom (Sigma.ι f j).base) y
⊢ ⟨i, x⟩ = ⟨j, y⟩

Tactic:
rw [← ι_sigmaIsoGlued_inv, ← ι_sigmaIsoGlued_inv] at H

Result:
case mp
ι : Type u
f : ι → Scheme
i j : ι
x : ↑↑(f i).toPresheafedSpace
y : ↑↑(f j).toPresheafedSpace
H :
  (ConcreteCategory.hom ((disjointGlueData f).ι i ≫ (sigmaIsoGlued f).inv).base) x =
    (ConcreteCategory.hom ((disjointGlueData f).ι j ≫ (sigmaIsoGlued f).inv).base) y
⊢ ⟨i, x⟩ = ⟨j, y⟩
-- Mathlib/Data/Setoid/Partition.lean
theorem card_classes_ker_le {α β : Type*} [Fintype β] (f : α → β)
    [Fintype (Setoid.ker f).classes] : Fintype.card (Setoid.ker f).classes ≤ Fintype.card β

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(ker f).classes
⊢ Fintype.card ↑(ker f).classes ≤ Fintype.card β

Tactic:
exact
le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(ker f).classes
⊢ Fintype.card ↑(ker f).classes ≤ Fintype.card β

Tactic:
classical exact
    le_trans (Set.card_le_card (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_toIcoMod (θ ψ : ℝ) : ↑(toIcoMod two_pi_pos ψ θ) = (θ : Angle)

Proof state:
θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
refine ⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩

Result:
θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)

Proof state:
θ ψ : ℝ
⊢ ↑(toIcoMod two_pi_pos ψ θ) = ↑θ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]

Result:
θ ψ : ℝ
⊢ ∃ k, toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Proof state:
θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)

Tactic:
rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem subset_iff_eq_or_mem (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ⊆ y ↔ x = y ∨ x ∈ y

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
⊢ x = y ∨ x ∈ y

Tactic:
by_cases hyx : y ⊆ x

Result:
case pos
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : y ⊆ x
⊢ x = y ∨ x ∈ y

case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ y.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
⊢ z ∈ x

Tactic:
by_contra hzx

Result:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ y.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
hzx : z ∉ x
⊢ False

Proof state:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ y.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
⊢ m ⊆ x

Tactic:
intro z hzm

Result:
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 => x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ y.toSet \ x.toSet
hm' : ∀ x_1 ∈ y.toSet \ x.toSet, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
⊢ z ∈ x

Proof state:
case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Tactic:
exact hy.subset_of_mem h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp]
lemma mul_le_iff_le_one_right [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) (mul_le_mul_left a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : PosMulReflectLE α
a0 : 0 < a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Basic.lean
theorem mapRange_eq_map {R S : Type*} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R)
    (f : R →+* S) : Finsupp.mapRange f f.map_zero p = map f p

Proof state:
σ : Type u
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange ⇑f ⋯ p = (map f) p

Tactic:
rw [p.as_sum, Finsupp.mapRange_finset_sum, map_sum (map f)]

Result:
σ : Type u
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x ∈ p.support, Finsupp.mapRange ⇑f ⋯ ((monomial x) (coeff x p)) =
    ∑ x ∈ p.support, (map f) ((monomial x) (coeff x p))

Proof state:
σ : Type u
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ ∑ x ∈ p.support, Finsupp.mapRange ⇑f ⋯ ((monomial x) (coeff x p)) =
    ∑ x ∈ p.support, (map f) ((monomial x) (coeff x p))

Tactic:
refine Finset.sum_congr rfl fun n _ => ?_

Result:
σ : Type u
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ p.support
⊢ Finsupp.mapRange ⇑f ⋯ ((monomial n) (coeff n p)) = (map f) ((monomial n) (coeff n p))

Proof state:
σ : Type u
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
x✝ : n ∈ p.support
⊢ Finsupp.mapRange ⇑f ⋯ ((monomial n) (coeff n p)) = (map f) ((monomial n) (coeff n p))

Tactic:
rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]

Result:
no goals