harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma toReal_klDiv_eq_integral_klFun (h : μ ≪ ν) :
    (klDiv μ ν).toReal = ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [integral_undef]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = 0

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
exact integral_nonneg fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = 0

Tactic:
rw [klDiv_of_not_integrable h_int, ENNReal.top_toReal]

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff h]

Result:
no goals

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

Tactic:
by_cases h_int : Integrable (llr μ ν) μ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [klDiv_eq_integral_klFun, if_pos ⟨h, h_int⟩, ENNReal.toReal_ofReal]

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem haveLebesgueDecomposition_mk' (μ : Measure α) {f : α → ℝ} (hf : Measurable f)
    (hfi : Integrable f μ) (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) (hadd : s = t + μ.withDensityᵥ f) :
    s.HaveLebesgueDecomposition μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ Measurable (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2 ∧
    (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 ⟂ₘ μ ∧
      s.toJordanDecomposition.posPart =
        (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 +
          μ.withDensity (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2

Tactic:
refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩

Result:
case h
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart =
    (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).1 +
      μ.withDensity (t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)).2

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ

Tactic:
rw [mutuallySingular_ennreal_iff] at htμ

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_cons : a ∈ (b :: l) ↔ a = b ∨ a ∈ l :=
  ⟨fun h => by cases h <;> simp [Membership.mem, *],
   fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption⟩

Proof state:
α✝ : Type u_1
b : α✝
l : List α✝
a : α✝
⊢ a ∈ a :: l

Tactic:
constructor

Result:
no goals

Proof state:
α✝ : Type u_1
b : α✝
l : List α✝
a : α✝
h : a ∈ b :: l
⊢ a = b ∨ a ∈ l

Tactic:
cases h <;> simp [Membership.mem, *]

Result:
no goals

Proof state:
α✝ : Type u_1
b✝ : α✝
l : List α✝
a b : α✝
h : a ∈ l
⊢ a ∈ b :: l

Tactic:
constructor

Result:
case a
α✝ : Type u_1
b✝ : α✝
l : List α✝
a b : α✝
h : a ∈ l
⊢ Mem a l

Proof state:
case a
α✝ : Type u_1
b✝ : α✝
l : List α✝
a b : α✝
h : a ∈ l
⊢ Mem a l

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma infs_compls_eq_diffs (s t : Finset α) : s ⊼ tᶜˢ = s \\ t

Proof state:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ⊼ tᶜˢ ↔ a✝ ∈ s \\ t

Tactic:
simp [sdiff_eq]

Result:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊼ tᶜˢ = s \\ t

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ s ⊼ tᶜˢ ↔ a✝ ∈ s \\ t

Proof state:
case h
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_eq_pow_single [DecidableEq α] (a : α) (h : ∀ a' ≠ a, a' ∈ s → a' = 1) :
    s.prod = a ^ s.count a

Proof state:
case h
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
inst✝ : DecidableEq α
a : α
a✝ : List α
h : ∀ (a' : α), a' ≠ a → a' ∈ ⟦a✝⟧ → a' = 1
⊢ prod ⟦a✝⟧ = a ^ count a ⟦a✝⟧

Tactic:
simp [List.prod_eq_pow_single a h]

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
inst✝ : DecidableEq α
a : α
h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1
⊢ s.prod = a ^ count a s

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
inst✝ : DecidableEq α
a : α
a✝ : List α
h : ∀ (a' : α), a' ≠ a → a' ∈ ⟦a✝⟧ → a' = 1
⊢ prod ⟦a✝⟧ = a ^ count a ⟦a✝⟧
-- Mathlib/Probability/Moments/Basic.lean
lemma exp_cgf [IsProbabilityMeasure μ] (hX : Integrable (fun ω ↦ exp (t * X ω)) μ) :
    exp (cgf X μ t) = mgf X μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsProbabilityMeasure μ
hX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (cgf X μ t) = mgf X μ t

Tactic:
rw [cgf, exp_log (mgf_pos hX)]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittNeg_zero : wittNeg p 0 = -X (0, 0)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittNeg p 0) = (map (Int.castRingHom ℚ)) (-X (0, 0))

Tactic:
simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
  map_neg, bind₁_X_right, map_wittStructureInt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittNeg p 0 = -X (0, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittNeg p 0) = (map (Int.castRingHom ℚ)) (-X (0, 0))
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem P_mk (x : F (M F)) : AllAgree (Approx.sMk x)
  | 0 => by constructor
  | succ n => by
    constructor
    introv
    apply (x.2 i).consistent

Proof state:
F : PFunctor.{u}
x : ↑F F.M
⊢ Agree (Approx.sMk x 0) (Approx.sMk x (succ 0))

Tactic:
constructor

Result:
no goals

Proof state:
case a
F : PFunctor.{u}
x : ↑F F.M
n : ℕ
i : F.B x.fst
⊢ Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))

Tactic:
apply (x.2 i).consistent

Result:
no goals

Proof state:
case a
F : PFunctor.{u}
x : ↑F F.M
n : ℕ
⊢ ∀ (i : F.B x.fst), Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))

Tactic:
introv

Result:
case a
F : PFunctor.{u}
x : ↑F F.M
n : ℕ
i : F.B x.fst
⊢ Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))

Proof state:
F : PFunctor.{u}
x : ↑F F.M
n : ℕ
⊢ Agree (Approx.sMk x n.succ) (Approx.sMk x n.succ.succ)

Tactic:
constructor

Result:
case a
F : PFunctor.{u}
x : ↑F F.M
n : ℕ
⊢ ∀ (i : F.B x.fst), Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
/-- Every property local at the target can be associated with an affine target property.
This is not an instance as the associated property can often take on simpler forms. -/
lemma of_isLocalAtTarget (P) [IsLocalAtTarget P] :
    HasAffineProperty P (AffineTargetMorphismProperty.of P) where
  isLocal_affineProperty := inferInstance
  eq_targetAffineLocally'

Proof state:
case h.mpr
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f

Tactic:
exact IsLocalAtTarget.of_openCover (P := P) Y.affineCover
  fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

Result:
no goals

Proof state:
case h
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
constructor

Result:
case h.mp
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f

case h.mpr
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f

Proof state:
case h.mp
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f → targetAffineLocally (AffineTargetMorphismProperty.of P) f

Tactic:
intro hf ⟨U, hU⟩

Result:
case h.mp
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (f ∣_ ↑⟨U, hU⟩)

Proof state:
case h.mp
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : P f
U : Y.Opens
hU : U ∈ Y.affineOpens
⊢ AffineTargetMorphismProperty.of P (f ∣_ ↑⟨U, hU⟩)

Tactic:
exact IsLocalAtTarget.restrict hf _

Result:
no goals

Proof state:
case h.mpr
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f

Tactic:
intro hf

Result:
case h.mpr
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
hf : targetAffineLocally (AffineTargetMorphismProperty.of P) f
⊢ P f

Proof state:
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
⊢ P = targetAffineLocally (AffineTargetMorphismProperty.of P)

Tactic:
ext X Y f

Result:
case h
P : MorphismProperty Scheme
inst✝ : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ targetAffineLocally (AffineTargetMorphismProperty.of P) f
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_eq_image : s.sym2 = (s ×ˢ s).image Sym2.mk

Proof state:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
h : x ∈ s ∧ y ∈ s
⊢ (x, y) ∈ s ×ˢ s ∧ s(x, y) = s(x, y)

Tactic:
simp only [mem_product, h, and_self, true_and]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym2 = image Sym2.mk (s ×ˢ s)

Tactic:
ext z

Result:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
⊢ z ∈ s.sym2 ↔ z ∈ image Sym2.mk (s ×ˢ s)

Proof state:
case h.mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
h : x ∈ s ∧ y ∈ s
⊢ ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

Tactic:
use (x, y)

Result:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
h : x ∈ s ∧ y ∈ s
⊢ (x, y) ∈ s ×ˢ s ∧ s(x, y) = s(x, y)

Proof state:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
⊢ z ∈ s.sym2 ↔ z ∈ image Sym2.mk (s ×ˢ s)

Tactic:
refine z.ind fun x y ↦ ?_

Result:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ s.sym2 ↔ s(x, y) ∈ image Sym2.mk (s ×ˢ s)

Proof state:
case h.mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ (∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)) → x ∈ s ∧ y ∈ s

Tactic:
rintro ⟨⟨a, b⟩, h⟩

Result:
case h.mpr.intro.mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y a b : α
h : (a, b) ∈ s ×ˢ s ∧ s(a, b) = s(x, y)
⊢ x ∈ s ∧ y ∈ s

Proof state:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ x ∈ s ∧ y ∈ s ↔ ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

Tactic:
constructor

Result:
case h.mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ x ∈ s ∧ y ∈ s → ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

case h.mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ (∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)) → x ∈ s ∧ y ∈ s

Proof state:
case h.mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ x ∈ s ∧ y ∈ s → ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

Tactic:
intro h

Result:
case h.mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
h : x ∈ s ∧ y ∈ s
⊢ ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

Proof state:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ s(x, y) ∈ s.sym2 ↔ s(x, y) ∈ image Sym2.mk (s ×ˢ s)

Tactic:
rw [mk_mem_sym2_iff, mem_image]

Result:
case h
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y : α
⊢ x ∈ s ∧ y ∈ s ↔ ∃ a ∈ s ×ˢ s, Sym2.mk a = s(x, y)

Proof state:
case h.mpr.intro.mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y a b : α
h : (a, b) ∈ s ×ˢ s ∧ s(a, b) = s(x, y)
⊢ x ∈ s ∧ y ∈ s

Tactic:
simp only [mem_product, Sym2.eq_iff] at h

Result:
case h.mpr.intro.mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y a b : α
h : (a ∈ s ∧ b ∈ s) ∧ (a = x ∧ b = y ∨ a = y ∧ b = x)
⊢ x ∈ s ∧ y ∈ s

Proof state:
case h.mpr.intro.mk
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
z : Sym2 α
x y a b : α
h : (a ∈ s ∧ b ∈ s) ∧ (a = x ∧ b = y ∨ a = y ∧ b = x)
⊢ x ∈ s ∧ y ∈ s

Tactic:
obtain ⟨h, (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)⟩ := h
  <;> simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_perm [DecidableEq ι] [Fintype ι] (v : ι → M) (σ : Equiv.Perm ι) :
    g (v ∘ σ) = Equiv.Perm.sign σ • g v

Proof state:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
f✝ : Equiv.Perm ι
x✝ y✝ : ι
a✝¹ : x✝ ≠ y✝
a✝ : g (v ∘ ⇑f✝) = Equiv.Perm.sign f✝ • g v
⊢ g (v ∘ ⇑(f✝ * Equiv.swap x✝ y✝)) = Equiv.Perm.sign (f✝ * Equiv.swap x✝ y✝) • g v

Tactic:
rename_i s x y hxy hI

Result:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
s : Equiv.Perm ι
x y : ι
hxy : x ≠ y
hI : g (v ∘ ⇑s) = Equiv.Perm.sign s • g v
⊢ g (v ∘ ⇑(s * Equiv.swap x y)) = Equiv.Perm.sign (s * Equiv.swap x y) • g v

Proof state:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
⊢ g (v ∘ ⇑1) = Equiv.Perm.sign 1 • g v

Tactic:
simp

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
s : Equiv.Perm ι
x y : ι
hxy : x ≠ y
hI : g (v ∘ ⇑s) = Equiv.Perm.sign s • g v
⊢ g (v ∘ ⇑(s * Equiv.swap x y)) = Equiv.Perm.sign (s * Equiv.swap x y) • g v

Tactic:
simpa [← Function.comp_assoc, g.map_swap (v ∘ s) hxy,
  Equiv.Perm.sign_swap hxy, -Equiv.Perm.sign_swap'] using hI

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
σ : Equiv.Perm ι
⊢ g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v

Tactic:
induction σ using Equiv.Perm.swap_induction_on'

Result:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
⊢ g (v ∘ ⇑1) = Equiv.Perm.sign 1 • g v

case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
f✝ : Equiv.Perm ι
x✝ y✝ : ι
a✝¹ : x✝ ≠ y✝
a✝ : g (v ∘ ⇑f✝) = Equiv.Perm.sign f✝ • g v
⊢ g (v ∘ ⇑(f✝ * Equiv.swap x✝ y✝)) = Equiv.Perm.sign (f✝ * Equiv.swap x✝ y✝) • g v
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
    gaussianReal μ v s = ENNReal.ofReal (∫ x in s, gaussianPDFReal μ v x)

Proof state:
case f_nn
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᶠ[ae (ℙ.restrict s)] gaussianPDFReal μ v

Tactic:
exact ae_of_all _ (gaussianPDFReal_nonneg _ _)

Result:
no goals

Proof state:
case hfi
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ Integrable (gaussianPDFReal μ v) (ℙ.restrict s)

Tactic:
exact (integrable_gaussianPDFReal _ _).restrict

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (gaussianReal μ v) s = ENNReal.ofReal (∫ (x : ℝ) in s, gaussianPDFReal μ v x)

Tactic:
rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)

case hfi
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ Integrable (gaussianPDFReal μ v) (ℙ.restrict s)

case f_nn
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᶠ[ae (ℙ.restrict s)] gaussianPDFReal μ v

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) : ((Ico n m).filter fun x => l ≤ x) = [] :=
  filter_eq_nil_iff.2 fun k hk => by
    rw [decide_eq_true_eq]
    exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

Proof state:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Result:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k

Proof state:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k

Tactic:
exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
theorem δ₀_mk₂_eq : (nerve C).δ 0 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ g :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 0 ((ComposableArrows.mk₁ g).precomp f)) = g

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 0 (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 0 ((ComposableArrows.mk₁ g).precomp f)) = g
-- Mathlib/Logic/Equiv/Fin.lean
theorem finRotate_apply_zero : finRotate n.succ 0 = 1

Proof state:
n : ℕ
⊢ (finRotate n.succ) 0 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Single.lean
@[reassoc (attr := simp)]
lemma single_map_singleObjApplyIso_hom (j : J) {X Y : C} (f : X ⟶ Y) :
    (single j).map f j ≫ (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom ≫ f

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
⊢ (single j).map f j ≫ (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom ≫ f

Tactic:
apply single_map_singleObjApplyIsoOfEq_hom

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem toSubring_injective {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] :
    Function.Injective (toSubring : Subalgebra R A → Subring A) := fun S T h =>
  ext fun x => by rw [← mem_toSubring, ← mem_toSubring, h]

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubring, ← mem_toSubring, h]

Result:
no goals