harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_word_prod_nontrivial_of_head_eq_last {i} (w : NeWord H i i) :
    lift f w.prod ≠ 1

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i : ι
w : NeWord H i i
⊢ (lift f) w.prod ≠ 1

Tactic:
obtain ⟨k, hk⟩ := exists_ne i

Result:
case intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i : ι
w : NeWord H i i
k : ι
hk : k ≠ i
⊢ (lift f) w.prod ≠ 1

Proof state:
case intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i : ι
w : NeWord H i i
k : ι
hk : k ≠ i
⊢ (lift f) w.prod ≠ 1

Tactic:
exact lift_word_prod_nontrivial_of_other_i f X hXnonempty hXdisj hpp w hk hk

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_div' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
    (f : F) (hf : ∀ a, f a⁻¹ = (f a)⁻¹) (a b : G) : f (a / b) = f a / f b

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
a b : G
⊢ f (a / b) = f a / f b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
lemma transpose_invOf [Invertible A] [Invertible Aᵀ] : (⅟A)ᵀ = ⅟(Aᵀ)

Proof state:
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
this : Invertible Aᵀ := A.invertibleTranspose
⊢ (⅟A)ᵀ = ⅟Aᵀ

Tactic:
convert (rfl : _ = ⅟(Aᵀ))

Result:
no goals

Proof state:
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
⊢ (⅟A)ᵀ = ⅟Aᵀ

Tactic:
letI := invertibleTranspose A

Result:
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
this : Invertible Aᵀ := A.invertibleTranspose
⊢ (⅟A)ᵀ = ⅟Aᵀ
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_le' (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})

Tactic:
have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by
  ext1 ω; simp only [Set.mem_inter_iff, Set.mem_setOf_eq, le_min_iff]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
⊢ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ i ⊓ j}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω ≤ i ⊓ j}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω ≤ i}

Tactic:
intro j

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet {ω | τ ω ≤ i ⊓ j}

Tactic:
exact f.mono (min_le_right i j) _ (hτ _)

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
⊢ ω ∈ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} ↔ ω ∈ {ω | τ ω ≤ i ⊓ j}

Tactic:
simp only [Set.mem_inter_iff, Set.mem_setOf_eq, le_min_iff]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet ({ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j})

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i j : ι
this : {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ j} = {ω | τ ω ≤ i ⊓ j}
⊢ MeasurableSet {ω | τ ω ≤ i ⊓ j}
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem mk_eq_div {r s} :
    (Localization.mk r s : FractionRing A) =
      (algebraMap _ _ r / algebraMap A _ s : FractionRing A)

Proof state:
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
r : A
s : ↥(nonZeroDivisors A)
⊢ Localization.mk r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s

Tactic:
rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem Filter.HasBasis.uniformEquicontinuous_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop}
    {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α}
    (hβ : (𝓤 β).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) :
    UniformEquicontinuous F ↔
      ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
simp only [Prod.forall]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (a b : β), (a, b) ∈ s₁ ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (a b : β), (a, b) ∈ s₁ ia → ((⇑ofFun ∘ swap F) a, (⇑ofFun ∘ swap F) b) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ UniformEquicontinuous F ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous,
  hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_diff (h : s ⊆ t) (f : α → G) :
    mulIndicator (t \ s) f = mulIndicator t f * (mulIndicator s f)⁻¹ :=
  eq_mul_inv_of_mul_eq <| by
    rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
      union_eq_self_of_subset_right h]
    exact disjoint_sdiff_self_left

Proof state:
α : Type u_1
G : Type u_5
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ (t \ s).mulIndicator f * s.mulIndicator f = t.mulIndicator f

Tactic:
rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
  union_eq_self_of_subset_right h]

Result:
case h
α : Type u_1
G : Type u_5
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s

Proof state:
case h
α : Type u_1
G : Type u_5
inst✝ : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s

Tactic:
exact disjoint_sdiff_self_left

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_toGraph_eq [DecidableEq α] : h.toGraph.adjMatrix α = A

Proof state:
case a
V : Type u_1
α : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α h.toGraph i j = A i j

Tactic:
obtain h' | h' := h.zero_or_one i j <;> simp [h']

Result:
no goals

Proof state:
V : Type u_1
α : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
⊢ adjMatrix α h.toGraph = A

Tactic:
ext i j

Result:
case a
V : Type u_1
α : Type u_2
inst✝² : MulZeroOneClass α
inst✝¹ : Nontrivial α
A : Matrix V V α
h : A.IsAdjMatrix
inst✝ : DecidableEq α
i j : V
⊢ adjMatrix α h.toGraph i j = A i j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_fill {w i : Nat} {v : Bool} :
    (fill w v).getLsbD i = (v && decide (i < w))

Proof state:
w i : Nat
v : Bool
⊢ (fill w v).getLsbD i = (v && decide (i < w))

Tactic:
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eval_eq_prod_roots_sub_of_monic_of_splits_id {p : K[X]} (m : Monic p)
    (hsplit : Splits (RingHom.id K) p) (v : K) :
    eval v p = (p.roots.map fun a ↦ v - a).prod

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
m : p.Monic
hsplit : Splits (RingHom.id K) p
v : K
⊢ eval v p = (Multiset.map (fun a => v - a) p.roots).prod

Tactic:
simp [eval_eq_prod_roots_sub_of_splits_id hsplit, m]

Result:
no goals
-- Mathlib/Analysis/Normed/Order/Lattice.lean
lemma isClosed_nonneg : IsClosed {x : α | 0 ≤ x}

Proof state:
case h
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x✝ : α
⊢ x✝ ∈ {x | 0 ≤ x} ↔ x✝ ∈ negPart ⁻¹' {0}

Tactic:
simp [negPart_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ IsClosed {x | 0 ≤ x}

Tactic:
have : {x : α | 0 ≤ x} = negPart ⁻¹' {0} := by ext; simp [negPart_eq_zero]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
this : {x | 0 ≤ x} = negPart ⁻¹' {0}
⊢ IsClosed {x | 0 ≤ x}

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
this : {x | 0 ≤ x} = negPart ⁻¹' {0}
⊢ IsClosed (negPart ⁻¹' {0})

Tactic:
exact isClosed_singleton.preimage continuous_negPart

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
⊢ {x | 0 ≤ x} = negPart ⁻¹' {0}

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x✝ : α
⊢ x✝ ∈ {x | 0 ≤ x} ↔ x✝ ∈ negPart ⁻¹' {0}

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
this : {x | 0 ≤ x} = negPart ⁻¹' {0}
⊢ IsClosed {x | 0 ≤ x}

Tactic:
rw [this]

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
this : {x | 0 ≤ x} = negPart ⁻¹' {0}
⊢ IsClosed (negPart ⁻¹' {0})
-- Mathlib/Algebra/Group/Hom/Basic.lean
@[to_additive]
lemma comp_mul [CommMonoid P] (g : N →* P) (f₁ f₂ : M →* N) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Proof state:
case h
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝

Tactic:
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext

Result:
case h
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Iio (y : ℝ) : Real.toEReal ⁻¹' Iio y = Iio y

Proof state:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑↑y = Iio y

Tactic:
refine preimage_comp.trans ?_

Result:
y : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑↑y) = Iio y

Proof state:
y : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑↑y) = Iio y

Tactic:
simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

Result:
no goals

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' Iio ↑y = Iio y

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (WithTop.some y))) = _

Result:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑↑y = Iio y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem zero_add [NeZero n] (k : Fin n) : (0 : Fin n) + k = k

Proof state:
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ 0 + k = k

Tactic:
ext

Result:
case h
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ ↑(0 + k) = ↑k

Proof state:
case h
n : Nat
inst✝ : NeZero n
k : Fin n
⊢ ↑(0 + k) = ↑k

Tactic:
simp [Fin.add_def, Nat.mod_eq_of_lt k.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
    (ne : i ≠ j) : (a.set i v)[j]? = a[j]?

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
j : Nat
v : α
ne : i ≠ j
⊢ (a.set i v h)[j]? = a[j]?

Tactic:
by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem udiv_eq_divRec (hd : 0#w < d) :
    let out := divRec w {n, d} (DivModState.init w)
    n / d = out.q

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
this✝ : DivModState.Lawful { n := n, d := d } (DivModState.init w)
this : DivModState.Lawful { n := n, d := d } (divRec (DivModState.init w).wn { n := n, d := d } (DivModState.init w))
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n / d = out.q

Tactic:
apply DivModState.udiv_eq_of_lawful this (wn_divRec ..)

Result:
no goals

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
this : DivModState.Lawful { n := n, d := d } (DivModState.init w)
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n / d = out.q

Tactic:
have := lawful_divRec this

Result:
w : Nat
d n : BitVec w
hd : 0#w < d
this✝ : DivModState.Lawful { n := n, d := d } (DivModState.init w)
this : DivModState.Lawful { n := n, d := d } (divRec (DivModState.init w).wn { n := n, d := d } (DivModState.init w))
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n / d = out.q

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n / d = out.q

Tactic:
have := DivModState.lawful_init {n, d} hd

Result:
w : Nat
d n : BitVec w
hd : 0#w < d
this : DivModState.Lawful { n := n, d := d } (DivModState.init w)
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n / d = out.q
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma opProdIsoCoprod_hom_snd : (opProdIsoCoprod A B).hom.unop ≫ prod.snd = coprod.inr.unop

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (opProdIsoCoprod A B).hom.unop ≫ prod.snd = coprod.inr.unop

Tactic:
simp [opProdIsoCoprod]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma InfClosed.insert_lowerBounds {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) :
    InfClosed (insert a s)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
h : InfClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
h : InfClosed s
ha : a ∈ lowerBounds s
⊢ InfClosed (insert a s)

Tactic:
rw [InfClosed]

Result:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
h : InfClosed s
ha : a ∈ lowerBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s
-- Mathlib/Data/Real/Sign.lean
theorem sign_mul_pos_of_ne_zero (r : ℝ) (hr : r ≠ 0) : 0 < sign r * r

Proof state:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r = 0

Tactic:
have hs0 := (zero_eq_mul.mp h).resolve_right hr

Result:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
hs0 : r.sign = 0
⊢ r = 0

Proof state:
r : ℝ
hr : r ≠ 0
⊢ 0 < r.sign * r

Tactic:
refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_

Result:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
⊢ r = 0

Proof state:
r : ℝ
hr : r ≠ 0
h : 0 = r.sign * r
hs0 : r.sign = 0
⊢ r = 0

Tactic:
exact sign_eq_zero_iff.mp hs0

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_map {l : List (Option α)} {f : α → β} :
    reduceOption (map (Option.map f) l) = map f (reduceOption l)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map (Option.map f) []).reduceOption = map f [].reduceOption

Tactic:
simp only [reduceOption_nil, map_nil]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption

Tactic:
cases hd <;>
  simpa [Option.map_some', map, eq_self_iff_true, reduceOption_cons_of_some] using hl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List (Option α)
f : α → β
⊢ (map (Option.map f) l).reduceOption = map f l.reduceOption

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map (Option.map f) []).reduceOption = map f [].reduceOption

case cons
α : Type u_1
β : Type u_2
f : α → β
hd : Option α
tl : List (Option α)
hl : (map (Option.map f) tl).reduceOption = map f tl.reduceOption
⊢ (map (Option.map f) (hd :: tl)).reduceOption = map f (hd :: tl).reduceOption
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
lemma rlp_isStableUnderProductsOfShape (J : Type*) :
    T.rlp.IsStableUnderProductsOfShape J

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ T.rlp.IsStableUnderProductsOfShape J

Tactic:
apply IsStableUnderProductsOfShape.mk

Result:
case hW
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ ∀ (X₁ X₂ : J → C) [inst : Limits.HasProduct X₁] [inst_1 : Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.map f)

Proof state:
case hW
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
⊢ ∀ (X₁ X₂ : J → C) [inst : Limits.HasProduct X₁] [inst_1 : Limits.HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.map f)

Tactic:
intro A B _ _ f hf X Y p hp

Result:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty p (Limits.Pi.map f)

Proof state:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty p (f j)
⊢ HasLiftingProperty p (Limits.Pi.map f)

Tactic:
infer_instance

Result:
no goals

Proof state:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty p (Limits.Pi.map f)

Tactic:
have := fun j ↦ hf j _ hp

Result:
case hW
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
this : ∀ (j : J), HasLiftingProperty p (f j)
⊢ HasLiftingProperty p (Limits.Pi.map f)
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToFun_le (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hC : 0 ≤ C) :
    ‖setToFun μ T hT f‖ ≤ C * ‖hf.toL1 f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
⊢ ‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_setToL1_le_mul_norm hT hC _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
rw [setToFun_eq hT hf]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
⊢ ‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ C * ‖Integrable.toL1 f hf‖
-- Mathlib/Data/Set/Function.lean
theorem piecewise_mono {δ : α → Type*} [∀ i, Preorder (δ i)] {s : Set α}
    [∀ j, Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : ∀ i, δ i} (h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i)
    (h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i) : s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Proof state:
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ i ∈ s, f₁ i ≤ g₁ i
h₂ : ∀ i ∉ s, f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
apply piecewise_le <;> intros <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
lemma cpolynomialAt  : CPolynomialAt 𝕜 f x :=
  f.hasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
    (by simp only [Metric.emetric_ball_top, Set.mem_univ])

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
x : (i : ι) → Em i
⊢ x ∈ EMetric.ball 0 ⊤

Tactic:
simp only [Metric.emetric_ball_top, Set.mem_univ]

Result:
no goals