harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/TraceForm.lean
@[simp]
lemma traceForm_genWeightSpace_eq [Module.Free R M]
    [IsDomain R] [IsPrincipalIdealRing R]
    [LieRing.IsNilpotent L] [IsNoetherian R M] [LinearWeights R L M] (χ : L → R) (x y : L) :
    traceForm R L (genWeightSpace M χ) x y = finrank R (genWeightSpace M χ) • (χ x * χ y)

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
inst✝⁵ : Free R M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • χ x • ↑d = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : ((traceForm R L ↥(shiftedGenWeightSpace R L M χ)) x) y = (0 x) y
⊢ ((traceForm R L ↥(genWeightSpace M χ)) x) y = d • (χ x * χ y)

Tactic:
rwa [LinearMap.zero_apply, LinearMap.zero_apply, traceForm_apply_apply,
  shiftedGenWeightSpace.toEnd_eq, shiftedGenWeightSpace.toEnd_eq,
  ← LinearEquiv.conj_comp, LinearMap.trace_conj', LinearMap.comp_sub, LinearMap.sub_comp,
  LinearMap.sub_comp, map_sub, map_sub, map_sub, LinearMap.comp_smul, LinearMap.smul_comp,
  LinearMap.comp_id, LinearMap.id_comp, LinearMap.map_smul, LinearMap.map_smul,
  trace_toEnd_genWeightSpace, trace_toEnd_genWeightSpace,
  LinearMap.comp_smul, LinearMap.smul_comp, LinearMap.id_comp, map_smul, map_smul,
  LinearMap.trace_id, ← traceForm_apply_apply, h₁, h₂, sub_zero, sub_eq_zero] at this

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_mul (n m : ℕ) :
    ascPochhammer S n * (ascPochhammer S m).comp (X + (n : S[X])) = ascPochhammer S (n + m)

Proof state:
case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer S n * (ascPochhammer S 0).comp (X + ↑n) = ascPochhammer S (n + 0)

Tactic:
simp

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n m : ℕ
⊢ ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)

Tactic:
induction' m with m ih

Result:
case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer S n * (ascPochhammer S 0).comp (X + ↑n) = ascPochhammer S (n + 0)

case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * (ascPochhammer S (m + 1)).comp (X + ↑n) = ascPochhammer S (n + (m + 1))

Proof state:
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : ascPochhammer S n * (ascPochhammer S m).comp (X + ↑n) = ascPochhammer S (n + m)
⊢ ascPochhammer S n * (ascPochhammer S (m + 1)).comp (X + ↑n) = ascPochhammer S (n + (m + 1))

Tactic:
rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
  ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma span_mono {s t : Set R} (h : s ⊆ t) : span s ≤ span t

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
⊢ span s ≤ span t

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : x ∈ span s
⊢ x ∈ span t

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : x ∈ span s
⊢ x ∈ span t

Tactic:
rw [mem_span_iff] at hx ⊢

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I
⊢ ∀ (I : TwoSidedIdeal R), t ⊆ ↑I → x ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
hx : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I
⊢ ∀ (I : TwoSidedIdeal R), t ⊆ ↑I → x ∈ I

Tactic:
exact fun I hI => hx I <| h.trans hI

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_reverseAux (ctx : Context) (p q : Poly) : denote ctx (List.reverseAux p q) = denote ctx (p ++ q)

Proof state:
ctx : Context
p q : Poly
⊢ denote ctx ([].reverseAux q) = denote ctx ([] ++ q)

Tactic:
simp [List.reverseAux]

Result:
no goals

Proof state:
ctx : Context
p✝ q : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (((k, v) :: p).reverseAux q) = denote ctx ((k, v) :: p ++ q)

Tactic:
simp [List.reverseAux, denote_reverseAux]

Result:
no goals

Proof state:
ctx : Context
p q : Poly
⊢ denote ctx (List.reverseAux p q) = denote ctx (p ++ q)

Tactic:
match p with
| [] => simp [List.reverseAux]
| (k, v) :: p => simp [List.reverseAux, denote_reverseAux]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_neg (x : ℝ≥0∞) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹

Proof state:
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case coe
y : ℝ
x : ℝ≥0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
by_cases h : x = 0

Result:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Proof state:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

Result:
no goals

Proof state:
case top
y : ℝ
⊢ ⊤ ^ (-y) = (⊤ ^ y)⁻¹

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]

Result:
no goals

Proof state:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
have A : x ^ y ≠ 0 := by simp [h]

Result:
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Proof state:
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
/-- The action of `R` on `P.Cotangent` for an `R`-extension `P → S`. -/
@[simp]
lemma Cotangent.val_smul'' (r : R) (x : P.Cotangent) : (r • x).val = r • x.val

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : R
x : P.Cotangent
⊢ (r • x).val = r • x.val

Tactic:
rw [← algebraMap_smul P.Ring, val_smul', algebraMap_smul]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem isSome_iff : ∀ {I : WithBot (Box ι)}, I.isSome ↔ (I : Set (ι → ℝ)).Nonempty
  | ⊥ => by
    erw [Option.isSome]
    simp
  | (I : Box ι) => by
    erw [Option.isSome]
    simp [I.nonempty_coe]

Proof state:
ι : Type u_1
⊢ false = true ↔ (↑⊥).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
⊢ Option.isSome ⊥ = true ↔ (↑⊥).Nonempty

Tactic:
erw [Option.isSome]

Result:
ι : Type u_1
⊢ false = true ↔ (↑⊥).Nonempty

Proof state:
ι : Type u_1
I : Box ι
⊢ true = true ↔ (↑↑I).Nonempty

Tactic:
simp [I.nonempty_coe]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
⊢ Option.isSome ↑I = true ↔ (↑↑I).Nonempty

Tactic:
erw [Option.isSome]

Result:
ι : Type u_1
I : Box ι
⊢ true = true ↔ (↑↑I).Nonempty
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_sup_le {K₀ : PositiveCompacts G} (K₁ K₂ : Compacts G) :
    chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)

Tactic:
apply continuous_iff_isClosed.mp this

Result:
case a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ IsClosed (Ici 0)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂

Tactic:
have : Continuous eval := by
  exact ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂
-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem volume_regionBetween_eq_integral' [SigmaFinite μ] (f_int : IntegrableOn f s μ)
    (g_int : IntegrableOn g s μ) (hs : MeasurableSet s) (hfg : f ≤ᵐ[μ.restrict s] g) :
    μ.prod volume (regionBetween f g s) = ENNReal.ofReal (∫ y in s, (g - f) y ∂μ)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
⊢ (μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
  hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal
⊢ (μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal
⊢ (μ.prod volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs,
  integral_congr_ae h, lintegral_congr_ae,
  lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun a => ↑(g a - f a).toNNReal

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun x => ↑(g x - f x).toNNReal
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun a => ↑(g a - f a).toNNReal

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem ext_aux [Inhabited (M F)] [DecidableEq F.A] {n : ℕ} (x y z : M F) (hx : Agree' n z x)
    (hy : Agree' n z y) (hrec : ∀ ps : Path F, n = ps.length → iselect ps x = iselect ps y) :
    x.approx (n + 1) = y.approx (n + 1)

Proof state:
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
n_ih✝ : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → x.approx (n + 1) = y.approx (n + 1)
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk ⟨a, f₃⟩ = M.mk ⟨a, f₃⟩
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
exact hrec

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
@[simp] lemma upShadow_compls : ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Tactic:
refine (compl_involutive.toPerm _).exists_congr_left.trans ?_

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∉ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b) = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ

Tactic:
simp only [mem_image, exists_prop, mem_shadow_iff, mem_upShadow_iff, mem_compls]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∉ s_1, insert a s_1 = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
⊢ ∂⁺ 𝒜ᶜˢ = (∂ 𝒜)ᶜˢ

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ ∂⁺ 𝒜ᶜˢ ↔ s ∈ (∂ 𝒜)ᶜˢ

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ b,
      ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧
        ∃ a ∉ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b,
          insert a ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b) = s) ↔
    ∃ s_1 ∈ 𝒜, ∃ a ∈ s_1, s_1.erase a = sᶜ

Tactic:
simp [← compl_involutive.eq_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.if' {s : Set α} {p : α → Prop} {f g : α → β} [∀ a, Decidable (p a)]
    (hpf : ∀ a ∈ s ∩ frontier { a | p a },
      Tendsto f (𝓝[s ∩ { a | p a }] a) (𝓝 <| if p a then f a else g a))
    (hpg :
      ∀ a ∈ s ∩ frontier { a | p a },
        Tendsto g (𝓝[s ∩ { a | ¬p a }] a) (𝓝 <| if p a then f a else g a))
    (hf : ContinuousOn f <| s ∩ { a | p a }) (hg : ContinuousOn g <| s ∩ { a | ¬p a }) :
    ContinuousOn (fun a => if p a then f a else g a) s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx : x ∈ s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ
hx' : x ∉ frontier {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x

Tactic:
rcases hx with hx | hx

Result:
case neg.inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x

case neg.inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a} ∪ s ∩ {a | p a}ᶜ) x

Proof state:
case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
this : x ∉ closure {a | p a}ᶜ
⊢ ContinuousWithinAt (fun a => if p a then f a else g a) (s ∩ {a | p a}ᶜ) x

Tactic:
exact continuousWithinAt_of_not_mem_closure fun h =>
  this (closure_inter_subset_inter_closure _ _ h).2

Result:
no goals
-- Mathlib/Data/Set/Function.lean
protected lemma LeftInvOn.extendDomain (h : LeftInvOn g₁ g₂ s) :
    LeftInvOn (g₁.extendDomain f) (g₂.extendDomain f) ((↑) ∘ f '' s)

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
⊢ LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_one_iff_mem_unitary {d : ℤ} {a : ℤ√d} : a.norm = 1 ↔ a ∈ unitary (ℤ√d)

Proof state:
d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ ↑a.norm = 1

Tactic:
norm_cast

Result:
no goals

Proof state:
d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ a ∈ unitary (ℤ√d)

Tactic:
rw [unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]

Result:
d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ ↑a.norm = 1
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem lift_sub_lift {X Y : C} (a b c d : X ⟶ Y) :
    prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d)

Tactic:
simp only [sub_def]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)

Proof state:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

Tactic:
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b) (prod.lift c d) ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ)

Tactic:
ext

Result:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.fst =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd

Proof state:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ (prod.lift (prod.lift a b) (prod.lift c d) ≫ σ) ≫ prod.snd =
    prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.snd

Tactic:
rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n

Proof state:
w n : Nat
l : BitVec w
⊢ l[n]? = none ↔ w ≤ n

Tactic:
simp only [getElem?_def]

Result:
w n : Nat
l : BitVec w
⊢ (if h : n < w then some l[n] else none) = none ↔ w ≤ n

Proof state:
case isFalse
w n : Nat
l : BitVec w
h✝ : ¬n < w
⊢ none = none ↔ w ≤ n

Tactic:
simp

Result:
case isFalse
w n : Nat
l : BitVec w
h✝ : ¬n < w
⊢ w ≤ n

Proof state:
case isTrue
w n : Nat
l : BitVec w
h✝ : n < w
⊢ some l[n] = none ↔ w ≤ n

Tactic:
simp_all

Result:
no goals

Proof state:
case isFalse
w n : Nat
l : BitVec w
h✝ : ¬n < w
⊢ w ≤ n

Tactic:
omega

Result:
no goals

Proof state:
w n : Nat
l : BitVec w
⊢ (if h : n < w then some l[n] else none) = none ↔ w ≤ n

Tactic:
split

Result:
case isTrue
w n : Nat
l : BitVec w
h✝ : n < w
⊢ some l[n] = none ↔ w ≤ n

case isFalse
w n : Nat
l : BitVec w
h✝ : ¬n < w
⊢ none = none ↔ w ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_of_get?_eq_some {xs : List α} (w : xs.get? (xs.findIdx p) = some y) : p y :=
  findIdx_of_getElem?_eq_some (by simpa using w)

Proof state:
α : Type u_1
p : α → Bool
y : α
xs : List α
w : xs.get? (findIdx p xs) = some y
⊢ ?m.117177[findIdx p ?m.117177]? = some y

Tactic:
simpa using w

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem foldr_eq_foldr_finRange (f : Fin n → α → α) (x) :
    foldr n f x = (List.finRange n).foldr f x

Proof state:
n : Nat
α : Type u_1
f : Fin n → α → α
x : α
⊢ foldr n f x = List.foldr f x (List.finRange n)

Tactic:
induction n with
| zero => rw [foldr_zero, List.finRange_zero, List.foldr_nil]
| succ n ih => rw [foldr_succ, ih, List.finRange_succ, List.foldr_cons, List.foldr_map]

Result:
no goals

Proof state:
case zero
α : Type u_1
x : α
f : Fin 0 → α → α
⊢ foldr 0 f x = List.foldr f x (List.finRange 0)

Tactic:
rw [foldr_zero, List.finRange_zero, List.foldr_nil]

Result:
no goals

Proof state:
case succ
α : Type u_1
x : α
n : Nat
ih : ∀ (f : Fin n → α → α), foldr n f x = List.foldr f x (List.finRange n)
f : Fin (n + 1) → α → α
⊢ foldr (n + 1) f x = List.foldr f x (List.finRange (n + 1))

Tactic:
rw [foldr_succ, ih, List.finRange_succ, List.foldr_cons, List.foldr_map]

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

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

Tactic:
rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem basis_repr_norm_le_const_mul_house (α : 𝓞 K) (i : K →+* ℂ) :
    ‖(((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ)‖  ≤
      (c K) * house (algebraMap (𝓞 K) K α)

Proof state:
case calc_2.h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∀ i ∈ univ,
    ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) i‖ ≤
      ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
intros j _

Result:
case calc_2.h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
a✝ : j ∈ univ
⊢ ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

Proof state:
case calc_2
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ j : K →+* ℂ, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ∑ x : K →+* ℂ, ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
apply sum_le_sum

Result:
case calc_2.h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∀ i ∈ univ,
    ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) i‖ ≤
      ‖fun i j => (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)