harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem absolutelyContinuous_inv : μ ≪ μ.inv

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
x✝ : MeasurableSet s
⊢ μ.inv s = 0 → μ s = 0

Tactic:
simp_rw [inv_apply μ s, measure_inv_null, imp_self]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ ≪ μ.inv

Tactic:
refine AbsolutelyContinuous.mk fun s _ => ?_

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
x✝ : MeasurableSet s
⊢ μ.inv s = 0 → μ s = 0
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem map_symm_apply_map_eq {x : FreeMonoid α} (e : α ≃ β) :
    (map ⇑e.symm) ((map ⇑e) x) = x

Proof state:
α : Type u_1
β : Type u_2
x : FreeMonoid α
e : α ≃ β
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
simp [map_map]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem inTangentCoordinates_model_space (f : N → H) (g : N → H') (ϕ : N → E →L[𝕜] E') (x₀ : N) :
    inTangentCoordinates I I' f g ϕ x₀ = ϕ

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_9
f : N → H
g : N → H'
ϕ : N → E →L[𝕜] E'
x₀ : N
⊢ inTangentCoordinates I I' f g ϕ x₀ = ϕ

Tactic:
simp (config := { unfoldPartialApp := true }) only [inTangentCoordinates,
  inCoordinates_tangent_bundle_core_model_space]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_eq_two_iff' (x : α) : #α = 2 ↔ ∃! y, y ≠ x

Proof state:
case mp.intro.intro.intro
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x

Tactic:
rcases h x with (rfl | rfl)

Result:
case mp.intro.intro.intro.inl
α : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y, y ≠ x

case mp.intro.intro.intro.inr
α : Type u
x a : α
hne : a ≠ x
h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x
⊢ ∃! y, y ≠ x

Proof state:
case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
rintro ⟨y, hne, hy⟩

Result:
case mpr.intro.intro
α : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y => y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Proof state:
case mp.intro.intro.intro
α : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x

Tactic:
simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h

Result:
case mp.intro.intro.intro
α : Type u
x a b : α
hne : a ≠ b
h : ∀ (x : α), x = a ∨ x = b
⊢ ∃! y, y ≠ x

Proof state:
α : Type u
x : α
⊢ #α = 2 ↔ ∃! y, y ≠ x

Tactic:
rw [mk_eq_two_iff]

Result:
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x

Proof state:
case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

Tactic:
rintro ⟨a, b, hne, h⟩

Result:
case mp.intro.intro.intro
α : Type u
x a b : α
hne : a ≠ b
h : {a, b} = univ
⊢ ∃! y, y ≠ x

Proof state:
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x

Tactic:
constructor

Result:
case mp
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃! y, y ≠ x

case mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ

Proof state:
case mpr.intro.intro
α : Type u
x y : α
hne : y ≠ x
hy : ∀ (y_1 : α), (fun y => y ≠ x) y_1 → y_1 = y
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.inl
α : Type u
x b : α
hne : x ≠ b
h : ∀ (x_1 : α), x_1 = x ∨ x_1 = b
⊢ ∃! y, y ≠ x

case mp.intro.intro.intro.inr
α : Type u
x a : α
hne : a ≠ x
h : ∀ (x_1 : α), x_1 = a ∨ x_1 = x
⊢ ∃! y, y ≠ x

Tactic:
exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_id : YonedaCollection.map₁ (𝟙 F) (X := X) = id

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
⊢ map₁ (𝟙 F) = id

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_mul_le (w₁ w₂ : W) :
    ℓ (w₁ * w₂) ≤ ℓ w₁ + ℓ w₂

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

Tactic:
rcases cs.exists_reduced_word w₁ with ⟨ω₁, hω₁, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₂ : W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
⊢ cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₂ : W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
⊢ cs.length (cs.wordProd ω₁ * w₂) ≤ cs.length (cs.wordProd ω₁) + cs.length w₂

Tactic:
rcases cs.exists_reduced_word w₂ with ⟨ω₂, hω₂, rfl⟩

Result:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
ω₂ : List B
hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Proof state:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
ω₂ : List B
hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
have := cs.length_wordProd_le (ω₁ ++ ω₂)

Result:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
ω₂ : List B
hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Proof state:
case intro.intro.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : ω₁.length = cs.length (cs.wordProd ω₁)
ω₂ : List B
hω₂ : ω₂.length = cs.length (cs.wordProd ω₂)
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
simpa [hω₁, hω₂, wordProd_append] using this

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_id_eq : image (id : α → α) = id

Proof state:
α : Type u_1
⊢ image id = id

Tactic:
ext

Result:
case h.h
α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹

Proof state:
case h.h
α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.elim_finite_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsCompact s)
    (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) :
    ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
case intro.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' ↑d, c i

Tactic:
rwa [biUnion_image]

Result:
no goals

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩

Result:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Proof state:
case intro.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ Subtype.val '' ↑d ⊆ b

Tactic:
simp

Result:
no goals

Proof state:
case intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
refine ⟨Subtype.val '' d.toSet, ?_, d.finite_toSet.image _, ?_⟩

Result:
case intro.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ Subtype.val '' ↑d ⊆ b

case intro.refine_2
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ (x : { a // a ∈ b }), IsOpen (c ↑x)
hc₂ : s ⊆ ⋃ x, c ↑x
d : Finset ↑b
hd : s ⊆ ⋃ i ∈ d, c ↑i
⊢ s ⊆ ⋃ i ∈ Subtype.val '' ↑d, c i
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_sub_smoothingFn_r_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < 1 - ε (r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 - ε ↑(r i x)

Tactic:
exact fun i => (R.tendsto_atTop_r_real i).eventually eventually_one_sub_smoothingFn_pos_real

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 - ε ↑(r i n)

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 - ε ↑(r i x)
-- Mathlib/Control/Applicative.lean
theorem map_pure (f : α → β) (x : α) : (f <$> pure x : Comp F G β) = pure (f x) :=
  Comp.ext <| by simp

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type v
f : α → β
x : α
⊢ (f <$> pure x).run = (pure (f x)).run

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive]
lemma dite_lt_one [LT α] (ha : ∀ h, a h < 1) (hb : ∀ h, b h < 1) : dite p a b < 1

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
⊢ dite p a b < 1

Tactic:
split

Result:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : p
⊢ a h✝ < 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : ¬p
⊢ b h✝ < 1

Proof state:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : p
⊢ a h✝ < 1

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h✝ : ¬p
⊢ b h✝ < 1

Tactic:
exacts [ha ‹_›, hb ‹_›]

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

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k : α
⊢ (m.erase k).getKey! k = default

Tactic:
simp_to_raw using Raw₀.getKey!_erase_self

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_tsub_tsub_le_tsub : c - a - (c - b) ≤ b - a

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c ≤ c - b + (a + (b - a))

Tactic:
exact le_tsub_add.trans (add_le_add_left le_add_tsub _)

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c - a - (c - b) ≤ b - a

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ c ≤ c - b + (a + (b - a))
-- Mathlib/CategoryTheory/Shift/Induced.lean
lemma shiftFunctor_of_induced (a : A) :
    letI := HasShift.induced F A s i
    shiftFunctor D a = s a

Proof state:
C : Type u_4
D : Type u_1
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_2, u_1} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a : A
⊢ shiftFunctor D a = s a

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swapAt_mk (a : Array α) (h : a.size = n) (i x) (hi) :
    (Vector.mk a h).swapAt i x =
      ((a.swapAt i x).fst, Vector.mk (a.swapAt i x).snd (by simp [h])) :=
  rfl

Proof state:
α : Type ?u.16042
n : Nat
a : Array α
h : a.size = n
i : Nat
x : α
hi : i < n
⊢ (a.swapAt i x ⋯).snd.size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_isTrail_iff_of_injective (hinj : Function.Injective f) :
    (p.map f).IsTrail ↔ p.IsTrail

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).IsTrail ↔ p✝.IsTrail
⊢ p✝.IsTrail ∧ s(f u✝, f v✝) ∉ (Walk.map f p✝).edges ↔ p✝.IsTrail ∧ s(u✝, v✝) ∉ p✝.edges

Tactic:
apply and_congr_right'

Result:
case cons.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).IsTrail ↔ p✝.IsTrail
⊢ s(f u✝, f v✝) ∉ (Walk.map f p✝).edges ↔ s(u✝, v✝) ∉ p✝.edges

Proof state:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ : V
⊢ (Walk.map f nil).IsTrail ↔ nil.IsTrail

Tactic:
simp

Result:
no goals

Proof state:
case cons.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).IsTrail ↔ p✝.IsTrail
⊢ s(f u✝, f v✝) ∉ (Walk.map f p✝).edges ↔ s(u✝, v✝) ∉ p✝.edges

Tactic:
rw [← Sym2.map_pair_eq, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]

Result:
no goals

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).IsTrail ↔ p✝.IsTrail
⊢ (Walk.map f (cons h✝ p✝)).IsTrail ↔ (cons h✝ p✝).IsTrail

Tactic:
rw [map_cons, cons_isTrail_iff, ih, cons_isTrail_iff]

Result:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (Walk.map f p✝).IsTrail ↔ p✝.IsTrail
⊢ p✝.IsTrail ∧ s(f u✝, f v✝) ∉ (Walk.map f p✝).edges ↔ p✝.IsTrail ∧ s(u✝, v✝) ∉ p✝.edges

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
hinj : Injective ⇑f
⊢ (Walk.map f p).IsTrail ↔ p.IsTrail

Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  rw [map_cons, cons_isTrail_iff, ih, cons_isTrail_iff]
  apply and_congr_right'
  rw [← Sym2.map_pair_eq, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem iSup_eq_span {ι : Sort*} (p : ι → Submodule R M) : ⨆ i, p i = span R (⋃ i, ↑(p i))

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
p : ι → Submodule R M
⊢ ⨆ i, p i = span R (⋃ i, ↑(p i))

Tactic:
simp_rw [← iSup_span, span_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_add_of_nonneg_right {a b : Int} (h : 0 ≤ b) : a ≤ a + b

Proof state:
a b : Int
h : 0 ≤ b
⊢ a ≤ a + b

Tactic:
have : a + b ≥ a + 0 := Int.add_le_add_left h a

Result:
a b : Int
h : 0 ≤ b
this : a + b ≥ a + 0
⊢ a ≤ a + b

Proof state:
a b : Int
h : 0 ≤ b
this : a + b ≥ a + 0
⊢ a ≤ a + b

Tactic:
rwa [Int.add_zero] at this

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.const_add [AddSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (a + x)) c := fun x => by simpa [add_assoc] using h (a + x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x => f (a + x)) (x + c) = -(fun x => f (a + x)) x

Tactic:
simpa [add_assoc] using h (a + x)

Result:
no goals
-- Mathlib/ModelTheory/LanguageMap.lean
theorem LHom.map_constants_comp_sumInl {f : α → β} :
    (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Proof state:
L : Language
α : Type w'
β : Type u_1
f : α → β
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem eventually_nhdsWithin' {x : X} (p : X → Prop) {s : Set X}
    (hx : x ∈ e.source) : (∀ᶠ y in 𝓝[e.symm ⁻¹' s] e x, p (e.symm y)) ↔ ∀ᶠ x in 𝓝[s] x, p x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
rw [e.eventually_nhdsWithin _ hx]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝[s] x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
y : X
hy : ↑e.symm (↑e y) = y
⊢ p (↑e.symm (↑e y)) ↔ p y

Tactic:
rw [hy]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝[s] x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
refine eventually_congr <|
  (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
s : Set X
hx : x ∈ e.source
y : X
hy : ↑e.symm (↑e y) = y
⊢ p (↑e.symm (↑e y)) ↔ p y
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem map_eq_lift : map f x = lift (of ∘ f) x :=
  Eq.symm <| map.unique _ fun x => by simp

Proof state:
α : Type u
β : Type v
f : α → β
x✝ : FreeGroup α
x : α
⊢ (lift (of ∘ f)) (of x) = of (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mapRange.linearMap_id :
    (mapRange.linearMap fun i => (LinearMap.id : β₂ i →ₗ[R] _)) = LinearMap.id

Proof state:
case h.h
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
β₂ : ι → Type u_8
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
x✝ : Π₀ (i : ι), β₂ i
i✝ : ι
⊢ ((linearMap fun i => LinearMap.id) x✝) i✝ = (LinearMap.id x✝) i✝

Tactic:
simp [linearMap]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
β₂ : ι → Type u_8
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
⊢ (linearMap fun i => LinearMap.id) = LinearMap.id

Tactic:
ext

Result:
case h.h
ι : Type u_1
R : Type u_2
inst✝² : Semiring R
β₂ : ι → Type u_8
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
x✝ : Π₀ (i : ι), β₂ i
i✝ : ι
⊢ ((linearMap fun i => LinearMap.id) x✝) i✝ = (LinearMap.id x✝) i✝
-- Mathlib/Logic/Equiv/Basic.lean
theorem sigmaEquivProd_sigmaCongrRight :
    (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)
    = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ⟨((sigmaEquivProd α₁ β₁).symm (a, b)).fst,
      (e ((sigmaEquivProd α₁ β₁).symm (a, b)).fst) ((sigmaEquivProd α₁ β₁).symm (a, b)).snd⟩ =
    (sigmaEquivProd α₁ β₂).symm (a, (e a) b)

Tactic:
rfl

Result:
no goals

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) =
    ((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)

Tactic:
simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ⟨((sigmaEquivProd α₁ β₁).symm (a, b)).fst,
      (e ((sigmaEquivProd α₁ β₁).symm (a, b)).fst) ((sigmaEquivProd α₁ β₁).symm (a, b)).snd⟩ =
    (sigmaEquivProd α₁ β₂).symm (a, (e a) b)

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) =
    ((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y

Proof state:
x y z : Nat
⊢ (x + y * 0) % y = x % y

Tactic:
rw [Nat.mul_zero, Nat.add_zero]

Result:
no goals

Proof state:
x y z✝ z : Nat
⊢ (x + y * z.succ) % y = x % y

Tactic:
rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]

Result:
no goals

Proof state:
x y z : Nat
⊢ (x + y * z) % y = x % y

Tactic:
match z with
| 0 => rw [Nat.mul_zero, Nat.add_zero]
| succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasDerivAtFilter.const_sub (c : F) (hf : HasDerivAtFilter f f' x L) :
    HasDerivAtFilter (fun x => c - f x) (-f') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
c : F
hf : HasDerivAtFilter f f' x L
⊢ HasDerivAtFilter (fun x => c - f x) (-f') x L

Tactic:
simpa only [sub_eq_add_neg] using hf.neg.const_add c

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) : x⁻¹ < 1 ↔ 1 < x

Proof state:
x : ℝ≥0
hx : x ≠ 0
⊢ x⁻¹ < 1 ↔ 1 < x

Tactic:
rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]

Result:
no goals