harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_nonpos_of_nonpos_of_nonneg [MulPosMono α] (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem Bijective.comp_right (hf : Bijective f) : Bijective fun g : β → γ ↦ g ∘ f :=
  ⟨hf.surjective.injective_comp_right, fun g ↦
    ⟨g ∘ surjInv hf.surjective,
     by simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]⟩⟩

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g => g ∘ f) (g ∘ surjInv ⋯) = g

Tactic:
simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    l.length ≤ (insertEntry k v l).length

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ (insertEntry k v l).length

Tactic:
rw [length_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ if containsKey k l = true then l.length else l.length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ if containsKey k l = true then l.length else l.length + 1

Tactic:
split <;> omega

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma ReflPrefunctor.congr_mk₁_map
    {Y : Type u'} [ReflQuiver.{v'} Y] {C : Type u} [Category.{v} C]
    (F : ReflPrefunctor Y (ReflQuiv.of C))
    {x₁ y₁ x₂ y₂ : Y} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂)
    (hx : x₁ = x₂) (hy : y₁ = y₂) (hfg : Quiver.homOfEq f hx hy = g) :
    ComposableArrows.mk₁ (C := C) (F.map f) = ComposableArrows.mk₁ (C := C) (F.map g)

Proof state:
Y : Type u'
inst✝¹ : ReflQuiver Y
C : Type u
inst✝ : Category.{v, u} C
F : Y ⥤rq ↑(ReflQuiv.of C)
x₁ y₁ x₂ y₂ : Y
f : x₁ ⟶ y₁
g : x₂ ⟶ y₂
hx : x₁ = x₂
hy : y₁ = y₂
hfg : Quiver.homOfEq f hx hy = g
⊢ ComposableArrows.mk₁ (F.map f) = ComposableArrows.mk₁ (F.map g)

Tactic:
subst hx hy hfg

Result:
Y : Type u'
inst✝¹ : ReflQuiver Y
C : Type u
inst✝ : Category.{v, u} C
F : Y ⥤rq ↑(ReflQuiv.of C)
x₁ y₁ : Y
f : x₁ ⟶ y₁
⊢ ComposableArrows.mk₁ (F.map f) = ComposableArrows.mk₁ (F.map (Quiver.homOfEq f ⋯ ⋯))

Proof state:
Y : Type u'
inst✝¹ : ReflQuiver Y
C : Type u
inst✝ : Category.{v, u} C
F : Y ⥤rq ↑(ReflQuiv.of C)
x₁ y₁ : Y
f : x₁ ⟶ y₁
⊢ ComposableArrows.mk₁ (F.map f) = ComposableArrows.mk₁ (F.map (Quiver.homOfEq f ⋯ ⋯))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_one : sign 1 = 1 :=
  sign_of_pos <| by norm_num

Proof state:
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piRight_symm_single (x : N) (i : ι) (m : M i) :
    (piRight R S N M).symm (Pi.single i (x ⊗ₜ m)) = x ⊗ₜ Pi.single i m

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
⊢ (piRight R S N M).symm (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

Tactic:
simp [piRight]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Hom/Ultra.lean
/-- Proves that when a `SeminormedAddGroup` structure is constructed from an
`AddGroupSeminormClass` that satisfies `IsNonarchimedean`, the group has an `IsUltrametricDist`. -/
lemma AddGroupSeminormClass.isUltrametricDist [AddGroup α] [AddGroupSeminormClass F α ℝ]
    [inst : Dist α] {f : F} (hna : IsNonarchimedean f)
    (hd : inst = (AddGroupSeminormClass.toSeminormedAddGroup f).toDist

Proof state:
F : Type u_1
α : Type u_2
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroup α
inst✝ : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean ⇑f
hd : autoParam (inst = PseudoMetricSpace.toDist) _auto✝
x y z : α
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
simpa only [hd, dist_eq_norm, AddGroupSeminormClass.toSeminormedAddGroup_norm_eq,
← sub_add_sub_cancel x y z] using hna _ _

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Int.lean
theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) : ¬ (harmonic n).isInt

Proof state:
n : ℕ
h : 2 ≤ n
⊢ ¬(harmonic n).isInt = true

Tactic:
apply padicNorm.not_int_of_not_padic_int 2

Result:
n : ℕ
h : 2 ≤ n
⊢ 1 < padicNorm 2 (harmonic n)

Proof state:
n : ℕ
h : 2 ≤ n
⊢ 1 < padicNorm 2 (harmonic n)

Tactic:
rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast]

Result:
n : ℕ
h : 2 ≤ n
⊢ 1 < ↑2 ^ Nat.log 2 n

Proof state:
n : ℕ
h : 2 ≤ n
⊢ 1 < ↑2 ^ Nat.log 2 n

Tactic:
exact one_lt_pow₀ one_lt_two (Nat.log_pos one_lt_two h).ne'

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem covBy_add_one [NoMaxOrder α] (x : α) : x ⋖ x + 1

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ succ x

Tactic:
exact covBy_succ x

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ x + 1

Tactic:
rw [← succ_eq_add_one]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
x : α
⊢ x ⋖ succ x
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_zero_left : (fun _ ↦ (0 : E')) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

Proof state:
α : Type u_1
E' : Type u_6
F'' : Type u_10
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup F''
g'' : α → F''
l : Filter α
⊢ (fun x => 0) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

Tactic:
simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
lemma cochainsMap_f_map_epi (hf : Function.Injective f) [Epi φ] (i : ℕ) :
    Epi ((cochainsMap f φ).f i)

Proof state:
k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
hf : Function.Injective ⇑f
inst✝ : Epi φ
i : ℕ
⊢ Epi ((cochainsMap f φ).f i)

Tactic:
simpa [ModuleCat.epi_iff_surjective] using
  ((Rep.epi_iff_surjective φ).1 inferInstance).comp_left.comp <|
  LinearMap.funLeft_surjective_of_injective k A _ hf.comp_left

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem algebraMap_mem_iff (S : Type*) {R A : Type*} [CommSemiring R] [CommSemiring S]
    [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} :
    algebraMap R S r ∈ spectrum S a ↔ r ∈ spectrum R a

Proof state:
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ spectrum S a ↔ r ∈ σ a

Tactic:
simp only [spectrum.mem_iff, Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range_eq_range' (n : Nat) : range n = range' 0 n

Proof state:
n : Nat
⊢ range n = range' 0 n

Tactic:
simp [range, range', Array.range_eq_range']

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem add_eq_right_iff_le : a + b = b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
a b : α
⊢ a + b = b ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_map (f : β → α) {l : List β} :
    Chain' R (map f l) ↔ Chain' (fun a b : β => R (f a) (f b)) l

Proof state:
α : Type u
β : Type v
R : α → α → Prop
f : β → α
l : List β
⊢ Chain' R (map f l) ↔ Chain' (fun a b => R (f a) (f b)) l

Tactic:
cases l <;> [rfl; exact chain_map _]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_neg (symmetric : ∀ x ∈ s, -x ∈ s) (x : E) : gauge s (-x) = gauge s x

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x✝ x : E
h : -x ∈ s
⊢ x ∈ s

Tactic:
simpa using symmetric _ h

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
⊢ gauge s (-x) = gauge s x

Tactic:
simp_rw [gauge_def', smul_neg, this]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
⊢ gauge s (-x) = gauge s x

Tactic:
have : ∀ x, -x ∈ s ↔ x ∈ s := fun x => ⟨fun h => by simpa using symmetric _ h, symmetric x⟩

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
x : E
this : ∀ (x : E), -x ∈ s ↔ x ∈ s
⊢ gauge s (-x) = gauge s x
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem List.aemeasurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) :
    AEMeasurable (fun x => (l.map fun f : α → M => f x).prod) μ

Proof state:
M : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable (fun x => (map (fun f => f x) l).prod) μ

Tactic:
simpa only [← Pi.list_prod_apply] using l.aemeasurable_prod' hl

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (image₂ f s t).image g = image₂ f' t (s.image g') :=
  coe_injective <| by
    push_cast
    exact image_image2_antidistrib_right h_antidistrib

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ g '' image2 f ↑s ↑t = image2 f' (↑t) (g' '' ↑s)

Tactic:
exact image_image2_antidistrib_right h_antidistrib

Result:
no goals

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' t (image g' s))

Tactic:
push_cast

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ g '' image2 f ↑s ↑t = image2 f' (↑t) (g' '' ↑s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (l : List α) :
    filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
a : α
l : List α
IH : filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l
⊢ filterMap g (filterMap f (a :: l)) = filterMap (fun x => (f x).bind g) (a :: l)

Tactic:
cases h : f a <;> simp [filterMap_cons, *]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
l : List α
⊢ filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l

Tactic:
induction l with
| nil => rfl
| cons a l IH => cases h : f a <;> simp [filterMap_cons, *]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
⊢ filterMap g (filterMap f []) = filterMap (fun x => (f x).bind g) []

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma inv_eq_conj (hz : ‖z‖ = 1) : z⁻¹ = conj z :=
  inv_eq_of_mul_eq_one_left <| by simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ‖z‖ = 1
⊢ (starRingEnd K) z * z = 1

Tactic:
simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_ediv : ∀ b : Int, 0 / b = 0
  | ofNat _ => show ofNat _ = _ by simp
  | -[_+1] => show -ofNat _ = _ by simp

Proof state:
a✝ : Nat
⊢ ofNat (0 / a✝) = 0

Tactic:
simp

Result:
no goals

Proof state:
a✝ : Nat
⊢ -ofNat (0 / a✝.succ) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_sup_le_or : blimsup u f p ⊔ blimsup u f q ≤ blimsup u f fun x => p x ∨ q x :=
  sup_le (blimsup_mono <| by tauto) (blimsup_mono <| by tauto)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), q x → p x ∨ q x

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x → p x ∨ q x

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem differentiableAt_dslope_of_ne (h : b ≠ a) :
    DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : b ≠ a
⊢ DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b

Tactic:
simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_toList_insert [@TransCmp α cmp] {t : RBSet α cmp} :
    v' ∈ toList (t.insert v) ↔ (v' ∈ toList t ∧ t.find? v ≠ some v') ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
⊢ v' ∈ (t.insert v).toList ↔ v' ∈ t.toList ∧ t.find? v ≠ some v' ∨ v' = v

Tactic:
let ⟨ht₁, _, _, ht₂⟩ := t.2.out

Result:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
ht₁ : RBNode.Ordered cmp t.val
w✝¹ : RBColor
w✝ : Nat
ht₂ : t.val.Balanced w✝¹ w✝
⊢ v' ∈ (t.insert v).toList ↔ v' ∈ t.toList ∧ t.find? v ≠ some v' ∨ v' = v

Proof state:
α : Type u_1
cmp : α → α → Ordering
v v' : α
inst✝ : TransCmp cmp
t : RBSet α cmp
ht₁ : RBNode.Ordered cmp t.val
w✝¹ : RBColor
w✝ : Nat
ht₂ : t.val.Balanced w✝¹ w✝
⊢ v' ∈ (t.insert v).toList ↔ v' ∈ t.toList ∧ t.find? v ≠ some v' ∨ v' = v

Tactic:
simpa [mem_toList] using RBNode.mem_insert ht₂ ht₁

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iSup_iff {f : ι → UpperSet α} : (a ∈ ⨆ i, f i) ↔ ∀ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⨆ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iSup]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i

Tactic:
exact mem_iInter

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
@[simp]
lemma coverEntropy_empty {T : X → X} : coverEntropy T ∅ = ⊥

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
⊢ coverEntropy T ∅ = ⊥

Tactic:
simp only [coverEntropy, coverEntropyEntourage_empty, iSup_bot]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurableSet_image (e : α ≃ᵐ β) :
    MeasurableSet (e '' s) ↔ MeasurableSet s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet (⇑e '' s) ↔ MeasurableSet s

Tactic:
rw [image_eq_preimage, measurableSet_preimage]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem nndist_le_distortion_mul (I : Box ι) (i : ι) :
    nndist I.lower I.upper ≤ I.distortion * nndist (I.lower i) (I.upper i) :=
  calc
    nndist I.lower I.upper =
        nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) :=
      (div_mul_cancel₀ _ <| mt nndist_eq_zero.1 (I.lower_lt_upper i).ne).symm
    _ ≤ I.distortion * nndist (I.lower i) (I.upper i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) * nndist (I.lower i) (I.upper i) ≤
    I.distortion * nndist (I.lower i) (I.upper i)

Tactic:
apply mul_le_mul_right'

Result:
case bc
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) ≤ I.distortion

Proof state:
case bc
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (I.lower i) (I.upper i) ≤ I.distortion

Tactic:
apply Finset.le_sup (Finset.mem_univ i)

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_add (M N : Matrix m n R) :
    (M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M N : Matrix m n R
⊢ (M + N).toMvPolynomial = M.toMvPolynomial + N.toMvPolynomial

Tactic:
ext i : 1

Result:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M N : Matrix m n R
i : m
⊢ (M + N).toMvPolynomial i = (M.toMvPolynomial + N.toMvPolynomial) i

Proof state:
case h
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M N : Matrix m n R
i : m
⊢ (M + N).toMvPolynomial i = (M.toMvPolynomial + N.toMvPolynomial) i

Tactic:
simp only [toMvPolynomial, add_apply, map_add, Finset.sum_add_distrib, Pi.add_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem card_quotient_mul_card_quotient (S T : Submodule R M) (hST : T ≤ S) :
    Nat.card (S.map T.mkQ) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)

Tactic:
rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
  Nat.card_congr (quotientQuotientEquivQuotient T S hST).toEquiv]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma divInt_one_one : 1 /. 1 = 1

Proof state:
⊢ 1 /. 1 = 1

Tactic:
rw [divInt_one, intCast_one]

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexBetween.lean
/-- In a strictly convex space, the triangle inequality turns into an equality if and only if the
middle point belongs to the segment joining two other points. -/
lemma dist_add_dist_eq_iff : dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ (fun x => x -ᵥ a) '' affineSegment ℝ a c
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
rwa [(vsub_left_injective _).mem_set_image] at this

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
have :
    dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔
      b -ᵥ a ∈ segment ℝ (a -ᵥ a) (c -ᵥ a) := by
  simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
    eq_comm]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a-[ℝ]c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
⊢ dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a-[ℝ]c -ᵥ a]

Tactic:
simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
  eq_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist (a -ᵥ a) (b -ᵥ a) + dist (b -ᵥ a) (c -ᵥ a) = dist (a -ᵥ a) (c -ᵥ a) ↔ b -ᵥ a ∈ [a -ᵥ a-[ℝ]c -ᵥ a]
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
simp_rw [dist_vsub_cancel_right, ← affineSegment_eq_segment, ← affineSegment_vsub_const_image]
  at this

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ (fun x => x -ᵥ a) '' affineSegment ℝ a c
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem bot_eq_zero {B : C} : (⊥ : Subobject B) = Subobject.mk (0 : 0 ⟶ B) :=
  mk_eq_mk_of_comm _ _ (initialIsInitial.uniqueUpToIso HasZeroObject.zeroIsInitial)
    (by simp [eq_iff_true_of_subsingleton])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ (initialIsInitial.uniqueUpToIso HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_trailing_coeff' (hkm : k < m) (hmn : m < n) :
    (trinomial k m n u v w).coeff k = u

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v w).coeff k = u

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
  if_pos rfl, if_neg hkm.ne, if_neg (hkm.trans hmn).ne, add_zero, add_zero]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_eq_iInf [CompleteLattice α] [SuccOrder α] (a : α) : succ a = ⨅ b > a, b

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = ⨅ b, ⨅ (_ : b > a), b

Tactic:
rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem append_toArray (l₁ l₂ : List α) :
    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l₁ l₂ : List α
⊢ (l₁.toArray ++ l₂.toArray).toList = (l₁ ++ l₂).toArray.toList

Proof state:
case h
α : Type u_1
l₁ l₂ : List α
⊢ (l₁.toArray ++ l₂.toArray).toList = (l₁ ++ l₂).toArray.toList

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma chromaticNumber_eq_card_iff_forall_surjective [Fintype α] (hG : G.Colorable (card α)) :
    G.chromaticNumber = card α ↔ ∀ C : G.Coloring α, Surjective C

Proof state:
V : Type u
G : SimpleGraph V
α : Type u_1
inst✝ : Fintype α
hG : G.Colorable (card α)
⊢ G.chromaticNumber = ↑(card α) ↔ ∀ (C : G.Coloring α), Surjective ⇑C

Tactic:
rw [← hG.chromaticNumber_le.ge_iff_eq, card_le_chromaticNumber_iff_forall_surjective]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma upperClosure_inf_sdiff (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :
    upperClosure t ⊓ s.sdiff t = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ upperClosure t ⊓ s.sdiff t = s

Tactic:
rw [inf_comm, sdiff_inf_upperClosure hts hst]

Result:
no goals