harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem map_proj_nhds (ex : x ∈ e.source) : map proj (𝓝 x) = 𝓝 (proj x)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map proj (𝓝 x) = 𝓝 (proj x)

Tactic:
rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe,
  e.map_nhds_eq ex, map_fst_nhds]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_of_one_le {x : ℝ} (hx : 1 ≤ x) : arccos x = 0

Proof state:
x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0

Tactic:
rw [arccos, arcsin_of_one_le hx, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/DecidableEq.lean
theorem beq_toArray [BEq α] (a b : Vector α n) : (a.toArray == b.toArray) = (a == b)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Vector α n
⊢ (a.toArray == b.toArray) = (a == b)

Tactic:
simp [beq_eq_decide, Array.beq_eq_decide]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsLowerSet.thickening' (hs : IsLowerSet s) (ε : ℝ) :
    IsLowerSet (thickening ε s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (thickening ε s)

Tactic:
rw [← ball_mul_one]

Result:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsLowerSet s
ε : ℝ
⊢ IsLowerSet (ball 1 ε * s)

Tactic:
exact hs.mul_left

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem rightHom_inl (n : N) : rightHom (inl n : N ⋊[φ] G) = 1

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
n : N
⊢ rightHom (inl n) = 1

Tactic:
simp [rightHom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_eq_true  {b : Bool} [Decidable (b = true)]  : decide (b = true)  =  b

Proof state:
b : Bool
inst✝ : Decidable (b = true)
⊢ decide (b = true) = b

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_range {n : Nat} : (range n).size = n

Proof state:
n : Nat
⊢ (range n).size = n

Tactic:
simp [range]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_one_succ (j : ℕ) (hj : j + 1 < n + 1 + 1) :
    map F f 1 ⟨j + 1, hj⟩ (by simp [Fin.le_def]) = F.map' 0 j := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.89329, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 1 < n + 1 + 1
⊢ 1 ≤ ⟨j + 1, hj⟩

Tactic:
simp [Fin.le_def]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem fineSubfamilyOn_of_frequently (v : VitaliFamily μ) (f : X → Set (Set X)) (s : Set X)
    (h : ∀ x ∈ s, ∃ᶠ t in v.filterAt x, t ∈ f x) : v.FineSubfamilyOn f s

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Tactic:
obtain ⟨t, tv, ht, tf⟩ : ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ t ∈ f x :=
  v.frequently_filterAt_iff.1 (h x hx) ε εpos

Result:
case intro.intro.intro
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tv : t ∈ v.setsAt x
ht : t ⊆ closedBall x ε
tf : t ∈ f x
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Proof state:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
⊢ v.FineSubfamilyOn f s

Tactic:
intro x hx ε εpos

Result:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tv : t ∈ v.setsAt x
ht : t ⊆ closedBall x ε
tf : t ∈ f x
⊢ ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε

Tactic:
exact ⟨t, ⟨tv, tf⟩, ht⟩

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_preimage_of_injective_subset_range (hf : f.Injective) (ht : t ⊆ range f) :
    (f ⁻¹' t).encard = t.encard

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem relindex_inf_mul_relindex : H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L

Proof state:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L

Tactic:
rw [← inf_relindex_right H (K ⊓ L), ← inf_relindex_right K L, ← inf_relindex_right (H ⊓ K) L,
  inf_assoc, relindex_mul_relindex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_mod (l : List α) (n : ℕ) : l.rotate' (n % l.length) = l.rotate' n :=
  calc
    l.rotate' (n % l.length) =
        (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) :=
      by rw [rotate'_length_mul]
    _ = l.rotate' n

Proof state:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n

Tactic:
rw [rotate'_rotate', length_rotate', Nat.mod_add_div]

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))

Tactic:
rw [rotate'_length_mul]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_add (x y : 𝕎 R) (n : ℕ) : init n (x + y) = init n (init n x + init n y)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x + y) = init n (init n x + init n y)

Tactic:
init_ring using wittAdd_vars

Result:
no goals
-- Mathlib/Logic/Function/CompTypeclasses.lean
lemma comp_inv {M N : Type*} {φ : M → N} {ψ : N → M}
    (h : Function.RightInverse φ ψ) {χ : M → M} [IsId χ] :
    CompTriple φ ψ χ where
  comp_eq

Proof state:
M : Type u_1
N : Type u_2
φ : M → N
ψ : N → M
h : Function.RightInverse φ ψ
χ : M → M
inst✝ : IsId χ
⊢ ψ ∘ φ = χ

Tactic:
simp only [IsId.eq_id, h.id]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.div_atTop {a : 𝕜} (h : Tendsto f l (𝓝 a)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x / g x) l (𝓝 0)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)

Tactic:
exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x / g x) l (𝓝 0)

Tactic:
simp only [div_eq_mul_inv]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b

Proof state:
a b : Int
⊢ (-a).gcd b = a.gcd b

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem prod_top (s : Submonoid M) : s.prod (⊤ : Submonoid N) = s.comap (MonoidHom.fst M N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
x : M × N
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (MonoidHom.fst M N) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_const_add (a x : 𝕜) (hf : HasDerivAt f f' (a + x)) :
    HasDerivAt (fun x ↦ f (a + x)) f' x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
a x : 𝕜
hf : HasDerivAt f f' (a + x)
⊢ HasDerivAt (fun x => f (a + x)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.const_add a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
     as.setIfInBounds n a = #[] ↔ as = #[]

Proof state:
α : Type u_1
as : Array α
n : Nat
a : α
⊢ as.setIfInBounds n a = #[] ↔ as = #[]

Tactic:
cases as <;> cases n <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_add {p : ℕ} (hp : p ≠ 0) (f g : R[X]) :
    contract p (f + g) = contract p f + contract p g

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f + g) = contract p f + contract p g

Tactic:
ext

Result:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n✝ : ℕ
⊢ (contract p (f + g)).coeff n✝ = (contract p f + contract p g).coeff n✝

Tactic:
simp_rw [coeff_add, coeff_contract hp, coeff_add]

Result:
no goals
-- Mathlib/Algebra/Lie/BaseChange.lean
@[simp]
lemma baseChange_top : (⊤ : LieSubmodule R L M).baseChange A = ⊤

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ { toSubmodule := ⊤, lie_mem := ⋯ } = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ baseChange A ⊤ = ⊤

Tactic:
simp only [baseChange, top_toSubmodule, Submodule.baseChange_top,
  Submodule.bot_toAddSubmonoid]

Result:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ { toSubmodule := ⊤, lie_mem := ⋯ } = ⊤
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_of_ge (h : b ≤ a) : [[a, b]] = Icc b a

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_vadd_eq_of_sum_eq_one (w : ι → k) (p : ι → P) (h : ∑ i ∈ s, w i = 1)
    (b₁ b₂ : P) : s.weightedVSubOfPoint p b₁ w +ᵥ b₁ = s.weightedVSubOfPoint p b₂ w +ᵥ b₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0

Tactic:
rw [← sum_smul, h, one_smul, vsub_add_vsub_cancel, vsub_self]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply, ← @vsub_eq_zero_iff_eq V,
  vadd_vsub_assoc, vsub_vadd_eq_vsub_sub, ← add_sub_assoc, add_comm, add_sub_assoc, ←
  sum_sub_distrib]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioc_bot : (some : α → WithBot α) ⁻¹' Ioc ⊥ a = Iic a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ioc ⊥ ↑a = Iic a

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
    m.isEmpty = false ↔ ∃ a, a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
⊢ m.isEmpty = false ↔ ∃ a, a ∈ m

Tactic:
simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem outerMeasure_le_iff {m : OuterMeasure α} : m ≤ μ.1 ↔ ∀ s, MeasurableSet s → m s ≤ μ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
m : OuterMeasure α
⊢ m ≤ μ.toOuterMeasure ↔ ∀ (s : Set α), MeasurableSet s → m s ≤ μ s

Tactic:
simpa only [μ.trimmed] using OuterMeasure.le_trim_iff (m₂ := μ.1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
⊢ a ∈ m.erase k → a ∈ m

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] protected lemma sdiff_eq_left : s.sdiff t = s ↔ Disjoint ↑s t

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s) t

Tactic:
simp [← SetLike.coe_set_eq]

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem relabel_not (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α k) :
    φ.not.relabel g = (φ.relabel g).not

Proof state:
L : Language
α : Type u'
β : Type v'
n : ℕ
g : α → β ⊕ Fin n
k : ℕ
φ : L.BoundedFormula α k
⊢ relabel g φ.not = (relabel g φ).not

Tactic:
simp [BoundedFormula.not]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[simp] lemma emod_two_ne_one : ¬n % 2 = 1 ↔ n % 2 = 0

Proof state:
n : ℤ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0

Tactic:
rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_eq_iff_surjOn_mapsTo : f '' s = t ↔ s.SurjOn f t ∧ s.MapsTo f t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)

Tactic:
exact ⟨s.surjOn_image f, s.mapsTo_image f⟩

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurableSet_image (hf : MeasurableEmbedding f) :
    MeasurableSet (f '' s) ↔ MeasurableSet s :=
  ⟨fun h => by simpa only [hf.injective.preimage_image] using hf.measurable h, fun h =>
    hf.measurableSet_image' h⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
h : MeasurableSet (f '' s)
⊢ MeasurableSet s

Tactic:
simpa only [hf.injective.preimage_image] using hf.measurable h

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem strictConcaveOn_sin_Icc : StrictConcaveOn ℝ (Icc 0 π) sin

Proof state:
⊢ StrictConcaveOn ℝ (Icc 0 π) sin

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_

Result:
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0

Proof state:
x : ℝ
hx : x ∈ Ioo 0 π
⊢ deriv^[2] sin x < 0

Tactic:
simp [sin_pos_of_mem_Ioo hx]

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0

Tactic:
rw [interior_Icc] at hx

Result:
x : ℝ
hx : x ∈ Ioo 0 π
⊢ deriv^[2] sin x < 0
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_hom₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d)
    (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) :
    (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ ∀ (a : M) (b : N) (i : ι), f (f₁ i * a) (f₂ i * b) = (fun x y => f (f₁ x) (f₂ x) * y) i (f a b)

Tactic:
simp [hf]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i => f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
rw [prod, prod, prod, foldr_map, foldr_map, foldr_map,
  ← l.foldr_hom₂ f _ _ (fun x y => f (f₁ x) (f₂ x) * y) _ _ (by simp [hf]), hf']

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma isLocallyInjective_of_isLocallyInjective_fac {φψ : F₁ ⟶ F₃} (fac : φ ≫ ψ = φψ)
    [IsLocallyInjective J φψ] : IsLocallyInjective J φ

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
⊢ IsLocallyInjective J φ

Tactic:
exact isLocallyInjective_of_isLocallyInjective J φ ψ

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst✝ : IsLocallyInjective J φψ
⊢ IsLocallyInjective J φ

Tactic:
subst fac

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
⊢ IsLocallyInjective J φ
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_of_subsingleton [Subsingleton R] : degree p = ⊥

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ p.degree = ⊥

Tactic:
rw [Subsingleton.elim p 0, degree_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
@[simp] lemma mk_mem_nonUniforms :
    (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Tactic:
rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem permCongr_trans (p p' : Equiv.Perm α') :
    (e.permCongr p).trans (e.permCongr p') = e.permCongr (p.trans p')

Proof state:
case H
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
x✝ : β'
⊢ (Equiv.trans (e.permCongr p) (e.permCongr p')) x✝ = (e.permCongr (Equiv.trans p p')) x✝

Tactic:
simp only [trans_apply, comp_apply, permCongr_apply, symm_apply_apply]

Result:
no goals

Proof state:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

Tactic:
ext

Result:
case H
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
x✝ : β'
⊢ (Equiv.trans (e.permCongr p) (e.permCongr p')) x✝ = (e.permCongr (Equiv.trans p p')) x✝
-- Mathlib/Tactic/Abel.lean
theorem term_atomg {α} [AddCommGroup α] (x : α) : x = termg 1 x 0

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
x : α
⊢ x = termg 1 x 0

Tactic:
simp [termg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_self (f : α → α → δ) (l : Vector α n) : zipWith f l l = l.map fun a => f a a

Proof state:
α : Type u_1
δ : Type u_2
n : Nat
f : α → α → δ
l : Vector α n
⊢ zipWith f l l = map (fun a => f a a) l

Tactic:
cases l

Result:
case mk
α : Type u_1
δ : Type u_2
n : Nat
f : α → α → δ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ }
      { toArray := toArray✝, size_toArray := size_toArray✝ } =
    map (fun a => f a a) { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
δ : Type u_2
n : Nat
f : α → α → δ
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ zipWith f { toArray := toArray✝, size_toArray := size_toArray✝ }
      { toArray := toArray✝, size_toArray := size_toArray✝ } =
    map (fun a => f a a) { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem coe_sSup_of_directedOn {S : Set (Subsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem dvd_two_of_totient_le_one {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2

Proof state:
a : ℕ
han : 0 < a
ha : φ a ≤ 1
⊢ a ∣ 2

Tactic:
rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl <;> norm_num

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
lemma smul_indicator_one_apply (s : Set α) (r : R) (a : α) :
    r • s.indicator (1 : α → R) a = s.indicator (fun _ ↦ r) a

Proof state:
α : Type u_1
R : Type u_2
inst✝ : MulZeroOneClass R
s : Set α
r : R
a : α
⊢ r • s.indicator 1 a = s.indicator (fun x => r) a

Tactic:
simp_rw [← indicator_const_smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_eq_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {a : α} {h} :
    m.getKey a h = m.getKey! a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h✝ : m.val.WF
a : α
h : m.contains a = true
⊢ m.getKey a h = m.getKey! a

Tactic:
simp_to_model using List.getKey_eq_getKey!

Result:
no goals