harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem dist_mulExpNegMulSq_le_dist (hε : 0 < ε) {x y : ℝ} :
    dist (mulExpNegMulSq ε x) (mulExpNegMulSq ε y) ≤ dist x y

Proof state:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ ↑1 * edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
rwa [ENNReal.coe_one, one_mul, ← (toReal_le_toReal (edist_ne_top _ _) (edist_ne_top _ _))] at h

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
have h := lipschitzWith_one_mulExpNegMulSq hε x y

Result:
ε : ℝ
hε : 0 < ε
x y : ℝ
h : edist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ ↑1 * edist x y
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp] lemma semilength_nest : p.nest.semilength = p.semilength + 1

Proof state:
p : DyckWord
⊢ p.nest.semilength = p.semilength + 1

Tactic:
simp [semilength, nest]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_none (f : α → Part β) : none.bind f = none :=
  eq_none_iff.2 fun a => by simp

Proof state:
α : Type u_1
β : Type u_2
f : α → Part β
a : β
⊢ a ∉ none.bind f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem surjective_iff_surjective_of_iUnion_eq_univ :
    Surjective f ↔ ∀ i, Surjective ((U i).restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ ∃ a, f a = x

Tactic:
obtain ⟨i, hi⟩ :=
  Set.mem_iUnion.mp
    (show x ∈ Set.iUnion U by rw [hU]; trivial)

Result:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x

Tactic:
exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)

Tactic:
refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ ∃ a, f a = x

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ

Tactic:
trivial

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ iUnion U

Tactic:
rw [hU]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_xor : ∀ (x y : Bool), (!x ^^ y) = !(x ^^ y)

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

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem equivNum_apply [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P}
    (h_nz : (I.den : R) ≠ 0) (x : I) :
    algebraMap R P (equivNum h_nz x) = I.den • x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : Nontrivial P
inst✝ : NoZeroSMulDivisors R P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (Algebra.linearMap R P) ↑((equivNum h_nz) x) = I.den • ↑x

Tactic:
rw [equivNum, LinearEquiv.trans_apply, LinearEquiv.ofBijective_apply, LinearMap.restrict_apply,
  Submodule.map_equivMapOfInjective_symm_apply, Subtype.coe_mk,
  DistribMulAction.toLinearMap_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : Nontrivial P
inst✝ : NoZeroSMulDivisors R P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (algebraMap R P) ↑((equivNum h_nz) x) = I.den • ↑x

Tactic:
change Algebra.linearMap R P _ = _

Result:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
inst✝¹ : Nontrivial P
inst✝ : NoZeroSMulDivisors R P
I : FractionalIdeal S P
h_nz : ↑I.den ≠ 0
x : ↥I
⊢ (Algebra.linearMap R P) ↑((equivNum h_nz) x) = I.den • ↑x
-- Mathlib/ModelTheory/Definability.lean
theorem definable_finset_sup {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i))
    (s : Finset ι) : A.Definable L (s.sup f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L (f i ⊔ s.sup f)

Tactic:
exact (hf i).union h

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
refine Finset.induction definable_empty (fun i s _ h => ?_) s

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L ((insert i s).sup f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L ((insert i s).sup f)

Tactic:
rw [Finset.sup_insert]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L (f i ⊔ s.sup f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
classical
  refine Finset.induction definable_empty (fun i s _ h => ?_) s
  rw [Finset.sup_insert]
  exact (hf i).union h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_eq_arccos {x : ℝ} (h : 0 ≤ x) : arcsin x = arccos (√(1 - x ^ 2))

Proof state:
x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos √(1 - x ^ 2)

Tactic:
rw [eq_comm, ← cos_arcsin]

Result:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x

Proof state:
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x

Tactic:
exact
  arccos_cos (arcsin_nonneg.2 h)
    ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))

Result:
no goals
-- Mathlib/Computability/Language.lean
@[simp]
lemma reverse_mul (l m : Language α) : (l * m).reverse = m.reverse * l.reverse

Proof state:
α : Type u_1
l m : Language α
⊢ (l * m).reverse = m.reverse * l.reverse

Tactic:
simp only [mul_def, reverse_eq_image, image2_image_left, image2_image_right, image_image2,
  List.reverse_append]

Result:
α : Type u_1
l m : Language α
⊢ image2 (fun a b => b.reverse ++ a.reverse) l m = image2 (fun a b => a.reverse ++ b.reverse) m l

Proof state:
α : Type u_1
l m : Language α
⊢ image2 (fun a b => b.reverse ++ a.reverse) l m = image2 (fun a b => a.reverse ++ b.reverse) m l

Tactic:
apply image2_swap

Result:
no goals
-- Mathlib/Data/Finsupp/Indicator.lean
theorem indicator_injective : Injective fun f : ∀ i ∈ s, α => indicator s f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
⊢ a = b

Tactic:
ext i hi

Result:
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ a i hi = b i hi

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
⊢ Injective fun f => indicator s f

Tactic:
intro a b h

Result:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
⊢ a = b

Proof state:
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ (indicator s a) i = (indicator s b) i

Tactic:
exact DFunLike.congr_fun h i

Result:
no goals

Proof state:
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ a i hi = b i hi

Tactic:
rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]

Result:
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ (indicator s a) i = (indicator s b) i
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem iInf_lcs_le_of_isNilpotent_quot (h : IsNilpotent L (M ⧸ N)) :
    ⨅ k, lowerCentralSeries R L M k ≤ N

Proof state:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : IsNilpotent L (M ⧸ N)
k : ℕ
hk : lowerCentralSeries R L M k ≤ N
⊢ ⨅ k, lowerCentralSeries R L M k ≤ N

Tactic:
exact iInf_le_of_le k hk

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : IsNilpotent L (M ⧸ N)
⊢ ⨅ k, lowerCentralSeries R L M k ≤ N

Tactic:
obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h

Result:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : IsNilpotent L (M ⧸ N)
k : ℕ
hk : lowerCentralSeries R L M k ≤ N
⊢ ⨅ k, lowerCentralSeries R L M k ≤ N
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_nat_ge [OrderedSemiring α] [Archimedean α] (x : α) : ∃ n : ℕ, x ≤ n

Proof state:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
⊢ ∃ n, x ≤ ↑n

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
a✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n

Proof state:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
a✝ : Nontrivial α
n : ℕ
h : x ≤ n • 1
⊢ x ≤ ↑n

Tactic:
rwa [← nsmul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
a✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n

Tactic:
exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_ofNat (n : ℕ) : preNormEDS b c d n = preNormEDS' b c d n

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
hn : n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

case neg
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
hn : ¬n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Proof state:
case pos
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
hn : n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Tactic:
rw [hn, preNormEDS, Nat.cast_zero, Int.sign_zero, Int.cast_zero, zero_mul, preNormEDS'_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
b c d : R
n : ℕ
hn : ¬n = 0
⊢ preNormEDS b c d ↑n = preNormEDS' b c d n

Tactic:
rw [preNormEDS, Int.sign_natCast_of_ne_zero hn, Int.cast_one, one_mul, Int.natAbs_cast]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem apply_norm_sq_eq_inner_adjoint_right (A : E →L[𝕜] F) (x : E) :
    ‖A x‖ ^ 2 = re ⟪x, (A† ∘L A) 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
x : E
⊢ ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜

Tactic:
rw [← adjoint_inner_right]

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
x : E
⊢ ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪x, (adjoint A) (A 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
x : E
⊢ ‖A x‖ ^ 2 = re ⟪x, ((adjoint A).comp A) x⟫_𝕜

Tactic:
have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl

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
x : E
h : ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪x, ((adjoint A).comp A) 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
x : E
⊢ ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪x, (adjoint A) (A x)⟫_𝕜

Tactic:
rfl

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
x : E
h : ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜
⊢ ‖A x‖ ^ 2 = re ⟪x, ((adjoint A).comp A) x⟫_𝕜

Tactic:
rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Composition.lean
lemma of_comp (W₃ : MorphismProperty C₁)
    [L₁.IsLocalization W₁] [(L₁ ⋙ L₂).IsLocalization W₃]
    (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ = W₃.map L₁) :
    L₂.IsLocalization W₂

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
X Y : C₁
f : X ⟶ Y
hf : W₃ f
⊢ W₂ (L₁.map f)

Tactic:
simpa only [hW₂₃] using W₃.map_mem_map _ _ hf

Result:
no goals

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ W₂ ≤ W₃.map L₁

Tactic:
rw [hW₂₃]

Result:
no goals

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ L₂.IsLocalization W₂

Tactic:
have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
  comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _
    (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
    (by rw [hW₂₃])

Result:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
this : (L₁ ⋙ W₂.Q).IsLocalization W₃
⊢ L₂.IsLocalization W₂

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
inst✝ : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
this : (L₁ ⋙ W₂.Q).IsLocalization W₃
⊢ L₂.IsLocalization W₂

Tactic:
exact IsLocalization.of_equivalence_target W₂.Q W₂ L₂
  (Localization.uniq (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃)
  (liftNatIso L₁ W₁ _ _ _ _
    ((Functor.associator _ _ _).symm ≪≫
      Localization.compUniqFunctor (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃))

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma ext {F G : ComposableArrows C n} (h : ∀ i, F.obj i = G.obj i)
    (w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) =
      eqToHom (h _) ≫ G.map' i (i + 1) ≫ eqToHom (h _).symm) : F = G :=
  Functor.ext_of_iso
    (isoMk (fun i => eqToIso (h i)) (fun i hi => by simp [w i hi])) h (fun _ => rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
F G : ComposableArrows C n
h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi ≫ ((fun i => eqToIso ⋯) ⟨i + 1, ⋯⟩).hom =
    ((fun i => eqToIso ⋯) ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi

Tactic:
simp [w i hi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b) / c = a * (b / c)
  | _, c, ⟨d, rfl⟩ =>
    if cz : c = 0 then by simp [cz, Int.mul_zero] else by
      rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]

Proof state:
a c d : Int
cz : c = 0
⊢ a * (c * d) / c = a * (c * d / c)

Tactic:
simp [cz, Int.mul_zero]

Result:
no goals

Proof state:
a c d : Int
cz : ¬c = 0
⊢ a * (c * d) / c = a * (c * d / c)

Tactic:
rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma isIso_map {i j : J} (φ : i ⟶ j) (ι : i₀ ⟶ i) : IsIso (F.map φ)

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this : IsIso (F.map ι)
⊢ IsIso (F.map φ)

Tactic:
have := h (ι ≫ φ)

Result:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this✝ : IsIso (F.map ι)
this : IsIso (F.map (ι ≫ φ))
⊢ IsIso (F.map φ)

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this✝ : IsIso (F.map ι)
this : IsIso (F.map (ι ≫ φ))
⊢ IsIso (F.map φ)

Tactic:
exact IsIso.of_isIso_fac_left (F.map_comp ι φ).symm

Result:
no goals

Proof state:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)

Tactic:
have := h ι

Result:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{u_3, u_1} J
inst✝ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this : IsIso (F.map ι)
⊢ IsIso (F.map φ)
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_add_mul_right_right (h : IsCoprime x (y + z * x)) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_right

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y

Tactic:
rw [mul_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
-- Mathlib/Data/NNReal/Basic.lean
theorem _root_.Real.toNNReal_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
    Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, Real.toNNReal (f a)

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, ↑(f i).toNNReal

Tactic:
exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
rw [← coe_inj, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]

Result:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, ↑(f i).toNNReal

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
x : ι
hxs : x ∈ s
⊢ f x = ↑(f x).toNNReal

Tactic:
rw [Real.coe_toNNReal _ (hf x hxs)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_udiv (n d : BitVec w) (hy : 0#w < d) (i : Nat) (hi : i < w) :
    (n / d)[i] = (divRec w {n, d} (DivModState.init w)).q[i]

Proof state:
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ 0#w < d

Tactic:
assumption

Result:
no goals

Proof state:
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ (n / d)[i] = (divRec w { n := n, d := d } (DivModState.init w)).q[i]

Tactic:
rw [udiv_eq_divRec (by assumption)]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem bddBelow_preimage (e : α ≃o β) {s : Set β} : BddBelow (e ⁻¹' s) ↔ BddBelow s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddBelow (⇑e ⁻¹' s) ↔ BddBelow s

Tactic:
rw [← e.bddBelow_image, e.image_preimage]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem range_lift (f : G →* K) (g : H →* K) :
    MonoidHom.range (lift f g) = MonoidHom.range f ⊔ MonoidHom.range g

Proof state:
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
K : Type u_3
inst✝ : Group K
f : G →* K
g : H →* K
⊢ (lift f g).range = f.range ⊔ g.range

Tactic:
simp [range_eq]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem stoppedValue_upperCrossingTime (h : upperCrossingTime a b f N (n + 1) ω ≠ N) :
    b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω

Proof state:
case intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω)
hj₂ : f j ω ∈ Set.Ici b
⊢ b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω

Tactic:
exact stoppedValue_hitting_mem ⟨j, ⟨hj₁.1, le_trans hj₁.2 (hitting_le _)⟩, hj₂⟩

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
⊢ b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := (hitting_le_iff_of_lt _ (lt_of_le_of_ne upperCrossingTime_le h)).1 le_rfl

Result:
case intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
h : upperCrossingTime a b f N (n + 1) ω ≠ N
j : ℕ
hj₁ : j ∈ Set.Icc (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) (upperCrossingTime a b f N (n + 1) ω)
hj₂ : f j ω ∈ Set.Ici b
⊢ b ≤ stoppedValue f (upperCrossingTime a b f N (n + 1)) ω