harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma norm_mul_eq_norm_right {x : E} (y : E) (h : ‖x‖ = 0) : ‖x * y‖ = ‖y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ = ‖y‖

Tactic:
apply le_antisymm ?_ ?_

Result:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖

E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x * y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x * y‖

Tactic:
simpa [h] using norm_le_mul_norm_add' x y

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x * y‖ ≤ ‖y‖

Tactic:
simpa [h] using norm_mul_le' x y

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean
lemma injective_of_mono [Mono f] (X : Cᵒᵖ) :
    Function.Injective (f.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Mono (f.app X)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
rw [← ModuleCat.mono_iff_injective]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Mono (f.app X)
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
  | (n : ℕ) => hs.pow
  | .negSucc n => by simpa using hs.pow

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using hs.pow

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr₂_right_right (f₁ : β → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).snd s₁)
    = let m := mapAccumr₂ (fun x y (s₁, s₂) =>
                let r₂ := f₂ x y s₂
                let r₁ := f₁ y r₂.snd s₁
                ((r₁.fst, r₂.fst), r₁.snd)
              )
            xs ys (s₁, s₂)
    (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : β → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ ys (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernelIsoOfEq_hom_comp_ι {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) :
    (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).hom ≫ kernel.ι f = kernel.ι f

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).hom ≫ kernel.ι f = kernel.ι f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
theorem norm_indicator_le_of_subset (h : s ⊆ t) (f : α → E) (a : α) :
    ‖indicator s f a‖ ≤ ‖indicator t f a‖

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖t.indicator f a‖

Tactic:
simp only [norm_indicator_eq_indicator_norm]

Result:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖) a ≤ t.indicator (fun a => ‖f a‖) a

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ s.indicator (fun a => ‖f a‖) a ≤ t.indicator (fun a => ‖f a‖) a

Tactic:
exact indicator_le_indicator_of_subset ‹_› (fun _ => norm_nonneg _) _

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma vecMul_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
    (ha : IsUnit A) : Function.Injective A.vecMul

Proof state:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
x y : m → R
hxy : (fun v => v ᵥ* A) x = (fun v => v ᵥ* A) y
⊢ x = y

Tactic:
simpa [hBl] using congrArg B.vecMul hxy

Result:
no goals

Proof state:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
⊢ Function.Injective fun v => v ᵥ* A

Tactic:
intro x y hxy

Result:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
x y : m → R
hxy : (fun v => v ᵥ* A) x = (fun v => v ᵥ* A) y
⊢ x = y

Proof state:
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
⊢ Function.Injective fun v => v ᵥ* A

Tactic:
obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha

Result:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
⊢ Function.Injective fun v => v ᵥ* A
-- Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
lemma Sieve.generateFamily_eq {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) :
    Sieve.generate (Presieve.ofArrows X π) = Sieve.generateFamily X π

Proof state:
case h.mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g

Tactic:
rintro ⟨a, g, rfl⟩

Result:
case h.mpr.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)

Proof state:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g → (generateFamily X π).arrows g

Tactic:
rintro ⟨W, g, f, ⟨a⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y✝ Y : C
a : α
g : Y✝ ⟶ X a
⊢ (generateFamily X π).arrows (g ≫ π a)

Proof state:
case h.mpr.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)

Tactic:
exact ⟨_, g, π a, ⟨a⟩, rfl⟩

Result:
no goals

Proof state:
case h.mp.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y✝ Y : C
a : α
g : Y✝ ⟶ X a
⊢ (generateFamily X π).arrows (g ≫ π a)

Tactic:
exact ⟨a, g, rfl⟩

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g ↔ (generateFamily X π).arrows g

Tactic:
constructor

Result:
case h.mp
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g → (generateFamily X π).arrows g

case h.mpr
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generateFamily X π).arrows g → (generate (Presieve.ofArrows X π)).arrows g

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
⊢ generate (Presieve.ofArrows X π) = generateFamily X π

Tactic:
ext Y g

Result:
case h
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
Y : C
g : Y ⟶ B
⊢ (generate (Presieve.ofArrows X π)).arrows g ↔ (generateFamily X π).arrows g
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem A_mono (L : E →L[𝕜] F) (r : ℝ) {ε δ : ℝ} (h : ε ≤ δ) : A f L r ε ⊆ A f L r δ

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
⊢ 0 ≤ r

Tactic:
linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
rintro x ⟨r', r'r, hr'⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ x ∈ A f L r δ

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ x ∈ A f L r δ

Tactic:
refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right h ?_)⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
x : E
r' : ℝ
r'r : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
y : E
hy : y ∈ ball x r'
z : E
hz : z ∈ ball x r'
⊢ 0 ≤ r
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- An object is not initial if and only if its fiber is nonempty. -/
lemma not_initial_iff_fiber_nonempty (X : C) : (IsInitial X → False) ↔ Nonempty (F.obj X)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
he : IsEmpty (F.obj X).carrier
⊢ False

Tactic:
exact Nonempty.elim ((initial_iff_fiber_empty F X).mpr he) h

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ IsInitial X → False ↔ ¬IsEmpty (F.obj X).carrier

Tactic:
refine ⟨fun h he ↦ ?_, fun h hin ↦ h <| (initial_iff_fiber_empty F X).mp ⟨hin⟩⟩

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
h : IsInitial X → False
he : IsEmpty (F.obj X).carrier
⊢ False

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ IsInitial X → False ↔ Nonempty (F.obj X).carrier

Tactic:
rw [← not_isEmpty_iff]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ IsInitial X → False ↔ ¬IsEmpty (F.obj X).carrier
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mul_mem_ball_iff_norm : a * b ∈ ball a r ↔ ‖b‖ < r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r

Tactic:
rw [mem_ball_iff_norm'', mul_div_cancel_left]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma sinZeta_eq (a : UnitAddCircle) (s : ℂ) :
    sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)

Proof state:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s * (2 * I) = I * sinZeta a s + I * sinZeta a s

Tactic:
ring_nf

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)

Tactic:
field_simp

Result:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s * (2 * I) = I * sinZeta a s + I * sinZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)

Tactic:
rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]

Result:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_sup_le {ι} {f : ι → Ordinal} (H : ∀ i, f i < sup.{u, u} f) :
    cof (sup.{u, u} f) ≤ #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ #ι

Tactic:
rw [← (#ι).lift_id]

Result:
ι : Type u
f : ι → Ordinal.{u}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ Cardinal.lift.{u, u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{u}
H : ∀ (i : ι), f i < sup f
⊢ (sup f).cof ≤ Cardinal.lift.{u, u} #ι

Tactic:
exact cof_sup_le_lift H

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_comap_setCoe_val (f : Filter β) (s : Set β) :
    (f.comap ((↑) : s → β)).map (↑) = f ⊓ 𝓟 s

Proof state:
β : Type u_2
f : Filter β
s : Set β
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s

Tactic:
rw [map_comap, Subtype.range_val]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem stronglyMeasurable_derivWithin_Ioi :
    StronglyMeasurable (fun x ↦ derivWithin f (Ioi x) x)

Proof state:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
⊢ StronglyMeasurable fun x => derivWithin f (Ioi x) x

Tactic:
simpa [derivWithin_Ioi_eq_Ici] using stronglyMeasurable_derivWithin_Ici f

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_eval' {σ₁ σ₂} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂)
    (H : Respects f₁ f₂ fun a b ↦ tr a = b) (a₁) : eval f₂ (tr a₁) = tr <$> eval f₁ a₁ :=
  Part.ext fun b₂ ↦
    ⟨fun h ↦
      let ⟨b₁, bb, hb⟩ := tr_eval_rev H rfl h
      (Part.mem_map_iff _).2 ⟨b₁, hb, bb⟩,
      fun h ↦ by
      rcases (Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩
      rcases tr_eval H rfl ab with ⟨_, rfl, h⟩
      rwa [bb] at h⟩

Proof state:
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rcases (Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩

Result:
case intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
⊢ b₂ ∈ eval f₂ (tr a₁)

Proof state:
case intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rcases tr_eval H rfl ab with ⟨_, rfl, h⟩

Result:
case intro.intro.intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Proof state:
case intro.intro.intro.intro
σ₁ σ₂ : Type u_1
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
H : Respects f₁ f₂ fun a b => tr a = b
a₁ : σ₁
b₂ : σ₂
h✝ : b₂ ∈ tr <$> eval f₁ a₁
b₁ : σ₁
ab : b₁ ∈ eval f₁ a₁
bb : tr b₁ = b₂
h : tr b₁ ∈ eval f₂ (tr a₁)
⊢ b₂ ∈ eval f₂ (tr a₁)

Tactic:
rwa [bb] at h

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toDFinsupp_union (s t : Multiset α) : toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t

Tactic:
ext i

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsLE_iff_exists_Ioc_subset' {a l' : α} {s : Set α} (hl' : l' < a) :
    s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s :=
  (TFAE_mem_nhdsLE hl' s).out 0 4 (by norm_num) (by norm_num)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s].get? 4 =
    some (∃ l ∈ Iio a, Ioc l a ⊆ s)

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s].get? 0 =
    some (s ∈ 𝓝[≤] a)

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List α} {k fallback : α}
    (contains_eq_false : l.contains k = false) :
    getKeyD (unitOfList l) k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k fallback : α
contains_eq_false : l.contains k = false
⊢ (unitOfList l).getKeyD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_circumcenter_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P}
    (h : ps ⊆ s) [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction]
    (hd : finrank ℝ s.direction = n) (hc : Cospherical ps) :
    ∃ c : P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumcenter = c

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
⊢ sx.circumcenter = c

Tactic:
have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc

Result:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc✝ : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : c ∈ affineSpan ℝ (Set.range sx.points)
⊢ sx.circumcenter = c
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_coe_pi_div_two : (↑(π / 2) : Angle).sign = 1

Proof state:
⊢ (↑(π / 2)).sign = 1

Tactic:
rw [sign, sin_coe, sin_pi_div_two, sign_one]

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_eq_embeddingsMatrixReindex_mul_trans [Fintype κ] (e : κ ≃ (L →ₐ[K] E)) :
    (traceMatrix K b).map (algebraMap K E) =
      embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ

Proof state:
K : Type u_4
L : Type u_5
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
κ : Type w
E : Type z
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Module.Finite K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsAlgClosed E
b : κ → L
inst✝ : Fintype κ
e : κ ≃ (L →ₐ[K] E)
⊢ (traceMatrix K b).map ⇑(algebraMap K E) = embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ

Tactic:
rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
  transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]

Result:
no goals
-- Mathlib/Data/Finset/Range.lean
theorem range_eq_empty_iff : range n = ∅ ↔ n = 0

Proof state:
n : ℕ
⊢ range n = ∅ ↔ n = 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_range_iff, not_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
    (set l i a)[i]? = Function.const _ a <$> l[i]?

Proof state:
case pos
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

Tactic:
simp [getElem?_set_self h, getElem?_eq_getElem h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

Tactic:
by_cases h : i < l.length

Result:
case pos
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

case neg
α : Type u_1
l : List α
i : Nat
a : α
h : ¬i < l.length
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

Proof state:
case neg
α : Type u_1
l : List α
i : Nat
a : α
h : l.length ≤ i
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

Tactic:
simpa [getElem?_eq_none_iff.2 h]

Result:
no goals

Proof state:
case neg
α : Type u_1
l : List α
i : Nat
a : α
h : ¬i < l.length
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?

Tactic:
simp only [Nat.not_lt] at h

Result:
case neg
α : Type u_1
l : List α
i : Nat
a : α
h : l.length ≤ i
⊢ (l.set i a)[i]? = Function.const α a <$> l[i]?
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.nat_mul_eq_of_eq_zero [Semiring α] [NegZeroClass β] (h : Antiperiodic f c)
    (hi : f 0 = 0) : ∀ n : ℕ, f (n * c) = 0
  | 0 => by rwa [Nat.cast_zero, zero_mul]
  | n + 1 => by simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑(n + 1) * c) = 0

Tactic:
simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Semiring α
inst✝ : NegZeroClass β
h : Antiperiodic f c
hi : f 0 = 0
⊢ f (↑0 * c) = 0

Tactic:
rwa [Nat.cast_zero, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma stabilizer_finite (hs₀ : s.Nonempty) (hs : s.Finite) : (stabilizer G s : Set G).Finite

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
hs₀ : s.Nonempty
hs : s.Finite
⊢ (↑(stabilizer G s)).Finite

Tactic:
obtain ⟨a, ha⟩ := hs₀

Result:
case intro
G : Type u_1
inst✝ : Group G
s : Set G
hs : s.Finite
a : G
ha : a ∈ s
⊢ (↑(stabilizer G s)).Finite

Proof state:
case intro
G : Type u_1
inst✝ : Group G
s : Set G
hs : s.Finite
a : G
ha : a ∈ s
⊢ (↑(stabilizer G s)).Finite

Tactic:
exact (hs.div <| finite_singleton _).subset <| stabilizer_subset_div_right ha

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : Coprime (n - m) m ↔ Coprime n m

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime m ↔ n.Coprime m

Tactic:
rw [Coprime, Coprime, gcd_sub_self_left h]

Result:
no goals