harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
@[to_additive]
lemma comp_apply {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : A) :
    (f ≫ g) a = g (f a)

Proof state:
A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (f ≫ g)) a = (Hom.hom g) ((Hom.hom f) a)

Tactic:
simp only [hom_comp, ContinuousMonoidHom.comp_toFun]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_mul_right {m n k : ℤ} : (m * n).lcm (k * n) = m.lcm k * natAbs n

Proof state:
m n k : ℤ
⊢ (m * n).lcm (k * n) = m.lcm k * n.natAbs

Tactic:
simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_right]

Result:
no goals
-- Mathlib/Data/Finset/Empty.lean
theorem exists_mem_empty_iff (p : α → Prop) : (∃ x, x ∈ (∅ : Finset α) ∧ p x) ↔ False

Proof state:
α : Type u_1
p : α → Prop
⊢ (∃ x ∈ ∅, p x) ↔ False

Tactic:
simp only [not_mem_empty, false_and, exists_false]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle_fst_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫
      pullback.snd _ _ = pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp only [t'_fst_fst_snd]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_eq_derivedSeriesOfIdeal_map (k : ℕ) :
    (derivedSeries R I k).map I.incl = derivedSeriesOfIdeal R L k I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ map I.incl (derivedSeries R (↥I) k) = derivedSeriesOfIdeal R L k I

Tactic:
rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I

Tactic:
apply derivedSeriesOfIdeal_le_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem two_pow_mod_two_eq_one {n : Nat} : 2 ^ n % 2 = 1 ↔ n = 0

Proof state:
n : Nat
⊢ 2 ^ n % 2 = 1 ↔ n = 0

Tactic:
cases n <;> simp [Nat.pow_succ]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_eq_nat_iff {α : Type u} {n : ℕ} : #α = n ↔ Nonempty (α ≃ Fin n)

Proof state:
α : Type u
n : ℕ
⊢ #α = ↑n ↔ Nonempty (α ≃ Fin n)

Tactic:
rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_comapDomain (f : α → α') (l : α' →₀ R)
    (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : linearCombination R v (Finsupp.comapDomain f l hf) =
      (l.support.preimage f hf).sum fun i => l (f i) • v i

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ (linearCombination R v) (comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
rw [linearCombination_apply]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a => a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α → α'
l : α' →₀ R
hf : InjOn f (f ⁻¹' ↑l.support)
⊢ ((comapDomain f l hf).sum fun i a => a • v i) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).sup' h f = t.sup' h.snd fun i' => s.sup' h.fst fun i => f ⟨i, i'⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
⊢ (s ×ˢ t).sup' h f = t.sup' ⋯ fun i' => s.sup' ⋯ fun i => f (i, i')

Tactic:
rw [sup'_product_left, Finset.sup'_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem succ_zero : succ (0 : Cardinal) = 1

Proof state:
⊢ succ 0 = 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sub : cos (x - y) = cos x * cos y + sin x * sin y

Proof state:
x y : ℂ
⊢ cos (x - y) = cos x * cos y + sin x * sin y

Tactic:
simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[simp] lemma append_right_inj : x ++ₛ a = x ++ₛ b ↔ a = b :=
  ⟨append_right_injective x a b, by simp (config := {contextual := true})⟩

Proof state:
α : Type u
x : List α
a b : Stream' α
⊢ a = b → x ++ₛ a = x ++ₛ b

Tactic:
simp (config := {contextual := true})

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Antivary.sum_smul_comp_perm_eq_sum_smul_iff (hfg : Antivary f g) :
    ∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Antivary f (g ∘ σ)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i : ι, f i • g (σ i) = ∑ i : ι, f i • g i ↔ Antivary f (g ∘ ⇑σ)

Tactic:
simp [(hfg.antivaryOn _).sum_smul_comp_perm_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_nonempty : hs.toFinset.Nonempty ↔ s.Nonempty

Proof state:
α : Type u
s : Set α
hs : s.Finite
⊢ hs.toFinset.Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem trans_ofSet {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e ⁻¹' s) :=
  PartialHomeomorph.ext _ _ (fun _ => rfl) (fun _ => rfl) <| by
    rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set Y
hs : IsOpen s
⊢ (e.trans (ofSet s hs)).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
rw [trans_source, restr_source, ofSet_source, ← preimage_interior, hs.interior_eq]

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
/-- An element `a` is right-regular if and only if a positive power of `a` is right-regular. -/
lemma IsRightRegular.pow_iff (n0 : 0 < n) : IsRightRegular (a ^ n) ↔ IsRightRegular a where
  mp

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']

Result:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Tactic:
exact .of_mul

Result:
no goals
-- Mathlib/Combinatorics/Additive/CauchyDavenport.lean
/-- The **Cauchy-Davenport Theorem** for torsion-free groups. The size of `s * t` is lower-bounded
by `|s| + |t| - 1`. -/
@[to_additive
"The **Cauchy-Davenport theorem** for torsion-free groups. The size of `s + t` is lower-bounded
by `|s| + |t| - 1`."]
lemma cauchy_davenport_mul_of_isTorsionFree (h : IsTorsionFree α)
    (hs : s.Nonempty) (ht : t.Nonempty) : #s + #t - 1 ≤ #(s * t)

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
h : IsTorsionFree α
hs : s.Nonempty
ht : t.Nonempty
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
simpa only [h.minOrder, min_eq_right, le_top, Nat.cast_le]
  using cauchy_davenport_minOrder_mul hs ht

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem closure_singleton_le_iff_mem (m : M) (p : Subsemigroup M) : closure {m} ≤ p ↔ m ∈ p

Proof state:
M : Type u_1
inst✝ : Mul M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p

Tactic:
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma lift_f_fst_v (p q : ℤ) (hpq : p + 1 = q) :
    (lift φ α β eq).f p ≫ (fst φ).1.v p q hpq = α.1.v p q hpq

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ (lift φ α β eq).f p ≫ (↑(fst φ)).v p q hpq = (↑α).v p q hpq

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_C_mul (n : M) (r : R) :
    weightedHomogeneousComponent w n (C r * φ) = C r * weightedHomogeneousComponent w n φ

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
n : M
r : R
⊢ (weightedHomogeneousComponent w n) (C r * φ) = C r * (weightedHomogeneousComponent w n) φ

Tactic:
simp only [C_mul', LinearMap.map_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.of_comp (f : M →ₗ[R] M') (hfv : LinearIndependent R (f ∘ v)) :
    LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndependent R (⇑f ∘ v)
⊢ LinearIndependent R v

Tactic:
rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv

Result:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v))
⊢ LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hfv : Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v))
⊢ LinearIndependent R v

Tactic:
exact hfv.of_comp

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma IccRightChart_extend_top_mem_frontier :
    (IccRightChart x y).extend (𝓡∂ 1) ⊤ ∈ frontier (range (𝓡∂ 1))

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
rw [IccRightChart_extend_top, frontier_range_modelWithCornersEuclideanHalfSpace,
  mem_setOf, PiLp.zero_apply]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
protected lemma add_comm : a + b = b + a

Proof state:
a b : ℚ
⊢ a + b = b + a

Tactic:
simp [add_def, Int.add_comm, Int.mul_comm, Nat.mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem zipIdx_toArray {l : List α} {k : Nat} :
    l.toArray.zipIdx k = (l.zipIdx k).toArray

Proof state:
α : Type u_1
l : List α
k : Nat
⊢ l.toArray.zipIdx k = (l.zipIdx k).toArray

Tactic:
ext i hi₁ hi₂ <;> simp [Nat.add_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem basisOf_apply (i : ι) (j : { j : ι // j ≠ i }) : b.basisOf i j = b ↑j -ᵥ b i

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i : ι
j : { j // j ≠ i }
⊢ (b.basisOf i) j = b ↑j -ᵥ b i

Tactic:
simp [basisOf]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
lemma «forall» {p : Sym α n → Prop} :
    (∀ s : Sym α n, p s) ↔ ∀ (s : Multiset α) (hs : Multiset.card s = n), p (Sym.mk s hs)

Proof state:
α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

Result:
no goals
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem closure_of_isSwap_of_isPretransitive [Finite α] {S : Set (Perm α)} (hS : ∀ σ ∈ S, σ.IsSwap)
    [MulAction.IsPretransitive (Subgroup.closure S) α] : Subgroup.closure S = ⊤

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Finite α
S : Set (Equiv.Perm α)
hS : ∀ σ ∈ S, σ.IsSwap
inst✝ : IsPretransitive (↥(closure S)) α
⊢ closure S = ⊤

Tactic:
simp [eq_top_iff', mem_closure_isSwap hS, orbit_eq_univ, Set.toFinite]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem leadingCoeff_quadratic (ha : a ≠ 0) : leadingCoeff (C a * X ^ 2 + C b * X + C c) = a

Proof state:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).leadingCoeff = a

Tactic:
rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
  leadingCoeff_C_mul_X_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
    l.toArray.foldl f init = l.foldl f init

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
l : List α
⊢ Array.foldl f init l.toArray = foldl f init l

Tactic:
rw [foldl_toList]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem ext : ∀ {v w : Vector α n} (_ : ∀ m : Fin n, Vector.get v m = Vector.get w m), v = w
  | ⟨v, hv⟩, ⟨w, hw⟩, h =>
    Subtype.eq (List.ext_get (by rw [hv, hw]) fun m hm _ => h ⟨m, hv ▸ hm⟩)

Proof state:
α : Type u_1
n : ℕ
v : List α
hv : v.length = n
w : List α
hw : w.length = n
h : ∀ (m : Fin n), get ⟨v, hv⟩ m = get ⟨w, hw⟩ m
⊢ (↑⟨v, hv⟩).length = (↑⟨w, hw⟩).length

Tactic:
rw [hv, hw]

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma RootedTree.mem_subtreeOf [DecidableEq t] {v : t} :
    v ∈ t.subtreeOf v

Proof state:
t : RootedTree
inst✝ : DecidableEq ↑t
v : ↑t
⊢ v ∈ t.subtreeOf v

Tactic:
simp [SubRootedTree.mem_iff, RootedTree.subtreeOf]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem nonempty_frontier_iff [PreconnectedSpace α] {s : Set α} :
    (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
⊢ (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ

Tactic:
simp only [nonempty_iff_ne_empty, Ne, frontier_eq_empty_iff, not_or]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
@[simp]
lemma factorsThruAlong_id {X : C} (S T : Presieve X) :
    S.FactorsThruAlong T (𝟙 X) ↔ S.FactorsThru T

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S T : Presieve X
⊢ S.FactorsThruAlong T (𝟙 X) ↔ S.FactorsThru T

Tactic:
simp [FactorsThruAlong, FactorsThru]

Result:
no goals
-- Mathlib/CategoryTheory/Core.lean
theorem id_hom (X : C) : Iso.hom (coreCategory.id X) = @CategoryStruct.id C _ X

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (𝟙 X).hom = 𝟙 X

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem not_mem_edges_of_loop {v : V} {e : Sym2 V} {p : G.Path v v} :
    ¬e ∈ (p : G.Walk v v).edges

Proof state:
V : Type u
G : SimpleGraph V
v : V
e : Sym2 V
p : G.Path v v
⊢ e ∉ (↑p).edges

Tactic:
simp [p.loop_eq]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
lemma summable_descFactorial_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    Summable (fun n ↦ (n + k).descFactorial k * r ^ n)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ↑((n + k).descFactorial k) * r ^ n

Tactic:
convert (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R)
  using 2 with n

Result:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
n : ℕ
⊢ ↑((n + k).descFactorial k) * r ^ n = ↑k ! * (↑((n + k).choose k) * r ^ n)

Proof state:
case h.e'_5.h
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
n : ℕ
⊢ ↑((n + k).descFactorial k) * r ^ n = ↑k ! * (↑((n + k).choose k) * r ^ n)

Tactic:
simp [← mul_assoc, descFactorial_eq_factorial_mul_choose (n + k) k]

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem CG.map {N : Type*} [L.Structure N] (f : M →[L] N) {s : L.Substructure M} (hs : s.CG) :
    (s.map f).CG :=
  let ⟨t, ht⟩ := cg_def.1 hs
  cg_def.2 ⟨f '' t, ht.1.image _, by rw [closure_image, ht.2]⟩

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M →[L] N
s : L.Substructure M
hs : s.CG
t : Set M
ht : t.Countable ∧ (closure L).toFun t = s
⊢ (closure L).toFun (⇑f '' t) = Substructure.map f s

Tactic:
rw [closure_image, ht.2]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem sInf_toNonUnitalSubalgebra (S : Set (NonUnitalStarSubalgebra R A)) :
    (sInf S).toNonUnitalSubalgebra = sInf (NonUnitalStarSubalgebra.toNonUnitalSubalgebra '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : Set (NonUnitalStarSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubalgebra = ↑(sInf (toNonUnitalSubalgebra '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem univ_pi_singleton (f : ∀ i, α i) : (pi univ fun i => {f i}) = ({f} : Set (∀ i, α i)) :=
  ext fun g => by simp [funext_iff]

Proof state:
ι : Type u_1
α : ι → Type u_2
f g : (i : ι) → α i
⊢ (g ∈ univ.pi fun i => {f i}) ↔ g ∈ {f}

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_mapIdx {l : Vector α n} {f : Nat → α → β} {g : Nat → β → γ} :
    (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
γ : Type u_3
l : Vector α n
f : Nat → α → β
g : Nat → β → γ
⊢ mapIdx g (mapIdx f l) = mapIdx (fun i => g i ∘ f i) l

Tactic:
simp [mapIdx_eq_iff]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem formalMultilinearSeries_geometric_eq_ofScalars :
    formalMultilinearSeries_geometric 𝕜 A =
      FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜)

Proof state:
𝕜 : Type u_9
A : Type u_10
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun x => 1

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars,
  formalMultilinearSeries_geometric, one_smul, implies_true]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_lt_pow_iff_norm_le_pow_sub_one (x : ℚ_[p]) (n : ℤ) :
    ‖x‖ < (p : ℝ) ^ n ↔ ‖x‖ ≤ (p : ℝ) ^ (n - 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Basic.lean
theorem isOpenEmbedding_iff_comp_isIso' {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] :
    IsOpenEmbedding (g ∘ f) ↔ IsOpenEmbedding f

Proof state:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom f)

Tactic:
exact isOpenEmbedding_iff_comp_isIso f g

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_monomial {r : R} {k : ℕ} : content (monomial k r) = normalize r

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ ((monomial k) r).content = normalize r

Tactic:
rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_zero : ⌊(0 : α)⌋₊ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
⊢ ⌊0⌋₊ = 0

Tactic:
rw [← Nat.cast_zero, floor_natCast]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_one (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma coeffsIn_le {N : Submodule R (MvPolynomial σ S)} :
    coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ i, monomial i m ∈ N

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
N : Submodule R (MvPolynomial σ S)
⊢ coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ N

Tactic:
simp [coeffsIn_eq_span_monomial, Submodule.span_le, Set.subset_def,
  forall_swap (α := MvPolynomial σ S)]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldrm.ofFreeMonoid_comp_of {m} [Monad m] [LawfulMonad m] (f : β → α → m α) :
    foldrM.ofFreeMonoid f ∘ FreeMonoid.of = foldrM.mk ∘ f

Proof state:
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f

Tactic:
ext

Result:
case h
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma support_tail (p : G.Walk v v) (hp : ¬ p.Nil) :
    p.tail.support = p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
v : V
p : G.Walk v v
hp : ¬p.Nil
⊢ p.tail.support = p.support.tail

Tactic:
rw [← cons_support_tail p hp, List.tail_cons]

Result:
no goals
-- Mathlib/NumberTheory/FunctionField.lean
theorem not_isField : ¬IsField (ringOfIntegers Fq F)

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ ¬IsField ↥(ringOfIntegers Fq F)

Tactic:
simpa [← (IsIntegralClosure.isIntegral_algebra Fq[X] F).isField_iff_isField
    (algebraMap_injective Fq F)] using
  Polynomial.not_isField Fq

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_one_eq_one_mod (n : ℕ) : (1 : ZMod n).val = 1 % n

Proof state:
n : ℕ
⊢ val 1 = 1 % n

Tactic:
rw [← Nat.cast_one, val_natCast]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpToOn.continuousOn (h : HasFTaylorSeriesUpToOn n f p s) :
    ContinuousOn f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
this : ContinuousOn (fun x => (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)) s
⊢ ContinuousOn f s

Tactic:
rwa [← (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_continuousOn_iff]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
⊢ ContinuousOn f s

Tactic:
have := (h.cont 0 bot_le).congr fun x hx => (h.zero_eq' hx).symm

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
this : ContinuousOn (fun x => (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)) s
⊢ ContinuousOn f s