harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Basic.lean
protected lemma pow_right_injective (ha : 2 ≤ a) : Injective (a ^ ·)

Proof state:
a : ℕ
ha : 2 ≤ a
⊢ Injective fun x => a ^ x

Tactic:
simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.map_pre [HasLimitsOfShape K C] (E : K ⥤ J) :
    lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
⊢ lim.map α ≫ pre G E = pre F E ≫ lim.map (whiskerLeft E α)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (lim.map α ≫ pre G E) ≫ π (E ⋙ G) j✝ = (pre F E ≫ lim.map (whiskerLeft E α)) ≫ π (E ⋙ G) j✝

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (lim.map α ≫ pre G E) ≫ π (E ⋙ G) j✝ = (pre F E ≫ lim.map (whiskerLeft E α)) ≫ π (E ⋙ G) j✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem mem_fin {n} {s : Finset ℕ} : ∀ a : Fin n, a ∈ s.fin n ↔ (a : ℕ) ∈ s
  | ⟨a, ha⟩ => by simp [Finset.fin, ha, and_comm]

Proof state:
n : ℕ
s : Finset ℕ
a : ℕ
ha : a < n
⊢ ⟨a, ha⟩ ∈ Finset.fin n s ↔ ↑⟨a, ha⟩ ∈ s

Tactic:
simp [Finset.fin, ha, and_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_map : (p.map f).darts = p.darts.map f.mapDart

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).darts = List.map f.mapDart p.darts

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesAt.isBigO_sub_partialSum_pow
    (hf : HasFPowerSeriesAt f p x) (n : ℕ) :
    (fun y : E => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
n : ℕ
⊢ (fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesWithinAt f p univ x
n : ℕ
⊢ (fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesWithinAt f p univ x
n : ℕ
⊢ (fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n

Tactic:
simpa using hf.isBigO_sub_partialSum_pow n

Result:
no goals
-- Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
@[simp, reassoc]
lemma induced_shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
    letI := (induced e M F' e')
    (F.shiftIso n a a' ha').hom.app (L.obj X) =
      (F.shift a).map ((L.commShiftIso n).inv.app X) ≫ (e' a).hom.app (X⟦n⟧) ≫
        (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_7, u_1} C
inst✝⁸ : Category.{u_6, u_2} D
inst✝⁷ : Category.{u_5, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n a a' : M
ha' : n + a = a'
X : C
⊢ (F.shiftIso n a a' ha').hom.app (L.obj X) =
    (F.shift a).map ((L.commShiftIso n).inv.app X) ≫
      (e' a).hom.app ((shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X

Tactic:
apply induced.shiftIso_hom_app_obj

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepSet_iff_iCondIndep (s : ι → Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun i ↦ generateFrom {s i}) μ

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun i => generateFrom {s i}) μ

Tactic:
simp only [iCondIndepSet, iCondIndep, Kernel.iIndepSet]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_filter_le_iff (s : Finset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
    #(s.filter P) ≤ n ↔ ∀ s' ⊆ s, n < #s' → ∃ a ∈ s', ¬ P a :=
  (s.1.card_filter_le_iff P n).trans ⟨fun H s' hs' h ↦ H s'.1 (by aesop) h,
    fun H s' hs' h ↦ H ⟨s', nodup_of_le hs' s.2⟩ (fun _ hx ↦ Multiset.subset_of_le hs' hx) h⟩

Proof state:
α : Type u_1
s : Finset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : ∀ s' ≤ s.val, n < s'.card → ∃ a ∈ s', ¬P a
s' : Finset α
hs' : s' ⊆ s
h : n < #s'
⊢ s'.val ≤ s.val

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} :
    (insertManyIfNewUnit m l).isEmpty = (m.isEmpty && l.isEmpty)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
⊢ (insertManyIfNewUnit m l).isEmpty = (m.isEmpty && l.isEmpty)

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_insertManyIfNewUnit_list

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_cons (i : B) (ω : List B) : π (i :: ω) = s i * π ω

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
simp [wordProd]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem one_of_isUnit' {x : O} (hx : IsUnit x) (H : ∀ x, v (algebraMap O R x) ≤ 1) :
    v (algebraMap O R x) = 1 :=
  let ⟨u, hu⟩ := hx
  le_antisymm (H _) <| by
    rw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
      (algebraMap O R).map_mul, v.map_mul]
    exact mul_le_mul_left' (H (u⁻¹ : Units O)) _

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ v ((algebraMap O R) x) * v ((algebraMap O R) ↑u⁻¹) ≤ v ((algebraMap O R) x) * 1

Tactic:
exact mul_le_mul_left' (H (u⁻¹ : Units O)) _

Result:
no goals

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ 1 ≤ v ((algebraMap O R) x)

Tactic:
rw [← v.map_one, ← (algebraMap O R).map_one, ← u.mul_inv, ← mul_one (v (algebraMap O R x)), hu,
  (algebraMap O R).map_mul, v.map_mul]

Result:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
x : O
hx : IsUnit x
H : ∀ (x : O), v ((algebraMap O R) x) ≤ 1
u : Oˣ
hu : ↑u = x
⊢ v ((algebraMap O R) x) * v ((algebraMap O R) ↑u⁻¹) ≤ v ((algebraMap O R) x) * 1
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem le_sum (μ : ι → Measure α) (i : ι) : μ i ≤ sum μ :=
  le_iff.2 fun s hs ↦ by simpa only [sum_apply μ hs] using ENNReal.le_tsum i

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
μ : ι → Measure α
i : ι
s : Set α
hs : MeasurableSet s
⊢ (μ i) s ≤ (sum μ) s

Tactic:
simpa only [sum_apply μ hs] using ENNReal.le_tsum i

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_monomial (r : R) : expand R p (monomial q r) = monomial (q * p) r

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ (expand R p) ((monomial q) r) = (monomial (q * p)) r

Tactic:
simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem mono_of_epi_of_mono_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact)
    (h₀ : Epi (app' φ 0)) (h₁ : Mono (app' φ 1)) (h₃ : Mono (app' φ 3)) :
    Mono (app' φ 2) :=
  mono_of_epi_of_mono_of_mono' φ
    (by simpa only [R₁.map'_comp 0 1 2] using hR₁.toIsComplex.zero 0)
    (hR₁.exact 1).exact_toComposableArrows (hR₂.exact 0).exact_toComposableArrows h₀ h₁ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 ⋯)
h₁ : Mono (app' φ 1 ⋯)
h₃ : Mono (app' φ 3 ⋯)
⊢ R₁.map' 0 2 ⋯ ⋯ = 0

Tactic:
simpa only [R₁.map'_comp 0 1 2] using hR₁.toIsComplex.zero 0

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_le_natCast {m : ℚ≥0} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ≥0)

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
m : ℚ≥0
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
rw [← cast_le (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem exists_nat_pos_mul_gt (ha : a ≠ 0) (hb : b ≠ ∞) : ∃ n > 0, b < (n : ℕ) * a :=
  let ⟨n, hn⟩ := ENNReal.exists_nat_gt (div_lt_top hb ha).ne
  ⟨n, Nat.cast_pos.1 ((zero_le _).trans_lt hn), by
    rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]⟩

Proof state:
a b : ℝ≥0∞
ha : a ≠ 0
hb : b ≠ ⊤
n : ℕ
hn : b / a < ↑n
⊢ b < ↑n * a

Tactic:
rwa [← ENNReal.div_lt_iff (Or.inl ha) (Or.inr hb)]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem maxPowDiv_eq_multiplicity {p n : ℕ} (hp : 1 < p) (hn : 0 < n) (h : FiniteMultiplicity p n) :
    p.maxPowDiv n = multiplicity p n

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
h : FiniteMultiplicity p n
⊢ p.maxPowDiv n = multiplicity p n

Tactic:
exact_mod_cast h.emultiplicity_eq_multiplicity ▸ maxPowDiv_eq_emultiplicity hp hn

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive sub_abs_eq_neg_two_nsmul_negPart]
lemma div_mabs_eq_inv_leOnePart_sq (a : α) : a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / mabs a = (a⁻ᵐ ^ 2)⁻¹

Tactic:
rw [← mabs_div_eq_leOnePart_sq, inv_div]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_nonneg' {α} {x y : α} (dist : α → α → ℝ)
    (dist_self : ∀ x : α, dist x x = 0) (dist_comm : ∀ x y : α, dist x y = dist y x)
    (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : 0 ≤ dist x y :=
  have : 0 ≤ 2 * dist x y :=
    calc 0 = dist x x := (dist_self _).symm
    _ ≤ dist x y + dist y x := dist_triangle _ _ _
    _ = 2 * dist x y

Proof state:
α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
⊢ dist x y + dist y x = 2 * dist x y

Tactic:
rw [two_mul, dist_comm]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramified_iff_mult_le :
    IsUnramified k w ↔ mult w ≤ mult (w.comap (algebraMap k K))

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (w.comap (algebraMap k K)).mult ≤ w.mult

Tactic:
exact mult_comap_le _ _

Result:
no goals

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ IsUnramified k w ↔ w.mult ≤ (w.comap (algebraMap k K)).mult

Tactic:
rw [IsUnramified, le_antisymm_iff, and_iff_right]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (w.comap (algebraMap k K)).mult ≤ w.mult
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_average_le (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ ⨍ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x

Tactic:
simpa [integral_neg, neg_div] using exists_not_mem_null_le_average hμ hf.neg hN

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_Ioi : #(Ioi a) = n - 1 - a

Proof state:
n : ℕ
a : Fin n
⊢ #(Ioi a) = n - 1 - ↑a

Tactic:
rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioc]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) enorm_norm]
lemma enorm_norm' (x : E) : ‖‖x‖‖ₑ = ‖x‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem IsLocalization.algebraMap_eq_map_map_submonoid :
    algebraMap Rₘ Sₘ =
      map Sₘ (algebraMap R S)
        (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :=
  Eq.symm <|
    IsLocalization.map_unique _ (algebraMap Rₘ Sₘ) fun x => by
      rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

Proof state:
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x) = (algebraMap S Sₘ) ((algebraMap R S) x)

Tactic:
rw [← IsScalarTower.algebraMap_apply R S Sₘ, ← IsScalarTower.algebraMap_apply R Rₘ Sₘ]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem Convex.mem_Ioo (h : x < y) :
    z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
simp only [← openSegment_eq_Ioo h, openSegment, smul_eq_mul, exists_and_left, mem_setOf_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[reassoc (attr := simp)]
lemma map_reflexion_comp_map_left (F : WalkingReflexivePair ⥤ C) :
    F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map reflexion ≫ F.map left = 𝟙 (F.obj zero)

Tactic:
rw [← F.map_comp, reflexion_comp_left, F.map_id]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma toNNReal_lt_natCast' {n : ℕ} {r : ℝ} : r.toNNReal < n ↔ r < n ∧ n ≠ 0

Proof state:
n : ℕ
r : ℝ
⊢ r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using toNNReal_lt_toNNReal_iff' (r := r) (p := n)

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem one_div_one_div : 1 / (1 / a) = a

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 / (1 / a) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_comp_mul_right (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) :
    mellin (fun t => f (t * a)) s = (a : ℂ) ^ (-s) • mellin f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun t => f (t * a)) s = ↑a ^ (-s) • mellin f s

Tactic:
simpa only [mul_comm] using mellin_comp_mul_left f s ha

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
lemma Spec.map_inj : Spec.map φ = Spec.map ψ ↔ φ = ψ

Proof state:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ

Tactic:
rfl

Result:
no goals

Proof state:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ map φ = map ψ ↔ φ = ψ

Tactic:
rw [iff_comm, ← Quiver.Hom.op_inj.eq_iff, ← Scheme.Spec.map_injective.eq_iff]

Result:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem nsmul (n : ℕ) (x : WittVector p R) : mapFun f (n • x) = n • mapFun f x

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
n : ℕ
x : 𝕎 R
⊢ mapFun (⇑f) (n • x) = n • mapFun (⇑f) x

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_C_mul_X_pow (a : R) (n : ℕ) :
    Polynomial.toFinsupp (C a * X ^ n) = Finsupp.single n a

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).toFinsupp = Finsupp.single n a

Tactic:
rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_fin_repeat {m} (a : Fin m → α) (n : ℕ) :
    List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten

Proof state:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

Tactic:
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
  Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
theorem mem_fixingSubgroup_compl_iff_movedBy_subset {s : Set α} {m : M} :
    m ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
m : M
⊢ m ∈ fixingSubgroup M sᶜ ↔ (fixedBy α m)ᶜ ⊆ s

Tactic:
rw [mem_fixingSubgroup_iff_subset_fixedBy, Set.compl_subset_comm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOn.comp (h : TendstoUniformlyOn F f p s) (g : γ → α) :
    TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
g : γ → α
⊢ TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter] at h ⊢

Result:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))

Proof state:
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa [TendstoUniformlyOn, comap_principal] using TendstoUniformlyOnFilter.comp h g

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_left (a b : α) : toIocMod hp a (p + b) = toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (p + b) = toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_right]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_range_inter {f : α → β} {s : Set β} : f ⁻¹' (range f ∩ s) = f ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s

Tactic:
rw [inter_comm, preimage_inter_range]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma add_of_Y_eq {x₁ x₂ y₁ y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂}
    (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) : some h₁ + some h₂ = 0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ some h₁ + some h₂ = 0

Tactic:
simpa only [add_def, add] using dif_pos ⟨hx, hy⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_default [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    ¬a ∈ m → m.get! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ ¬a ∈ m → m.get! a = default

Tactic:
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem self_comp_symm (f : M ≃[L] N) : f.comp f.symm = refl L N

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.comp f.symm = refl L N

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : N
⊢ (f.comp f.symm) x✝ = (refl L N) x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
x✝ : N
⊢ (f.comp f.symm) x✝ = (refl L N) x✝

Tactic:
rw [comp_apply, apply_symm_apply, refl_apply]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_of_isEmpty [IsEmpty α] {f : α → β} {la : Filter α} {lb : Filter β} :
    Tendsto f la lb

Proof state:
α : Type u_1
β : Type u_2
inst✝ : IsEmpty α
f : α → β
la : Filter α
lb : Filter β
⊢ Tendsto f la lb

Tactic:
simp only [filter_eq_bot_of_isEmpty la, tendsto_bot]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_top_order [TopologicalSpace α] [Preorder α] [OrderTop α] [OrderTopology α] :
    𝓝 (⊤ : α) = ⨅ (l) (_ : l < ⊤), 𝓟 (Ioi l)

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : OrderTopology α
⊢ 𝓝 ⊤ = ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l)

Tactic:
simp [nhds_eq_order (⊤ : α)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_map' {x : Option α} : (x.map f).isSome = x.isSome

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝
x : Option α
⊢ (Option.map f x).isSome = x.isSome

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem true_eq (b : Bool) : (true = b) = (b = true)

Proof state:
b : Bool
⊢ (true = b) = (b = true)

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem ofFn_eq_map {n} {f : Fin n → α} : ofFn f = (finRange n).map f

Proof state:
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = map f (finRange n)

Tactic:
rw [← ofFn_id, map_ofFn, Function.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertManyIfNewUnit_list
    {l : List α} {k : α} {h} :
    get (insertManyIfNewUnit m l) k h = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
l : List α
k : α
h : k ∈ insertManyIfNewUnit m l
⊢ get (insertManyIfNewUnit m l) k h = ()

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem fstIdx_ne_iff {w : Word M} {i} :
    fstIdx w ≠ some i ↔ ∀ l ∈ w.toList.head?, i ≠ Sigma.fst l :=
  not_iff_not.mp <| by simp [fstIdx]

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
w : Word M
i : ι
⊢ ¬w.fstIdx ≠ some i ↔ ¬∀ l ∈ w.toList.head?, i ≠ l.fst

Tactic:
simp [fstIdx]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem inv_smul_integral_comp_div_sub (c d) :
    (c⁻¹ • ∫ x in a..b, f (x / c - d)) = ∫ x in a / c - d..b / c - d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_div_sub]

Result:
no goals