harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id [TopologicalSpace F]
    (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable[m.prod mΩ] (fun x : Ω × Ω => f x.2)
      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)

Tactic:
rw [← aestronglyMeasurable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)

Tactic:
simp_rw [id] at hf ⊢

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)
⊢ AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)

Tactic:
exact hf

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem card_isPrincipal_norm_eq_mul_torsion (n : ℕ) :
    Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧
      absNorm (I : Ideal (𝓞 K)) = n} * torsionOrder K =
        Nat.card {a : integerSet K | mixedEmbedding.norm (a : mixedSpace K) = n}

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card (↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} × ↥(Units.torsion K)) = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
exact Nat.card_congr (integerSetEquivNorm K n).symm

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * ↑(torsionOrder K) = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card (↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} × ↥(Units.torsion K)) = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_replicate {n : Nat} {a : α} {b : β} :
    unzip (replicate n (a, b)) = (replicate n a, replicate n b)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
a : α
b : β
⊢ (replicate n (a, b)).unzip = (replicate n a, replicate n b)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_sInf' (s : Set (Ideal S)) : (sInf s).comap f = ⨅ I ∈ comap f '' s, I :=
  _root_.trans (comap_sInf f s) (by rw [iInf_image])

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set (Ideal S)
⊢ ⨅ I ∈ s, comap f I = ⨅ I ∈ comap f '' s, I

Tactic:
rw [iInf_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem unsat_of_verifyBVExpr_eq_true (bv : BVLogicalExpr) (c : String)
    (h : verifyBVExpr bv c = true) :
    bv.Unsat

Proof state:
case a.a
bv : BVLogicalExpr
c : String
h✝ : verifyBVExpr bv c = true
h : verifyCert (AIG.toCNF bv.bitblast.relabelNat) c = true
⊢ verifyCert (AIG.toCNF bv.bitblast.relabelNat) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ String

Tactic:
assumption

Result:
no goals

Proof state:
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ bv.Unsat

Tactic:
apply BVLogicalExpr.unsat_of_bitblast

Result:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ bv.bitblast.Unsat

Proof state:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).Unsat

Tactic:
apply verifyCert_correct

Result:
case a.a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ verifyCert (AIG.toCNF bv.bitblast.relabelNat) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ String

Proof state:
case a.a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ verifyCert (AIG.toCNF bv.bitblast.relabelNat) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ String

Tactic:
rw [verifyBVExpr] at h

Result:
case a.a
bv : BVLogicalExpr
c : String
h✝ : verifyBVExpr bv c = true
h : verifyCert (AIG.toCNF bv.bitblast.relabelNat) c = true
⊢ verifyCert (AIG.toCNF bv.bitblast.relabelNat) ?a.cert✝ = true

case a.cert
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ String

Proof state:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ bv.bitblast.Unsat

Tactic:
rw [← AIG.Entrypoint.relabelNat_unsat_iff]

Result:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.Unsat

Proof state:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ bv.bitblast.relabelNat.Unsat

Tactic:
rw [← AIG.toCNF_equisat]

Result:
case a
bv : BVLogicalExpr
c : String
h : verifyBVExpr bv c = true
⊢ (AIG.toCNF bv.bitblast.relabelNat).Unsat
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem EqOnSource.restr {e e' : PartialEquiv α β} (he : e ≈ e') (s : Set α) :
    e.restr s ≈ e'.restr s

Proof state:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ ↑(e.restr s) x = ↑(e'.restr s) x

Tactic:
simp only [mem_inter_iff, restr_source] at hx

Result:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ e.source ∧ x ∈ s
⊢ ↑(e.restr s) x = ↑(e'.restr s) x

Proof state:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ e.source ∧ x ∈ s
⊢ ↑(e.restr s) x = ↑(e'.restr s) x

Tactic:
exact he.2 hx.1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ e.restr s ≈ e'.restr s

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ (e.restr s).source = (e'.restr s).source

case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source

Proof state:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source

Tactic:
intro x hx

Result:
case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ ↑(e.restr s) x = ↑(e'.restr s) x

Proof state:
case left
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ (e.restr s).source = (e'.restr s).source

Tactic:
simp [he.1]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_symm_orderTop (x : (HahnSeries Γ R)ᵃᵒᵖ) :
    (addOppositeEquiv.symm x).orderTop = x.unop.orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : (HahnSeries Γ R)ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop

Tactic:
rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem symmetric (h : Symmetric r) : Symmetric (ReflTransGen r)

Proof state:
α : Type u_1
r : α → α → Prop
h : Symmetric r
⊢ Symmetric (ReflTransGen r)

Tactic:
intro x y h

Result:
α : Type u_1
r : α → α → Prop
h✝ : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x

Proof state:
case tail
α : Type u_1
r : α → α → Prop
h : Symmetric r
x y b✝ c✝ : α
a✝ : ReflTransGen r x b✝
b : r b✝ c✝
c : ReflTransGen r b✝ x
⊢ ReflTransGen r c✝ x

Tactic:
apply Relation.ReflTransGen.head (h b) c

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
h : Symmetric r
x y : α
⊢ ReflTransGen r x x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
h✝ : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x

Tactic:
induction h with
| refl => rfl
| tail _ b c => apply Relation.ReflTransGen.head (h b) c

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem finsum_weightedHomogeneousComponent :
    (finsum fun m => weightedHomogeneousComponent w m φ) = φ

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ = φ

Tactic:
rw [sum_weightedHomogeneousComponent]

Result:
no goals
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csSup_of_not_bdd_above {s : Set ℤ} (h : ¬BddAbove s) : sSup s = 0 :=
  dif_neg (by simp [h])

Proof state:
s : Set ℤ
h : ¬BddAbove s
⊢ ¬(s.Nonempty ∧ BddAbove s)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem pow_multiset_sum_mem_span_pow [DecidableEq α] (s : Multiset α) (n : ℕ) :
    s.sum ^ (Multiset.card s * n + 1) ∈
    span ((s.map fun (x : α) ↦ x ^ (n + 1)).toFinset : Set α)

Proof state:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset

Tactic:
replace h : c ≤ n := Nat.lt_succ_iff.mp (not_le.mp h)

Result:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset

Proof state:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)

Tactic:
rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset

Tactic:
rw [this, pow_add]

Result:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * (s.sum ^ (s.card * n + 1) * s.sum ^ (n - c)) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_vsub_const_iff {x y z : P} (p : P) :
    Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_vsub_const_iff, (vsub_left_injective p).ne_iff,
  (vsub_left_injective p).ne_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis.closure_eq_closure (h : M.IsBasis I X) : M.closure I = M.closure X

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure {x | M.IsBasis I (insert x I)}

Tactic:
exact M.closure_subset_closure fun e he ↦ (h.isBasis_subset (subset_insert _ _)
  (insert_subset he h.subset))

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure I = M.closure X

Tactic:
refine subset_antisymm (M.closure_subset_closure h.subset) ?_

Result:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I

Tactic:
rw [← M.closure_closure I, h.indep.closure_eq_setOf_isBasis_insert]

Result:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure {x | M.IsBasis I (insert x I)}
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem tendsto_card_div_pow (b : Basis ι ℤ L) {s : Set (ι → ℝ)} (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
    Tendsto (fun n : ℕ ↦ (Nat.card (s ∩ (n : ℝ)⁻¹ • L : Set (ι → ℝ)) : ℝ) / n ^ card ι)
      atTop (𝓝 ((volume s).toReal / covolume L))

Proof state:
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0

Tactic:
rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]

Result:
no goals

Proof state:
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ Tendsto (fun n => ↑(Nat.card ↑(s ∩ (↑n)⁻¹ • ↑L)) / ↑n ^ card ι) atTop (𝓝 ((volume s).toReal / covolume L volume))

Tactic:
convert tendsto_card_div_pow'' b hs₁ hs₂ ?_

Result:
case h.e'_5.h.e'_3
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ (volume s).toReal / covolume L volume = (volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)).toReal

ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0

Proof state:
case h.e'_5.h.e'_3
ι : Type u_1
inst✝² : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ (volume s).toReal / covolume L volume = (volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)).toReal

Tactic:
rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
  ENNReal.toReal_ofReal (covolume_pos L volume).le]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_inj_of_nonpos_of_nonneg {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) :
    natAbs a = natAbs b ↔ -a = b

Proof state:
a b : ℤ
ha : a ≤ 0
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ -a = b

Tactic:
simpa only [Int.natAbs_neg] using natAbs_inj_of_nonneg_of_nonneg (neg_nonneg_of_nonpos ha) hb

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
lemma comp_assoc {a₁ a₂ a₃ a₁₂ a₂₃ a : M}
    (α : ShiftedHom X Y a₁) (β : ShiftedHom Y Z a₂) (γ : ShiftedHom Z T a₃)
    (h₁₂ : a₂ + a₁ = a₁₂) (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a) :
    (α.comp β h₁₂).comp γ (show a₃ + a₁₂ = a by rw [← h₁₂, ← add_assoc, h]) =
      α.comp (β.comp γ h₂₃) (by rw [← h₂₃, h])

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
simp only [comp, assoc, Functor.map_comp,
  shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
  ← NatTrans.naturality_assoc, Functor.comp_map]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.3241, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.3248, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.3255, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a

Tactic:
rw [← h₂₃, h]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.3241, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.3248, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.3255, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a

Tactic:
rw [← h₁₂, ← add_assoc, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_one_is_zero (x : Int) : Int.bmod x 1 = 0

Proof state:
x : Int
⊢ x.bmod 1 = 0

Tactic:
simp [Int.bmod]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_apply_mem_eq_next (s : Cycle α) (h : Nodup s) (x : α) (hx : x ∈ s) :
    formPerm s h x = next s h x hx

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
x : α
hx : x ∈ s
⊢ (s.formPerm h) x = s.next h x hx

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h) x = next (Quot.mk (⇑(IsRotated.setoid α)) a✝) h x hx

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h) x = next (Quot.mk (⇑(IsRotated.setoid α)) a✝) h x hx

Tactic:
simpa using List.formPerm_apply_mem_eq_next h _ (by simp_all)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝

Tactic:
simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ιMulti_succ_apply {n : ℕ} (v : Fin n.succ → M) :
    ιMulti R _ v = ι R (v 0) * ιMulti R _ (Matrix.vecTail v)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n.succ → M
⊢ (ιMulti R n.succ) v = (ι R) (v 0) * (ιMulti R n) (Matrix.vecTail v)

Tactic:
simp [ιMulti, Matrix.vecTail]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coeff_zero_of_lt_intValuation {n d : ℕ} {f : K⟦X⟧}
    (H : Valued.v (f : K⸨X⸩) ≤ Multiplicative.ofAdd (-d : ℤ)) :
    n < d → coeff K n f = 0

Proof state:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
⊢ n < d → (PowerSeries.coeff K n) f = 0

Tactic:
intro hnd

Result:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ (PowerSeries.coeff K n) f = 0

Proof state:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ (PowerSeries.coeff K n) f = 0

Tactic:
apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd

Result:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f

Proof state:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ PowerSeries.X ^ d ∣ f

Tactic:
erw [← span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow,
  ← (intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d), ← intValuation_apply,
  ← valuation_of_algebraMap (R := K⟦X⟧) (K := K⸨X⸩)]

Result:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑f ≤ ↑(Multiplicative.ofAdd (-↑d))

Proof state:
K : Type u_2
inst✝ : Field K
n d : ℕ
f : K⟦X⟧
H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
hnd : n < d
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑f ≤ ↑(Multiplicative.ofAdd (-↑d))

Tactic:
exact H

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem exp_one_mul_le_exp {x : ℝ} : exp 1 * x ≤ exp x

Proof state:
x : ℝ
⊢ rexp 1 * x ≤ rexp x

Tactic:
by_cases hx0 : x ≤ 0

Result:
case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Proof state:
case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)

Result:
no goals

Proof state:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
⊢ rexp 1 * x ≤ rexp x

Tactic:
rwa [← exp_le_exp, exp_add, exp_log (lt_of_not_le hx0), mul_comm] at h

Result:
no goals

Proof state:
case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
have h := add_one_le_exp (log x)

Result:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : log x + 1 ≤ rexp (log x)
⊢ rexp 1 * x ≤ rexp x
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_basis_left {ι : Type*} (m : Basis ι R M)
    (H : LinearMap.ker (mulLeftMap N m) = ⊥) : M.LinearDisjoint N

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis ι R ↥M
H : LinearMap.ker (mulLeftMap N ⇑m) = ⊥
this : AddCommGroup (ι →₀ ↥N) := Finsupp.instAddCommGroup
⊢ M.LinearDisjoint N

Tactic:
exact of_basis_left' M N m (LinearMap.ker_eq_bot.1 H)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis ι R ↥M
H : LinearMap.ker (mulLeftMap N ⇑m) = ⊥
⊢ M.LinearDisjoint N

Tactic:
letI : AddCommGroup (ι →₀ N) := Finsupp.instAddCommGroup

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis ι R ↥M
H : LinearMap.ker (mulLeftMap N ⇑m) = ⊥
this : AddCommGroup (ι →₀ ↥N) := Finsupp.instAddCommGroup
⊢ M.LinearDisjoint N