harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all `n : ℕ`,
`X ^ n * exp (v * X)` is integrable. -/
lemma integrable_pow_mul_exp_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) (n : ℕ) :
    Integrable (fun ω ↦ X ω ^ n * exp (v * X ω)) μ

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
⊢ Integrable (fun ω => X ω ^ n * rexp (v * X ω)) μ

Tactic:
convert integrable_rpow_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n
-- Mathlib/Topology/Algebra/Module/LinearPMap.lean
theorem closure_def' {f : E →ₗ.[R] F} (hf : ¬f.IsClosable) : f.closure = f

Proof state:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬f.IsClosable
⊢ f.closure = f

Tactic:
simp [closure, hf]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma IsBlock.smul_eq_smul_of_subset (hB : IsBlock G B) (hg : g₁ • B ⊆ g₂ • B) :
    g₁ • B = g₂ • B

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ B = ∅

Tactic:
simpa using (hB hg').eq_bot_of_le hg

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g₁ g₂ : G
hB : IsBlock G ∅
hg : g₁ • ∅ ⊆ g₂ • ∅
hg' : g₁ • ∅ ≠ g₂ • ∅
⊢ False

Tactic:
simp at hg'

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
⊢ g₁ • B = g₂ • B

Tactic:
by_contra! hg'

Result:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ False

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ False

Tactic:
obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg

Result:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g₁ g₂ : G
hB : IsBlock G ∅
hg : g₁ • ∅ ⊆ g₂ • ∅
hg' : g₁ • ∅ ≠ g₂ • ∅
⊢ False
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem union_ae_eq_univ_of_ae_eq_univ_left (h : s =ᵐ[μ] univ) : (s ∪ t : Set α) =ᵐ[μ] univ :=
  (ae_eq_set_union h (ae_eq_refl t)).trans <| by rw [univ_union]

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᶠ[ae μ] univ
⊢ univ ∪ t =ᶠ[ae μ] univ

Tactic:
rw [univ_union]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_strict_mono_right (hb : b < b') (hr : 0 < r) : lineMap a b r < lineMap a b' r

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (lineMap a b) r < (lineMap a b') r

Tactic:
simp only [lineMap_apply_module]

Result:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b b' : E
r : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'

Tactic:
exact add_lt_add_left (smul_lt_smul_of_pos_left hb hr) _

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_iSup_right (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (t : ι → Submodule R N) :
    map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))

Tactic:
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_right]

Result:
no goals

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
t : ι → Submodule R N
this : map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))
⊢ map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)

Tactic:
simpa only [span_eq] using this

Result:
no goals

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i)

Tactic:
suffices map₂ f (span R s) (⨆ i, span R (t i : Set N)) = ⨆ i, map₂ f (span R s) (span R (t i)) by
  simpa only [span_eq] using this

Result:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Submodule R M
t : ι → Submodule R N
⊢ map₂ f (span R ↑s) (⨆ i, span R ↑(t i)) = ⨆ i, map₂ f (span R ↑s) (span R ↑(t i))
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_factorial_mul (n : ℕ) [hp : Fact p.Prime] :
    padicValNat p (p * n) ! = padicValNat p n ! + n

Proof state:
case a
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(padicValNat p (p * n)!) = ↑(padicValNat p n ! + n)

Tactic:
rw [padicValNat_eq_emultiplicity <| factorial_pos (p * n), Nat.cast_add,
    padicValNat_eq_emultiplicity <| factorial_pos n]

Result:
case a
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + ↑n

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValNat p (p * n)! = padicValNat p n ! + n

Tactic:
apply Nat.cast_injective (R := ℕ∞)

Result:
case a
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(padicValNat p (p * n)!) = ↑(padicValNat p n ! + n)

Proof state:
case a
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ emultiplicity p (p * n)! = emultiplicity p n ! + ↑n

Tactic:
exact Prime.emultiplicity_factorial_mul hp.out

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isZero_of_isStrictlyLE (n i : ℤ) (hi : n < i) [K.IsStrictlyLE n] :
    IsZero (K.X i) :=
  isZero_X_of_isStrictlySupported K (embeddingUpIntLE n) i
    (by simpa only [not_mem_range_embeddingUpIntLE_iff] using hi)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
n i : ℤ
hi : n < i
inst✝ : K.IsStrictlyLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [not_mem_range_embeddingUpIntLE_iff] using hi

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma isUnit_iff : IsUnit u ↔ u = 1 ∨ u = -1

Proof state:
u : ℤ
⊢ IsUnit u ↔ u = 1 ∨ u = -1

Tactic:
refine ⟨fun h ↦ isUnit_eq_one_or h, fun h ↦ ?_⟩

Result:
u : ℤ
h : u = 1 ∨ u = -1
⊢ IsUnit u

Proof state:
⊢ -1 * -1 = 1

Tactic:
decide

Result:
no goals

Proof state:
case inr

⊢ IsUnit (-1)

Tactic:
exact ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩

Result:
no goals

Proof state:
u : ℤ
h : u = 1 ∨ u = -1
⊢ IsUnit u

Tactic:
rcases h with (rfl | rfl)

Result:
case inl

⊢ IsUnit 1

case inr

⊢ IsUnit (-1)

Proof state:
case inl

⊢ IsUnit 1

Tactic:
exact isUnit_one

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_bot_of_ne (h : u ≠ v) : (⊥ : SimpleGraph V).edist u v = ⊤

Proof state:
V : Type u_1
u v : V
h : u ≠ v
⊢ ⊥.edist u v = ⊤

Tactic:
rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Partition.lean
theorem ofComposition_surj {n : ℕ} : Function.Surjective (ofComposition n)

Proof state:
n : ℕ
⊢ Function.Surjective (ofComposition n)

Tactic:
rintro ⟨b, hb₁, hb₂⟩

Result:
case mk
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : b.sum = n
⊢ ∃ a, ofComposition n a = { parts := b, parts_pos := hb₁, parts_sum := hb₂ }

Proof state:
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ b.sum = n

Tactic:
simpa using hb₂

Result:
no goals

Proof state:
case mk
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : b.sum = n
⊢ ∃ a, ofComposition n a = { parts := b, parts_pos := hb₁, parts_sum := hb₂ }

Tactic:
induction b using Quotient.inductionOn with | _ b => ?_

Result:
case mk.h
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ ∃ a, ofComposition n a = { parts := ⟦b⟧, parts_pos := hb₁, parts_sum := hb₂ }

Proof state:
case mk.h
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ ∃ a, ofComposition n a = { parts := ⟦b⟧, parts_pos := hb₁, parts_sum := hb₂ }

Tactic:
exact ⟨⟨b, hb₁, by simpa using hb₂⟩, Partition.ext rfl⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem natDegree_linear (ha : a ≠ 0) : natDegree (C a * X + C b) = 1

Proof state:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).natDegree = 1

Tactic:
rw [natDegree_add_C, natDegree_C_mul_X a ha]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_neg (P : Fin 3 → R) : W'.addZ P (W'.neg P) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addZ P (W'.neg P) = 0

Tactic:
rw [addZ, neg_X, neg_Y, neg_Z, negY]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 -
                      (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mul_mem_closedBall_iff_norm : a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Tactic:
rw [mem_closedBall_iff_norm'', mul_div_cancel_left]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem none : Partrec fun _ => none :=
  (of_primrec (Nat.Primrec.const 1)).rfind.of_eq fun _ =>
    eq_none_iff.2 fun _ ⟨h, _⟩ => by simp at h

Proof state:
x✝² x✝¹ : ℕ
x✝ : x✝¹ ∈ Nat.rfind fun n => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair x✝² n)
h : (Nat.rfind fun n => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair x✝² n)).Dom
h✝ : (Nat.rfind fun n => (fun m => decide (m = 0)) <$> (↑fun x => 1) (Nat.pair x✝² n)).get h = x✝¹
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem replaceF_cons_of_some {l : List α} (p) (h : p a = some a') :
    (a :: l).replaceF p = a' :: l

Proof state:
α : Type u_1
a' a : α
l : List α
p : α → Option α
h : p a = some a'
⊢ replaceF p (a :: l) = a' :: l

Tactic:
simp [replaceF_cons, h]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem sSup_eq_conGen (S : Set (Con M)) :
    sSup S = conGen fun x y => ∃ c : Con M, c ∈ S ∧ c x y

Proof state:
case h
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝ : Con M
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}

Tactic:
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = sInf {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}

Tactic:
apply congr_arg sInf

Result:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ upperBounds S = {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ upperBounds S = {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}

Tactic:
ext

Result:
case h
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x✝ : Con M
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = conGen fun x y => ∃ c ∈ S, c x y

Tactic:
rw [conGen_eq]

Result:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = sInf {s | ∀ (x y : M), (∃ c ∈ S, c x y) → s x y}
-- Mathlib/GroupTheory/Nilpotent.lean
theorem comap_upperCentralSeries_quotient_center (n : ℕ) :
    comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeriesStep Hn) =
    comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn)))

Tactic:
rw [upperCentralSeriesStep_eq_comap_center]

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Tactic:
let Hn := upperCentralSeries (G ⧸ center G) n

Result:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Proof state:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Tactic:
calc
  comap (mk' (center G)) (upperCentralSeriesStep Hn) =
      comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) := by
    rw [upperCentralSeriesStep_eq_comap_center]
  _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
    QuotientGroup.comap_comap_center
  _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
    (comap_center_subst ih)
  _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
    symm (upperCentralSeriesStep_eq_comap_center _)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ

Tactic:
induction' n with n ih

Result:
case zero
G : Type u_1
inst✝ : Group G
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) 0) = upperCentralSeries G (Nat.succ 0)

case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (n + 1)) = upperCentralSeries G (n + 1).succ

Proof state:
case zero
G : Type u_1
inst✝ : Group G
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) 0) = upperCentralSeries G (Nat.succ 0)

Tactic:
simp only [upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
  (upperCentralSeries_one G).symm]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem coe_jacobson_quotient (I : Ideal R) [I.IsTwoSided] :
    (jacobson (R ⧸ I) : Set (R ⧸ I)) = Module.jacobson R (R ⧸ I)

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ 0 ∈ Module.jacobson R (R ⧸ I)

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
let f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨AddHom.id _, fun _ _ ↦ rfl⟩

Result:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(Submodule.map f (Module.jacobson R (R ⧸ I))) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
apply Set.image_id

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ LinearMap.ker f ≤ Module.jacobson R (R ⧸ I)

Tactic:
rintro _ rfl

Result:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ 0 ∈ Module.jacobson R (R ⧸ I)

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

Tactic:
rw [jacobson, ← Module.map_jacobson_of_ker_le (f := f) Function.surjective_id]

Result:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ ↑(Submodule.map f (Module.jacobson R (R ⧸ I))) = ↑(Module.jacobson R (R ⧸ I))

R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ LinearMap.ker f ≤ Module.jacobson R (R ⧸ I)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_coe_ne_top_iff_summable_coe {f : α → ℝ≥0} :
    (∑' a, (f a : ℝ≥0∞)) ≠ ∞ ↔ Summable fun a => (f a : ℝ)

Proof state:
α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable f

Tactic:
exact tsum_coe_ne_top_iff_summable

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun a => ↑(f a)

Tactic:
rw [NNReal.summable_coe]

Result:
α : Type u_1
f : α → ℝ≥0
⊢ ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable f
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv (h : S.RightHomologyData) :
    h.homologyIso.hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.homologyIso.hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv

Tactic:
dsimp only [homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF)
    {f : Option (β k) → Option (β k)} : (m.alter k f).getKey! k' =
      if k == k' then
        if (f (m.get? k)).isSome then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
h : m.val.WF
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKey! k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'

Tactic:
simp_to_model [alter] using List.getKey!_alterKey

Result:
no goals
-- Mathlib/Algebra/Group/Action/Sum.lean
theorem smul_swap : (a • x).swap = a • x.swap

Proof state:
M : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : SMul M α
inst✝ : SMul M β
a : M
x : α ⊕ β
⊢ (a • x).swap = a • x.swap

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma image_subset_Iic_sup [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) :
    s.image f ⊆ Iic (s.sup f)

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
⊢ image f s ⊆ Iic (s.sup f)

Tactic:
refine fun i hi ↦ mem_Iic.2 ?_

Result:
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
i : α
hi : i ∈ image f s
⊢ i ≤ s.sup f

Proof state:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f

Tactic:
exact le_sup hj

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
i : α
hi : i ∈ image f s
⊢ i ≤ s.sup f

Tactic:
obtain ⟨j, hj, rfl⟩ := mem_image.1 hi

Result:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
f : ι → α
s : Finset ι
j : ι
hj : j ∈ s
hi : f j ∈ image f s
⊢ f j ≤ s.sup f