harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_two_eq (x : Int) : x % 2 = 0 ∨ x % 2 = 1

Proof state:
x : Int
⊢ x % 2 = 0 ∨ x % 2 = 1

Tactic:
have h₁ : 0 ≤ x % 2 := Int.emod_nonneg x (by decide)

Result:
x : Int
h₁ : 0 ≤ x % 2
⊢ x % 2 = 0 ∨ x % 2 = 1

Proof state:
x : Int
h₁ : 0 ≤ x % 2
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
x : Int
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
x : Int
h₁ : 0 ≤ x % 2
h₂ : x % 2 < 2
x✝¹ : 0 ≤ 0
x✝ : 0 < 2
⊢ 0 = 0 ∨ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
x : Int
h₁ : 0 ≤ x % 2
h₂ : x % 2 < 2
x✝¹ : 0 ≤ 1
x✝ : 1 < 2
⊢ 1 = 0 ∨ 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
x : Int
h₁ : 0 ≤ x % 2
h₂ : x % 2 < 2
⊢ x % 2 = 0 ∨ x % 2 = 1

Tactic:
match x % 2, h₁, h₂ with
| 0, _, _ => simp
| 1, _, _ => simp

Result:
no goals

Proof state:
x : Int
h₁ : 0 ≤ x % 2
⊢ x % 2 = 0 ∨ x % 2 = 1

Tactic:
have h₂ : x % 2 < 2 := Int.emod_lt_of_pos x (by decide)

Result:
x : Int
h₁ : 0 ≤ x % 2
h₂ : x % 2 < 2
⊢ x % 2 = 0 ∨ x % 2 = 1
-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
theorem iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute
    [FiniteDimensional K M] (f : ι → Module.End K M) (h : Pairwise fun i j ↦ Commute (f i) (f j))
    (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) :
    ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Proof state:
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j => Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
⊢ ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤

Tactic:
refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
  (fun i j ↦ Module.End.mapsTo_maxGenEigenspace_of_comm ?_) h'

Result:
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j => Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
⊢ Commute (f j) (f i)

Proof state:
ι : Type u_1
K : Type u_3
M : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun i j => Commute (f i) (f j)
h' : ∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤
i j : ι
⊢ Commute (f j) (f i)

Tactic:
rcases eq_or_ne j i with rfl | hij <;> tauto

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_sup_right {S T : Submonoid M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
M : Type u_1
inst✝ : MulOneClass M
S T : Submonoid M
⊢ T ≤ S ⊔ T
-- Mathlib/Data/Sym/Sym2.lean
lemma lift_map_apply {g : γ → α} (f : {f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁}) (p : Sym2 γ) :
    lift f (map g p) = lift ⟨fun (c₁ c₂ : γ) => f.val (g c₁) (g c₂), fun _ _ => f.prop _ _⟩ p

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
⊢ lift f (map g p) = lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩ p

Tactic:
conv_rhs => rw [← lift_comp_map, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub (a b : α) : toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_sub_zsmul hp a b 1

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zpow_of_gcd_eq_one (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : i.gcd k = 1) :
    IsPrimitiveRoot (ζ ^ i) k

Proof state:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift i to ℕ using h0

Result:
case pos.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : (↑i).gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k

Proof state:
case pos.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : (↑i).gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k

Tactic:
exact_mod_cast h.pow_of_coprime i hi

Result:
no goals

Proof state:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
lift -i to ℕ using this with i' hi'

Result:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k

Tactic:
apply h.pow_of_coprime

Result:
case neg.intro.hi
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ i'.Coprime k

Proof state:
case neg.intro.hi
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ i'.Coprime k

Tactic:
rwa [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi

Result:
no goals

Proof state:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
have : 0 ≤ -i := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le

Result:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
this : 0 ≤ -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by_cases h0 : 0 ≤ i

Result:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : 0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
⊢ IsPrimitiveRoot (ζ ^ i) k

Proof state:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
rw [← inv_iff, ← zpow_neg, ← hi', zpow_natCast]

Result:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
h0 : ¬0 ≤ i
i' : ℕ
hi' : ↑i' = -i
⊢ IsPrimitiveRoot (ζ ^ i') k
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f]
    (b : β) : limsup (fun _ => b) f = b

Proof state:
β : Type u_2
α : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : f.NeBot
b : β
⊢ limsup (fun x => b) f = b

Tactic:
simpa only [limsup_eq, eventually_const] using csInf_Ici

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem lift_comp_reindex_symm (e : ι ≃ ι₂) (φ : MultilinearMap R s E) :
    lift φ ∘ₗ (reindex R s e).symm = lift (domDomCongrLinearEquiv' R R s _ e φ)

Proof state:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
x✝ : (i : ι₂) → s (e.symm i)
⊢ ((lift φ ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) x✝ =
    ((lift ((domDomCongrLinearEquiv' R R s E e) φ)).compMultilinearMap (tprod R)) x✝

Tactic:
simp [reindex]

Result:
no goals

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
⊢ lift φ ∘ₗ ↑(reindex R s e).symm = lift ((domDomCongrLinearEquiv' R R s E e) φ)

Tactic:
ext

Result:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R s E
x✝ : (i : ι₂) → s (e.symm i)
⊢ ((lift φ ∘ₗ ↑(reindex R s e).symm).compMultilinearMap (tprod R)) x✝ =
    ((lift ((domDomCongrLinearEquiv' R R s E e) φ)).compMultilinearMap (tprod R)) x✝
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@[simp]
lemma mem_toTwoSided {I : Ideal R} {h} {x : R} :
    x ∈ I.toTwoSided h ↔ x ∈ I

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ∀ {x y : R}, x ∈ I → x * y ∈ I
x : R
⊢ x ∈ I.toTwoSided h ↔ x ∈ I

Tactic:
simp [toTwoSided]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
theorem preserves_cokernel_iso_comp_cokernel_map {X' Y' : C} (g : X' ⟶ Y') [HasCokernel g]
    [HasCokernel (G.map g)] [PreservesColimit (parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y')
    (hpq : f ≫ q = p ≫ g) :
    (PreservesCokernel.iso G _).hom ≫
        cokernel.map (G.map f) (G.map g) (G.map p) (G.map q)
          (by rw [← G.map_comp, hpq, G.map_comp]) =
      G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G _).hom

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom

Tactic:
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
  cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive] lemma subset_div_left (ht : 1 ∈ t) : s ⊆ s / t

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
exact subset_mul_left _ <| by simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem forall_of_forall_mem_ball (p : α → Prop) (x : α)
    (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ ball x R, p y) (y : α) : p y

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
R : ℝ
hR : R > dist y x
h : ∀ z ∈ ball x R, p z
⊢ p y

Tactic:
exact h _ hR

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
  frequently_iff.1 H (Ioi_mem_atTop (dist y x))

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
R : ℝ
hR : R > dist y x
h : ∀ z ∈ ball x R, p z
⊢ p y
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem neg_mem {x : L} (hx : x ∈ S) : -x ∈ S

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S.toSubalgebra

Tactic:
simpa

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S

Tactic:
show -x ∈S.toSubalgebra

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S.toSubalgebra
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem tendsto_approxOn_range_Lp [BorelSpace E] {f : β → E} [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞)
    {μ : Measure β} (fmeas : Measurable f) [SeparableSpace (range f ∪ {0} : Set E)]
    (hf : MemLp f p μ) :
    Tendsto
      (fun n =>
        (memLp_approxOn_range fmeas hf n).toLp (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n))
      atTop (𝓝 (hf.toLp f))

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
⊢ Tendsto (fun n => MemLp.toLp ⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) atTop (𝓝 (MemLp.toLp f hf))

Tactic:
simpa only [Lp.tendsto_Lp_iff_tendsto_eLpNorm''] using
  tendsto_approxOn_range_Lp_eLpNorm hp_ne_top fmeas hf.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
@[simp] lemma snd_compProd_prodMkLeft
    (κ : Kernel α β) (η : Kernel β γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    snd (κ ⊗ₖ prodMkLeft α η) = η ∘ₖ κ

Proof state:
case h.h.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.2 ∈ s}

Tactic:
exact measurable_snd hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
⊢ (κ ⊗ₖ prodMkLeft α η).snd = η ∘ₖ κ

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ ⊗ₖ prodMkLeft α η).snd a) s = ((η ∘ₖ κ) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((κ ⊗ₖ prodMkLeft α η).snd a) s = ((η ∘ₖ κ) a) s

Tactic:
rw [snd_apply' _ _ hs, compProd_apply, comp_apply' _ _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((prodMkLeft α η) (a, b)) {c | (b, c) ∈ {p | p.2 ∈ s}} ∂κ a = ∫⁻ (b : β), (η b) s ∂κ a

case h.h.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.2 ∈ s}

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((prodMkLeft α η) (a, b)) {c | (b, c) ∈ {p | p.2 ∈ s}} ∂κ a = ∫⁻ (b : β), (η b) s ∂κ a

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_eq_max_sub_min {i j : ℕ} : dist i j = (max i j) - min i j :=
  Or.elim (lt_or_ge i j)
  (by intro h; rw [max_eq_right_of_lt h, min_eq_left_of_lt h, dist_eq_sub_of_le (Nat.le_of_lt h)])
  (by intro h; rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h])

Proof state:
i j : ℕ
h : i ≥ j
⊢ i.dist j = i ⊔ j - i ⊓ j

Tactic:
rw [max_eq_left h, min_eq_right h, dist_eq_sub_of_le_right h]

Result:
no goals

Proof state:
i j : ℕ
h : i < j
⊢ i.dist j = i ⊔ j - i ⊓ j

Tactic:
rw [max_eq_right_of_lt h, min_eq_left_of_lt h, dist_eq_sub_of_le (Nat.le_of_lt h)]

Result:
no goals

Proof state:
i j : ℕ
⊢ i ≥ j → i.dist j = i ⊔ j - i ⊓ j

Tactic:
intro h

Result:
i j : ℕ
h : i ≥ j
⊢ i.dist j = i ⊔ j - i ⊓ j

Proof state:
i j : ℕ
⊢ i < j → i.dist j = i ⊔ j - i ⊓ j

Tactic:
intro h

Result:
i j : ℕ
h : i < j
⊢ i.dist j = i ⊔ j - i ⊓ j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_mkArray_iff {a : α} {n} {l : Array α} :
    l = mkArray n a ↔ l.size = n ∧ ∀ (b) (_ : b ∈ l), b = a

Proof state:
α : Type u_1
a : α
n : Nat
l : Array α
⊢ l = mkArray n a ↔ l.size = n ∧ ∀ (b : α), b ∈ l → b = a

Tactic:
rw [← toList_inj]

Result:
α : Type u_1
a : α
n : Nat
l : Array α
⊢ l.toList = (mkArray n a).toList ↔ l.size = n ∧ ∀ (b : α), b ∈ l → b = a

Proof state:
α : Type u_1
a : α
n : Nat
l : Array α
⊢ l.toList = (mkArray n a).toList ↔ l.size = n ∧ ∀ (b : α), b ∈ l → b = a

Tactic:
simpa using List.eq_replicate_iff (l := l.toList)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasFDerivAtFilter.add (hf : HasFDerivAtFilter f f' x L)
    (hg : HasFDerivAtFilter g g' x L) : HasFDerivAtFilter (fun y => f y + g y) (f' + g') x L :=
  .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun _ => by
    simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]
    abel

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
L : Filter E
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - (f' x✝ - f' x) + (g x✝ - g x - (g' x✝ - g' x)) =
    f x✝ + g x✝ - (f x + g x) - (f' x✝ + g' x✝ - (f' x + g' x))

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
L : Filter E
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - f' (x✝ - x) + (g x✝ - g x - g' (x✝ - x)) = f x✝ + g x✝ - (f x + g x) - (f' + g') (x✝ - x)

Tactic:
simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
L : Filter E
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - (f' x✝ - f' x) + (g x✝ - g x - (g' x✝ - g' x)) =
    f x✝ + g x✝ - (f x + g x) - (f' x✝ + g' x✝ - (f' x + g' x))
-- Mathlib/Data/Finset/CastCard.lean
lemma cast_card_inter [AddGroupWithOne R] :
    (#(s ∩ t) : R) = #s + #t - #(s ∪ t)

Proof state:
α : Type u_1
R : Type u_3
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t)) = ↑(#s) + ↑(#t) - ↑(#(s ∪ t))

Tactic:
rw [eq_sub_iff_add_eq, ← cast_add, card_inter_add_card_union, cast_add]

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
lemma card_mod_card_parts_le : #s % #P.parts ≤ #P.parts

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0

Tactic:
rw [h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
rw [h]

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0

Proof state:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts

Tactic:
exact (Nat.mod_lt _ h).le

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % 0 ≤ 0

Tactic:
rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #s = 0
⊢ #s % 0 ≤ 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #s % #P.parts ≤ #P.parts

Tactic:
obtain h | h := (#P.parts).eq_zero_or_pos

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts = 0
⊢ #s % #P.parts ≤ #P.parts

case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
h : #P.parts > 0
⊢ #s % #P.parts ≤ #P.parts