harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.leadingCoeff_mul_eq_right
    (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hp : p.Monic D) :
    (p * q).leadingCoeff D = q.leadingCoeff D

Proof state:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Tactic:
rw [leadingCoeff, hp.supDegree_mul_of_ne_zero_right hD hadd hq,
  apply_supDegree_add_supDegree hD hadd, hp, one_mul]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Result:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
⊢ leadingCoeff D (p * 0) = leadingCoeff D 0

case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Proof state:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
⊢ leadingCoeff D (p * 0) = leadingCoeff D 0

Tactic:
rw [mul_zero]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem FermatLastTheorem.of_odd_primes
    (hprimes : ∀ p : ℕ, Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheorem

Proof state:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
⊢ FermatLastTheoremFor n

Tactic:
obtain hdvd|⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h <;>
  apply FermatLastTheoremWith.mono hdvd

Result:
case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

case inr.intro.intro.intro
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremWith ℕ p

Proof state:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
⊢ FermatLastTheorem

Tactic:
intro n h

Result:
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
⊢ FermatLastTheoremFor n

Proof state:
case inr.intro.intro.intro
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremWith ℕ p

Tactic:
exact hprimes p hpprime hpodd

Result:
no goals

Proof state:
case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4

Tactic:
exact fermatLastTheoremFour

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem le_cons_of_not_mem (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t

Proof state:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))

Result:
no goals

Proof state:
α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂

Tactic:
rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩

Result:
case intro.intro
α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)

Proof state:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by
  exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))

Result:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'

Proof state:
case intro.intro
α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ : List α
m₁ : ¬a ∈ ↑l₁
r₁ r₂ : List α
s : l₁ <+ r₁ ++ a :: r₂
m₂ : a ∈ ↑(r₁ ++ a :: r₂)
⊢ a ::ₘ ↑l₁ ≤ ↑(r₁ ++ a :: r₂)

Tactic:
exact
  perm_middle.subperm_left.2
    ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

Result:
no goals

Proof state:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩

Result:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t → s ≤ t

Proof state:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'

Tactic:
refine leInductionOn h ?_

Result:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂

Proof state:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'

Tactic:
introv h

Result:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'

Proof state:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂

Tactic:
introv s m₁ m₂

Result:
α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂

Proof state:
α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'

Tactic:
revert m

Result:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem norm_normedMk (S : AddSubgroup M) (h : (S.topologicalClosure : Set M) ≠ univ) :
    ‖S.normedMk‖ = 1

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ∃ x, 0 < ‖↑x‖

Tactic:
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : x ∈ (↑S.topologicalClosure)ᶜ
⊢ 0 < ‖↑x‖

Proof state:
case intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
refine (le_mul_iff_one_le_left hx).1 ?_

Result:
case intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖S.normedMk‖ * ‖↑x‖

Proof state:
case intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖S.normedMk‖ * ‖↑x‖

Tactic:
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : x ∈ (↑S.topologicalClosure)ᶜ
⊢ 0 < ‖↑x‖

Tactic:
exact (norm_nonneg _).lt_of_ne' <| mt (quotient_norm_eq_zero_iff S x).1 hx

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ‖S.normedMk‖ = 1

Tactic:
refine le_antisymm (norm_normedMk_le S) ?_

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ 1 ≤ ‖S.normedMk‖

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ 1 ≤ ‖S.normedMk‖

Tactic:
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖ := by
  refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
  exact (norm_nonneg _).lt_of_ne' <| mt (quotient_norm_eq_zero_iff S x).1 hx

Result:
case intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖S.normedMk‖
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem triple_product_eq_det (u v w : Fin 3 → R) : u ⬝ᵥ v ×₃ w = Matrix.det ![u, v, w]

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    ![u, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 -
            ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 +
          ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 +
        ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 -
      ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0

Tactic:
norm_num

Result:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    u 0 * v 1 * w 2 - u 0 * v 2 * w 1 - u 1 * v 0 * w 2 + u 1 * v 2 * w 0 + u 2 * v 0 * w 1 - u 2 * v 1 * w 0

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = det ![u, v, w]

Tactic:
rw [vec3_dotProduct, cross_apply, det_fin_three]

Result:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    ![u, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 -
            ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 +
          ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 +
        ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 -
      ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0

Proof state:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * (v 1 * w 2 - v 2 * w 1) + u 1 * (v 2 * w 0 - v 0 * w 2) + u 2 * (v 0 * w 1 - v 1 * w 0) =
    u 0 * v 1 * w 2 - u 0 * v 2 * w 1 - u 1 * v 0 * w 2 + u 1 * v 2 * w 0 + u 2 * v 0 * w 1 - u 2 * v 1 * w 0

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem truncate_zero_one {a b : X} (γ : Path a b) :
    γ.truncate 0 1 = γ.cast (by simp [zero_le_one, extend_zero]) (by simp)

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
this : ↑x ∈ Icc 0 1
⊢ (γ.truncate 0 1) x = γ x

Tactic:
rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']

Result:
no goals

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = (γ.cast ⋯ ⋯) x

Tactic:
rw [cast_coe]

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = γ x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend 1 = b

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (0 ⊓ 1) = a

Tactic:
simp [zero_le_one, extend_zero]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 1 = γ.cast ⋯ ⋯

Tactic:
ext x

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = (γ.cast ⋯ ⋯) x

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = γ x

Tactic:
have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
this : ↑x ∈ Icc 0 1
⊢ (γ.truncate 0 1) x = γ x
-- Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean
private lemma exists_variableChange_of_char_two_of_j_ne_zero
    [E.IsCharTwoJNeZeroNF] [E'.IsCharTwoJNeZeroNF] (heq : E.a₆ = E'.a₆) :
    ∃ C : VariableChange F, E.variableChange C = E'

Proof state:
case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ (E.variableChange { u := 1, r := 0, s := s, t := 0 }).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]

Result:
case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (0 + 0 * E.a₁ + 2 * 0) = 0

Proof state:
case h.a₂
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 2 * (E.a₂ - s * 1 + 3 * 0 - s ^ 2) = E'.a₂

Tactic:
linear_combination -hs + E.a₂ * CharP.cast_eq_zero F 2

Result:
no goals

Proof state:
case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (0 + 0 * E.a₁ + 2 * 0) = 0

Tactic:
ring1

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem strict_initial {I : C} (t : IsInitial I) (f : A ⟶ I) : IsIso f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono (ChosenFiniteProducts.lift (𝟙 A) f ≫ (zeroMul t).hom)

Tactic:
exact mono_comp _ _

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f

Tactic:
haveI : IsSplitEpi f := IsSplitEpi.mk' ⟨t.to _, t.hom_ext _ _⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this✝ : Mono f
this : IsSplitEpi f
⊢ IsIso f

Tactic:
apply isIso_of_mono_of_isSplitEpi

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono f

Tactic:
rw [← ChosenFiniteProducts.lift_snd (𝟙 A) f, ← zeroMul_hom t]

Result:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ Mono (ChosenFiniteProducts.lift (𝟙 A) f ≫ (zeroMul t).hom)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
⊢ IsIso f

Tactic:
haveI : Mono f := by
  rw [← ChosenFiniteProducts.lift_snd (𝟙 A) f, ← zeroMul_hom t]
  exact mono_comp _ _

Result:
C : Type u
inst✝² : Category.{v, u} C
A : C
inst✝¹ : ChosenFiniteProducts C
inst✝ : Exponentiable A
I : C
t : IsInitial I
f : A ⟶ I
this : Mono f
⊢ IsIso f
-- Mathlib/Data/PNat/Factors.lean
theorem prod_sup (u v : PrimeMultiset) : (u ⊔ v).prod = PNat.lcm u.prod v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = n.lcm m

Tactic:
have : u = n.factorMultiset := u.factorMultiset_prod.symm

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊔ v).prod = n.lcm m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
let m := v.prod

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m

Tactic:
rw [← PNat.factorMultiset_lcm n m, PNat.prod_factorMultiset]

Result:
no goals

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m

Tactic:
have : v = m.factorMultiset := v.factorMultiset_prod.symm

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m

Tactic:
rw [this]

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this✝ : u = n.factorMultiset
this : v = m.factorMultiset
⊢ (n.factorMultiset ⊔ m.factorMultiset).prod = n.lcm m

Proof state:
u v : PrimeMultiset
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
let n := u.prod

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (u ⊔ v).prod = n.lcm m

Tactic:
rw [this]

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
this : u = n.factorMultiset
⊢ (n.factorMultiset ⊔ v).prod = n.lcm m

Proof state:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = u.prod.lcm v.prod

Tactic:
change (u ⊔ v).prod = PNat.lcm n m

Result:
u v : PrimeMultiset
n : ℕ+ := u.prod
m : ℕ+ := v.prod
⊢ (u ⊔ v).prod = n.lcm m
-- Mathlib/Data/Int/Init.lean
lemma sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Proof state:
⊢ 1 ≠ -1

Tactic:
decide

Result:
no goals

Proof state:
⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
have : (1 : ℤ) ≠ -1 := by decide

Result:
this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Proof state:
this : 1 ≠ -1
⊢ ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign

Tactic:
rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm, Int.negSucc_add_negSucc]

Result:
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ (↑m + 1 + (↑n + 1)).sign = 1

Proof state:
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1 + (↑n + 1)

Tactic:
omega

Result:
no goals

Proof state:
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ (↑m + 1 + (↑n + 1)).sign = 1

Tactic:
rw [Int.sign_eq_one_iff_pos]

Result:
case ofNat.succ.ofNat.succ
this : 1 ≠ -1
m n : ℕ
⊢ 0 < ↑m + 1 + (↑n + 1)
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive] lemma inv_smul_eq_iff : g⁻¹ • a = b ↔ a = g • b :=
  ⟨fun h ↦ by rw [← h, smul_inv_smul], fun h ↦ by rw [h, inv_smul_smul]⟩

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • b

Tactic:
rw [← h, smul_inv_smul]

Result:
no goals

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • a = b

Tactic:
rw [h, inv_smul_smul]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the L-series of the constant sequence `1` on its domain of convergence `re s > 1`. -/
lemma LSeries_vonMangoldt_eq {s : ℂ} (hs : 1 < s.re) : L ↗Λ s = - deriv (L 1) s / L 1 s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(Λ n)) s = -deriv (L 1) s / L 1 s

Tactic:
refine (LSeries_congr s fun {n} _ ↦ ?_).trans <|
  LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs

Result:
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ : n ≠ 0
⊢ ↑(Λ n) = ((fun n => 1 ↑n) * fun n => ↑(Λ n)) n

Proof state:
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ : n ≠ 0
⊢ ↑(Λ n) = ((fun n => 1 ↑n) * fun n => ↑(Λ n)) n

Tactic:
simp [Subsingleton.eq_one (n : ZMod 1)]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma sup_iInf₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊔ ⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, a ⊔ f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
a : α
⊢ a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j

Tactic:
simp only [sup_iInf_eq]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_inv_iff {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} :
    Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹) ↔ Tendsto m f (𝓝 a) :=
  ⟨fun h => by simpa only [inv_inv] using Tendsto.inv h, Tendsto.inv⟩

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a : ℝ≥0∞
h : Tendsto (fun x => (m x)⁻¹) f (𝓝 a⁻¹)
⊢ Tendsto m f (𝓝 a)

Tactic:
simpa only [inv_inv] using Tendsto.inv h

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem differentiableAt_cuspFunction [NeZero n] [ModularFormClass F Γ(n) k]
    {q : ℂ} (hq : ‖q‖ < 1) :
    DifferentiableAt ℂ (cuspFunction n f) q

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
npos : 0 < ↑n
⊢ DifferentiableAt ℂ (cuspFunction n f) q

Tactic:
rcases eq_or_ne q 0 with rfl | hq'

Result:
case inl
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
npos : 0 < ↑n
hq : ‖0‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction n f) 0

case inr
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
npos : 0 < ↑n
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction n f) q

Proof state:
case inr
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
npos : 0 < ↑n
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction n f) q

Tactic:
exact Periodic.qParam_right_inv npos.ne' hq' ▸
  (periodic_comp_ofComplex n f).differentiableAt_cuspFunction npos.ne'
    <| differentiableAt_comp_ofComplex _ <| Periodic.im_invQParam_pos_of_norm_lt_one npos hq hq'

Result:
no goals

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction n f) q

Tactic:
have npos : 0 < (n : ℝ) := mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _))

Result:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
q : ℂ
hq : ‖q‖ < 1
npos : 0 < ↑n
⊢ DifferentiableAt ℂ (cuspFunction n f) q

Proof state:
case inl
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
npos : 0 < ↑n
hq : ‖0‖ < 1
⊢ DifferentiableAt ℂ (cuspFunction n f) 0

Tactic:
exact (periodic_comp_ofComplex n f).differentiableAt_cuspFunction_zero npos
  (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
    (fun _ ↦ differentiableAt_comp_ofComplex f))
  (bounded_at_infty_comp_ofComplex f)

Result:
no goals