harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem ofWithBot_le {boxes : Finset (WithBot (Box ι))}
    {le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I}
    {pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint}
    (H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J') :
    ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Tactic:
simpa [ofWithBot, le_def]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Tactic:
have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
  simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ boxes, J ≠ ⊥ → ∃ J' ∈ π, J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J' ∈ π, J ≤ J'

Tactic:
simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k

Proof state:
n m k : Nat
⊢ (n - m) * k = n * k - m * k

Tactic:
induction m with
| zero => simp
| succ m ih => rw [Nat.sub_succ, Nat.pred_mul, ih, succ_mul, Nat.sub_sub]; done

Result:
no goals

Proof state:
case zero
n k : Nat
⊢ (n - 0) * k = n * k - 0 * k

Tactic:
simp

Result:
no goals

Proof state:
case succ
n k m : Nat
ih : (n - m) * k = n * k - m * k
⊢ (n - (m + 1)) * k = n * k - (m + 1) * k

Tactic:
rw [Nat.sub_succ, Nat.pred_mul, ih, succ_mul, Nat.sub_sub]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem exists_sum {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) :
    (∃ fab, p fab) ↔ (∃ fa fb, p (Sum.rec fa fb))

Proof state:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t => rec fa fb t

Tactic:
rw [← not_forall_not, forall_sum]

Result:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t => rec fa fb t) ↔
    ∃ fa fb, p fun t => rec fa fb t

Proof state:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t => rec fa fb t) ↔
    ∃ fa fb, p fun t => rec fa fb t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem image (h : SpectrumRestricts a f) : f '' spectrum S a = spectrum R a

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ f '' spectrum S a = spectrum R a

Tactic:
simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem card_neighborSet_union_compl_neighborSet [Fintype V] (G : SimpleGraph V) (v : V)
    [Fintype (G.neighborSet v ∪ Gᶜ.neighborSet v : Set V)] :
    #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Proof state:
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
Finset.card_compl, Set.toFinset_card, Set.card_singleton]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v ∪ Gᶜ.neighborSet v)
⊢ #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset = Fintype.card V - 1

Tactic:
classical simp_rw [neighborSet_union_compl_neighborSet_eq, Set.toFinset_compl,
    Finset.card_compl, Set.toFinset_card, Set.card_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
    a ∈ m ↔ b ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a b : α
hab : (a == b) = true
⊢ a ∈ m ↔ b ∈ m

Tactic:
simp [mem_iff_contains, contains_congr h hab]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_flatMap (f : β → γ) (g : α → Vector β m) (l : Vector α n) :
     (l.flatMap g).map f = l.flatMap fun a => (g a).map f

Proof state:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
m : Nat
f : β → γ
g : α → Vector β m
l : Array α
⊢ map f ({ toArray := l, size_toArray := ⋯ }.flatMap g) =
    { toArray := l, size_toArray := ⋯ }.flatMap fun a => map f (g a)

Tactic:
simp [Array.map_flatMap]

Result:
no goals

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
m n : Nat
f : β → γ
g : α → Vector β m
l : Vector α n
⊢ map f (l.flatMap g) = l.flatMap fun a => map f (g a)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
m : Nat
f : β → γ
g : α → Vector β m
l : Array α
⊢ map f ({ toArray := l, size_toArray := ⋯ }.flatMap g) =
    { toArray := l, size_toArray := ⋯ }.flatMap fun a => map f (g a)
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
private lemma jacobiMatrix_comp_inr_inr (i j : P.rels) :
    (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) =
      MvPolynomial.rename Sum.inr (P.jacobiMatrix i j)

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_4
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (pderiv (Sum.inr (P.map i))) ((Q.comp P).relation (Sum.inr j)) = (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))

Tactic:
apply pderiv_rename Sum.inr_injective

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_4
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (pderiv ((Q.comp P).map (Sum.inr i))) ((Q.comp P).relation (Sum.inr j)) =
    (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))

Tactic:
simp only [comp_map, Sum.elim_inr]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_4
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (pderiv (Sum.inr (P.map i))) ((Q.comp P).relation (Sum.inr j)) = (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_4
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (Q.comp P).jacobiMatrix (Sum.inr i) (Sum.inr j) = (rename Sum.inr) (P.jacobiMatrix i j)

Tactic:
rw [jacobiMatrix_apply, jacobiMatrix_apply]

Result:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_4
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝³ : DecidableEq (Q.comp P).rels
inst✝² : Fintype (Q.comp P).rels
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ (pderiv ((Q.comp P).map (Sum.inr i))) ((Q.comp P).relation (Sum.inr j)) =
    (rename Sum.inr) ((pderiv (P.map i)) (P.relation j))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_mkArray_of_some {f : α → Option β} (h : f a = some b) :
    (mkArray n a).filterMap f = mkArray n b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
n : Nat
f : α → Option β
h : f a = some b
⊢ filterMap f (mkArray n a) = mkArray n b

Tactic:
simp [filterMap_mkArray, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : tmod a b = a

Proof state:
a b : Int
H1 : 0 ≤ a
H2 : a < b
⊢ a.tmod b = a

Tactic:
rw [tmod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
  | n, 0 => by simp [Nat.min_zero]
  | 0, m => by simp [Nat.zero_min]
  | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]

Proof state:
α : Type u_1
a : α
m : Nat
⊢ take 0 (replicate m a) = replicate (min 0 m) a

Tactic:
simp [Nat.zero_min]

Result:
no goals

Proof state:
α : Type u_1
a : α
n m : Nat
⊢ take n.succ (replicate m.succ a) = replicate (min n.succ m.succ) a

Tactic:
simp [replicate_succ, succ_min_succ, take_replicate]

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
⊢ take n (replicate 0 a) = replicate (min n 0) a

Tactic:
simp [Nat.min_zero]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq' : a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b :=
  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ (a == a) = true

Tactic:
exact LawfulBEq.rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ a = b → (a == b) = true

Tactic:
intro h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a = b
⊢ (a == b) = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a = b
⊢ (a == b) = true

Tactic:
subst h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ (a == a) = true
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurable_inv_iff₀ {G₀ : Type*} [GroupWithZero G₀] [MeasurableSpace G₀]
    [MeasurableInv G₀] {f : α → G₀} : (Measurable fun x => (f x)⁻¹) ↔ Measurable f :=
  ⟨fun h => by simpa only [inv_inv] using h.inv, fun h => h.inv⟩

Proof state:
α : Type u_3
m : MeasurableSpace α
G₀ : Type u_4
inst✝² : GroupWithZero G₀
inst✝¹ : MeasurableSpace G₀
inst✝ : MeasurableInv G₀
f : α → G₀
h : Measurable fun x => (f x)⁻¹
⊢ Measurable f

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem id : MeasurableEmbedding (id : α → α) :=
  ⟨injective_id, measurable_id, fun s hs => by rwa [image_id]⟩

Proof state:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (_root_.id '' s)

Tactic:
rwa [image_id]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem length_eq_zero {s : Seq α} {h : s.Terminates} :
    s.length h = 0 ↔ s = nil

Proof state:
α : Type u
s : Seq α
h : s.Terminates
⊢ s.length h = 0 ↔ s = nil

Tactic:
simp [length, TerminatedAt]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
lemma congr_map_apply {X Y : Cᵒᵖ} {f g : X ⟶ Y} (h : f = g) (m : M.obj X) :
    M.map f m = M.map g m

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f g : X ⟶ Y
h : f = g
m : ↑(M.obj X)
⊢ (ConcreteCategory.hom (M.map f)) m = (ConcreteCategory.hom (M.map g)) m

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_map_left (l₁ : Vector α n) (l₂ : Vector β n) (f : α → α') (g : α' → β → γ) :
    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Proof state:
α : Type u_1
n : Nat
β : Type u_2
α' : Type u_3
γ : Type u_4
l₁ : Vector α n
l₂ : Vector β n
f : α → α'
g : α' → β → γ
⊢ zipWith g (map f l₁) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith g (map f { toArray := l₁, size_toArray := ⋯ }) l₂ =
    zipWith (fun a b => g (f a) b) { toArray := l₁, size_toArray := ⋯ } l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith g (map f { toArray := l₁, size_toArray := ⋯ }) { toArray := l₂, size_toArray := h } =
    zipWith (fun a b => g (f a) b) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Tactic:
simp [Array.zipWith_map_left]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith g (map f { toArray := l₁, size_toArray := ⋯ }) l₂ =
    zipWith (fun a b => g (f a) b) { toArray := l₁, size_toArray := ⋯ } l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
f : α → α'
g : α' → β → γ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith g (map f { toArray := l₁, size_toArray := ⋯ }) { toArray := l₂, size_toArray := h } =
    zipWith (fun a b => g (f a) b) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }
-- Mathlib/GroupTheory/Nilpotent.lean
theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {n : ℕ} :
    upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n

Proof state:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n

Tactic:
intro h

Result:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ nilpotencyClass G ≤ n

Proof state:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ nilpotencyClass G ≤ n

Tactic:
exact Nat.find_le h

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ ↔ nilpotencyClass G ≤ n

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n

case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n

Tactic:
exact upperCentralSeries_mono _ h

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G n = ⊤

Tactic:
rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]

Result:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤

Tactic:
intro h

Result:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G n = ⊤
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_map {β} [MeasurableSpace β] {φ : α → β} (hφ : AEMeasurable φ μ) {f : β → G}
    (hfm : AEStronglyMeasurable f (Measure.map φ μ)) :
    ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ :=
  let g := hfm.mk f
  calc
    ∫ y, f y ∂Measure.map φ μ = ∫ y, g y ∂Measure.map φ μ := integral_congr_ae hfm.ae_eq_mk
    _ = ∫ y, g y ∂Measure.map (hφ.mk φ) μ

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ μ
f : β → G
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → G := AEStronglyMeasurable.mk f hfm
⊢ ∫ (y : β), g y ∂Measure.map φ μ = ∫ (y : β), g y ∂Measure.map (AEMeasurable.mk φ hφ) μ

Tactic:
congr 1

Result:
case e_μ
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ μ
f : β → G
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → G := AEStronglyMeasurable.mk f hfm
⊢ Measure.map φ μ = Measure.map (AEMeasurable.mk φ hφ) μ

Proof state:
case e_μ
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ μ
f : β → G
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → G := AEStronglyMeasurable.mk f hfm
⊢ Measure.map φ μ = Measure.map (AEMeasurable.mk φ hφ) μ

Tactic:
exact Measure.map_congr hφ.ae_eq_mk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f)

Proof state:
α : Type u_1
f : α → Bool
l : List (List α)
⊢ l.flatten.any f = l.any fun x => x.any f

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem dart_snd_mem_support_of_mem_darts {u v : V} (p : G.Walk u v) {d : G.Dart}
    (h : d ∈ p.darts) : d.snd ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.toProd.2 ∈ p.support

Tactic:
simpa using p.reverse.dart_fst_mem_support_of_mem_darts (by simp [h] : d.symm ∈ p.reverse.darts)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
d : G.Dart
h : d ∈ p.darts
⊢ d.symm ∈ p.reverse.darts

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem nhds_basis_uniformity' {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {x : α} : (𝓝 x).HasBasis p fun i => ball x (s i)

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap (Prod.mk x) (𝓤 α)).HasBasis p fun i => ball x (s i)

Tactic:
exact h.comap (Prod.mk x)

Result:
no goals

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun i => ball x (s i)

Tactic:
rw [nhds_eq_comap_uniformity]

Result:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap (Prod.mk x) (𝓤 α)).HasBasis p fun i => ball x (s i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
    (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.length

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (if findIdx (fun x => x == a) l₁ < l₁.length then findIdx (fun x => x == a) l₁
    else findIdx (fun x => x == a) l₂ + l₁.length) =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.length
⊢ findIdx (fun x => x == a) l₁ =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.length
⊢ findIdx (fun x => x == a) l₂ + l₁.length =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length

Proof state:
case isFalse.hnc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.length
⊢ ¬a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.length
⊢ findIdx (fun x => x == a) l₂ + l₁.length =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length

Tactic:
rw [if_neg]

Result:
case isFalse.hnc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : ¬findIdx (fun x => x == a) l₁ < l₁.length
⊢ ¬a ∈ l₁

Proof state:
case isTrue.hc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.length
⊢ a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.length
⊢ findIdx (fun x => x == a) l₁ =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length

Tactic:
rw [if_pos]

Result:
case isTrue.hc
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h : findIdx (fun x => x == a) l₁ < l₁.length
⊢ a ∈ l₁

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.length

Tactic:
rw [idxOf, findIdx_append]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (if findIdx (fun x => x == a) l₁ < l₁.length then findIdx (fun x => x == a) l₁
    else findIdx (fun x => x == a) l₂ + l₁.length) =
    if a ∈ l₁ then findIdx (fun x => x == a) l₁ else findIdx (fun x => x == a) l₂ + l₁.length
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma dite_mul (a : P → α) (b : ¬ P → α) (c : α) :
    (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem bsize : ∀ {s}, ValidFor l m r s → s.bsize = utf8Len m
  | _, ⟨⟩ => by simp [Substring.bsize, Nat.add_sub_cancel_left]

Proof state:
l m r : List Char
⊢ { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } }.bsize =
    utf8Len m

Tactic:
simp [Substring.bsize, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_self : relrank A A = 1

Proof state:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relrank A = 1

Tactic:
rw [relrank_eq_rank_of_le (le_refl A), extendScalars_self, IntermediateField.rank_bot]

Result:
no goals