harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/Maschke.lean
theorem conjugate_i (h : ∀ v : V, π (i v) = v) (g : G) (v : V) :
    (conjugate π g : W → V) (i v) = v

Proof state:
k : Type u
inst✝⁹ : CommRing k
G : Type u
inst✝⁸ : Group G
V : Type v
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ (π.conjugate g) (i v) = v

Tactic:
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
  ← one_def, one_smul]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma add_pow_eq_mul_pow_add_pow_div_expChar_of_commute (h : Commute x y) :
    (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
    (replicate n (a, b)).lookup k = if k == a then some b else none

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
n : Nat
a : α
α✝ : Type u_1
b : α✝
k : α
h : 0 < n
⊢ lookup k (replicate n (a, b)) = if (k == a) = true then some b else none

Tactic:
simp [lookup_replicate, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_cons_succ (l : List α) (a : α) (n : ℕ) :
    (a :: l : List α).rotate' n.succ = (l ++ [a]).rotate' n

Proof state:
α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' n.succ = (l ++ [a]).rotate' n

Tactic:
simp [rotate']

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_sup_left {S T : NonUnitalStarSubalgebra R A} : ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem MeasurableSpace.comap_compl {m' : MeasurableSpace β} [BooleanAlgebra β]
    (h : Measurable (compl : β → β)) (f : α → β) :
    MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance =
      MeasurableSpace.comap f inferInstance

Proof state:
case e_m
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap compl inferInstance = inferInstance

Tactic:
exact (MeasurableEquiv.ofInvolutive _ compl_involutive h).measurableEmbedding.comap_eq

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance

Tactic:
congr

Result:
case e_m
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap compl inferInstance = inferInstance

Proof state:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap (fun a => (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance

Tactic:
rw [← Function.comp_def, ← MeasurableSpace.comap_comp]

Result:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_Iic : #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → DecidableEq (α i)
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iic f) = ∏ i ∈ f.support, #(Iic (f i))

Tactic:
simp_rw [Iic_eq_Icc, card_Icc, DFinsupp.bot_eq_zero, support_zero, empty_union, zero_apply,
  bot_eq_zero]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_reverse (l : List α) : sublists (reverse l) = map reverse (sublists' l)

Proof state:
α : Type u
l : List α
⊢ l.reverse.sublists = map reverse l.sublists'

Tactic:
induction' l with hd tl ih <;> [rfl;
  simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
    map_eq_map, bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil,
    Function.comp_def]]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_filter_mul_prod_filter_not [CommMonoid N] (g : α → M → N) :
    (f.filter p).prod g * (f.filter fun a => ¬p a).prod g = f.prod g

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g * (filter (fun a => ¬p a) f).prod g = f.prod g

Tactic:
simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not,
Finsupp.prod]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g * (filter (fun a => ¬p a) f).prod g = f.prod g

Tactic:
classical simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not,
  Finsupp.prod]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem scalar_eq_self_of_mem_center
    {A : SpecialLinearGroup n R} (hA : A ∈ center (SpecialLinearGroup n R)) (i : n) :
    scalar n (A i i) = A

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
obtain ⟨r : R, hr : scalar n r = A⟩ := mem_range_scalar_of_commute_transvectionStruct fun t ↦
  Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩

Result:
case intro
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
r : R
hr : (scalar n) r = ↑A
⊢ (scalar n) (↑A i i) = ↑A

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
t : TransvectionStruct n R
⊢ t.toMatrix.det = 1

Tactic:
simp

Result:
no goals

Proof state:
case intro
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hA : A ∈ center (SpecialLinearGroup n R)
i : n
r : R
hr : (scalar n) r = ↑A
⊢ (scalar n) (↑A i i) = ↑A

Tactic:
simp [← congr_fun₂ hr i i, ← hr]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma defaultRatCDF_nonneg (q : ℚ) : 0 ≤ defaultRatCDF q

Proof state:
q : ℚ
⊢ 0 ≤ if q < 0 then 0 else 1

Tactic:
split_ifs

Result:
case pos
q : ℚ
h✝ : q < 0
⊢ 0 ≤ 0

case neg
q : ℚ
h✝ : ¬q < 0
⊢ 0 ≤ 1

Proof state:
q : ℚ
⊢ 0 ≤ defaultRatCDF q

Tactic:
unfold defaultRatCDF

Result:
q : ℚ
⊢ 0 ≤ if q < 0 then 0 else 1

Proof state:
case pos
q : ℚ
h✝ : q < 0
⊢ 0 ≤ 0

case neg
q : ℚ
h✝ : ¬q < 0
⊢ 0 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma eq_rpow_inv (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x = y ^ z⁻¹ ↔ x ^ z = y

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_left_inj hx _ hz, rpow_inv_rpow hy hz]

Result:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ y ^ z⁻¹
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[mono, gcongr, bound]
lemma div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a / b ≤ c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹

Tactic:
exact mul_le_mul hac ((inv_le_inv₀ (hd.trans_le hdb) hd).2 hdb)
  (inv_nonneg.2 <| hd.le.trans hdb) hc

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma ι_image_le (W : U.toScheme.Opens) : U.ι ''ᵁ W ≤ U

Proof state:
X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U

Tactic:
simp_rw [← U.ι_image_top]

Result:
X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤

Proof state:
X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤

Tactic:
exact U.ι.image_le_image_of_le le_top

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem Filter.HasBasis.isUniformEmbedding_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'}
    (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} :
    IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧
      (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j)

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h']

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive]
lemma disjoint_smul_set_right : Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Set β
a : α
⊢ Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t

Tactic:
simpa using disjoint_smul_set (a := a) (s := a⁻¹ • s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1

Proof state:
v : Nat
⊢ ((2 ^ v - 1)#'⋯).toNat = 2 ^ v - 1

Tactic:
simp

Result:
no goals

Proof state:
v : Nat
⊢ (allOnes v).toNat = 2 ^ v - 1

Tactic:
unfold allOnes

Result:
v : Nat
⊢ ((2 ^ v - 1)#'⋯).toNat = 2 ^ v - 1
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem eq_adjoin_of_eq_algebra_adjoin (K : IntermediateField F E)
    (h : K.toSubalgebra = Algebra.adjoin F S) : K = adjoin F S

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ Algebra.adjoin F S = (adjoin F S).toSubalgebra

Tactic:
refine (adjoin_eq_algebra_adjoin F _ fun x ↦ ?_).symm

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ Algebra.adjoin F S → x⁻¹ ∈ Algebra.adjoin F S

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K = adjoin F S

Tactic:
apply toSubalgebra_injective

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K.toSubalgebra = (adjoin F S).toSubalgebra

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ K.toSubalgebra = (adjoin F S).toSubalgebra

Tactic:
rw [h]

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ Algebra.adjoin F S = (adjoin F S).toSubalgebra

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ Algebra.adjoin F S → x⁻¹ ∈ Algebra.adjoin F S

Tactic:
rw [← h]

Result:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra

Proof state:
case a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra

Tactic:
exact K.inv_mem

Result:
no goals
-- Mathlib/Dynamics/Flow.lean
theorem continuous_toFun (t : τ) : Continuous (ϕ.toFun t)

Proof state:
case h
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (uncurry ϕ.toFun)

Tactic:
exact ϕ.cont'

Result:
no goals

Proof state:
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (ϕ.toFun t)

Tactic:
rw [← curry_uncurry ϕ.toFun]

Result:
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (Function.curry (uncurry ϕ.toFun) t)

Proof state:
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (Function.curry (uncurry ϕ.toFun) t)

Tactic:
apply continuous_curry

Result:
case h
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
t : τ
⊢ Continuous (uncurry ϕ.toFun)
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem coe_support {u v : V} (p : G.Walk u v) :
    (p.support : Multiset V) = {u} + p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ ↑p.support = {u} + ↑p.support.tail

Tactic:
cases p <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α} :
    k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
⊢ k ∈ insertMany m l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true

Tactic:
simp [mem_iff_contains, contains_insertMany_list h]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.interior_sInter {S : Set (Set X)} (hS : S.Finite) :
    interior (⋂₀ S) = ⋂ s ∈ S, interior s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
rw [sInter_eq_biInter, hS.interior_biInter]

Result:
no goals
-- Mathlib/Data/Multiset/Defs.lean
theorem pairwise_coe_iff {r : α → α → Prop} {l : List α} :
    Multiset.Pairwise r l ↔ ∃ l' : List α, l ~ l' ∧ l'.Pairwise r :=
  exists_congr <| by simp

Proof state:
α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (a : List α), ↑l = ↑a ∧ List.Pairwise r a ↔ l ~ a ∧ List.Pairwise r a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Iic_iff_integrableOn_Iio' (hb : μ {b} ≠ ∞) :
    IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
b : α
hb : μ {b} ≠ ⊤
⊢ IntegrableOn f (Iic b) μ ↔ IntegrableOn f (Iio b) μ

Tactic:
rw [← Iio_union_right, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α} :
    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j]

Proof state:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ find? p { toArray := xs, size_toArray := ⋯ } = some b ↔
    p b = true ∧
      ∃ i h,
        { toArray := xs, size_toArray := ⋯ }[i] = b ∧
          ∀ (j : Nat) (hj : j < i), (!p { toArray := xs, size_toArray := ⋯ }[j]) = true

Tactic:
simp [Array.find?_eq_some_iff_getElem]

Result:
no goals

Proof state:
α : Type
n : Nat
xs : Vector α n
p : α → Bool
b : α
⊢ find? p xs = some b ↔ p b = true ∧ ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ find? p { toArray := xs, size_toArray := ⋯ } = some b ↔
    p b = true ∧
      ∃ i h,
        { toArray := xs, size_toArray := ⋯ }[i] = b ∧
          ∀ (j : Nat) (hj : j < i), (!p { toArray := xs, size_toArray := ⋯ }[j]) = true
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atTop_ciInf (h_anti : Antitone f) (hbdd : BddBelow <| range f) :
    Tendsto f atTop (𝓝 (⨅ i, f i))

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ i, f i))

Tactic:
convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1

Result:
no goals
-- Mathlib/Data/Set/MemPartition.lean
lemma memPartitionSet_succ (f : ℕ → Set α) (n : ℕ) (a : α) [Decidable (a ∈ f n)] :
    memPartitionSet f (n + 1) a
      = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Proof state:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
inst✝ : Decidable (a ∈ f n)
⊢ memPartitionSet f (n + 1) a = if a ∈ f n then memPartitionSet f n a ∩ f n else memPartitionSet f n a \ f n

Tactic:
simp [memPartitionSet]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem continuous_pi_iff : Continuous f ↔ ∀ i, Continuous fun a => f a i

Proof state:
X : Type u
ι : Type u_5
π : ι → Type u_6
inst✝ : TopologicalSpace X
T : (i : ι) → TopologicalSpace (π i)
f : X → (i : ι) → π i
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f a i

Tactic:
simp only [continuous_iInf_rng, continuous_induced_rng, comp_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem strictConvexOn_of_deriv2_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf'' : ∀ x ∈ interior D, 0 < (deriv^[2] f) x) :
    StrictConvexOn ℝ D f :=
  ((strictMonoOn_of_deriv_pos hD.interior fun z hz =>
          (differentiableAt_of_deriv_ne_zero
                (hf'' z hz).ne').differentiableWithinAt.continuousWithinAt) <|
        by rwa [interior_interior]).strictConvexOn_of_deriv
    hD hf

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf'' : ∀ x ∈ interior D, 0 < deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 < deriv (deriv f) x

Tactic:
rwa [interior_interior]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem kernel.ι_op :
    (kernel.ι f.op).unop = eqToHom (Opposite.unop_op _) ≫ cokernel.π f ≫ (kernelOpUnop f).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (kernel.ι f.op).unop = eqToHom ⋯ ≫ cokernel.π f ≫ (kernelOpUnop f).inv

Tactic:
simp [kernelOpUnop]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.sSup {ι} {f : ι → δ → α} {s : Set ι} (hs : s.Countable)
    (hf : ∀ i ∈ s, Measurable (f i)) :
    Measurable fun x => sSup ((fun i => f i x) '' s)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x => sSup (range fun x_1 => f (↑x_1) x)

Tactic:
have : Countable s := hs.to_subtype

Result:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Countable ↑s
⊢ Measurable fun x => sSup (range fun x_1 => f (↑x_1) x)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
this : Countable ↑s
⊢ Measurable fun x => sSup (range fun x_1 => f (↑x_1) x)

Tactic:
exact .iSup fun i ↦ hf i i.2

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x => sSup ((fun i => f i x) '' s)

Tactic:
simp_rw [image_eq_range]

Result:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
f : ι → δ → α
s : Set ι
hs : s.Countable
hf : ∀ i ∈ s, Measurable (f i)
⊢ Measurable fun x => sSup (range fun x_1 => f (↑x_1) x)
-- Mathlib/Data/Fin/Basic.lean
theorem last_sub (i : Fin (n + 1)) : last n - i = Fin.rev i :=
  Fin.ext <| by rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ ↑(last n - i) = ↑i.rev

Tactic:
rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

Result:
no goals