harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Countable.lean
theorem Countable.biUnion_iff {s : Set α} {t : ∀ a ∈ s, Set β} (hs : s.Countable) :
    (⋃ a ∈ s, t a ‹_›).Countable ↔ ∀ a (ha : a ∈ s), (t a ha).Countable

Proof state:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable ↑s
⊢ (⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
⊢ (⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable

Tactic:
have := hs.to_subtype

Result:
α : Type u
β : Type v
s : Set α
t : (a : α) → a ∈ s → Set β
hs : s.Countable
this : Countable ↑s
⊢ (⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measurePreserving_mul_prod_inv [IsMulLeftInvariant ν] :
    MeasurePreserving (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Proof state:
case h.e'_5.h.mk
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
x y : G
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) = ((fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)) (x, y)

Tactic:
simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
⊢ MeasurePreserving (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
convert (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν)
  using 1

Result:
case h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
⊢ (fun z => (z.2 * z.1, z.1⁻¹)) = (fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)

Proof state:
case h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
⊢ (fun z => (z.2 * z.1, z.1⁻¹)) = (fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)

Tactic:
ext1 ⟨x, y⟩

Result:
case h.e'_5.h.mk
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
x y : G
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) = ((fun z => (z.2, z.2⁻¹ * z.1)) ∘ fun z => (z.2, z.2 * z.1)) (x, y)
-- Mathlib/Topology/Basic.lean
theorem frontier_univ : frontier (univ : Set X) = ∅

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ frontier univ = ∅

Tactic:
simp [frontier]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
    a ≤ l.max?.get (isSome_max?_of_mem h)

Proof state:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ b :: t
⊢ a ≤ (b :: t).max?.get ⋯

Tactic:
simp only [max?_cons, Option.get_some] at ih ⊢

Result:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ b :: t
⊢ a ≤ t.max?.elim b (max b)

Proof state:
case cons.inr.intro
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.max? = some q
⊢ a ≤ t.max?.elim b (max b)

Tactic:
simp only [hq, Option.elim_some] at ih ⊢

Result:
case cons.inr.intro
a b : Nat
t : List Nat
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.max? = some q
ih : ∀ (h : a ∈ t), a ≤ (some q).get ⋯
⊢ a ≤ max b q

Proof state:
case nil
a : Nat
h : a ∈ []
⊢ a ≤ [].max?.get ⋯

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.inl
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ a :: t
⊢ a ≤ t.max?.elim a (max a)

Tactic:
cases t.max? with
| none => simp
| some b => simpa using Nat.le_max_left _ _

Result:
no goals

Proof state:
case cons
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ b :: t
⊢ a ≤ t.max?.elim b (max b)

Tactic:
rcases mem_cons.1 h with (rfl|h)

Result:
case cons.inl
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ a :: t
⊢ a ≤ t.max?.elim a (max a)

case cons.inr
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h✝ : a ∈ b :: t
h : a ∈ t
⊢ a ≤ t.max?.elim b (max b)

Proof state:
case cons.inr
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h✝ : a ∈ b :: t
h : a ∈ t
⊢ a ≤ t.max?.elim b (max b)

Tactic:
obtain ⟨q, hq⟩ := Option.isSome_iff_exists.1 (isSome_max?_of_mem h)

Result:
case cons.inr.intro
a b : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.max? = some q
⊢ a ≤ t.max?.elim b (max b)

Proof state:
case cons.inl.some
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ a :: t
b : Nat
⊢ a ≤ (some b).elim a (max a)

Tactic:
simpa using Nat.le_max_left _ _

Result:
no goals

Proof state:
case cons.inr.intro
a b : Nat
t : List Nat
h✝ : a ∈ b :: t
h : a ∈ t
q : Nat
hq : t.max? = some q
ih : ∀ (h : a ∈ t), a ≤ (some q).get ⋯
⊢ a ≤ max b q

Tactic:
exact Nat.le_trans (ih h) (Nat.le_max_right _ _)

Result:
no goals

Proof state:
case cons.inl.none
a : Nat
t : List Nat
ih : ∀ (h : a ∈ t), a ≤ t.max?.get ⋯
h : a ∈ a :: t
⊢ a ≤ none.elim a (max a)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b :=
  (lt_div_iff₀ <| pos_iff_ne_zero.2 fun hr => False.elim <| by simp [hr] at h).1 h

Proof state:
a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False

Tactic:
simp [hr] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_signExtend (x : BitVec w) :
    (x.signExtend v).toInt = Int.bmod x.toNat (2^(min v w))

Proof state:
case neg
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Tactic:
rw [toInt_signExtend_of_lt hv, Nat.min_eq_right (by omega), toInt_eq_toNat_bmod]

Result:
no goals

Proof state:
w v : Nat
x : BitVec w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Tactic:
by_cases hv : v ≤ w

Result:
case pos
w v : Nat
x : BitVec w
hv : v ≤ w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

case neg
w v : Nat
x : BitVec w
hv : ¬v ≤ w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Proof state:
w v : Nat
x : BitVec w
hv : w < v
⊢ w ≤ v

Tactic:
omega

Result:
no goals

Proof state:
case neg
w v : Nat
x : BitVec w
hv : ¬v ≤ w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Tactic:
simp only [Nat.not_le] at hv

Result:
case neg
w v : Nat
x : BitVec w
hv : w < v
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Proof state:
case pos
w v : Nat
x : BitVec w
hv : v ≤ w
⊢ (signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

Tactic:
simp [toInt_signExtend_of_le hv, Nat.min_eq_left hv]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem image_setOf_maximal : f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_maximal (by simp [f.le_iff_le])

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_replicate :
    (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none

Proof state:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ findIdx? p (replicate (n + 1) a) = if 0 < n + 1 ∧ p a = true then some 0 else none

Tactic:
simp only [replicate, findIdx?_cons, Nat.zero_add, zero_lt_succ, true_and]

Result:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ (if p a = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (replicate n a))) =
    if p a = true then some 0 else none

Proof state:
case zero
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ findIdx? p (replicate 0 a) = if 0 < 0 ∧ p a = true then some 0 else none

Tactic:
simp

Result:
no goals

Proof state:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ (if p a = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (replicate n a))) =
    if p a = true then some 0 else none

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ findIdx? p (replicate n a) = if 0 < n ∧ p a = true then some 0 else none

Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [replicate, findIdx?_cons, Nat.zero_add, zero_lt_succ, true_and]
  split <;> simp_all

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dOne_comp_dZero : dOne A ∘ₗ dZero A = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ dOne A ∘ₗ dZero A = 0

Tactic:
ext x g

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
g : G × G
⊢ (dOne A ∘ₗ dZero A) x g = 0 x g

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
g : G × G
⊢ 0 = 0 x g

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
g : G × G
⊢ (dOne A ∘ₗ dZero A) x g = 0 x g

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, dOne_apply A, dZero_apply A, map_sub,
  map_mul, LinearMap.mul_apply, sub_sub_sub_cancel_left, sub_add_sub_cancel, sub_self]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
g : G × G
⊢ 0 = 0 x g
-- Mathlib/Data/Matroid/Basic.lean
theorem Dep.nonempty (hD : M.Dep D) : D.Nonempty

Proof state:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅

Proof state:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False

Tactic:
exact hD.not_indep M.empty_indep

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.getElem {x y : List α} (h : x <+: y) {n} (hn : n < x.length) :
    x[n] = y[n]'(Nat.le_trans hn h.length_le)

Proof state:
case intro
α : Type u_1
x : List α
n : Nat
hn : n < x.length
w✝ : List α
⊢ x[n] = (x ++ w✝)[n]

Tactic:
exact (List.getElem_append_left hn).symm

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <+: y
n : Nat
hn : n < x.length
⊢ x[n] = y[n]

Tactic:
obtain ⟨_, rfl⟩ := h

Result:
case intro
α : Type u_1
x : List α
n : Nat
hn : n < x.length
w✝ : List α
⊢ x[n] = (x ++ w✝)[n]
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_finsupp (ι : Type w) :
    Module.rank R (ι →₀ M) = Cardinal.lift.{v} #ι * Cardinal.lift.{w} (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Tactic:
obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
case intro.mk
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Proof state:
case intro.mk
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Free R M
ι : Type w
fst✝ : Type v
bs : Basis fst✝ R M
⊢ Module.rank R (ι →₀ M) = lift.{v, w} #ι * lift.{w, v} (Module.rank R M)

Tactic:
rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
  Cardinal.sum_const]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem equivOfRoot_map (pb : PowerBasis A S) (e : S ≃ₐ[A] S') (h₁ h₂) :
    pb.equivOfRoot (pb.map e) h₁ h₂ = e

Proof state:
case h
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
x : S
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) x = e x

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Result:
case h.intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) ((aeval pb.gen) f) = e ((aeval pb.gen) f)

Proof state:
case h.intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
f : A[X]
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) ((aeval pb.gen) f) = e ((aeval pb.gen) f)

Tactic:
simp [aeval_algEquiv]

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e

Tactic:
ext x

Result:
case h
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
S' : Type u_7
inst✝² : CommRing S'
inst✝¹ : Algebra A S
inst✝ : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : (aeval pb.gen) (minpoly A (pb.map e).gen) = 0
h₂ : (aeval (pb.map e).gen) (minpoly A pb.gen) = 0
x : S
⊢ (pb.equivOfRoot (pb.map e) h₁ h₂) x = e x
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem comp_eq : (f ≫ ofHom g) = f ≫ ofHom h

Proof state:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
this : (ConcreteCategory.hom f) a ∈ {b | h b = g b}
⊢ (g ((Hom.hom f) a)) x✝ = (h ((Hom.hom f) a)) x✝

Tactic:
rw [this]

Result:
no goals

Proof state:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (g ((Hom.hom f) a)) x✝ = (h ((Hom.hom f) a)) x✝

Tactic:
have : f a ∈ { b | h b = g b } := by
  rw [← agree]
  use a

Result:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
this : (ConcreteCategory.hom f) a ∈ {b | h b = g b}
⊢ (g ((Hom.hom f) a)) x✝ = (h ((Hom.hom f) a)) x✝

Proof state:
A B : Grp
f : A ⟶ B
⊢ f ≫ ofHom g = f ≫ ofHom h

Tactic:
ext a

Result:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ ((Hom.hom (f ≫ ofHom g)) a) x✝ = ((Hom.hom (f ≫ ofHom h)) a) x✝

Proof state:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ ((Hom.hom (f ≫ ofHom g)) a) x✝ = ((Hom.hom (f ≫ ofHom h)) a) x✝

Tactic:
simp only [hom_comp, hom_ofHom, MonoidHom.coe_comp, Function.comp_apply]

Result:
case hf.h.H
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (g ((Hom.hom f) a)) x✝ = (h ((Hom.hom f) a)) x✝

Proof state:
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (ConcreteCategory.hom f) a ∈ {b | h b = g b}

Tactic:
rw [← agree]

Result:
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (ConcreteCategory.hom f) a ∈ ↑(Hom.hom f).range

Proof state:
A B : Grp
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (ConcreteCategory.hom f) a ∈ ↑(Hom.hom f).range

Tactic:
use a

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
/-- The residue of the Hurwitz zeta function at `s = 1` is `1`. -/
lemma hurwitzZeta_residue_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))

Tactic:
refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)

Result:
case refine_1
a : UnitAddCircle
⊢ Tendsto (fun s => s - 1) (𝓝 1) (𝓝 (1 - 1))

case refine_2
a : UnitAddCircle
⊢ Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))

Proof state:
case refine_1
a : UnitAddCircle
⊢ Tendsto (fun s => s - 1) (𝓝 1) (𝓝 (1 - 1))

case refine_2
a : UnitAddCircle
⊢ Tendsto (hurwitzZetaOdd a) (𝓝 1) (𝓝 (hurwitzZetaOdd a 1))

Tactic:
exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ 𝓝 1 = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1)

Tactic:
simp

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]

Result:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))
-- Mathlib/RingTheory/PowerBasis.lean
theorem exists_eq_aeval [Nontrivial S] (pb : PowerBasis R S) (y : S) :
    ∃ f : R[X], f.natDegree < pb.dim ∧ y = aeval pb.gen f :=
  (mem_span_pow pb.dim_ne_zero).mp (by simpa using pb.basis.mem_span y)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
pb : PowerBasis R S
y : S
⊢ y ∈ Submodule.span R (Set.range fun i => pb.gen ^ ↑i)

Tactic:
simpa using pb.basis.mem_span y

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem isGLB_sInf (S : Set (Subfield K)) : IsGLB S (sInf S)

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)

Tactic:
convert isGLB_biInf (s := S) (f := SetLike.coe)

Result:
case h.e'_4
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ ↑(sInf S) = ⨅ x ∈ S, ↑x

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
⊢ IsGLB S (sInf S)

Tactic:
have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]

Result:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ IsGLB S (sInf S)

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
⊢ ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t

Tactic:
simp [SetLike.coe_subset_coe]

Result:
no goals

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ IsGLB S (sInf S)

Tactic:
refine IsGLB.of_image this ?_

Result:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)

Proof state:
case h.e'_4
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ≤ ↑t ↔ s ≤ t
⊢ ↑(sInf S) = ⨅ x ∈ S, ↑x

Tactic:
exact coe_sInf _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem singleton_eq_flatten_iff {xs : List (List α)} {y : α} :
    [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = [])

Proof state:
α : Type u_1
xs : List (List α)
y : α
⊢ [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ∀ (l : List α), l ∈ bs → l = []

Tactic:
rw [eq_comm, flatten_eq_singleton_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem ker_inl : ker (inl R M M₂) = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ker (inl R M M₂) = ⊥

Tactic:
rw [ker, ← prod_bot, prod_comap_inl]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_rpow_of_exponent_nonneg [IsTopologicalRing A] [T2Space A] (a : A) (x y : ℝ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) (ha₂ : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Tactic:
simp [NNReal.rpow_mul]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) a = cfc (fun x_1 => x_1 ^ (x * y)) a

Tactic:
refine cfc_congr fun _ _ => ?_

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 a
⊢ ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) x✝¹ = x✝¹ ^ (x * y)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ y) (cfc (fun x_1 => x_1 ^ x) a) = cfc (fun x_1 => x_1 ^ (x * y)) a

Tactic:
rw [← cfc_comp _ _ a]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc ((fun x => x ^ y) ∘ fun x_1 => x_1 ^ x) a = cfc (fun x_1 => x_1 ^ (x * y)) a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
simp only [rpow_def]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha₂ : autoParam (0 ≤ a) _auto✝
⊢ cfc (fun x => x ^ y) (cfc (fun x_1 => x_1 ^ x) a) = cfc (fun x_1 => x_1 ^ (x * y)) a
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1))

Proof state:
case zero

⊢ (fib 0).Coprime (fib (0 + 1))

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
induction' n with n ih

Result:
case zero

⊢ (fib 0).Coprime (fib (0 + 1))

case succ
n : ℕ
ih : (fib n).Coprime (fib (n + 1))
⊢ (fib (n + 1)).Coprime (fib (n + 1 + 1))

Proof state:
case succ
n : ℕ
ih : (fib n).Coprime (fib (n + 1))
⊢ (fib (n + 1)).Coprime (fib (n + 1 + 1))

Tactic:
simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

Result:
no goals