harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem zmodEquivTrunc_compat (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂) :
    (TruncatedWittVector.truncate hk).comp
        ((zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) =
      (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k₁ k₂ : ℕ
hk : k₁ ≤ k₂
⊢ (TruncatedWittVector.truncate hk).comp ((zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) =
    (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

Tactic:
rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc,
  PadicInt.zmod_cast_comp_toZModPow _ _ hk]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_injective : Function.Injective (f ''ᵁ ·)

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
⊢ Function.Injective fun x => f ''ᵁ x

Tactic:
intro U V hUV

Result:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U V : X.Opens
hUV : (fun x => f ''ᵁ x) U = (fun x => f ''ᵁ x) V
⊢ U = V
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivRight_C (r : R) : optionEquivRight R S₁ (C r) = C (Polynomial.C r)

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivRight R S₁) (C r) = C (Polynomial.C r)

Tactic:
simp only [optionEquivRight_apply, aeval_C, algebraMap_apply, Polynomial.algebraMap_eq]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_empty (α : Type*) : (∅ : Set α).ncard = 0

Proof state:
α : Type u_3
⊢ ∅.ncard = 0

Tactic:
rw [ncard_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The upper part of the second column of the snake diagram is exact. -/
lemma exact_C₂_up : (ShortComplex.mk S.v₀₁.τ₂ S.v₁₂.τ₂
    (by rw [← comp_τ₂, S.w₀₂, zero_τ₂])).Exact :=
  exact_of_f_is_kernel _ S.h₀τ₂

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.30975, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₀₂, zero_τ₂]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem dvd_of_mod_eq_zero {a b : Ordinal} (H : a % b = 0) : b ∣ a :=
  ⟨a / b, by simpa [H] using (div_add_mod a b).symm⟩

Proof state:
a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)

Tactic:
simpa [H] using (div_add_mod a b).symm

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_isOrtho [Invertible (2 : R)] {x y : M} :
    Q.associated.IsOrtho x y ↔ Q.IsOrtho x y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
Q : QuadraticMap R M N
inst✝ : Invertible 2
x y : M
⊢ LinearMap.IsOrtho (associated Q) x y ↔ Q.IsOrtho x y

Tactic:
simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
  smul_zero, sub_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_neg_neg (x y : V) : angle (-x) (-y) = angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) (-y) = angle x y

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner (-x) (-y) / (‖-x‖ * ‖-y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner (-x) (-y) / (‖-x‖ * ‖-y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))

Tactic:
rw [inner_neg_neg, norm_neg, norm_neg]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem countable_of_isolated_left' [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y < x ∧ Ioo y x = ∅ }

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | ∃ y < x, Ioo y x = ∅}.Countable

Tactic:
simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_left

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem repr_self [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι) :
    b.repr (b i) = lp.single 2 i (1 : 𝕜)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ b.repr (b i) = lp.single 2 i 1

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply, ← b.repr_symm_single]

Result:
no goals
-- Mathlib/Topology/Order/LawsonTopology.lean
/-- An upper set is Lawson open if and only if it is Scott open -/
lemma lawsonOpen_iff_scottOpen_of_isUpperSet' (s : Set α) (h : IsUpperSet s) :
    IsOpen[L] s ↔ IsOpen[S] s

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen s ↔ IsOpen s

Tactic:
exact lawsonOpen_iff_scottOpen_of_isUpperSet h

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map₂_flip (f : α → β → γ) :
    map₂ f xs ys = map₂ (flip f) ys xs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = map₂ (flip f) ys xs

Tactic:
induction xs, ys using Vector.inductionOn₂ <;> simp_all[flip]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem mul_add : a * (b + c) = a * b + a * c

Proof state:
a b c : ℚ
⊢ a * (b + c) = a * b + a * c

Tactic:
rw [Rat.mul_comm, Rat.add_mul, Rat.mul_comm, Rat.mul_comm c a]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_one_of_associated_mul_one [CommMonoid M] {a b : M} : a * b ~ᵤ 1 → a ~ᵤ 1
  | ⟨u, h⟩ => associated_one_of_mul_eq_one (b * u) <| by simpa [mul_assoc] using h

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
u : Mˣ
h : a * b * ↑u = 1
⊢ a * (b * ↑u) = 1

Tactic:
simpa [mul_assoc] using h

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem coe_sort_false : (false : Prop) = False

Proof state:
⊢ (false = true) = False

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem prime_pow_dvd_iff_le {m p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} :
    p ^ k ≤ m ↔ k ≤ count p m.factors

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors

Tactic:
rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount h₁]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vadd_vsub_vadd_cancel_left (v : G) (p₁ p₂ : P) : (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
p₁ p₂ : P
⊢ (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂

Tactic:
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/Finset/Functor.lean
theorem id_traverse [DecidableEq α] (s : Finset α) : traverse (pure : α → Id α) s = s

Proof state:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s

Tactic:
exact s.val_toFinset

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = s

Tactic:
rw [traverse, Multiset.id_traverse]

Result:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s
-- Mathlib/Data/Nat/Count.lean
theorem count_lt_count_succ_iff {n : ℕ} : count p n < count p (n + 1) ↔ p n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n

Tactic:
by_cases h : p n <;> simp [count_succ, h]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_algebraMap {S : Type*} [CommSemiring S] [Algebra S K[X]] (p : S) :
    eval f a (algebraMap _ _ p) = (algebraMap _ K[X] p).eval₂ f a

Proof state:
K : Type u
inst✝³ : Field K
L : Type u
inst✝² : Field L
f : K →+* L
a : L
S : Type u_1
inst✝¹ : CommSemiring S
inst✝ : Algebra S K[X]
p : S
⊢ eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S K[X]) p)

Tactic:
simp [eval, IsScalarTower.algebraMap_apply S K[X] (RatFunc K)]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A row partitioned matrix when transposed gives a column partitioned matrix with rows of the
initial matrix transposed to become columns. -/
lemma transpose_fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
    transpose (fromRows A₁ A₂) = fromCols (transpose A₁) (transpose A₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᵀ = A₁ᵀ.fromCols A₂ᵀ

Tactic:
ext i (j | j) <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_id_id {X Y : C} [HasBinaryCoproduct X Y] : coprod.map (𝟙 X) (𝟙 Y) = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨿ Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem uniq_cocone_morphism {s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f' :=
  have : ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s

Proof state:
case w
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g.hom = (h.descCoconeMorphism s).hom

Tactic:
exact h.uniq _ _ g.w

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g = h.descCoconeMorphism s

Tactic:
ext

Result:
case w
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g.hom = (h.descCoconeMorphism s).hom

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' : t ⟶ s
⊢ ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s

Tactic:
intro g

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g = h.descCoconeMorphism s
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_neg (n : ℤ) : preNormEDS b c d (-n) = -preNormEDS b c d n

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ preNormEDS b c d (-n) = -preNormEDS b c d n

Tactic:
rw [preNormEDS, Int.sign_neg, Int.cast_neg, neg_mul, Int.natAbs_neg, preNormEDS]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_eq_empty_iff [DenselyOrdered α] : Ioo a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b

Tactic:
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIco : Fintype.card (Set.Ico a b) = b - a

Proof state:
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a

Tactic:
rw [← card_Ico, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/OneHypercover.lean
lemma OneHypercover.mem_sieve₁' {S : C} (E : J.OneHypercover S)
    (i₁ i₂ : E.I₀) [HasPullback (E.f i₁) (E.f i₂)] :
    E.sieve₁' i₁ i₂ ∈ J _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
rw [E.sieve₁'_eq_sieve₁]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
exact mem₁ _ _ _ _ _ pullback.condition

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_find : Equiv (self.find x).1 a b ↔ Equiv self a b

Proof state:
a b : Nat
self : UnionFind
x : Fin self.size
⊢ (self.find x).fst.Equiv a b ↔ self.Equiv a b

Tactic:
simp [Equiv, find_root_1]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.nsmul [AddMonoid α] (h : Periodic f c) (n : ℕ) : Periodic f (n • c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)

Tactic:
induction n <;> simp_all [add_nsmul, ← add_assoc, zero_nsmul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_zero : p.comp (0 : R[X]) = C (p.eval 0)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp 0 = C (eval 0 p)

Tactic:
rw [← C_0, comp_C]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_star (f : R → R) (a : A)
    (hf : ContinuousOn f (star '' (spectrum R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (star '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (star x)) a = cfc f (star a)

Tactic:
rw [cfc_comp' .., cfc_star_id ..]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a

Proof state:
α✝ : Type u_1
l : List α✝
p : α✝ → Bool
⊢ countP p l = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true

Tactic:
rw [countP_eq_length_filter, filter_length_eq_length]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_smul_measure (c : ℝ≥0∞) :
    ∫ x in a..b, f x ∂c • μ = c.toReal • ∫ x in a..b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
c : ℝ≥0∞
⊢ ∫ (x : ℝ) in a..b, f x ∂c • μ = c.toReal • ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
simp only [intervalIntegral, Measure.restrict_smul, integral_smul_measure, smul_sub]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.toENat_eq_natCast_iff {c : Cardinal} {n : ℕ} :
    Cardinal.toENat c = n ↔ c = n

Proof state:
c : Cardinal.{u_3}
n : ℕ
⊢ toENat c = ↑n ↔ c = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_zsmul (n : ℤ) (y : HomogeneousLocalization 𝒜 x) : (n • y).val = n • y.val

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
n : ℤ
y : HomogeneousLocalization 𝒜 x
⊢ (n • y).val = n • y.val

Tactic:
rw [val_smul, OreLocalization.zsmul_eq_zsmul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.IsClosed.cthickening_eq_biUnion_closedBall {α : Type*} [PseudoMetricSpace α]
    [ProperSpace α] {E : Set α} (hE : IsClosed E) (hδ : 0 ≤ δ) :
    cthickening δ E = ⋃ x ∈ E, closedBall x δ

Proof state:
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_reverse (l : List α) : l.reverse.getLast? = l.head?

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.getLast? = l.head?

Tactic:
cases l <;> simp [getLast?_concat]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFinset_map (f : α ↪ β) (hn : n ≠ 1) :
    (G.map f).cliqueFinset n = (G.cliqueFinset n).map ⟨map f, Finset.map_injective _⟩ :=
  coe_injective <| by
    simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
n : ℕ
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α ↪ β
hn : n ≠ 1
⊢ ↑((SimpleGraph.map f G).cliqueFinset n) = ↑(map { toFun := map f, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformly_iff_forall_tendsto :
    TendstoLocallyUniformly F f p ↔
      ∀ x, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem iterate_pos_lt_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) :
    f^[n] x < x + n * m ↔ f x < x + m

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ioc_left [NoMinOrder α] (b : α) : ⋃ a, Ioc a b = Iic b

Proof state:
α : Type v
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ a, Ioc a b = Iic b

Tactic:
simp only [← Ioi_inter_Iic, ← iUnion_inter, iUnion_Ioi, univ_inter]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem norm_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) :
    ‖z ^ w‖ = ‖z‖ ^ w.re / Real.exp (arg z * im w)

Proof state:
z : ℂ
hz : z ≠ 0
w : ℂ
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rw [cpow_def_of_ne_zero hz, norm_exp, mul_re, log_re, log_im, Real.exp_sub,
  Real.rpow_def_of_pos (norm_pos_iff.mpr hz)]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
/-- Special case of `inner_smul_left_eq_star_smul` when the acting ring has a trivial star
(eg `ℕ`, `ℤ`, `ℚ≥0`, `ℚ`, `ℝ`). -/
lemma inner_smul_left_eq_smul [TrivialStar 𝕝] (x y : E) (r : 𝕝) : ⟪r • x, y⟫ = r • ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁹ : RCLike 𝕜
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
𝕝 : Type u_4
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : Module 𝕝 E
inst✝² : IsScalarTower 𝕝 𝕜 E
inst✝¹ : StarModule 𝕝 𝕜
inst✝ : TrivialStar 𝕝
x y : E
r : 𝕝
⊢ ⟪r • x, y⟫_𝕜 = r • ⟪x, y⟫_𝕜

Tactic:
rw [inner_smul_left_eq_star_smul, starRingEnd_apply, star_trivial]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem CauchySeq.subseq_subseq_mem {V : ℕ → Set (α × α)} (hV : ∀ n, V n ∈ 𝓤 α) {u : ℕ → α}
    (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Proof state:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : CauchySeq u
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
rw [cauchySeq_iff_tendsto] at hu

Result:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Proof state:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → Set (α × α)
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
exact ((hu.comp <| hf.prod_atTop hg).comp tendsto_atTop_diagonal).subseq_mem hV

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftMonoidWithZeroHom_apply {L : Type*} [CommGroupWithZero L] (φ : K[X] →*₀ L)
    (hφ : K[X]⁰ ≤ L⁰.comap φ) (f : RatFunc K) :
    liftMonoidWithZeroHom φ hφ f = φ f.num / φ f.denom

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
f : RatFunc K
⊢ (liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom

Tactic:
rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_eq_iSup_genEigenspace_nat (f : End R M) (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k = ⨆ l : {l : ℕ // l ≤ k}, f.genEigenspace μ l

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k = ⨆ l, (f.genEigenspace μ) ↑↑l

Tactic:
simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem id_comp (f : α →o β) : comp id f = f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ id.comp f = f

Tactic:
ext

Result:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (id.comp f) x✝ = f x✝

Proof state:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (id.comp f) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
    decide (∃ x, x ∈ xs ∧ p x) = xs.any p

Proof state:
α : Type u_1
xs : Array α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, x ∈ xs ∧ p x) = xs.any fun b => decide (p b)

Tactic:
simp [any_eq']

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem disjoint_map_cocompact {g : X → Y} {f : Filter X} (hg : Continuous g)
    (hf : Disjoint f (Filter.cocompact X)) : Disjoint (map g f) (Filter.cocompact Y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥

Tactic:
calc
  f ⊓ (comap g (cocompact Y))
  _ ≤ f ⊓ Filter.cocompact X := inf_le_inf_left f (Filter.comap_cocompact_le hg)
  _ = ⊥ := disjoint_iff.mp hf

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous g
hf : Disjoint f (cocompact X)
⊢ Disjoint (map g f) (cocompact Y)

Tactic:
rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.comp_contDiffWithinAt_iff (e : F ≃L[𝕜] G) :
    ContDiffWithinAt 𝕜 n (e ∘ f) s x ↔ ContDiffWithinAt 𝕜 n f s x :=
  ⟨fun H => by
    simpa only [Function.comp_def, e.symm.coe_coe, e.symm_apply_apply] using
      H.continuousLinearMap_comp (e.symm : G →L[𝕜] F),
    fun H => H.continuousLinearMap_comp (e : F →L[𝕜] G)⟩

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
e : F ≃L[𝕜] G
H : ContDiffWithinAt 𝕜 n (⇑e ∘ f) s x
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
simpa only [Function.comp_def, e.symm.coe_coe, e.symm_apply_apply] using
  H.continuousLinearMap_comp (e.symm : G →L[𝕜] F)

Result:
no goals