harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma aemeasurable_of_integrable_exp_mul (huv : u ≠ v)
    (hu_int : Integrable (fun ω ↦ exp (u * X ω)) μ)
    (hv_int : Integrable (fun ω ↦ exp (v * X ω)) μ) :
    AEMeasurable X μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : u = 0
⊢ AEMeasurable X μ

Tactic:
have hv : v ≠ 0 := ne_of_ne_of_eq huv.symm hu

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : u = 0
hv : v ≠ 0
⊢ AEMeasurable X μ

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hu hu_int.aemeasurable

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
⊢ AEMeasurable X μ

Tactic:
by_cases hu : u = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : u = 0
⊢ AEMeasurable X μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : ¬u = 0
⊢ AEMeasurable X μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
u v : ℝ
huv : u ≠ v
hu_int : Integrable (fun ω => rexp (u * X ω)) μ
hv_int : Integrable (fun ω => rexp (v * X ω)) μ
hu : u = 0
hv : v ≠ 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hv hv_int.aemeasurable

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_ne_zero [Nontrivial S] : minpolyDiv R x ≠ 0

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)
⊢ False

Tactic:
rw [e, zero_mul] at this

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : 0 = map (algebraMap R S) (minpoly R x)
⊢ False

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ minpolyDiv R x ≠ 0

Tactic:
intro e

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
⊢ False

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : 0 = map (algebraMap R S) (minpoly R x)
⊢ False

Tactic:
exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
⊢ False

Tactic:
have := minpolyDiv_spec R x

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
e : minpolyDiv R x = 0
this : minpolyDiv R x * (X - C x) = map (algebraMap R S) (minpoly R x)
⊢ False
-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem dvd_pow_natDegree_of_eval₂_eq_zero {f : R →+* A} (hf : Function.Injective f) {p : R[X]}
    (hp : p.Monic) (x y : R) (z : A) (h : p.eval₂ f z = 0) (hz : f x * z = f y) :
    x ∣ y ^ p.natDegree

Proof state:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval₂ f (f x * z) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y

Tactic:
rwa [hz, Polynomial.eval₂_at_apply, hf] at this

Result:
no goals

Proof state:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
rw [injective_iff_map_eq_zero'] at hf

Result:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Proof state:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ y ^ (p.scaleRoots x).natDegree ∈ span {x}

Tactic:
refine
  (scaleRoots.isWeaklyEisensteinAt _
        (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
    ?_ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl

Result:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Proof state:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ x ∣ y ^ p.natDegree

Tactic:
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]

Result:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ y ^ (p.scaleRoots x).natDegree ∈ span {x}

Proof state:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ (p.scaleRoots x).IsRoot y

Tactic:
have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h

Result:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval₂ f (f x * z) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_inj (h : IsPrimitiveRoot ζ k) ⦃i j : ℕ⦄ (hi : i < k) (hj : j < k) (H : ζ ^ i = ζ ^ j) :
    i = j

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j ≤ i

Tactic:
rw [← tsub_eq_zero_iff_le]

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ i = j

Tactic:
apply le_antisymm hij

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j ≤ i

Proof state:
case a
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) = 1

Tactic:
rw [← ((h.isUnit (lt_of_le_of_lt (Nat.zero_le _) hi)).pow i).mul_left_inj, ← pow_add,
  tsub_add_cancel_of_le hij, H, one_mul]

Result:
no goals

Proof state:
case inr
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j

Tactic:
exact (this hj hi H.symm (le_of_not_le hij)).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ k ∣ j - i

Tactic:
apply h.dvd_of_pow_eq_one

Result:
case a
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ (j - i) = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ j - i = 0

Tactic:
apply Nat.eq_zero_of_dvd_of_lt _ (lt_of_le_of_lt tsub_le_self hj)

Result:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ k ∣ j - i

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j

Tactic:
wlog hij : i ≤ j generalizing i j

Result:
case inr
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j

M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ i = j
-- Mathlib/Deprecated/Logic.lean
theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : ∀ x : α, β x)
    (h : a₁ = a₂) : HEq (let x : α := a₁; b x) (let x : α := a₂; b x)

Proof state:
α : Sort v
β : α → Sort u
a₁ a₂ : α
b : (x : α) → β x
h : a₁ = a₂
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₂;
    b x)

Tactic:
cases h

Result:
case refl
α : Sort v
β : α → Sort u
a₁ : α
b : (x : α) → β x
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₁;
    b x)

Proof state:
case refl
α : Sort v
β : α → Sort u
a₁ : α
b : (x : α) → β x
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₁;
    b x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_le (a b c : α) : ((Ico a b).filter fun x => c ≤ x) = Ico (max a c) b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico (a ⊔ c) b

Tactic:
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem tprod_eq_zero_mul'
    {f : ℕ → M} (hf : Multipliable (fun n ↦ f (n + 1))) :
    ∏' b, f b = f 0 * ∏' b, f (b + 1)

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousMul M
f : ℕ → M
hf : Multipliable fun n => f (n + 1)
⊢ ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)

Tactic:
simpa only [prod_range_one] using (prod_mul_tprod_nat_mul' hf).symm

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem Principal.iterate_lt (hao : a < o) (ho : Principal op o) (n : ℕ) : (op a)^[n] a < o

Proof state:
case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
⊢ (op a)^[0] a < o

Tactic:
rwa [Function.iterate_zero]

Result:
no goals

Proof state:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
n : ℕ
⊢ (op a)^[n] a < o

Tactic:
induction' n with n hn

Result:
case zero
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
⊢ (op a)^[0] a < o

case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a)^[n + 1] a < o

Proof state:
case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a)^[n + 1] a < o

Tactic:
rw [Function.iterate_succ']

Result:
case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Proof state:
case succ
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Tactic:
exact ho hao hn

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem ext {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
  Hom.ext α β w h

Proof state:
C : Type u_1
inst✝ : Category.{?u.16554, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
rw [w]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic'_symm_apply {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1)
    (x : EuclideanSpace ℝ (Fin n)) :
    ((stereographic' n v).symm x : E) =
      let U : (ℝ ∙ (v : E))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) :=
        (OrthonormalBasis.fromOrthogonalSpanSingleton n (ne_zero_of_mem_unit_sphere v)).repr
      (‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (4 : ℝ) • (U.symm x : E) +
        (‖(U.symm x : E)‖ ^ 2 + 4)⁻¹ • (‖(U.symm x : E)‖ ^ 2 - 4) • v.val

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
x : EuclideanSpace ℝ (Fin n)
⊢ ↑(↑(stereographic' n v).symm x) =
    let U := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr;
    (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • 4 • ↑(U.symm x) + (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • (‖↑(U.symm x)‖ ^ 2 - 4) • ↑v

Tactic:
simp [real_inner_comm, stereographic, stereographic', ← Submodule.coe_norm]

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem exists_subgroup_card_pow_prime_le [Finite G] (p : ℕ) :
    ∀ {n m : ℕ} [_hp : Fact p.Prime] (_hdvd : p ^ m ∣ Nat.card G) (H : Subgroup G)
      (_hH : Nat.card H = p ^ n) (_hnm : n ≤ m), ∃ K : Subgroup G, Nat.card K = p ^ m ∧ H ≤ K
  | n, m => fun {hdvd H hH hnm} =>
    (lt_or_eq_of_le hnm).elim
      (fun hnm : n < m =>
        have h0m : 0 < m := lt_of_le_of_lt n.zero_le hnm
        have _wf : m - 1 < m := Nat.sub_lt h0m zero_lt_one
        have hnm1 : n ≤ m - 1 := le_tsub_of_add_le_right hnm
        let ⟨K, hK⟩ :=
          @exists_subgroup_card_pow_prime_le _ _ n (m - 1) _
            (Nat.pow_dvd_of_le_of_pow_dvd tsub_le_self hdvd) H hH hnm1
        have hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n = m
⊢ Nat.card ↥H = p ^ m ∧ H ≤ H

Tactic:
simp [hH, hnm]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
⊢ p ^ (m - 1 + 1) ∣ Nat.card G

Tactic:
rwa [tsub_add_cancel_of_le h0m.nat_succ_le]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n < m
h0m : 0 < m
_wf : m - 1 < m
hnm1 : n ≤ m - 1
K : Subgroup G
hK : Nat.card ↥K = p ^ (m - 1) ∧ H ≤ K
hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G
K' : Subgroup G
hK' : Nat.card ↥K' = p ^ (m - 1 + 1) ∧ K ≤ K'
⊢ Nat.card ↥K' = p ^ m

Tactic:
rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_eq_of_lt {a b : Ordinal} (h : a < b) : a % b = a

Proof state:
a b : Ordinal.{u_4}
h : a < b
⊢ a % b = a

Tactic:
simp only [mod_def, div_eq_zero_of_lt h, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α → m α) :
    SatisfiesM (·.size = a.size) (a.modifyM i f)

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
h✝ : ¬i < a.size
⊢ SatisfiesM (fun x => x.size = a.size) (pure a)

Tactic:
exact .pure rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
⊢ SatisfiesM (fun x => x.size = a.size)
    (if h : i < a.size then
      let v := a[i];
      do
      let v ← f v
      pure (a.set i v h)
    else pure a)

Tactic:
split

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
h✝ : i < a.size
⊢ SatisfiesM (fun x => x.size = a.size)
    (let v := a[i];
    do
    let v ← f v
    pure (a.set i v h✝))

case isFalse
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
h✝ : ¬i < a.size
⊢ SatisfiesM (fun x => x.size = a.size) (pure a)

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
h✝ : i < a.size
⊢ SatisfiesM (fun x => x.size = a.size)
    (let v := a[i];
    do
    let v ← f v
    pure (a.set i v h✝))

Tactic:
exact .bind_pre <| .of_true fun _ => .pure <| by simp only [size_set]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
⊢ SatisfiesM (fun x => x.size = a.size) (a.modifyM i f)

Tactic:
unfold modifyM

Result:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
⊢ SatisfiesM (fun x => x.size = a.size)
    (if h : i < a.size then
      let v := a[i];
      do
      let v ← f v
      pure (a.set i v h)
    else pure a)

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
i : Nat
f : α → m α
h✝ : i < a.size
x✝ : α
⊢ (a.set i x✝ h✝).size = a.size

Tactic:
simp only [size_set]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem summable_iff_not_tendsto_nat_atTop {f : ℕ → ℝ≥0} :
    Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Proof state:
f : ℕ → ℝ≥0
⊢ Summable f ↔ ¬Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop]

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem basic_inter {X : Compactum} (A B : Set X) : basic (A ∩ B) = basic A ∩ basic B

Proof state:
case h.mpr.intro
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ Compactum.basic A
h2 : G ∈ Compactum.basic B
⊢ G ∈ Compactum.basic (A ∩ B)

Tactic:
exact inter_mem h1 h2

Result:
no goals

Proof state:
case h.mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B → G ∈ Compactum.basic (A ∩ B)

Tactic:
rintro ⟨h1, h2⟩

Result:
case h.mpr.intro
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
h1 : G ∈ Compactum.basic A
h2 : G ∈ Compactum.basic B
⊢ G ∈ Compactum.basic (A ∩ B)

Proof state:
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) ↔ G ∈ Compactum.basic A ∩ Compactum.basic B

Tactic:
constructor

Result:
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) → G ∈ Compactum.basic A ∩ Compactum.basic B

case h.mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B → G ∈ Compactum.basic (A ∩ B)

Proof state:
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) → G ∈ Compactum.basic A ∩ Compactum.basic B

Tactic:
intro hG

Result:
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B

Proof state:
X : Compactum
A B : Set X.A
⊢ Compactum.basic (A ∩ B) = Compactum.basic A ∩ Compactum.basic B

Tactic:
ext G

Result:
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ Compactum.basic (A ∩ B) ↔ G ∈ Compactum.basic A ∩ Compactum.basic B

Proof state:
case h.mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
⊢ G ∈ Compactum.basic A ∩ Compactum.basic B

Tactic:
constructor <;> filter_upwards [hG] with _

Result:
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ A

case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ B

Proof state:
case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ A

case h
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ Compactum.basic (A ∩ B)
a✝ : X.A
⊢ a✝ ∈ A ∩ B → a✝ ∈ B

Tactic:
exacts [And.left, And.right]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.exists_is_const_of_deriv_eq_zero
    (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (deriv f) 0) : ∃ a, ∀ x ∈ s, f x = a :=
  hs.exists_is_const_of_fderiv_eq_zero hs' hf (fun {x} hx ↦ by ext; simp [← deriv_fderiv, hf' hx])

Proof state:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (0 x) 1

Tactic:
simp [← deriv_fderiv, hf' hx]

Result:
no goals

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ fderiv 𝕜 f x = 0 x

Tactic:
ext

Result:
case h
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : 𝕜 → G
s : Set 𝕜
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (deriv f) 0 s
x : 𝕜
hx : x ∈ s
⊢ (fderiv 𝕜 f x) 1 = (0 x) 1
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma ExactAt.of_iso (hK : K.ExactAt i) {L : HomologicalComplex C c} (e : K ≅ L) :
    L.ExactAt i

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex C c
e : K ≅ L
⊢ (L.sc i).Exact

Tactic:
exact ShortComplex.exact_of_iso ((shortComplexFunctor C c i).mapIso e) hK

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : K.ExactAt i
L : HomologicalComplex C c
e : K ≅ L
⊢ L.ExactAt i

Tactic:
rw [exactAt_iff] at hK ⊢

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex C c
e : K ≅ L
⊢ (L.sc i).Exact
-- Mathlib/RingTheory/Ideal/Prime.lean
theorem IsPrime.mem_of_pow_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) :
    r ∈ I

Proof state:
case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ (n + 1) ∈ I
⊢ r ∈ I

Tactic:
rw [pow_succ] at H

Result:
case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Proof state:
case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ n * r ∈ I
⊢ r ∈ I

Tactic:
exact Or.casesOn (hI.mem_or_mem H) ih id

Result:
no goals

Proof state:
case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I

Tactic:
exact (mt (eq_top_iff_one _).2 hI.1).elim H

Result:
no goals

Proof state:
case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : r ^ 0 ∈ I
⊢ r ∈ I

Tactic:
rw [pow_zero] at H

Result:
case zero
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
H : 1 ∈ I
⊢ r ∈ I

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
H : r ^ n ∈ I
⊢ r ∈ I

Tactic:
induction n with
| zero =>
  rw [pow_zero] at H
  exact (mt (eq_top_iff_one _).2 hI.1).elim H
| succ n ih =>
  rw [pow_succ] at H
  exact Or.casesOn (hI.mem_or_mem H) ih id

Result:
no goals