harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem of_prime_card [hGX : IsPretransitive G X] (hp : Nat.Prime (Nat.card X)) :
    IsPreprimitive G X

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B = Set.univ

Tactic:
rw [Set.eq_univ_iff_ncard, eq_comm, ← hp.dvd_iff_eq ((Set.one_lt_ncard).mpr hB').ne']

Result:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B.ncard ∣ Nat.card X

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
⊢ IsPreprimitive G X

Tactic:
refine ⟨fun {B} hB ↦ B.subsingleton_or_nontrivial.imp id fun hB' ↦ ?_⟩

Result:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
⊢ B = Set.univ

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
⊢ B = Set.univ

Tactic:
have : Finite X := (Nat.card_ne_zero.mp hp.ne_zero).2

Result:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B = Set.univ

Proof state:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
hGX : IsPretransitive G X
hp : Nat.Prime (Nat.card X)
B : Set X
hB : IsBlock G B
hB' : B.Nontrivial
this : Finite X
⊢ B.ncard ∣ Nat.card X

Tactic:
exact hB.ncard_dvd_card hB'.nonempty

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[field_simps]
lemma divp_eq_div [DivisionMonoid α] (a : α) (u : αˣ) : a /ₚ u = a / u

Proof state:
α : Type u
inst✝ : DivisionMonoid α
a : α
u : αˣ
⊢ a /ₚ u = a / ↑u

Tactic:
rw [div_eq_mul_inv, divp, u.val_inv_eq_inv_val]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_id_of_epi {x : SimplexCategory} (i : x ⟶ x) [Epi i] : i = 𝟙 _

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective ⇑(Hom.toOrderHom i)

Tactic:
rw [Fintype.bijective_iff_surjective_and_card i.toOrderHom, ← epi_iff_surjective,
  eq_self_iff_true, and_true]

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Epi i

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective (Hom.toOrderHom i).toFun

Tactic:
dsimp

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective ⇑(Hom.toOrderHom i)

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
this : IsIso i
⊢ i = 𝟙 x

Tactic:
haveI := this

Result:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
this✝ this : IsIso i
⊢ i = 𝟙 x

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ i = 𝟙 x

Tactic:
suffices IsIso i by
  haveI := this
  apply eq_id_of_isIso

Result:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ IsIso i

Proof state:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Epi i

Tactic:
infer_instance

Result:
no goals

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ IsIso i

Tactic:
apply isIso_of_bijective

Result:
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective (Hom.toOrderHom i).toFun

Proof state:
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
this✝ this : IsIso i
⊢ i = 𝟙 x

Tactic:
apply eq_id_of_isIso

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α}
    (hs : s.SupIndep fun i => t.sup fun i' => f (i, i'))
    (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, i') = f ((i, i').1, (i, i').2)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mapFinIdx_mk (a : Array α) (h : a.size = n) (f : (i : Nat) → α → (h : i < n) → β) :
    (Vector.mk a h).mapFinIdx f =
      Vector.mk (a.mapFinIdx fun i a h' => f i a (by simpa [h] using h')) (by simp [h]) := rfl

Proof state:
α : Type ?u.11069
n : Nat
β : Type ?u.11102
a : Array α
h : a.size = n
f : (i : Nat) → α → i < n → β
⊢ (a.mapFinIdx fun i a_1 h' => f i a_1 ⋯).size = n

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type ?u.11069
n : Nat
β : Type ?u.11102
a✝ : Array α
h : a✝.size = n
f : (i : Nat) → α → i < n → β
i : Nat
a : α
h' : i < a✝.size
⊢ i < n

Tactic:
simpa [h] using h'

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomialY_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialY / P z ^ 3 =
      W.toAffine.polynomialY.evalEval (P x / P z ^ 2) (P y / P z ^ 3)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 3 + (W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) (toAffine W).polynomialY +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0

Tactic:
rw [eval_polynomialY, Affine.evalEval_polynomialY]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3) / P z ^ 3 + (W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * 1) -
      (2 * (P y / P z ^ 3) + (toAffine W).a₁ * (P x / P z ^ 2) + (toAffine W).a₃ +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 3 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) (toAffine W).polynomialY

Tactic:
linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
  W.a₁ * P x / P z ^ 2 * div_self hPz + W.a₃ * div_self (pow_ne_zero 3 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3) / P z ^ 3 + (W.a₁ * P x / P z ^ 2 * 1 + W.a₃ * 1) -
      (2 * (P y / P z ^ 3) + (toAffine W).a₁ * (P x / P z ^ 2) + (toAffine W).a₃ +
        (W.a₁ * P x / P z ^ 2 * (P z / P z) + W.a₃ * (P z ^ 3 / P z ^ 3))) =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem abs_self_eq_nnrealPart_add_nnrealPart_neg (f : α →ᵇ ℝ) :
    abs ∘ ⇑f = (↑) ∘ f.nnrealPart + (↑) ∘ (-f).nnrealPart

Proof state:
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ abs ∘ ⇑f = toReal ∘ ⇑f.nnrealPart + toReal ∘ ⇑(-f).nnrealPart

Tactic:
funext x

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (abs ∘ ⇑f) x = (toReal ∘ ⇑f.nnrealPart + toReal ∘ ⇑(-f).nnrealPart) x

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (abs ∘ ⇑f) x = (toReal ∘ ⇑f.nnrealPart + toReal ∘ ⇑(-f).nnrealPart) x

Tactic:
dsimp

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ |f x| = f x ⊔ 0 + -f x ⊔ 0

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ |f x| = f x ⊔ 0 + -f x ⊔ 0

Tactic:
simp only [max_zero_add_max_neg_zero_eq_abs_self]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem univ_sum_single_apply [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
    ∑ j : α, single i m j = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, (single i m) j = m

Tactic:
rw [single, coe_mk, Finset.sum_pi_single']

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, (single i m) j = m

Tactic:
classical rw [single, coe_mk, Finset.sum_pi_single']

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_cases (f : ℝ → E) (a b) :
    (∫ x in a..b, f x ∂μ) ∈ ({∫ x in Ι a b, f x ∂μ, -∫ x in Ι a b, f x ∂μ} : Set E)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Tactic:
rw [intervalIntegral_eq_integral_uIoc]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ ∈ {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Data/Fintype/Perm.lean
theorem mem_perms_of_finset_iff :
    ∀ {s : Finset α} {f : Perm α}, f ∈ permsOfFinset s ↔ ∀ {x}, f x ≠ x → x ∈ s

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs } ↔
    ∀ {x : α}, f x ≠ x → x ∈ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs }

Tactic:
exact mem_permsOfList_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s

Tactic:
rintro ⟨⟨l⟩, hs⟩ f

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs } ↔
    ∀ {x : α}, f x ≠ x → x ∈ { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs }
-- Mathlib/CategoryTheory/Generator/Basic.lean
lemma IsSeparating.of_equivalence
    {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) :
    IsSeparating (α.functor.obj '' 𝒢) := fun X Y f g H =>
  α.inverse.map_injective (h _ _ (fun Z hZ h => by
    obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h
    simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
      H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']))

Proof state:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h : IsSeparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : Z ∈ 𝒢
h' : α.functor.obj Z ⟶ X
⊢ (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map f = (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map g

Tactic:
simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
  H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h']

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h✝ : IsSeparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : Z ∈ 𝒢
h : Z ⟶ α.inverse.obj X
⊢ h ≫ α.inverse.map f = h ≫ α.inverse.map g

Tactic:
obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h

Result:
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h : IsSeparating 𝒢
D : Type u_1
inst✝ : Category.{u_2, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ G ∈ α.functor.obj '' 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : Z ∈ 𝒢
h' : α.functor.obj Z ⟶ X
⊢ (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map f = (α.toAdjunction.homEquiv Z X) h' ≫ α.inverse.map g
-- Mathlib/Data/List/TakeDrop.lean
theorem takeI_left (l₁ l₂ : List α) : takeI (length l₁) (l₁ ++ l₂) = l₁ :=
  (takeI_eq_take (by simp only [length_append, Nat.le_add_right])).trans (take_left _ _)

Proof state:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
⊢ l₁.length ≤ (l₁ ++ l₂).length

Tactic:
simp only [length_append, Nat.le_add_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) : W'.addX P Q = P y ^ 2 * Q z * Q x

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addX P Q = P y ^ 2 * Q z * Q x

Tactic:
rw [addX, hPz, X_eq_zero_of_Z_eq_zero hP hPz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * Q y ^ 2 * 0 + Q x * P y ^ 2 * Q z - 2 * 0 * P y * Q y * Q z + 2 * Q x * P y * Q y * 0 -
                            W'.a₁ * 0 ^ 2 * Q y * Q z +
                          W'.a₁ * Q x ^ 2 * P y * 0 +
                        W'.a₂ * 0 ^ 2 * Q x * Q z -
                      W'.a₂ * 0 * Q x ^ 2 * 0 -
                    W'.a₃ * 0 * P y * Q z ^ 2 +
                  W'.a₃ * Q x * Q y * 0 ^ 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * 0 ^ 2 * Q z ^ 2 -
          W'.a₄ * Q x ^ 2 * 0 ^ 2 +
        3 * W'.a₆ * 0 * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q x

Tactic:
ring1

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem card_eq_or_dvd : Nat.card G = 1 ∨ p ∣ Nat.card G

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
cases finite_or_infinite G

Result:
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Proof state:
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
rw [Nat.card_eq_zero_of_infinite]

Result:
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0

Proof state:
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
hn : Nat.card G = p ^ 0
⊢ p ^ 0 = 1 ∨ p ∣ p ^ 0

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Tactic:
exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩

Result:
no goals

Proof state:
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n

Tactic:
rcases n with - | n

Result:
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
hn : Nat.card G = p ^ 0
⊢ p ^ 0 = 1 ∨ p ∣ p ^ 0

case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Proof state:
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
obtain ⟨n, hn⟩ := iff_card.mp hG

Result:
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Proof state:
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0

Tactic:
exact Or.inr ⟨0, rfl⟩

Result:
no goals

Proof state:
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
rw [hn]

Result:
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
rw [pow_succ']

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_one_oreDiv_one_smul (r : R) (x : X[S⁻¹]) :
    ((r • 1 : M) /ₒ (1 : S)) • x = r • x

Proof state:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ (r • 1 /ₒ 1) • x = r • x

Tactic:
rw [oreDiv_one_smul, smul_one_smul]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem sup_eq_eqvGen (r s : Setoid α) :
    r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y

Proof state:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Tactic:
apply congr_arg sInf

Result:
α : Type u_1
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Proof state:
α : Type u_1
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Result:
no goals

Proof state:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y

Tactic:
rw [eqvGen_eq]

Result:
α : Type u_1
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, r x y ∨ s x y → s_1 x y}
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem IsNatPowModT.bit1 :
    IsNatPowModT (Nat.mod (Nat.pow a b) m = c) a (nat_lit 2 * b + 1) m
      (Nat.mod (Nat.mul c (Nat.mod (Nat.mul c a) m)) m) :=
  ⟨by
    rintro rfl
    show a ^ (2 * b + 1) % m = (a ^ b % m) * ((a ^ b % m * a) % m) % m
    rw [pow_add, two_mul, pow_add, pow_one, Nat.mul_mod (a ^ b % m) a, Nat.mod_mod,
      ← Nat.mul_mod (a ^ b) a, ← Nat.mul_mod, mul_assoc]⟩

Proof state:
a b m : ℕ
⊢ (a.pow (2 * b + 1)).mod m = (((a.pow b).mod m).mul ((((a.pow b).mod m).mul a).mod m)).mod m

Tactic:
show a ^ (2 * b + 1) % m = (a ^ b % m) * ((a ^ b % m * a) % m) % m

Result:
a b m : ℕ
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m

Proof state:
a b m : ℕ
⊢ a ^ (2 * b + 1) % m = a ^ b % m * (a ^ b % m * a % m) % m

Tactic:
rw [pow_add, two_mul, pow_add, pow_one, Nat.mul_mod (a ^ b % m) a, Nat.mod_mod,
  ← Nat.mul_mod (a ^ b) a, ← Nat.mul_mod, mul_assoc]

Result:
no goals

Proof state:
a b m : ℕ
c : ℕ
⊢ (a.pow b).mod m = c → (a.pow (2 * b + 1)).mod m = (c.mul ((c.mul a).mod m)).mod m

Tactic:
rintro rfl

Result:
a b m : ℕ
⊢ (a.pow (2 * b + 1)).mod m = (((a.pow b).mod m).mul ((((a.pow b).mod m).mul a).mod m)).mod m
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_le {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ x in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

Proof state:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

Tactic:
obtain ⟨c₁, _, c₂, hc₂, h⟩ := hf b hb

Result:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

Proof state:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x

Tactic:
filter_upwards [h]

Result:
case h
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a

Proof state:
case h
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a

Tactic:
exact fun _ H u hu => (H u hu).2

Result:
no goals

Proof state:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

Tactic:
refine ⟨c₂, hc₂, ?_⟩

Result:
case intro.intro.intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c₁ : ℝ
left✝ : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x