harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.noSibling_combine (le) (s : Heap α) :
    (s.combine le).NoSibling

Proof state:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)).NoSibling

Tactic:
exact noSibling_merge _ _ _

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s✝ x✝¹ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
x✝ :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ (node a✝¹ child✝¹ (node a✝ child✝ s)).NoSibling

Tactic:
rename_i h

Result:
α : Type u_1
le : α → α → Bool
s✝ x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
h :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ (node a✝¹ child✝¹ (node a✝ child✝ s)).NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
a✝ : α
child✝ : Heap α
x✝ :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s : Heap α),
    node a✝ child✝ nil = node a child (node a_1 child_1 s) → False
⊢ (node a✝ child✝ nil).NoSibling

Tactic:
constructor

Result:
no goals

Proof state:
case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ s.NoSibling

Tactic:
match s with
| nil | node _ _ nil => constructor
| node _ _ (node _ _ s) => rename_i h; exact (h _ _ _ _ _ rfl).elim

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s✝ x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s : Heap α
h :
  ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α),
    node a✝¹ child✝¹ (node a✝ child✝ s) = node a child (node a_1 child_1 s_1) → False
⊢ (node a✝¹ child✝¹ (node a✝ child✝ s)).NoSibling

Tactic:
exact (h _ _ _ _ _ rfl).elim

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (match s with
    | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
    | h => h).NoSibling

Tactic:
split

Result:
case h_1
α : Type u_1
le : α → α → Bool
x✝ : Heap α
a✝¹ : α
child✝¹ : Heap α
a✝ : α
child✝ s✝ : Heap α
⊢ (merge le (merge le (node a✝¹ child✝¹ (node a✝ child✝ s✝)) (node a✝ child✝ s✝)) (combine le s✝)).NoSibling

case h_2
α : Type u_1
le : α → α → Bool
s x✝¹ : Heap α
x✝ : ∀ (a : α) (child : Heap α) (a_1 : α) (child_1 s_1 : Heap α), s = node a child (node a_1 child_1 s_1) → False
⊢ s.NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (combine le s).NoSibling

Tactic:
unfold combine

Result:
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ (match s with
    | h₁@h_1:(node a child h₂@h:(node a_1 child_1 s)) => merge le (merge le h₁ h₂) (combine le s)
    | h => h).NoSibling
-- Mathlib/RingTheory/Flat/Stability.lean
theorem of_isLocalizedModule [Flat R M] (S : Submonoid R) [IsLocalization S Rp]
    (f : M →ₗ[R] Mp) [h : IsLocalizedModule S f] : Flat Rp Mp

Proof state:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ IsBaseChange Rp ?m.26775

R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ M →ₗ[R] Mp

Tactic:
exact (isLocalizedModule_iff_isBaseChange S Rp f).mp h

Result:
no goals

Proof state:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ Flat Rp Mp

Tactic:
fapply Flat.isBaseChange (R := R) (M := M) (S := Rp) (N := Mp)

Result:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ IsBaseChange Rp ?m.26775

R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ M →ₗ[R] Mp
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem evenOdd_comap_reverse (n : ZMod 2) :
    (evenOdd Q n).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = evenOdd Q n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.comap reverse (evenOdd Q n) = evenOdd Q n

Tactic:
rw [← submodule_map_reverse_eq_comap, evenOdd_map_reverse]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_add_iff_add_lt_ne_self : Principal (· + ·) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a :=
  ⟨fun ha _ hb _ hc => (ha hb hc).ne, fun H => by
    by_contra! ha
    rcases exists_lt_add_of_not_principal_add ha with ⟨b, hb, c, hc, rfl⟩
    exact (H b hb c hc).irrefl⟩

Proof state:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬Principal (fun x1 x2 => x1 + x2) a
⊢ False

Tactic:
rcases exists_lt_add_of_not_principal_add ha with ⟨b, hb, c, hc, rfl⟩

Result:
case intro.intro.intro.intro
b c : Ordinal.{u}
H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c
ha : ¬Principal (fun x1 x2 => x1 + x2) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False

Proof state:
case intro.intro.intro.intro
b c : Ordinal.{u}
H : ∀ b_1 < b + c, ∀ c_1 < b + c, b_1 + c_1 ≠ b + c
ha : ¬Principal (fun x1 x2 => x1 + x2) (b + c)
hb : b < b + c
hc : c < b + c
⊢ False

Tactic:
exact (H b hb c hc).irrefl

Result:
no goals

Proof state:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
⊢ Principal (fun x1 x2 => x1 + x2) a

Tactic:
by_contra! ha

Result:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬Principal (fun x1 x2 => x1 + x2) a
⊢ False
-- Mathlib/Algebra/CharZero/Quotient.lean
theorem zmultiples_nsmul_eq_nsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {n : ℕ} (hz : n ≠ 0) :
    n • ψ = n • θ ↔ ∃ k : Fin n, ψ = θ + (k : ℕ) • (p / n : R)

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
  zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_natCast]

Result:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Proof state:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ (∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
/-- If the pullback comparison map for `G` at `(f,g)` is an isomorphism, then `G` preserves the
pullback of `(f,g)`. -/
lemma PreservesPullback.of_iso_comparison [i : IsIso (pullbackComparison G f g)] :
    PreservesLimit (cospan f g) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (PullbackCone.mk (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) ⋯)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (PullbackCone.mk (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) ⋯)

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (cospan (G.map f) (G.map g))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ PreservesLimit (cospan f g) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (pullbackIsPullback f g)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯))
-- Mathlib/Data/Int/AbsoluteValue.lean
theorem AbsoluteValue.map_units_int (abv : AbsoluteValue ℤ S) (x : ℤˣ) : abv x = 1

Proof state:
S : Type u_2
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ abv ↑x = 1

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    m.size ≤ (m.insert k v).size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ m.size ≤ (m.insert k v).size

Tactic:
simp_to_raw using Raw₀.size_le_size_insert ⟨m, _⟩ h

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma inv_hom_apply {X Y : CommGrp} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : CommGrp
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_caratheodory : p.toOuterMeasure.caratheodory = ⊤

Proof state:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory
y : α
hy : (fun i => (p i • dirac i).caratheodory) y = x
⊢ ⊤ ≤ x

Tactic:
exact
  ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory
⊢ ⊤ ≤ x

Tactic:
have ⟨y, hy⟩ := hx

Result:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory
y : α
hy : (fun i => (p i • dirac i).caratheodory) y = x
⊢ ⊤ ≤ x

Proof state:
α : Type u_1
p : PMF α
⊢ p.toOuterMeasure.caratheodory = ⊤

Tactic:
refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)

Result:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => (p i • dirac i).caratheodory
⊢ ⊤ ≤ x
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem iSup_approx_apply [TopologicalSpace β] [CompleteLattice β] [OrderClosedTopology β] [Zero β]
    [MeasurableSpace β] [OpensMeasurableSpace β] (i : ℕ → β) (f : α → β) (a : α) (hf : Measurable f)
    (h_zero : (0 : β) = ⊥) : ⨆ n, (approx i f n : α →ₛ β) a = ⨆ (k) (_ : i k ≤ f a), i k

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ (Finset.range (k + 1)).sup fun k => if i k ≤ f a then i k else 0

Tactic:
have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
⊢ i k ≤ (Finset.range (k + 1)).sup fun k => if i k ≤ f a then i k else 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_of_char_three : W.j = W.Δ'⁻¹ * W.b₂ ^ 6

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = ↑W.Δ'⁻¹ * W.b₂ ^ 6

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

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem NullMeasurableSet.smul {s} (hs : NullMeasurableSet s μ) (c : G) :
    NullMeasurableSet (c • s) μ

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
μ : Measure α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ NullMeasurableSet (c • s) μ

Tactic:
simpa only [← preimage_smul_inv] using
  hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_ite_mem (s t : Finset ι) (f : ι → M) :
    𝔼 i ∈ s, (if i ∈ t then f i else 0) = (#(s ∩ t) / #s : ℚ≥0) • 𝔼 i ∈ s ∩ t, f i

Proof state:
case inl
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : s ∩ t = ∅
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
simp [expect, hst]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
obtain hst | hst := (s ∩ t).eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : s ∩ t = ∅
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

case inr
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Proof state:
case inr
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma op_smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
    MulOpposite.op a • (s : Set G) = s

Proof state:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ MulOpposite.op a • ↑s = ↑s

Tactic:
ext

Result:
case h
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s

Proof state:
case h
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s

Tactic:
simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_right, ha]

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_add_left (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η]
    (f : α → β → ℝ≥0∞) : withDensity (κ + η) f = withDensity κ f + withDensity η f

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
simp_rw [withDensity_of_not_measurable _ hf]

Result:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = 0 + 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ 0 = 0 + 0

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : ¬Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
ext a s

Result:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (((κ + η).withDensity f) a) s = ((κ.withDensity f + η.withDensity f) a) s

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (((κ + η).withDensity f) a) s = ((κ.withDensity f + η.withDensity f) a) s

Tactic:
simp only [Kernel.withDensity_apply _ hf, coe_add, Pi.add_apply, withDensity_add_measure,
  Measure.add_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_reverse {l : List α} {f : (i : Nat) → α → (h : i < l.reverse.length) → β} :
    l.reverse.mapFinIdx f =
      (l.mapFinIdx (fun i a h => f (l.length - 1 - i) a (by simp; omega))).reverse

Proof state:
α : Type ?u.68699
β : Type ?u.68725
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
a : α
h : i < l.length
⊢ l.length - 1 - i < l.reverse.length

Tactic:
simp

Result:
α : Type ?u.68699
β : Type ?u.68725
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
a : α
h : i < l.length
⊢ l.length - 1 - i < l.length

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
⊢ l.reverse.mapFinIdx f = (l.mapFinIdx fun i a h => f (l.length - 1 - i) a ⋯).reverse

Tactic:
simp [mapFinIdx_eq_iff]

Result:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
⊢ ∀ (i : Nat) (h : i < l.length),
    f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] ⋯ = f i l[l.length - 1 - i] ⋯

Proof state:
α : Type ?u.68699
β : Type ?u.68725
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
a : α
h : i < l.length
⊢ l.length - 1 - i < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
h : i < l.length
⊢ f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] ⋯ = f i l[l.length - 1 - i] ⋯

Tactic:
congr

Result:
case e_i
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
h : i < l.length
⊢ l.length - 1 - (l.length - 1 - i) = i

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
⊢ ∀ (i : Nat) (h : i < l.length),
    f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] ⋯ = f i l[l.length - 1 - i] ⋯

Tactic:
intro i h

Result:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
h : i < l.length
⊢ f (l.length - 1 - (l.length - 1 - i)) l[l.length - 1 - i] ⋯ = f i l[l.length - 1 - i] ⋯

Proof state:
case e_i
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.reverse.length → β
i : Nat
h : i < l.length
⊢ l.length - 1 - (l.length - 1 - i) = i

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isBasis_iff_insert_eq (hC : M.IsCircuit C) :
    M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Proof state:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

Tactic:
rw [hI, insert_diff_singleton, insert_eq_of_mem he]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
refine ⟨fun ⟨e, he, hI⟩ ↦ ⟨e, ⟨he, fun heI ↦ (hI.subset heI).2 rfl⟩, ?_⟩,
  fun ⟨e, he, hC⟩ ↦ ⟨e, he.1, ?_⟩⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
x✝ : ∃ e ∈ C, I = C \ {e}
e : α
he : e ∈ C
hI : I = C \ {e}
⊢ C = insert e I

case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC✝ : M.IsCircuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}

Proof state:
case refine_2
α : Type u_1
M : Matroid α
C I : Set α
hC✝ : M.IsCircuit C
x✝ : ∃ e ∈ C \ I, C = insert e I
e : α
he : e ∈ C \ I
hC : C = insert e I
⊢ I = C \ {e}

Tactic:
rw [hC, insert_diff_self_of_not_mem he.2]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Tactic:
rw [hC.isBasis_iff_eq_diff_singleton]

Result:
α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ (∃ e ∈ C, I = C \ {e}) ↔ ∃ e ∈ C \ I, C = insert e I