harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_le_sum {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
  ⟨(Embedding.refl _).sigmaMap fun i =>
      Classical.choice <| by have := H i; rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this⟩

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this

Result:
no goals

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
have := H i

Result:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLintegral_compl {f : α → ℝ≥0∞} {s : Set α} (hsm : MeasurableSet s)
    (hfs : ∫⁻ x in s, f x ∂μ ≠ ∞) :
    ∫⁻ x in sᶜ, f x ∂μ = ∫⁻ x, f x ∂μ - ∫⁻ x in s, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤
⊢ ∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← lintegral_add_compl (μ := μ) f hsm, ENNReal.add_sub_cancel_left hfs]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    ∫ x, (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal

Tactic:
rw [← setIntegral_univ, setIntegral_toReal_rnDeriv hμν Set.univ]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_comm (s t : Set E) : convexJoin 𝕜 s t = convexJoin 𝕜 t s :=
  (iUnion₂_comm _).trans <| by simp_rw [convexJoin, segment_symm]

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ⋃ i₂ ∈ t, ⋃ i₁ ∈ s, segment 𝕜 i₁ i₂ = convexJoin 𝕜 t s

Tactic:
simp_rw [convexJoin, segment_symm]

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem _root_.Irreducible.addVal_pow {ϖ : R} (h : Irreducible ϖ) (n : ℕ) :
    addVal R (ϖ ^ n) = n

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDiscreteValuationRing R
ϖ : R
h : Irreducible ϖ
n : ℕ
⊢ (addVal R) (ϖ ^ n) = ↑n

Tactic:
rw [addVal_pow, addVal_uniformizer h, nsmul_one]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma covBy_iff_exists_insert : s ⋖ t ↔ ∃ a ∉ s, insert a s = t

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⋖ t ↔ ∃ a ∉ s, insert a s = t

Tactic:
simp only [← coe_covBy_coe, Set.covBy_iff_exists_insert, ← coe_inj, coe_insert, mem_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/BasicAux.lean
theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b

Proof state:
case mk
α : Type u_1
a b : α
bs : Array α
h₂ : a = b
toList✝ : List α
h : { toList := toList✝ }.toList.concat a = bs.toList.concat b
h₁ : { toList := toList✝ }.toList = bs.toList
⊢ { toList := toList✝ } = bs ∧ a = b

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
a b : α
h₂ : a = b
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.toList.concat a = { toList := toList✝ }.toList.concat b
h₁ : { toList := toList✝¹ }.toList = { toList := toList✝ }.toList
⊢ { toList := toList✝¹ } = { toList := toList✝ } ∧ a = b

Proof state:
case mk.mk
α : Type u_1
a b : α
h₂ : a = b
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.toList.concat a = { toList := toList✝ }.toList.concat b
h₁ : { toList := toList✝¹ }.toList = { toList := toList✝ }.toList
⊢ { toList := toList✝¹ } = { toList := toList✝ } ∧ a = b

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
a b : α
as bs : Array α
h : as.toList.concat a = bs.toList.concat b
⊢ as = bs ∧ a = b

Tactic:
have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h

Result:
α : Type u_1
a b : α
as bs : Array α
h : as.toList.concat a = bs.toList.concat b
h₁ : as.toList = bs.toList
h₂ : a = b
⊢ as = bs ∧ a = b

Proof state:
α : Type u_1
a b : α
as bs : Array α
h : as.toList.concat a = bs.toList.concat b
h₁ : as.toList = bs.toList
h₂ : a = b
⊢ as = bs ∧ a = b

Tactic:
cases as

Result:
case mk
α : Type u_1
a b : α
bs : Array α
h₂ : a = b
toList✝ : List α
h : { toList := toList✝ }.toList.concat a = bs.toList.concat b
h₁ : { toList := toList✝ }.toList = bs.toList
⊢ { toList := toList✝ } = bs ∧ a = b

Proof state:
α : Type u_1
a b : α
as bs : Array α
h : as.push a = bs.push b
⊢ as = bs ∧ a = b

Tactic:
simp only [push, mk.injEq] at h

Result:
α : Type u_1
a b : α
as bs : Array α
h : as.toList.concat a = bs.toList.concat b
⊢ as = bs ∧ a = b
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem constantCoeff_C (r : R) : constantCoeff (C r : MvPolynomial σ R) = r

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ constantCoeff (C r) = r

Tactic:
simp [constantCoeff_eq]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ constantCoeff (C r) = r

Tactic:
classical simp [constantCoeff_eq]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma limsup_top_eq_ciSup [Nonempty β] (hu : BddAbove (range u)) : limsup u ⊤ = ⨆ i, u i

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddAbove (range u)
⊢ limsup u ⊤ = ⨆ i, u i

Tactic:
rw [limsup, map_top, limsSup_principal_eq_csSup hu (range_nonempty _), sSup_range]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
lemma take_add : a.take (m + n) = a.take m ++ (a.drop m).take n

Proof state:
α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a = take m a ++ take n (drop m a)

Tactic:
apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n) <;>
  simp [- drop_drop]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem Tendsto.atTop_mul_atTop₀ (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun x => f x * g x

Tactic:
filter_upwards [hg.eventually (eventually_ge_atTop 0),
  hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ hg

Result:
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun x => f x * g x
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_else_true {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ h : p, x h

Proof state:
p : Prop
inst✝ : Decidable p
x : p → Prop
⊢ (if h : p then x h else True) ↔ ∀ (h : p), x h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma add_comp : (κ + η) ∘ₘ μ = κ ∘ₘ μ + η ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
⊢ ⇑(κ + η) ∘ₘ μ = ⇑κ ∘ₘ μ + ⇑η ∘ₘ μ

Tactic:
simp_rw [comp_eq_comp_const_apply, Kernel.comp_add_left, Kernel.add_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
theorem coconeOfRepresentable_naturality {P₁ P₂ : Cᵒᵖ ⥤ Type v₁} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) :
    (coconeOfRepresentable P₁).ι.app j ≫ α =
      (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type v₁
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
⊢ (coconeOfRepresentable P₁).ι.app j ≫ α = (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)

Tactic:
ext T f

Result:
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type v₁
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables P₁).obj j).obj T
⊢ ((coconeOfRepresentable P₁).ι.app j ≫ α).app T f =
    ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)).app T f

Proof state:
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type v₁
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables P₁).obj j).obj T
⊢ ((coconeOfRepresentable P₁).ι.app j ≫ α).app T f =
    ((coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)).app T f

Tactic:
simpa [coconeOfRepresentable_ι_app] using FunctorToTypes.naturality _ _ α f.op _

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n * c ≡ b [ZMOD n] :=
  calc
    a + n * c ≡ b + n * c [ZMOD n] := ha.add_right _
    _ ≡ b + 0 [ZMOD n] := (dvd_mul_right _ _).modEq_zero_int.add_left _
    _ ≡ b [ZMOD n]

Proof state:
a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ b + 0 ≡ b [ZMOD n]

Tactic:
rw [add_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc]
lemma L₀X₂ToP_comp_pullback_snd : S.L₀X₂ToP ≫ pullback.snd _ _ = S.L₀.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = S.L₀.g

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem Nontrivial.of_not_isCyclic (nc : ¬IsCyclic α) : Nontrivial α

Proof state:
α : Type u_1
inst✝ : Group α
nc : ¬Nontrivial α
⊢ IsCyclic α

Tactic:
exact @isCyclic_of_subsingleton _ _ (not_nontrivial_iff_subsingleton.mp nc)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
nc : ¬IsCyclic α
⊢ Nontrivial α

Tactic:
contrapose! nc

Result:
α : Type u_1
inst✝ : Group α
nc : ¬Nontrivial α
⊢ IsCyclic α
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_of_char_two : W.j = W.Δ'⁻¹ * W.a₁ ^ 12

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ W.j = ↑W.Δ'⁻¹ * W.a₁ ^ 12

Tactic:
rw [j, W.c₄_of_char_two, ← pow_mul]

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem IsCompact.exists_isMinOn [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)
    (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩

Result:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x ∈ s, IsMinOn f s x

Proof state:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
refine ⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩

Result:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
x✝ : β
hb : x✝ ∈ (fun a => a) '' s
⊢ x✝ ∈ s

Proof state:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : s.Nonempty
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
x✝ : β
hb : x✝ ∈ (fun a => a) '' s
⊢ x✝ ∈ s

Tactic:
rwa [(image_id' s).symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Fiber.lean
lemma Scheme.Hom.range_fiberι (f : X.Hom Y) (y : Y) :
    Set.range (f.fiberι y).base = f.base ⁻¹' {y}

Proof state:
X Y : Scheme
f : X.Hom Y
y : ↑↑Y.toPresheafedSpace
⊢ Set.range ⇑(ConcreteCategory.hom (f.fiberι y).base) = ⇑(ConcreteCategory.hom f.base) ⁻¹' {y}

Tactic:
simp [fiber, fiberι, Scheme.Pullback.range_fst, Scheme.range_fromSpecResidueField]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
lemma tsum_dirichletSummand {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
    ∑' (n : ℕ), dirichletSummandHom χ (ne_zero_of_one_lt_re hs) n = L ↗χ s

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ ∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = L (fun n => χ ↑n) s

Tactic:
simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
  LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem mem_singleton_self (a : α) : a ∈ ({a} : Multiset α)

Proof state:
α : Type u_1
a : α
⊢ a ∈ {a}

Tactic:
rw [← cons_zero]

Result:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Proof state:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Tactic:
exact mem_cons_self _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem array₃_induction (P : Array (Array (Array α)) → Prop)
    (of : ∀ (xss : List (List (List α))), P ((xss.map (fun xs => xs.map List.toArray)).map List.toArray).toArray)
    (ass : Array (Array (Array α))) : P ass

Proof state:
α : Type u_1
P : Array (Array (Array α)) → Prop
of :
  ∀ (xss : List (List (List α))), P (List.map List.toArray (List.map (fun xs => List.map List.toArray xs) xss)).toArray
ass : Array (Array (Array α))
⊢ P ass

Tactic:
specialize of ((ass.toList.map toList).map (fun as => as.map toList))

Result:
α : Type u_1
P : Array (Array (Array α)) → Prop
ass : Array (Array (Array α))
of :
  P
    (List.map List.toArray
        (List.map (fun xs => List.map List.toArray xs)
          (List.map (fun as => List.map toList as) (List.map toList ass.toList)))).toArray
⊢ P ass

Proof state:
α : Type u_1
P : Array (Array (Array α)) → Prop
ass : Array (Array (Array α))
of :
  P
    (List.map List.toArray
        (List.map (fun xs => List.map List.toArray xs)
          (List.map (fun as => List.map toList as) (List.map toList ass.toList)))).toArray
⊢ P ass

Tactic:
simpa [← toList_map, Function.comp_def, map_id] using of

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_sub_of_gt {p a b : α} (h : emultiplicity p b < emultiplicity p a) :
    emultiplicity p (a - b) = emultiplicity p b

Proof state:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
rw [sub_eq_add_neg, emultiplicity_add_of_gt] <;> rw [emultiplicity_neg]

Result:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a

Proof state:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
lemma NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra
    (S : NonUnitalStarSubalgebra R A) (h1 : (1 : A) ∈ S) :
    (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toStarSubalgebra h1).toNonUnitalStarSubalgebra = S

Tactic:
cases S

Result:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }.toStarSubalgebra
        h1).toNonUnitalStarSubalgebra =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }

Proof state:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toNonUnitalSubalgebra✝ : NonUnitalSubalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toNonUnitalSubalgebra✝.carrier → star a ∈ toNonUnitalSubalgebra✝.carrier
h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }
⊢ ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }.toStarSubalgebra
        h1).toNonUnitalStarSubalgebra =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.concaveOn (hf : UniformConcaveOn s φ f) (hφ : 0 ≤ φ) : ConcaveOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : 0 ≤ φ
⊢ ConcaveOn ℝ s f

Tactic:
simpa using hf.mono hφ

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_filter_xor (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    (∏ x ∈ s with (Xor' (p x) (q x)), f x) =
      (∏ x ∈ s with (p x ∧ ¬ q x), f x) * (∏ x ∈ s with (q x ∧ ¬ p x), f x)

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝² : CommMonoid β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ filter (fun x => Xor' (p x) (q x)) s, f x =
    (∏ x ∈ filter (fun x => p x ∧ ¬q x) s, f x) * ∏ x ∈ filter (fun x => q x ∧ ¬p x) s, f x

Tactic:
rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝² : CommMonoid β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ filter (fun x => Xor' (p x) (q x)) s, f x = ∏ x ∈ filter (fun a => p a ∧ ¬q a ∨ q a ∧ ¬p a) s, f x

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝² : CommMonoid β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ filter (fun x => Xor' (p x) (q x)) s, f x =
    (∏ x ∈ filter (fun x => p x ∧ ¬q x) s, f x) * ∏ x ∈ filter (fun x => q x ∧ ¬p x) s, f x

Tactic:
classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝² : CommMonoid β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ filter (fun x => Xor' (p x) (q x)) s, f x = ∏ x ∈ filter (fun a => p a ∧ ¬q a ∨ q a ∧ ¬p a) s, f x

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝² : CommMonoid β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ filter (fun x => Xor' (p x) (q x)) s, f x = ∏ x ∈ filter (fun a => p a ∧ ¬q a ∨ q a ∧ ¬p a) s, f x

Tactic:
simp only [Xor']

Result:
no goals
-- Mathlib/Order/Monotone/Defs.lean
theorem StrictMono.prod_map (hf : StrictMono f) (hg : StrictMono g) : StrictMono (Prod.map f g) :=
  fun a b ↦ by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.monotone.imp) (And.imp hf.monotone.imp hg.imp)

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b

Tactic:
simp only [Prod.lt_iff]

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g a).fst < (Prod.map f g b).fst ∧ (Prod.map f g a).snd ≤ (Prod.map f g b).snd ∨
      (Prod.map f g a).fst ≤ (Prod.map f g b).fst ∧ (Prod.map f g a).snd < (Prod.map f g b).snd
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_nonempty_iff : (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
rw [← coe_nonempty, coe_image₂]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image2 f ↑s ↑t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image2 f ↑s ↑t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
exact image2_nonempty_iff

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquivOfAlgEquiv_eq (x : R) :
    algEquivOfAlgEquiv S Q h H ((algebraMap R S) x) = algebraMap P Q (h x)

Proof state:
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : R
⊢ (algEquivOfAlgEquiv S Q h H) ((algebraMap R S) x) = (algebraMap P Q) (h x)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_zero_of_invariant (h : IsFundamentalDomain G s μ) (t : Set α)
    (ht : ∀ g : G, g • t = t) (hts : μ (t ∩ s) = 0) : μ t = 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ ∑' (g : G), μ (g • t ∩ s) = 0

Tactic:
simp [ht, hts]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ μ t = 0

Tactic:
rw [measure_eq_tsum h]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
t : Set α
ht : ∀ (g : G), g • t = t
hts : μ (t ∩ s) = 0
⊢ ∑' (g : G), μ (g • t ∩ s) = 0
-- Mathlib/Analysis/Complex/UnitDisc/Basic.lean
theorem coe_ne_one (z : 𝔻) : (z : ℂ) ≠ 1 :=
  ne_of_apply_ne (‖·‖) <| by simp [z.norm_ne_one]

Proof state:
z : 𝔻
⊢ (fun x => ‖x‖) ↑z ≠ (fun x => ‖x‖) 1

Tactic:
simp [z.norm_ne_one]

Result:
no goals