harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_naturality {f g : β → C} (z : ∀ b, f b ⟶ g b) {j j' : β} (w : j = j') :
    z j ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ z j'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j'

Tactic:
cases w

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp, nolint simpNF] protected lemma add_eq_left : a + b = a ↔ b = 0

Proof state:
a b : ℕ
⊢ a + b = a ↔ b = 0

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- We can always derive `PreservesFiniteLimits C` by showing that we are preserving limits at an
arbitrary universe. -/
lemma preservesFiniteLimits_of_preservesFiniteLimitsOfSize (F : C ⥤ D)
    (h :
      ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), PreservesLimitsOfShape J F) :
    PreservesFiniteLimits F where
      preservesFiniteLimits J (_ : SmallCategory J) _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : PreservesLimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesLimitsOfShape J F

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
this : PreservesLimitsOfShape (ULiftHom (ULift.{w, 0} J)) F
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv (ULiftHomULiftCategory.equiv J).symm F

Result:
no goals
-- Mathlib/RingTheory/EuclideanDomain.lean
theorem right_div_gcd_ne_zero {p q : R} (hq : q ≠ 0) : q / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
nth_rw 1 [hr]

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0

Tactic:
exact r0

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0

Tactic:
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q

Result:
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ pq0]

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_insertListIfNewUnit [BEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α} :
    (List.insertListIfNewUnit l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Proof state:
case nil
α : Type u
inst✝ : BEq α
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit l []).isEmpty = (l.isEmpty && [].isEmpty)

Tactic:
simp [insertListIfNewUnit]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : BEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((_ : α) × Unit)
⊢ (false && tl.isEmpty) = (l.isEmpty && false)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : BEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((_ : α) × Unit)
⊢ (insertListIfNewUnit l (hd :: tl)).isEmpty = (l.isEmpty && (hd :: tl).isEmpty)

Tactic:
rw [insertListIfNewUnit, List.isEmpty_cons, ih, isEmpty_insertEntryIfNew]

Result:
case cons
α : Type u
inst✝ : BEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, (insertListIfNewUnit l tl).isEmpty = (l.isEmpty && tl.isEmpty)
l : List ((_ : α) × Unit)
⊢ (false && tl.isEmpty) = (l.isEmpty && false)

Proof state:
α : Type u
inst✝ : BEq α
l : List ((_ : α) × Unit)
toInsert : List α
⊢ (insertListIfNewUnit l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Tactic:
induction toInsert generalizing l with
| nil => simp [insertListIfNewUnit]
| cons hd tl ih =>
  rw [insertListIfNewUnit, List.isEmpty_cons, ih, isEmpty_insertEntryIfNew]
  simp

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.nth_succ {Γ} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) :
    l.nth (n + 1) = l.tail.nth n

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ (cons l.head l.tail).nth (n + 1) = l.tail.nth n

Tactic:
exact Quotient.inductionOn' l.tail fun l ↦ rfl

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ l.nth (n + 1) = l.tail.nth n

Tactic:
conv => lhs; rw [← ListBlank.cons_head_tail l]

Result:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ (cons l.head l.tail).nth (n + 1) = l.tail.nth n
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma map_id : map φ φ (𝟙 _) (𝟙 _) (by rw [id_comp, comp_id]) = 𝟙 _

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (map φ φ (𝟙 K) (𝟙 L) ⋯).f n = (𝟙 (mappingCone φ)).f n

Tactic:
simp [ext_from_iff _ (n + 1) n rfl, map]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ map φ φ (𝟙 K) (𝟙 L) ⋯ = 𝟙 (mappingCone φ)

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (map φ φ (𝟙 K) (𝟙 L) ⋯).f n = (𝟙 (mappingCone φ)).f n

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.70628, u_1} C
inst✝⁴ : Category.{?u.70632, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
⊢ φ ≫ 𝟙 L = 𝟙 K ≫ φ

Tactic:
rw [id_comp, comp_id]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma norm_le_natCast_iff_of_nonneg (a : A) (n : ℕ) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
n : ℕ
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖ ≤ ↑n ↔ a ≤ ↑n

Tactic:
simpa using norm_le_iff_le_algebraMap a n.cast_nonneg

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem univ_fin2 : (univ : Finset (Fin 2)) = {0, 1}

Proof state:
⊢ univ = {0, 1}

Tactic:
ext x

Result:
case h
x : Fin 2
⊢ x ∈ univ ↔ x ∈ {0, 1}

Proof state:
case h
x : Fin 2
⊢ x ∈ univ ↔ x ∈ {0, 1}

Tactic:
fin_cases x <;> simp

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_lsingle (i : ι) :
    comul ∘ₗ (lsingle i : A →ₗ[R] _) = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Proof state:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
x✝ : A
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ comul ∘ₗ lsingle i = TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul

Tactic:
ext

Result:
case h
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
x✝ : A
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_symm_comm {α : R₁ ⟶ R₂} {β : R₂ ⟶ R₁} (αβ : α ≫ β = 𝟙 _) :
    (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 _

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
β : R₂ ⟶ R₁
αβ : α ≫ β = 𝟙 R₁
⊢ (conjugateEquiv adj₂ adj₁).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = 𝟙 L₁

Tactic:
rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem mul_liftRight_inv (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
    f x * ↑(IsUnit.liftRight f h x)⁻¹ = 1 := Units.mul_liftRight_inv (by intro; rfl) x

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x : M
⊢ ∀ (x : M), ↑⋯.unit = f x

Tactic:
intro

Result:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.Const.insertMany {β : Type v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ (α × β)]
    {m : Raw α (fun _ => β)} {l : ρ} (h : m.WF) : (Const.insertMany m l).WF

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
ρ : Type w
inst✝ : ForIn Id ρ (α × β)
m : Raw α fun x => β
l : ρ
h : m.WF
⊢ (Raw.Const.insertMany m l).WF

Tactic:
simpa [Raw.Const.insertMany, h.size_buckets_pos] using
  (Raw₀.Const.insertMany ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insert₀ h

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem pow_end {f : Function.End α} {K} (h : LipschitzWith K f) :
    ∀ n : ℕ, LipschitzWith (K ^ n) (f ^ n : Function.End α)
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by
    rw [pow_succ, pow_succ]
    exact (LipschitzWith.pow_end h n).mul_end h

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ n * f)

Tactic:
exact (LipschitzWith.pow_end h n).mul_end h

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) (f ^ 0)

Tactic:
simpa only [pow_zero] using LipschitzWith.id

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ n * f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem xor_left_comm : ∀ (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z))

Proof state:
⊢ ∀ (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z))

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem normalize_eq_inv_mass_smul_of_nonzero (nonzero : μ ≠ 0) :
    μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure

Tactic:
simp only [μ.mass_nonzero_iff.mpr nonzero, Algebra.id.smul_eq_mul, inv_mul_cancel₀, Ne,
  not_false_iff, one_smul]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ

Tactic:
nth_rw 3 [μ.self_eq_mass_smul_normalize]

Result:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = μ.mass⁻¹ • μ.mass • μ.normalize.toFiniteMeasure

Tactic:
rw [← smul_assoc]

Result:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ μ.normalize.toFiniteMeasure = (μ.mass⁻¹ • μ.mass) • μ.normalize.toFiniteMeasure
-- Mathlib/Data/List/Iterate.lean
theorem getElem_iterate (f : α → α) (a : α) (n : ℕ) (i : Nat) (h : i < (iterate f a n).length) :
    (iterate f a n)[i] = f^[i] a :=
  getElem_eq_iff.2 <| getElem?_iterate _ _ _ _ <| by rwa [length_iterate] at h

Proof state:
α : Type u_1
f : α → α
a : α
n i : ℕ
h : i < (iterate f a n).length
⊢ i < n

Tactic:
rwa [length_iterate] at h

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atBot_mul_const' (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atBot

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atBot

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢

Result:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x * r) l atTop

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x * r) l atTop

Tactic:
exact hf.atTop_mul_const' hr

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) :
    ⟪y, x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(-π / 2)
⊢ inner y x = 0

Tactic:
rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_of_im_neg {z : ℂ} (hz : z.im < 0) : arg z = -Real.arccos (z.re / ‖z‖)

Proof state:
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π

Tactic:
exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le]

Result:
no goals

Proof state:
z : ℂ
hz : z.im < 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)

Tactic:
have h₀ : z ≠ 0 := mt (congr_arg im) hz.ne

Result:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)

Proof state:
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ z.arg = -Real.arccos (z.re / ‖z‖)

Tactic:
rw [← cos_arg h₀, ← Real.cos_neg, Real.arccos_cos, neg_neg]

Result:
case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma nat_lt_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) < n ↔ m < n

Proof state:
m : ℕ
n : ℕ∞
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem exists_sq_eq_neg_one_iff : IsSquare (-1 : ZMod p) ↔ p % 4 ≠ 3

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsSquare (-1) ↔ p % 4 ≠ 3

Tactic:
rw [FiniteField.isSquare_neg_one_iff, card p]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic {k K : Type*} [Field k] [Field K]
    [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsAlgebraic k L] :
    L = ⊥ := bot_unique fun x hx ↦ by
  obtain ⟨y, hy⟩ := IsAlgClosed.algebraMap_surjective_of_isIntegral (k := k) (⟨x, hx⟩ : L)
  exact ⟨y, congr_arg (algebraMap L K) hy⟩

Proof state:
case intro
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : IsAlgClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsAlgebraic k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Tactic:
exact ⟨y, congr_arg (algebraMap L K) hy⟩

Result:
no goals

Proof state:
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : IsAlgClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsAlgebraic k ↥L
x : K
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsAlgClosed.algebraMap_surjective_of_isIntegral (k := k) (⟨x, hx⟩ : L)

Result:
case intro
k : Type u_1
K : Type u_2
inst✝⁴ : Field k
inst✝³ : Field K
inst✝² : IsAlgClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsAlgebraic k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥
-- Mathlib/Algebra/FreeAlgebra.lean
theorem ι_comp_lift (f : X → A) : (lift R f : FreeAlgebra R X → A) ∘ ι R = f

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ⇑((lift R) f) ∘ ι R = f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (⇑((lift R) f) ∘ ι R) x✝ = f x✝

Proof state:
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (⇑((lift R) f) ∘ ι R) x✝ = f x✝

Tactic:
rw [Function.comp_apply, ι_def, lift]

Result:
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ({ toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/RelabelFin.lean
theorem of_maxLiteral_eq_some (f : CNF Nat) (h : f.maxLiteral = some maxLit) :
    ∀ lit, Mem lit f → lit ≤ maxLit

Proof state:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
⊢ lit ≤ maxLit

Tactic:
have h2 := Clause.of_maxLiteral_eq_some clause hlocal lit hclause2

Result:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
h2 : lit ≤ localMax
⊢ lit ≤ maxLit

Proof state:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
h2 : lit ≤ localMax
⊢ lit ≤ maxLit

Tactic:
omega

Result:
no goals

Proof state:
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
⊢ ∀ (lit : Nat), Mem lit f → lit ≤ maxLit

Tactic:
intro lit hlit

Result:
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
hlit : Mem lit f
⊢ lit ≤ maxLit

Proof state:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
⊢ lit ≤ maxLit

Tactic:
have h1 := of_maxLiteral_eq_some' f h clause hclause1 hlocal

Result:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
h1 : localMax ≤ maxLit
⊢ lit ≤ maxLit

Proof state:
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
hlit : Mem lit f
⊢ lit ≤ maxLit

Tactic:
dsimp [Mem] at hlit

Result:
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
hlit : ∃ c, c ∈ f ∧ Clause.Mem lit c
⊢ lit ≤ maxLit

Proof state:
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
hlit : ∃ c, c ∈ f ∧ Clause.Mem lit c
⊢ lit ≤ maxLit

Tactic:
rcases hlit with ⟨clause, ⟨hclause1, hclause2⟩⟩

Result:
case intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
⊢ lit ≤ maxLit

Proof state:
case intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
⊢ lit ≤ maxLit

Tactic:
rcases Clause.maxLiteral_eq_some_of_mem clause hclause2 with ⟨localMax, hlocal⟩

Result:
case intro.intro.intro
maxLit : Nat
f : CNF Nat
h : f.maxLiteral = some maxLit
lit : Nat
clause : Clause Nat
hclause1 : clause ∈ f
hclause2 : Clause.Mem lit clause
localMax : Nat
hlocal : clause.maxLiteral = some localMax
⊢ lit ≤ maxLit
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_eq_iff {m : M} {s : S} {m' : M'} : mk' f m s = m' ↔ f m = s • m'

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
⊢ mk' f m s = m' ↔ f m = s • m'

Tactic:
rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive] lemma inv_div_comm (a b : α) : a⁻¹ / b = b⁻¹ / a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b = b⁻¹ / a

Tactic:
simp

Result:
no goals