harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Basic.lean
lemma natCast_le_natCast (han : a ≤ n) (hbn : b ≤ n) : (a : Fin (n + 1)) ≤ b ↔ a ≤ b

Proof state:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
rw [← Nat.lt_succ_iff] at han hbn

Result:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a ≤ ↑b ↔ a ≤ b

Proof state:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem exists_eq_inl_mul : ∃ n : N, σ g = S.inl n * σ' g

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = σ g * (σ' g)⁻¹
⊢ σ g = S.inl n * σ' g

Tactic:
rw [hn, inv_mul_cancel_right]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ ∃ n, σ g = S.inl n * σ' g

Tactic:
obtain ⟨n, hn⟩ := mul_inv_mem_range_inl σ σ' g

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = σ g * (σ' g)⁻¹
⊢ ∃ n, σ g = S.inl n * σ' g

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = σ g * (σ' g)⁻¹
⊢ ∃ n, σ g = S.inl n * σ' g

Tactic:
exact ⟨n, by rw [hn, inv_mul_cancel_right]⟩

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem Ioc_subset_closure_interior (a b : α) : Ioc a b ⊆ closure (interior (Ioc a b))

Proof state:
case inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure (interior (Ioc a b))

Tactic:
calc
  Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
  _ = closure (Ioo a b) := (closure_Ioo h).symm
  _ ⊆ closure (interior (Ioc a b)) :=
    closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
⊢ Ioc a a ⊆ closure (interior (Ioc a a))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ Ioc a b ⊆ closure (interior (Ioc a b))

Tactic:
rcases eq_or_ne a b with (rfl | h)

Result:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
⊢ Ioc a a ⊆ closure (interior (Ioc a a))

case inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure (interior (Ioc a b))
-- Mathlib/RingTheory/TensorProduct/Basic.lean
/-- If `M` is a `B`-module that is also an `A`-module, the canonical map
`M →ₗ[A] B ⊗[A] M` is injective. -/
lemma mk_one_injective_of_isScalarTower (M : Type*) [AddCommGroup M]
    [Module R M] [Module S M] [IsScalarTower R S M] :
    Function.Injective (TensorProduct.mk R S M 1)

Proof state:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.RightInverse ⇑((TensorProduct.mk R S M) 1) ⇑(LinearMap.liftBaseChange S LinearMap.id)

Tactic:
intro m

Result:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
m : M
⊢ (LinearMap.liftBaseChange S LinearMap.id) (((TensorProduct.mk R S M) 1) m) = m

Proof state:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
m : M
⊢ (LinearMap.liftBaseChange S LinearMap.id) (((TensorProduct.mk R S M) 1) m) = m

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.Injective ⇑((TensorProduct.mk R S M) 1)

Tactic:
apply Function.RightInverse.injective (g := LinearMap.liftBaseChange S LinearMap.id)

Result:
R : Type uR
S : Type uS
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ Function.RightInverse ⇑((TensorProduct.mk R S M) 1) ⇑(LinearMap.liftBaseChange S LinearMap.id)
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- We relate a finite product over primes in `s` to an infinite sum over `s`-factored numbers. -/
lemma summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m)
        (∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n))

Proof state:
case insert
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m)
      (∏ p ∈ if Nat.Prime p then insert p (filter (fun p => Nat.Prime p) s) else filter (fun p => Nat.Prime p) s,
        ∑' (n : ℕ), f (p ^ n))

Tactic:
split_ifs with hpp

Result:
case pos
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m) (∏ x ∈ insert p (filter (fun p => Nat.Prime p) s), ∑' (n : ℕ), f (x ^ n))

case neg
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n))
hpp : ¬Nat.Prime p
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ x ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (x ^ n))
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_of_fintype [Decidable s.Nontrivial] [DecidableEq α] [Fintype s] : s.infsep =
    if hs : s.Nontrivial then s.offDiag.toFinset.inf' (by simpa) (uncurry dist) else 0

Proof state:
case neg
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
rw [not_nontrivial_iff] at hs

Result:
case neg
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Subsingleton
⊢ s.infsep = 0

Proof state:
case pos
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
case pos
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs

Result:
case pos
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

case neg
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝³ : PseudoMetricSpace α
s : Set α
inst✝² : Decidable s.Nontrivial
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem eq_adjoint_iff (A : E →L[𝕜] F) (B : F →L[𝕜] E) : A = B† ↔ ∀ x y, ⟪A x, y⟫ = ⟪x, B y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪(adjoint B) x, y⟫_𝕜

Tactic:
simp only [adjoint_inner_left, h x y]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
⊢ A x = (adjoint B) x

Tactic:
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
⊢ A = adjoint B

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
⊢ A x = (adjoint B) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
⊢ A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
⊢ A = adjoint B
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma _root_.MeasureTheory.OuterMeasure.toMeasure_eq_zero {ms : MeasurableSpace α}
    {μ : OuterMeasure α} (h : ms ≤ μ.caratheodory) : μ.toMeasure h = 0 ↔ μ = 0 where
  mp hμ

Proof state:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
s : Set α
⊢ μ s = 0 s

Tactic:
exact le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)

Result:
no goals

Proof state:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
⊢ μ = 0 → μ.toMeasure h = 0

Tactic:
rintro rfl

Result:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0

Proof state:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
⊢ μ = 0

Tactic:
ext s

Result:
case h
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
s : Set α
⊢ μ s = 0 s
-- Mathlib/Data/Finsupp/Fin.lean
theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ cons 0 0 = 0

Tactic:
ext a

Result:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
⊢ (cons 0 0) a = 0 a

Proof state:
case h
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
⊢ (cons 0 0) a = 0 a

Tactic:
by_cases c : a = 0

Result:
case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : a = 0
⊢ (cons 0 0) a = 0 a

case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : ¬a = 0
⊢ (cons 0 0) a = 0 a

Proof state:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : ¬a = 0
⊢ (cons 0 0) a = 0 a

Tactic:
rw [← Fin.succ_pred a c, cons_succ]

Result:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : ¬a = 0
⊢ 0 (a.pred c) = 0 (a.pred c).succ

Proof state:
case pos
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : a = 0
⊢ (cons 0 0) a = 0 a

Tactic:
simp [c]

Result:
no goals

Proof state:
case neg
n : ℕ
M : Type u_1
inst✝ : Zero M
a : Fin (n + 1)
c : ¬a = 0
⊢ 0 (a.pred c) = 0 (a.pred c).succ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem disjoint_toFinset [Fintype s] [Fintype t] :
    Disjoint s.toFinset t.toFinset ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ Disjoint s.toFinset t.toFinset ↔ Disjoint s t

Tactic:
simp only [← disjoint_coe, coe_toFinset]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_eq_gcd_ab : ∀ x y : ℤ, (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y
  | (m : ℕ), (n : ℕ) => Nat.gcd_eq_gcd_ab _ _
  | (m : ℕ), -[n+1] =>
    show (_ : ℤ) = _ + -(n + 1) * -_ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
  | -[m+1], (n : ℕ) =>
    show (_ : ℤ) = -(m + 1) * -_ + _ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
  | -[m+1], -[n+1] =>
    show (_ : ℤ) = -(m + 1) * -_ + -(n + 1) * -_ by
      rw [Int.neg_mul_neg, Int.neg_mul_neg]
      apply Nat.gcd_eq_gcd_ab

Proof state:
m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = -(↑m + 1) * -m.succ.gcdA -[n+1].natAbs + -(↑n + 1) * - -[m+1].natAbs.gcdB n.succ

Tactic:
rw [Int.neg_mul_neg, Int.neg_mul_neg]

Result:
m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ

Proof state:
m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Tactic:
apply Nat.gcd_eq_gcd_ab

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = -(↑m + 1) * -m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Tactic:
rw [Int.neg_mul_neg]

Result:
m n : ℕ
⊢ ↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n

Proof state:
m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + -(↑n + 1) * -(↑m).natAbs.gcdB n.succ

Tactic:
rw [Int.neg_mul_neg]

Result:
m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ

Proof state:
m n : ℕ
⊢ ↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ

Tactic:
apply Nat.gcd_eq_gcd_ab

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem le_log_of_pow_le {b x y : ℕ} (hb : 1 < b) (h : b ^ x ≤ y) : x ≤ log b y

Proof state:
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0

Tactic:
exacts [(pow_le_iff_le_log hb hy).1 h, (h.not_lt (Nat.pow_pos (Nat.zero_lt_one.trans hb))).elim]

Result:
no goals

Proof state:
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
⊢ x ≤ log b y

Tactic:
rcases ne_or_eq y 0 with (hy | rfl)

Result:
case inl
b x y : ℕ
hb : 1 < b
h : b ^ x ≤ y
hy : y ≠ 0
⊢ x ≤ log b y

case inr
b x : ℕ
hb : 1 < b
h : b ^ x ≤ 0
⊢ x ≤ log b 0
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem of_d (j : α) : (of X d sq).d j (j + 1) = d j

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ (of X d sq).d j (j + 1) = d j

Tactic:
dsimp [of]

Result:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j

Proof state:
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j

Tactic:
rw [if_pos rfl, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma PosSMulReflectLT.lift [PosSMulReflectLT α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b) : PosSMulReflectLT α β where
  elim a ha b₁ b₂ h

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : α → β → True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : α → β → True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂

Tactic:
exact lt_of_smul_lt_smul_left h ha

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Multilinear/Bounded.lean
theorem image_multilinear [ContinuousSMul 𝕜 F] {s : Set (∀ i, E i)} (hs : IsVonNBounded 𝕜 s)
    (f : ContinuousMultilinearMap 𝕜 E F) : IsVonNBounded 𝕜 (f '' s)

Proof state:
case inl
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : IsEmpty ι
⊢ IsVonNBounded 𝕜 (⇑f '' s)

Tactic:
exact (isBounded_iff_isVonNBounded _).1 <|
  @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
⊢ IsVonNBounded 𝕜 (⇑f '' s)

Tactic:
cases isEmpty_or_nonempty ι with
| inl h =>
  exact (isBounded_iff_isVonNBounded _).1 <|
    @Set.Finite.isBounded _ (vonNBornology 𝕜 F) _ (s.toFinite.image _)
| inr h => exact hs.image_multilinear' f

Result:
no goals

Proof state:
case inr
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : ContinuousSMul 𝕜 F
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
h : Nonempty ι
⊢ IsVonNBounded 𝕜 (⇑f '' s)

Tactic:
exact hs.image_multilinear' f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_toExpr_go (ctx : Context) (e : Expr) (p : Poly) : (toExpr.go e p).denote ctx = e.denote ctx + p.denote ctx

Proof state:
case nil
ctx : Context
e : Expr
⊢ Expr.denote ctx (toExpr.go e []) = Expr.denote ctx e + denote ctx []

Tactic:
simp [toExpr.go, Poly.denote]

Result:
no goals

Proof state:
case cons
ctx : Context
kv : Nat × Var
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
⊢ Expr.denote ctx (toExpr.go e (kv :: p)) = Expr.denote ctx e + denote ctx (kv :: p)

Tactic:
cases kv

Result:
case cons.mk
ctx : Context
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
fst✝ : Nat
snd✝ : Var
⊢ Expr.denote ctx (toExpr.go e ((fst✝, snd✝) :: p)) = Expr.denote ctx e + denote ctx ((fst✝, snd✝) :: p)

Proof state:
case cons.mk
ctx : Context
p : List (Nat × Var)
ih : ∀ (e : Expr), Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p
e : Expr
fst✝ : Nat
snd✝ : Var
⊢ Expr.denote ctx (toExpr.go e ((fst✝, snd✝) :: p)) = Expr.denote ctx e + denote ctx ((fst✝, snd✝) :: p)

Tactic:
simp [toExpr.go, ih, Expr.denote, Poly.denote]

Result:
no goals

Proof state:
ctx : Context
e : Expr
p : Poly
⊢ Expr.denote ctx (toExpr.go e p) = Expr.denote ctx e + denote ctx p

Tactic:
induction p generalizing e with
| nil => simp [toExpr.go, Poly.denote]
| cons kv p ih => cases kv; simp [toExpr.go, ih, Expr.denote, Poly.denote]

Result:
no goals