harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    trace ((M : Matrix _ _ _) * N * (↑M⁻¹ : Matrix _ _ _)) = trace N

Proof state:
m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).trace = N.trace

Tactic:
rw [trace_mul_cycle, Units.inv_mul, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_cons_eq_append (l : List α) : l.foldr cons l' = l ++ l'

Proof state:
α : Type u_1
l' l : List α
⊢ foldr cons l' l = l ++ l'

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_mul_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a b : G) :
    f (a * b⁻¹) = f a * (f b)⁻¹

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ f (a * b⁻¹) = f a * (f b)⁻¹

Tactic:
rw [map_mul, map_inv]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFactor_ne_zero : convexBodySumFactor K ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ convexBodySumFactor K ≠ 0

Tactic:
refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (NNReal.pi / 2) ^ nrComplexPlaces K ≠ 0

Tactic:
exact mul_ne_zero (pow_ne_zero _ two_ne_zero)
  (pow_ne_zero _ (div_ne_zero NNReal.pi_ne_zero two_ne_zero))

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_sub_one (n : ℤ) : U R (n - 1) = 2 * X * U R n - U R (n + 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R (n - 1) = 2 * X * U R n - U R (n + 1)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 1)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_eq_left_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} :
    lineMap p₀ p₁ c = p₀ ↔ p₀ = p₁ ∨ c = 0

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AffineSpace V1 P1
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0

Tactic:
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathConnectedSpace_iff_univ : PathConnectedSpace X ↔ IsPathConnected (univ : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ IsPathConnected univ

Tactic:
simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Norm.lean
theorem extends_norm (hf1 : f 1 = 1) (a : R) : f (algebraMap R S a) = ‖a‖

Proof state:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f ((algebraMap R S) a) = ‖a‖

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Proof state:
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
exact extends_norm' hf1 _

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
/-- Note that the `IsScalarTower α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
lemma smul_div_assoc [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) :
    r • x / y = r • (x / y)

Proof state:
α : Type u_5
β : Type u_6
inst✝² : DivInvMonoid β
inst✝¹ : SMul α β
inst✝ : IsScalarTower α β β
r : α
x y : β
⊢ r • x / y = r • (x / y)

Tactic:
simp [div_eq_mul_inv, smul_mul_assoc]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_sdiff_cancel' (hab : a ≤ b) (hbc : b ≤ c) : b ⊔ c \ a = c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c \ a = c

Tactic:
rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.neg_to_eq {α} [DivisionRing α] {n d} :
    {a n' d' : α} → IsRat a (.negOfNat n) d → n = n' → d = d' → a = -(n' / d')
  | _, _, _, ⟨_, rfl⟩, rfl, rfl => by simp [div_eq_mul_inv]

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem isLeast_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) :
    IsLeast {C : ℝ≥0 | ∀ m, ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsLeast {C | ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊

Tactic:
simpa only [← opNNNorm_le_iff] using isLeast_Ici

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat

Proof state:
b : Bool
⊢ (ofBool b).toNat = b.toNat

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_pred_castSucc_iff {a b : Fin (n + 1)} (ha : castSucc a ≠ 0) :
    b ≤ (castSucc a).pred ha ↔ b < a

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ b ≤ a.castSucc.pred ha ↔ b < a

Tactic:
rw [le_pred_iff, succ_le_castSucc_iff]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem insert_insert_of_ne {a a'} {b : β a} {b' : β a'} (s : Finmap β) (h : a ≠ a') :
    (s.insert a b).insert a' b' = (s.insert a' b').insert a b :=
  induction_on s fun s => by
    simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s✝ : Finmap β
h : a ≠ a'
s : AList β
⊢ insert a' b' (insert a b ⟦s⟧) = insert a b (insert a' b' ⟦s⟧)

Tactic:
simp only [insert_toFinmap, AList.toFinmap_eq, AList.insert_insert_of_ne _ h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
    getKey! (insertManyIfNewUnit m l) k = default

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey! k = default

Tactic:
exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
  ⟨m.1, _⟩ m.2 not_mem contains_eq_false

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k : α
not_mem : ¬k ∈ m
contains_eq_false : l.contains k = false
⊢ (insertManyIfNewUnit m l).getKey! k = default

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey! k = default
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_right_strictAnti₀ (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·) :=
  strictAnti_nat_of_succ_lt fun n => by
    simpa only [pow_succ', one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
n : ℕ
⊢ a ^ (n + 1) < a ^ n

Tactic:
simpa only [pow_succ', one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
/-- A product `M × [x,y]` for `M` boundaryless has boundary `M × {x, y}`. -/
lemma boundary_product [I.Boundaryless] :
    (I.prod (𝓡∂ 1)).boundary (M × Icc x y) = Set.prod univ {⊥, ⊤}

Proof state:
x y : ℝ
hxy : Fact (x < y)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
⊢ ModelWithCorners.boundary (M × ↑(Icc x y)) = univ.prod {⊥, ⊤}

Tactic:
rw [I.boundary_of_boundaryless_left, boundary_Icc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_closure_eq (δ : ℝ) (E : Set α) :
    thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E

Tactic:
simp (config := { unfoldPartialApp := true }) only [thickenedIndicatorAux, infEdist_closure]

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem end_path : f x₁ = g x₃

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ f x₁ = g x₃

Tactic:
convert hfg 1 <;> simp only [Path.target]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e

Proof state:
α : Type u_1
b : Bool
t e : α
⊢ (bif b then t else e) = if b = true then t else e

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_surj_iff_rTensor_surj :
    Function.Surjective (lTensor M f) ↔ Function.Surjective (rTensor M f)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ Function.Surjective ⇑(lTensor M f) ↔ Function.Surjective ⇑(rTensor M f)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem mem_quotient_iff_mem {I J : Ideal R} [I.IsTwoSided] (hIJ : I ≤ J) {x : R} :
    Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J

Proof state:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ (Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J

Tactic:
rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j)

Proof state:
i j x : Nat
⊢ (x >>> i).testBit j = x.testBit (i + j)

Tactic:
simp [testBit, ←shiftRight_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
@[simp] lemma mkDerivationEquiv_apply (a : A) :
    mkDerivationEquiv R a = mkDerivation R a

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ (mkDerivationEquiv R) a = (mkDerivation R) a

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem id_apply_of_ne (M : Mat_ C) (i j : M.ι) (h : i ≠ j) : (𝟙 M : Hom M M) i j = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : i ≠ j
⊢ 𝟙 M i j = 0

Tactic:
simp [id_apply, h]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iSup_join {ι : Sort w} {f : ι → Filter (Filter α)} : ⨆ x, join (f x) = join (⨆ x, f x) :=
  Filter.ext fun x => by simp only [mem_iSup, mem_join]

Proof state:
α : Type u
ι : Sort w
f : ι → Filter (Filter α)
x : Set α
⊢ x ∈ ⨆ x, (f x).join ↔ x ∈ (⨆ x, f x).join

Tactic:
simp only [mem_iSup, mem_join]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Ioo_mul_right (h : a < b) : (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

Tactic:
rw [mul_comm, right_mul_prod_Ioo h]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Ring.lean
theorem toOrderRingHom_injective : Injective (toOrderRingHom : α ≃+*o β → α →+*o β) :=
  fun f g h => DFunLike.coe_injective <| by convert DFunLike.ext'_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : NonAssocSemiring α
inst✝² : Preorder α
inst✝¹ : NonAssocSemiring β
inst✝ : Preorder β
f g : α ≃+*o β
h : f.toOrderRingHom = g.toOrderRingHom
⊢ (fun f => ⇑f) f = (fun f => ⇑f) g

Tactic:
convert DFunLike.ext'_iff.1 h using 0

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma range_comp_le (f : F ⟶ F') (g : F' ⟶ F'') :
    range (f ≫ g) ≤ range g := fun _ _ _ ↦ by aesop

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
x✝² : Cᵒᵖ
x✝¹ : F''.obj x✝²
x✝ : x✝¹ ∈ (range (f ≫ g)).obj x✝²
⊢ x✝¹ ∈ (range g).obj x✝²

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem duplicate_cons_iff_of_ne {y : α} (hne : x ≠ y) : x ∈+ y :: l ↔ x ∈+ l

Proof state:
α : Type u_1
l : List α
x y : α
hne : x ≠ y
⊢ x ∈+ y :: l ↔ x ∈+ l

Tactic:
simp [duplicate_cons_iff, hne.symm]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem one_div_div : 1 / (a / b) = b / a

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / (a / b) = b / a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.setLIntegral_comp_preimage {mb : MeasurableSpace β} {ν : Measure β}
    {g : α → β} (hg : MeasurePreserving g μ ν) {s : Set β} (hs : MeasurableSet s) {f : β → ℝ≥0∞}
    (hf : Measurable f) : ∫⁻ a in g ⁻¹' s, f (g a) ∂μ = ∫⁻ b in s, f b ∂ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
s : Set β
hs : MeasurableSet s
f : β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem foldrIdx_eq_foldr_enum (f : ℕ → α → β → β) (b : β) (as : List α) :
    foldrIdx f b as = foldr (uncurry f) b (enum as)

Proof state:
α : Type u
β : Type v
f : ℕ → α → β → β
b : β
as : List α
⊢ foldrIdx f b as = foldr (uncurry f) b as.enum

Tactic:
simp only [foldrIdx, foldrIdxSpec, foldrIdx_eq_foldrIdxSpec, enum]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_dist_eq_of_L2 (x y : WithLp 2 (α × β)) :
    dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(dist x.1 y.1 ^ 2 + dist x.2 y.2 ^ 2)

Tactic:
simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
@[simp] lemma toSubspace_isMono {l : Line (η → α) ι} {C : (ι × η → α) → κ} :
    l.toSubspace.IsMono C ↔ l.IsMono fun x : ι → η → α  ↦ C fun (i, e) ↦ x i e

Proof state:
η : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
l : Line (η → α) ι
C : (ι × η → α) → κ
⊢ Subspace.IsMono C l.toSubspace ↔
    IsMono
      (fun x =>
        C fun x_1 =>
          match x_1 with
          | (i, e) => x i e)
      l

Tactic:
simp [Subspace.IsMono, IsMono, funext (toSubspace_apply _ _)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem neg (hf : UnifTight f p μ) : UnifTight (-f) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
⊢ UnifTight (-f) p μ

Tactic:
simp_rw [UnifTight, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
⊢ ∀ ⦃ε : ℝ≥0⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
⊢ ∀ ⦃ε : ℝ≥0⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
exact hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_zero_of_ediv_eq_zero {d n : Int} (h : d ∣ n) (H : n / d = 0) : n = 0

Proof state:
d n : Int
h : d ∣ n
H : n / d = 0
⊢ n = 0

Tactic:
rw [← Int.mul_ediv_cancel' h, H, Int.mul_zero]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_swap (m : α → β → γ) (f : Filter α) (g : Filter β) :
    map₂ m f g = map₂ (fun a b => m b a) g f

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = map₂ (fun a b => m b a) g f

Tactic:
rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasFDerivAtFilter.const_sub (hf : HasFDerivAtFilter f f' x L) (c : F) :
    HasFDerivAtFilter (fun x => c - f x) (-f') x L

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter E
hf : HasFDerivAtFilter f f' x L
c : F
⊢ HasFDerivAtFilter (fun x => c - f x) (-f') x L

Tactic:
simpa only [sub_eq_add_neg] using hf.neg.const_add c

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem interior_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc a b) = Ioo a b

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Icc a b) = Ioo a b

Tactic:
rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem lowerClosure_mul_distrib : lowerClosure (s * t) = lowerClosure s * lowerClosure t :=
  SetLike.coe_injective <| by
    rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure s * lowerClosure t)

Tactic:
rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem ι_range_comap_involute :
    (ι Q).range.comap (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap =
      LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap involute.toLinearMap (LinearMap.range (ι Q)) = LinearMap.range (ι Q)

Tactic:
rw [← submodule_map_involute_eq_comap, ι_range_map_involute]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Sum.lean
theorem Coloring.sum_sumLeft_sumRight (c : (G ⊕g H).Coloring γ) : c.sumLeft.sum c.sumRight = c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
G : SimpleGraph α
H : SimpleGraph β
c : (G ⊕g H).Coloring γ
⊢ c.sumLeft.sum c.sumRight = c

Tactic:
ext (u | u) <;> rfl

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem append_append_stream : ∀ (l₁ l₂ : List α) (s : Stream' α),
    l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)
  | [], _, _ => rfl
  | List.cons a l₁, l₂, s => by
    rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]

Proof state:
α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem accPt_sup (x : X) (F G : Filter X) :
    AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
F G : Filter X
⊢ AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

Tactic:
simp only [AccPt, inf_sup_left, sup_neBot]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Iio_add_one_eq_Iic_of_not_isMax (hb : ¬ IsMax b) : Iio (b + 1) = Iic b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem getLast_append_singleton {a : α} (l : List α) :
    getLast (l ++ [a]) (append_ne_nil_of_right_ne_nil l (cons_ne_nil a _)) = a

Proof state:
α : Type u
a : α
l : List α
⊢ (l ++ [a]).getLast ⋯ = a

Tactic:
simp [getLast_append]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_inr_range_inl : Sum.inr ⁻¹' range (Sum.inl : α → α ⊕ β) = ∅

Proof state:
α : Type u_1
β : Type u_2
⊢ Sum.inr ⁻¹' range Sum.inl = ∅

Tactic:
rw [← image_univ, preimage_inr_image_inl]

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem isEmbedding_iff_restrictPreimage (h : Continuous f) :
    IsEmbedding f ↔ ∀ i, IsEmbedding ((U i).1.restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ↔ ∀ (i : ι), IsEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simpa [isEmbedding_iff, forall_and] using and_congr (hU.isInducing_iff_restrictPreimage h)
  (injective_iff_injective_of_iUnion_eq_univ hU.iSup_set_eq_univ)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
⊢ m.isEmpty = (m.size == 0)

Tactic:
simp [isEmpty]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Sbtw.oangle_eq_left_right {p₁ p₁' p₂ p₃ p₃' : P} (h₁ : Sbtw ℝ p₁ p₂ p₁')
    (h₃ : Sbtw ℝ p₃ p₂ p₃') : ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ p₃' : P
h₁ : Sbtw ℝ p₁ p₂ p₁'
h₃ : Sbtw ℝ p₃ p₂ p₃'
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃'

Tactic:
rw [h₁.oangle_eq_add_pi_left h₃.left_ne, h₃.oangle_eq_add_pi_right h₁.right_ne, add_assoc,
  Real.Angle.coe_pi_add_coe_pi, add_zero]

Result:
no goals
-- Mathlib/Order/Height.lean
theorem one_le_chainHeight_iff : 1 ≤ s.chainHeight ↔ s.Nonempty

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
⊢ (∃ l ∈ s.subchain, l.length = 1) ↔ s.Nonempty

Tactic:
simp only [length_eq_one, @and_comm (_ ∈ _), @eq_comm _ _ [_], exists_exists_eq_and,
  singleton_mem_subchain_iff, Set.Nonempty]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
⊢ 1 ≤ s.chainHeight ↔ s.Nonempty

Tactic:
rw [← Nat.cast_one, Set.le_chainHeight_iff]

Result:
α : Type u_1
inst✝ : LT α
s : Set α
⊢ (∃ l ∈ s.subchain, l.length = 1) ↔ s.Nonempty
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.filter (p : α → Bool) {l} : Nodup l → Nodup (filter p l)

Proof state:
α : Type u
p : α → Bool
l : List α
⊢ l.Nodup → (List.filter p l).Nodup

Tactic:
simpa using Pairwise.filter p

Result:
no goals