harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop (h_le : ∀ n, s n ≤ m0)
    (h_indep : iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet[limsup s atTop] t) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
  ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure (κ a)
⊢ IsFiniteMeasure (κ a)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)

Tactic:
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma sum_balance (f : ι → G) : ∑ x, balance f x = 0

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ ∑ x : ι, balance f x = 0

Tactic:
cases isEmpty_or_nonempty ι <;> simp [balance_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem IsSheaf.amalgamate_map {A : Type u₂} [Category.{v₂} A] {E : A} {X : C} {P : Cᵒᵖ ⥤ A}
    (hP : Presheaf.IsSheaf J P) (S : J.Cover X) (x : ∀ I : S.Arrow, E ⟶ P.obj (op I.Y))
    (hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂),
       x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op)
    (I : S.Arrow) :
    hP.amalgamate S x hx ≫ P.map I.f.op = x _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : J.Cover X
x : (I : S.Arrow) → E ⟶ P.obj (op I.Y)
hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op
I : S.Arrow
⊢ hP.amalgamate S x hx ≫ P.map I.f.op = x I

Tactic:
apply (hP _ _ S.condition).valid_glue

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_rotate' (a b c : G) : a * (b * c) = b * (c * a)

Proof state:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (c * a)

Tactic:
simp only [mul_left_comm, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).1.isEmpty = false

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insertIfNew k v).val.isEmpty = false

Tactic:
simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j

Proof state:
i j k : Int
⊢ k + i = k + j ↔ i = j

Tactic:
simp [Int.add_comm k]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Ioc (x y : ℝ) : Real.toEReal '' Ioc x y = Ioc ↑x ↑y

Proof state:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioc x y) = Ioc ↑x ↑y

Tactic:
rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]

Result:
x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y

Proof state:
x y : ℝ
⊢ Ioc ↑↑x ↑↑y = Ioc ↑x ↑y

Tactic:
rfl

Result:
no goals

Proof state:
x y : ℝ
⊢ Real.toEReal '' Ioc x y = Ioc ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Ioc x y) = Ioc ↑x ↑y
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.subset_ground (hI : M.Indep I) : I ⊆ M.E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ I ⊆ M.E

Tactic:
exact hIB.trans hB.subset_ground

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ I ⊆ M.E

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ I ⊆ M.E
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a

Tactic:
rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem card_support_eq_one {f : α →₀ M} :
    #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)

Tactic:
simp only [card_eq_one, support_eq_singleton]

Result:
no goals
-- Mathlib/Algebra/Star/Center.lean
theorem Set.star_centralizer : star s.centralizer = (star s).centralizer

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ {a | ∀ m ∈ s, Commute (star m) a} = {c | ∀ m ∈ star s, Commute m c}

Tactic:
conv_rhs => simp only [← image_star, forall_mem_image]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, Commute m c} = {c | ∀ m ∈ star s, Commute m c}

Tactic:
conv_lhs => simp only [← star_preimage, preimage_setOf_eq, ← commute_star_comm]

Result:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ {a | ∀ m ∈ s, Commute (star m) a} = {c | ∀ m ∈ star s, Commute m c}

Proof state:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
simp_rw [centralizer, ← commute_iff_eq]

Result:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, Commute m c} = {c | ∀ m ∈ star s, Commute m c}
-- Mathlib/Topology/Constructions.lean
theorem set_pi_mem_nhds {i : Set ι} {s : ∀ a, Set (π a)} {x : ∀ a, π a} (hi : i.Finite)
    (hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)) : pi i s ∈ 𝓝 x

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x

Tactic:
exact fun a ha => (continuous_apply a).continuousAt (hs a ha)

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ i.pi s ∈ 𝓝 x

Tactic:
rw [pi_def, biInter_mem hi]

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
i : Set ι
s : (a : ι) → Set (π a)
x : (a : ι) → π a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma type_ext {x y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) : x = y :=
  (equivPullbackObj hc).injective (by ext <;> assumption)

Proof state:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : c.fst x = c.fst y
h₂ : c.snd x = c.snd y
⊢ (equivPullbackObj hc) x = (equivPullbackObj hc) y

Tactic:
ext <;> assumption

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_natAbs (n : ℤ) : T R n.natAbs = T R n

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ T R ↑n.natAbs = T R (-↑n.natAbs)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R ↑n.natAbs = T R n

Tactic:
obtain h | h := Int.natAbs_eq n <;> nth_rw 2 [h]

Result:
case inr
R : Type u_1
inst✝ : CommRing R
n : ℤ
h : n = -↑n.natAbs
⊢ T R ↑n.natAbs = T R (-↑n.natAbs)
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma carrierEquiv_symm_snd (T : Triplet f g) (p : Spec T.tensor) :
    (pullback.snd f g).base (carrierEquiv.symm ⟨T, p⟩) = T.y

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.snd f g).base) (carrierEquiv.symm ⟨T, p⟩) = T.y

Tactic:
simp [carrierEquiv]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.ne_zero {a b : α} (h : FiniteMultiplicity a b) : b ≠ 0 :=
  let ⟨n, hn⟩ := h
  fun hb => by simp [hb] at hn

Proof state:
α : Type u_1
inst✝ : MonoidWithZero α
a b : α
h : FiniteMultiplicity a b
n : ℕ
hn : ¬a ^ (n + 1) ∣ b
hb : b = 0
⊢ False

Tactic:
simp [hb] at hn

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_fuzzy_zero_iff {x : PGame} : -x ‖ 0 ↔ x ‖ 0

Proof state:
x : PGame
⊢ -x ‖ 0 ↔ x ‖ 0

Tactic:
rw [neg_fuzzy_iff, neg_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_true_of_imp_eq_false {a b : Prop} (h : (a → b) = False) : a = True

Proof state:
a b : Prop
h : (a → b) = False
⊢ a = True

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem comap_const {m} (b : β) : MeasurableSpace.comap (fun _a : α => b) m = ⊥ :=
  eq_bot_iff.2 <| by rintro _ ⟨s, -, rfl⟩; by_cases b ∈ s <;> simp [*]

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a => b) ⁻¹' s)

Tactic:
by_cases b ∈ s <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
⊢ MeasurableSpace.comap (fun _a => b) m ≤ ⊥

Tactic:
rintro _ ⟨s, -, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a => b) ⁻¹' s)
-- Mathlib/SetTheory/Game/Basic.lean
/-- `1 * x` has the same moves as `x`. -/
protected lemma one_mul : ∀ (x : PGame), 1 * x ≡ x
  | ⟨xl, xr, xL, xR⟩ => by
    refine Identical.of_equiv ((Equiv.sumEmpty _ _).trans (Equiv.punitProd _))
      ((Equiv.sumEmpty _ _).trans (Equiv.punitProd _)) ?_ ?_ <;>
    · rintro (⟨⟨⟩, _⟩ | ⟨⟨⟩, _⟩)
      exact ((((PGame.zero_mul (mk _ _ _ _)).add (PGame.one_mul _)).trans (PGame.zero_add _)).sub
        (PGame.zero_mul _)).trans (PGame.sub_zero _)

Proof state:
case refine_2
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
⊢ ∀ (i : (1 * mk xl xr xL xR).RightMoves),
    (1 * mk xl xr xL xR).moveRight i ≡
      (mk xl xr xL xR).moveRight
        (((Equiv.sumEmpty (PUnit.{u_1 + 1} × xr) (PEmpty.{u_1 + 1} × xl)).trans (Equiv.punitProd xr)) i)

Tactic:
rintro (⟨⟨⟩, _⟩ | ⟨⟨⟩, _⟩)

Result:
case refine_2.inl.mk.unit
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
snd✝ : xr
⊢ (1 * mk xl xr xL xR).moveRight (Sum.inl (PUnit.unit, snd✝)) ≡
    (mk xl xr xL xR).moveRight
      (((Equiv.sumEmpty (PUnit.{u_1 + 1} × xr) (PEmpty.{u_1 + 1} × xl)).trans (Equiv.punitProd xr))
        (Sum.inl (PUnit.unit, snd✝)))

Proof state:
case refine_2.inl.mk.unit
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
snd✝ : xr
⊢ (1 * mk xl xr xL xR).moveRight (Sum.inl (PUnit.unit, snd✝)) ≡
    (mk xl xr xL xR).moveRight
      (((Equiv.sumEmpty (PUnit.{u_1 + 1} × xr) (PEmpty.{u_1 + 1} × xl)).trans (Equiv.punitProd xr))
        (Sum.inl (PUnit.unit, snd✝)))

Tactic:
exact ((((PGame.zero_mul (mk _ _ _ _)).add (PGame.one_mul _)).trans (PGame.zero_add _)).sub
  (PGame.zero_mul _)).trans (PGame.sub_zero _)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff_integrableOn_Icc_of_le {f : ℝ → E} {a b : ℝ} (hab : a ≤ b)
    {μ : Measure ℝ} [NoAtoms μ] : IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hab : a ≤ b
μ : Measure ℝ
inst✝ : NoAtoms μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem natDegree_le_rankOfDiscrBdd (a : 𝓞 K) (h : ℚ⟮(a : K)⟯ = ⊤) :
    natDegree (minpoly ℤ (a : K)) ≤ rankOfDiscrBdd N

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
a : 𝓞 K
h : (minpoly ℤ ((algebraMap (𝓞 K) K) a)).natDegree = finrank ℚ K
⊢ (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N

Tactic:
exact h.symm ▸ rank_le_rankOfDiscrBdd hK

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
a : 𝓞 K
h : ℚ⟮↑a⟯ = ⊤
⊢ (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N

Tactic:
rw [Field.primitive_element_iff_minpoly_natDegree_eq,
  minpoly.isIntegrallyClosed_eq_field_fractions' ℚ a.isIntegral_coe,
  (minpoly.monic a.isIntegral_coe).natDegree_map] at h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
a : 𝓞 K
h : (minpoly ℤ ((algebraMap (𝓞 K) K) a)).natDegree = finrank ℚ K
⊢ (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N
-- Mathlib/Order/Filter/Map.lean
theorem pure_le_principal {s : Set α} (a : α) : pure a ≤ 𝓟 s ↔ a ∈ s

Proof state:
α : Type u_1
s : Set α
a : α
⊢ pure a ≤ 𝓟 s ↔ a ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_assoc {γ} (f : Part α) (g : α → Part β) (k : β → Part γ) :
    (f.bind g).bind k = f.bind fun x => (g x).bind k :=
  ext fun a => by
    simp only [mem_bind_iff]
    exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ a_1, (∃ a ∈ f, a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1 ∈ f, ∃ a_2 ∈ g a_1, a ∈ k a_2

Tactic:
exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
       fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ a ∈ (f.bind g).bind k ↔ a ∈ f.bind fun x => (g x).bind k

Tactic:
simp only [mem_bind_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ a_1, (∃ a ∈ f, a_1 ∈ g a) ∧ a ∈ k a_1) ↔ ∃ a_1 ∈ f, ∃ a_2 ∈ g a_1, a ∈ k a_2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem beq_not_self : ∀ (x : Bool), (x   == !x) = false

Proof state:
⊢ ∀ (x : Bool), (x == !x) = false

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_add_le (f g : M →ₛₗ[σ₁₂] M₂) : map (f + g) p ≤ map f p ⊔ map g p

Proof state:
case intro.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ ↑p
⊢ (f + g) m ∈ map f p ⊔ map g p

Tactic:
exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
⊢ map (f + g) p ≤ map f p ⊔ map g p

Tactic:
rintro x ⟨m, hm, rfl⟩

Result:
case intro.intro
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ ↑p
⊢ (f + g) m ∈ map f p ⊔ map g p
-- Mathlib/Probability/IdentDistrib.lean
theorem ae_snd (h : IdentDistrib f g μ ν) {p : γ → Prop} (pmeas : MeasurableSet {x | p x})
    (hp : ∀ᵐ x ∂μ, p (f x)) : ∀ᵐ x ∂ν, p (g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map f μ, p y

Tactic:
exact (ae_map_iff h.aemeasurable_fst pmeas).2 hp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map g ν, p y

Tactic:
rw [← h.map_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map f μ, p y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (x : β) ∂ν, p (g x)

Tactic:
apply (ae_map_iff h.aemeasurable_snd pmeas).1

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
p : γ → Prop
pmeas : MeasurableSet {x | p x}
hp : ∀ᵐ (x : α) ∂μ, p (f x)
⊢ ∀ᵐ (y : γ) ∂Measure.map g ν, p y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
  ext_get? fun n => by simp_all

Proof state:
α : Type u_1
l₁ l₂ : List α
h : ∀ (i : Nat), l₁[i]? = l₂[i]?
n : Nat
⊢ l₁.get? n = l₂.get? n

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_nat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
    (f : F) (n : ℕ) : f n = f 0 + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
⊢ f ↑n = f 0 + n • b

Tactic:
simpa using map_add_nat' f 0 n

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_endomorphism {M : Type*} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M)
    (v : M) (p : R[X]) : aeval f p v = p.sum fun n b => b • (f ^ n) v

Proof state:
R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ (p.sum fun e a => (algebraMap R (M →ₗ[R] M)) a * f ^ e) v = p.sum fun n b => b • (f ^ n) v

Tactic:
exact map_sum (LinearMap.applyₗ v) _ _

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ ((aeval f) p) v = p.sum fun n b => b • (f ^ n) v

Tactic:
rw [aeval_def, eval₂_eq_sum]

Result:
R : Type u
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ (p.sum fun e a => (algebraMap R (M →ₗ[R] M)) a * f ^ e) v = p.sum fun n b => b • (f ^ n) v
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem ε_app_obj (n : M) (X : C) [F.Monoidal] :
    (ε F).app ((F.obj n).obj X) = (F.map (ρ_ n).inv).app X ≫ (δ F n (𝟙_ M)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) = (F.map (ρ_ n).inv).app X ≫ (δ F n (𝟙_ M)).app X

Tactic:
rw [map_rightUnitor_inv]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) = ((ρ_ (F.obj n)).inv ≫ F.obj n ◁ ε F ≫ μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) = ((ρ_ (F.obj n)).inv ≫ F.obj n ◁ ε F ≫ μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) =
    (𝟙 ((F.obj n).obj X) ≫ (ε F).app ((F.obj n).obj X) ≫ (μ F n (𝟙_ M)).app X) ≫ (δ F n (𝟙_ M)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (ε F).app ((F.obj n).obj X) =
    (𝟙 ((F.obj n).obj X) ≫ (ε F).app ((F.obj n).obj X) ≫ (μ F n (𝟙_ M)).app X) ≫ (δ F n (𝟙_ M)).app X

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app,
  endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_ssubset_closure (hI : M.Indep I) (hJI : J ⊂ I) : M.closure J ⊂ M.closure I

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
e : α
heI : e ∈ I
heJ : e ∉ J
⊢ M.closure J ⊂ M.closure I

Tactic:
exact (M.closure_subset_closure hJI.subset).ssubset_of_not_subset fun hss ↦ heJ <|
  (hI.closure_inter_eq_self_of_subset hJI.subset).subset ⟨hss (M.mem_closure_of_mem heI), heI⟩

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
⊢ M.closure J ⊂ M.closure I

Tactic:
obtain ⟨e, heI, heJ⟩ := exists_of_ssubset hJI

Result:
case intro.intro
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊂ I
e : α
heI : e ∈ I
heJ : e ∉ J
⊢ M.closure J ⊂ M.closure I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem toNat_eq_zero {b : Bool} : b.toNat = 0 ↔ b = false

Proof state:
b : Bool
⊢ b.toNat = 0 ↔ b = false

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem intro' {K : Set α} (hK : IsCompact K) (h'K : IsClosed K)
    (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
⊢ HasCompactMulSupport f

Tactic:
have : mulTSupport f ⊆ K := by
  rw [← h'K.closure_eq]
  apply closure_mono (mulSupport_subset_iff'.2 hfK)

Result:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
this : mulTSupport f ⊆ K
⊢ HasCompactMulSupport f

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ K

Tactic:
rw [← h'K.closure_eq]

Result:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ closure K

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
this : mulTSupport f ⊆ K
⊢ HasCompactMulSupport f

Tactic:
exact IsCompact.of_isClosed_subset hK ( isClosed_mulTSupport f) this

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
K : Set α
hK : IsCompact K
h'K : IsClosed K
hfK : ∀ x ∉ K, f x = 1
⊢ mulTSupport f ⊆ closure K

Tactic:
apply closure_mono (mulSupport_subset_iff'.2 hfK)

Result:
no goals