harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_iterate_le (k : ℕ) (x : α) : pred^[k] x ≤ x

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
k : ℕ
x : α
⊢ pred^[k] x ≤ id^[k] x

Tactic:
exact Monotone.iterate_le_of_le pred_mono pred_le k x

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
k : ℕ
x : α
⊢ x = id^[k] x

Tactic:
simp only [Function.iterate_id, id]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
k : ℕ
x : α
⊢ pred^[k] x ≤ x

Tactic:
conv_rhs => rw [(by simp only [Function.iterate_id, id] : x = id^[k] x)]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
k : ℕ
x : α
⊢ pred^[k] x ≤ id^[k] x
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * c / c / b = a / b

Tactic:
simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel_right]

Result:
no goals

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

Tactic:
rw [div_mul_eq_div_div_swap]

Result:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * c / c / b = a / b
-- Mathlib/Algebra/CharP/Two.lean
theorem multiset_sum_mul_self (l : Multiset R) :
    l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
l : Multiset R
⊢ l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum

Tactic:
simp_rw [← pow_two, multiset_sum_sq]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mem_add (I J : FractionalIdeal S P) (x : P) :
    x ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
⊢ x ∈ I + J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
rw [← mem_coe, coe_add, Submodule.add_eq_sup]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
⊢ x ∈ ↑I ⊔ ↑J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
⊢ x ∈ ↑I ⊔ ↑J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = x

Tactic:
exact Submodule.mem_sup

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
lemma measure_preimage_snd_singleton_eq_tsum [Countable α] (μ : Measure (α × β)) (y : β) :
    μ (Prod.snd ⁻¹' {y}) = ∑' x, μ {(x, y)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Tactic:
have : Prod.snd ⁻¹' {y} = ⋃ x : α, {(x, y)} := by ext y; simp [Prod.ext_iff, eq_comm]

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
⊢ Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}

Tactic:
ext y

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y✝ : β
y : α × β
⊢ y ∈ Prod.snd ⁻¹' {y✝} ↔ y ∈ ⋃ x, {(x, y✝)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Tactic:
rw [this, measure_iUnion] <;> simp [Pairwise]

Result:
no goals

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y✝ : β
y : α × β
⊢ y ∈ Prod.snd ⁻¹' {y✝} ↔ y ∈ ⋃ x, {(x, y✝)}

Tactic:
simp [Prod.ext_iff, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem MultilinearMap.curry_uncurryRight
    (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) :
    f.uncurryRight.curryRight = f

Proof state:
case H.h
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f (init (snoc m x))) x = (f m) x

Tactic:
rw [init_snoc]

Result:
no goals

Proof state:
case H.h
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x

Tactic:
simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]

Result:
case H.h
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f (init (snoc m x))) x = (f m) x

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)
⊢ f.uncurryRight.curryRight = f

Tactic:
ext m x

Result:
case H.h
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R (fun i => M i.castSucc) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M i.castSucc
x : M (last n)
⊢ (f.uncurryRight.curryRight m) x = (f m) x
-- Mathlib/Topology/Instances/ENat.lean
theorem isOpen_singleton {x : ℕ∞} (hx : x ≠ ⊤) : IsOpen {x}

Proof state:
x : ℕ∞
hx : x ≠ ⊤
⊢ IsOpen {x}

Tactic:
rw [isOpen_singleton_iff_nhds_eq_pure, ENat.nhds_eq_pure hx]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
lemma unique_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) {g : t2Quotient X → Y} (hfg : g ∘ mk = f) :
    g = lift hf

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
g : t2Quotient X → Y
hfg : g ∘ mk = f
⊢ ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x

Tactic:
simp [← hfg]

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
g : t2Quotient X → Y
hfg : g ∘ mk = f
⊢ g = lift hf

Tactic:
apply surjective_mk X |>.right_cancellable |>.mp <| funext _

Result:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
g : t2Quotient X → Y
hfg : g ∘ mk = f
⊢ ∀ (x : X), (g ∘ mk) x = (lift hf ∘ mk) x
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem finTwoProd_zero (R : Type*) [Semiring R] : Basis.finTwoProd R 0 = (1, 0)

Proof state:
R : Type u_7
inst✝ : Semiring R
⊢ (Basis.finTwoProd R) 0 = (1, 0)

Tactic:
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
lemma pow_self_mono : Monotone fun n : ℕ ↦ n ^ n

Proof state:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)

Tactic:
exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Result:
no goals

Proof state:
⊢ Monotone fun n => n ^ n

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Result:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)

Proof state:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ (n + 1)

Tactic:
rw [Nat.pow_succ]

Result:
n : ℕ
⊢ n ^ n ≤ (n + 1) ^ n * (n + 1)
-- Mathlib/Data/NNRat/Floor.lean
theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉

Proof state:
case right
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ x ≤ ↑⌈x⌉₊

Tactic:
exact Nat.le_ceil _

Result:
no goals

Proof state:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑(x + 1)
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Tactic:
rw [NNRat.cast_add, NNRat.cast_one] at this

Result:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑x + 1
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Proof state:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑x + 1
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Tactic:
refine Eq.trans_lt ?_ this

Result:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑x + 1
⊢ ↑↑⌈x⌉₊ = ↑↑⌈x⌉₊

Proof state:
case right
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
rw [Int.cast_natCast, NNRat.cast_le_natCast]

Result:
case right
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ x ≤ ↑⌈x⌉₊

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌈↑x⌉ = ⌈↑x⌉

Tactic:
rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1 ∧ ↑x ≤ ↑↑⌈x⌉₊

Proof state:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Tactic:
have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x

Result:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑(x + 1)
⊢ ↑↑⌈x⌉₊ < ↑x + 1

Proof state:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
this : ↑↑⌈x⌉₊ < ↑x + 1
⊢ ↑↑⌈x⌉₊ = ↑↑⌈x⌉₊

Tactic:
norm_cast

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1 ∧ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
constructor

Result:
case left
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1

case right
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑x ≤ ↑↑⌈x⌉₊
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_Φ_le (n : ℤ) : (W.Φ n).natDegree ≤ n.natAbs ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.Φ n).natDegree ≤ n.natAbs ^ 2

Tactic:
induction n using Int.negInduction with
| nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
| neg ih => simp only [Φ_neg, Int.natAbs_neg, ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2

Tactic:
exact (W.natDegree_coeff_Φ_ofNat n).left

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2
n✝ : ℕ
⊢ (W.Φ (-↑n✝)).natDegree ≤ (-↑n✝).natAbs ^ 2

Tactic:
simp only [Φ_neg, Int.natAbs_neg, ih]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_append_left : Disjoint (l₁ ++ l₂) l ↔ Disjoint l₁ l ∧ Disjoint l₂ l

Proof state:
α✝ : Type u_1
l₁ l₂ l : List α✝
⊢ (l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l

Tactic:
simp [Disjoint, or_imp, forall_and]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem comp_explicitCokernelπ {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    f ≫ explicitCokernelπ f = 0

Proof state:
case h.e'_3.h
X Y : SemiNormedGrp
f : X ⟶ Y
e_1✝ :
  (X ⟶ explicitCokernel f) =
    ((parallelPair f 0).obj WalkingParallelPair.zero ⟶
      ((Functor.const WalkingParallelPair).obj (cokernelCocone f).pt).obj WalkingParallelPair.one)
⊢ 0 = (cokernelCocone f).ι.app WalkingParallelPair.zero

Tactic:
simp

Result:
no goals

Proof state:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ f ≫ explicitCokernelπ f = 0

Tactic:
convert (cokernelCocone f).w WalkingParallelPairHom.left

Result:
case h.e'_3.h
X Y : SemiNormedGrp
f : X ⟶ Y
e_1✝ :
  (X ⟶ explicitCokernel f) =
    ((parallelPair f 0).obj WalkingParallelPair.zero ⟶
      ((Functor.const WalkingParallelPair).obj (cokernelCocone f).pt).obj WalkingParallelPair.one)
⊢ 0 = (cokernelCocone f).ι.app WalkingParallelPair.zero
-- Mathlib/Order/Chain.lean
theorem ChainClosure.isChain (hc : ChainClosure r c) : IsChain r c

Proof state:
case union
α : Type u_1
r : α → α → Prop
c : Set α
s✝ : Set (Set α)
hs : ∀ a ∈ s✝, ChainClosure r a
h : ∀ a ∈ s✝, IsChain r a
⊢ IsChain r (⋃₀ s✝)

Tactic:
exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
  ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
    h t₁ ht₁ hc₁ (ht hc₂) hneq

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
⊢ IsChain r c

Tactic:
induction hc with
| succ _ h => exact h.succ
| union hs h =>
  exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
    ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
      h t₁ ht₁ hc₁ (ht hc₂) hneq

Result:
no goals

Proof state:
case succ
α : Type u_1
r : α → α → Prop
c s✝ : Set α
a✝ : ChainClosure r s✝
h : IsChain r s✝
⊢ IsChain r (SuccChain r s✝)

Tactic:
exact h.succ

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp] lemma div_dvd_iff_dvd_mul (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c :=
  exists_congr <| fun d ↦ by
  have := Int.dvd_trans (Int.dvd_mul_left _ _) (Int.mul_dvd_mul_left d h)
  rw [eq_comm, Int.mul_comm, ← Int.mul_ediv_assoc d h, Int.ediv_eq_iff_eq_mul_right hb this,
    Int.mul_comm, eq_comm]

Proof state:
a b c : ℤ
h : b ∣ a
hb : b ≠ 0
d : ℤ
⊢ c = a / b * d ↔ b * c = a * d

Tactic:
have := Int.dvd_trans (Int.dvd_mul_left _ _) (Int.mul_dvd_mul_left d h)

Result:
a b c : ℤ
h : b ∣ a
hb : b ≠ 0
d : ℤ
this : b ∣ d * a
⊢ c = a / b * d ↔ b * c = a * d

Proof state:
a b c : ℤ
h : b ∣ a
hb : b ≠ 0
d : ℤ
this : b ∣ d * a
⊢ c = a / b * d ↔ b * c = a * d

Tactic:
rw [eq_comm, Int.mul_comm, ← Int.mul_ediv_assoc d h, Int.ediv_eq_iff_eq_mul_right hb this,
  Int.mul_comm, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.bijective_pi' (he : CompleteOrthogonalIdempotents (1 - e ·)) :
    Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {e i}))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents fun x => 1 - e x
⊢ Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e i}))

Tactic:
obtain ⟨e', rfl, h⟩ : ∃ e' : I → R, (e' = e) ∧ Function.Bijective (Pi.ringHom fun i ↦
    Ideal.Quotient.mk (Ideal.span {e' i})) := ⟨_, funext (by simp), he.bijective_pi⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e' : I → R
h : Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))
he : CompleteOrthogonalIdempotents fun x => 1 - e' x
⊢ Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e' : I → R
h : Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))
he : CompleteOrthogonalIdempotents fun x => 1 - e' x
⊢ Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e' i}))

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents fun x => 1 - e x
⊢ ∀ (x : I), 1 - (1 - e x) = e x

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
/-- A version of `Submodule.span_eq` for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects. -/
lemma coe_span_eq_self [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
    (span R (s : Set M) : Set M) = s

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
s' : Submodule R M := { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ↑(span R ↑s) ≤ ↑s

Tactic:
exact span_le (p := s') |>.mpr le_rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
⊢ ↑(span R ↑s) ≤ ↑s

Tactic:
let s' : Submodule R M :=
  { carrier := s
    add_mem' := add_mem
    zero_mem' := zero_mem _
    smul_mem' := SMulMemClass.smul_mem }

Result:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
s' : Submodule R M := { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ↑(span R ↑s) ≤ ↑s

Proof state:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
⊢ ↑(span R ↑s) = ↑s

Tactic:
refine le_antisymm ?_ subset_span

Result:
R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
⊢ ↑(span R ↑s) ≤ ↑s
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma norm_eq_one_iff_ne_zero_of_discrete {x : 𝕜} : ‖x‖ = 1 ↔ x ≠ 0

Proof state:
case mpr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1

Tactic:
obtain ⟨ε, εpos, h'⟩ := this

Result:
case mpr.intro.intro
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
⊢ ‖x‖ = 1

Proof state:
case mpr.intro.intro.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [inst_1 : DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h : 1 ≤ ‖x‖
⊢ ‖x‖ = 1

Tactic:
rcases h.eq_or_lt with h|h

Result:
case mpr.intro.intro.inr.inl
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [inst_1 : DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h✝ : 1 ≤ ‖x‖
h : 1 = ‖x‖
⊢ ‖x‖ = 1

case mpr.intro.intro.inr.inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [inst_1 : DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h✝ : 1 ≤ ‖x‖
h : 1 < ‖x‖
⊢ ‖x‖ = 1
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem le_lexOrder_mul (φ ψ : MvPowerSeries σ R) :
    lexOrder φ + lexOrder ψ ≤ lexOrder (φ * ψ)

Proof state:
case h.mk
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ (coeff R (u, v).1) φ * (coeff R (u, v).2) ψ = 0

Tactic:
simp only

Result:
case h.mk
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ ψ : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑(toLex d) < φ.lexOrder + ψ.lexOrder
u v : σ →₀ ℕ
h : u + v = d
⊢ (coeff R u) φ * (coeff R v) ψ = 0
-- Mathlib/RingTheory/Int/Basic.lean
theorem Int.Prime.dvd_pow' {n : ℤ} {k p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ n ^ k) :
    (p : ℤ) ∣ n

Proof state:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ ↑p ∣ n

Tactic:
rw [Int.natCast_dvd]

Result:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs

Proof state:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : ↑p ∣ n ^ k
⊢ p ∣ n.natAbs

Tactic:
exact Int.Prime.dvd_pow hp h

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem smul_mem_orbit_smul (g h : G) (a : α) : g • a ∈ orbit G (h • a)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)

Tactic:
simp only [orbit_smul, mem_orbit]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_iInf (f : ι → G.Subgraph) (v : V) :
    (⨅ i, f i).neighborSet v = (⋂ i, (f i).neighborSet v) ∩ G.neighborSet v

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
v : V
⊢ (⨅ i, f i).neighborSet v = (⋂ i, (f i).neighborSet v) ∩ G.neighborSet v

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem measure_sum_seq (κ : Kernel α β) [h : IsSFiniteKernel κ] (a : α) :
    (Measure.sum fun n => seq κ n a) = κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
a : α
⊢ (Measure.sum fun n => (κ.seq n) a) = κ a

Tactic:
rw [← Kernel.sum_apply, kernel_sum_seq κ]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem pi_diff_pi_subset (i : Set α) (s t : ∀ a, Set (π a)) :
    pi i s \ pi i t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)

Proof state:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ i.pi s \ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a

Tactic:
simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not,
  eval_apply] at hx

Result:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ x_1 ∈ i, eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a

Proof state:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
⊢ i.pi s \ i.pi t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)

Tactic:
refine diff_subset_comm.2 fun x hx a ha => ?_

Result:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ i.pi s \ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a

Proof state:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ x_1 ∈ i, eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a

Tactic:
exact hx.2 _ ha (hx.1 _ ha)

Result:
no goals