harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_inter (hs : s.Finite) :
    uniformOn s (t ∩ u) = uniformOn (s ∩ t) u * uniformOn s t

Proof state:
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ 0

Tactic:
rwa [← Measure.count_eq_zero_iff] at hst

Result:
no goals

Proof state:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Tactic:
rw [hst, uniformOn_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul,
  uniformOn_eq_zero_iff hs, ← Set.inter_assoc, hst, Set.empty_inter]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Tactic:
by_cases hst : s ∩ t = ∅

Result:
case pos
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Proof state:
case neg
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ (uniformOn s) (t ∩ u) = (uniformOn (s ∩ t)) u * (uniformOn s) t

Tactic:
rw [uniformOn, uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
  cond_apply (hs.inter_of_left _).measurableSet, mul_comm _ (Measure.count (s ∩ t)),
  ← mul_assoc, mul_comm _ (Measure.count (s ∩ t)), ← mul_assoc, ENNReal.mul_inv_cancel, one_mul,
  mul_comm, Set.inter_assoc]

Result:
case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ 0

case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ ⊤

Proof state:
case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ ⊤

Tactic:
exact (Measure.count_apply_lt_top.2 <| hs.inter_of_left _).ne

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem none : Partrec fun _ : α => @Part.none σ :=
  Nat.Partrec.none.of_eq fun n => by cases decode (α := α) n <;> simp

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
⊢ Part.none = (↑(decode n)).bind fun a => map encode ((fun x => Part.none) a)

Tactic:
cases decode (α := α) n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = []

Proof state:
α : Type u_1
l : List α
⊢ l.isEmpty = true ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem continuous_of_distribMulActionHom (φ : A →+[R] B) : Continuous φ

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁷ : Semiring R
A : Type u_2
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_3
inst✝³ : AddCommMonoid B
inst✝² : Module R B
aB : TopologicalSpace B
inst✝¹ : ContinuousAdd B
inst✝ : ContinuousSMul R B
φ : A →+[R] B
⊢ Continuous ⇑φ

Tactic:
rw [eq_moduleTopology R A, continuous_iff_le_induced]

Result:
R : Type u_1
τR : TopologicalSpace R
inst✝⁷ : Semiring R
A : Type u_2
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_3
inst✝³ : AddCommMonoid B
inst✝² : Module R B
aB : TopologicalSpace B
inst✝¹ : ContinuousAdd B
inst✝ : ContinuousSMul R B
φ : A →+[R] B
⊢ moduleTopology R A ≤ TopologicalSpace.induced (⇑φ) aB

Proof state:
R : Type u_1
τR : TopologicalSpace R
inst✝⁷ : Semiring R
A : Type u_2
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B : Type u_3
inst✝³ : AddCommMonoid B
inst✝² : Module R B
aB : TopologicalSpace B
inst✝¹ : ContinuousAdd B
inst✝ : ContinuousSMul R B
φ : A →+[R] B
⊢ moduleTopology R A ≤ TopologicalSpace.induced (⇑φ) aB

Tactic:
exact sInf_le <| ⟨continuousSMul_induced (φ.toMulActionHom),
  continuousAdd_induced φ.toAddMonoidHom⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.comp_of_eq (hh₂ : HasDerivAtFilter h₂ h₂' y L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') (hy : y = h x) :
    HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
hy : y = h x
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Tactic:
exact hh₂.comp x hh hL

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' y L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
hy : y = h x
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
y : 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
hy : y = h x
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L
-- Mathlib/Data/Rat/Lemmas.lean
theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a

Proof state:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : (a * ↑d).natAbs = (n * b).natAbs
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
simp only [Int.natAbs_mul, Int.natAbs_ofNat] at this

Result:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : a.natAbs * d = n.natAbs * b.natAbs
⊢ n.natAbs ∣ a.natAbs * d

Proof state:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
have := congr_arg Int.natAbs e

Result:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : (a * ↑d).natAbs = (n * b).natAbs
⊢ n.natAbs ∣ a.natAbs * d

Proof state:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Tactic:
refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
  c.dvd_of_dvd_mul_right ?_

Result:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ n.natAbs ∣ a.natAbs * d

Proof state:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Tactic:
rw [Rat.mk'_eq_divInt, divInt_eq_iff b0 (mod_cast h)] at e

Result:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Proof state:
a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩

Result:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Proof state:
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
this : a.natAbs * d = n.natAbs * b.natAbs
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
simp [this]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem hasSum_repr_symm (b : HilbertBasis ι 𝕜 E) (f : ℓ²(ι, 𝕜)) :
    HasSum (fun i => f i • b i) (b.repr.symm f)

Proof state:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i * 1) = ↑f i • lp.single 2 i 1
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Tactic:
rw [mul_one] at this

Result:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
⊢ NormedSpace 𝕜 ↥(lp (fun _i => 𝕜) 2)

Tactic:
infer_instance

Result:
no goals

Proof state:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
⊢ ↑f i • b i = b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i)

Tactic:
apply b.repr.injective

Result:
case h.a
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
⊢ b.repr (↑f i • b i) = b.repr (b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i))

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
⊢ (fun i => ↑f i • b i) = fun b_1 => b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) b_1)

Tactic:
ext i

Result:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun i => 𝕜) 2)
i : ι
⊢ ↑f i • b i = b.repr.symm.toContinuousLinearEquiv ((fun i => lp.single 2 i (↑f i)) i)
-- Mathlib/Data/Fintype/List.lean
theorem lists_nodup_finset (l : Finset α) : (lists (l.val)).Nodup

Proof state:
α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup

Tactic:
rw [← Finset.coe_toList l, Multiset.coe_nodup] at h_nodup

Result:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup

Proof state:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ (↑l.toList).lists.Nodup

Tactic:
exact nodup_permutations l.val.toList (h_nodup)

Result:
no goals

Proof state:
α : Type u_1
l : Finset α
⊢ l.val.lists.Nodup

Tactic:
have h_nodup : l.val.Nodup := l.nodup

Result:
α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup

Proof state:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ l.val.lists.Nodup

Tactic:
rw [← Finset.coe_toList l]

Result:
α : Type u_1
l : Finset α
h_nodup : l.toList.Nodup
⊢ (↑l.toList).lists.Nodup
-- Mathlib/Order/Cover.lean
@[simp] lemma wcovBy_insert (x : α) (s : Set α) : s ⩿ insert x s

Proof state:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t ⊆ s

Tactic:
rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]

Result:
no goals

Proof state:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Tactic:
refine Or.inl (subset_antisymm ?_ hst)

Result:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t ⊆ s

Proof state:
case pos
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

Tactic:
exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)

Result:
no goals

Proof state:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s

Tactic:
by_cases h : x ∈ t

Result:
case pos
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s

case neg
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∉ t
⊢ t = s ∨ t = insert x s

Proof state:
α : Type u_1
x : α
s : Set α
⊢ s ⩿ insert x s

Tactic:
refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_

Result:
α : Type u_1
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s
-- Mathlib/Data/List/InsertIdx.lean
theorem insertIdx_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} {a : α} {n : ℕ}
    (hl : ∀ x ∈ l, p x) (ha : p a) :
    (l.pmap f hl).insertIdx n (f a ha) = (insertIdx n a l).pmap f
      (fun _ h ↦ (eq_or_mem_of_mem_insertIdx h).elim (fun heq ↦ heq ▸ ha) (hl _))

Proof state:
case zero
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ insertIdx 0 (f a ha) (pmap f l hl) = pmap f (insertIdx 0 a l) ⋯

Tactic:
cases l <;> simp

Result:
no goals

Proof state:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
⊢ insertIdx n (f a ha) (pmap f l hl) = pmap f (insertIdx n a l) ⋯

Tactic:
induction n generalizing l with
| zero => cases l <;> simp
| succ n ihn => cases l <;> simp_all

Result:
no goals

Proof state:
case succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), insertIdx n (f a ha) (pmap f l hl) = pmap f (insertIdx n a l) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ insertIdx (n + 1) (f a ha) (pmap f l hl) = pmap f (insertIdx (n + 1) a l) ⋯

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isLowerSet_iff_forall_lt : IsLowerSet s ↔ ∀ ⦃a b : α⦄, b < a → a ∈ s → b ∈ s :=
  forall_congr' fun a => by simp [le_iff_eq_or_lt, or_imp, forall_and]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
⊢ (∀ ⦃b : α⦄, b ≤ a → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, b < a → a ∈ s → b ∈ s

Tactic:
simp [le_iff_eq_or_lt, or_imp, forall_and]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem diagonal [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
    {d : n → R} (h : ∀ i, 0 < d i) :
    PosDef (diagonal d) :=
  ⟨isHermitian_diagonal_of_self_adjoint _ <| funext fun i => IsSelfAdjoint.of_nonneg (h i).le,
    fun x hx => by
      refine Fintype.sum_pos ?_
      simp_rw [mulVec_diagonal, ← mul_assoc, Pi.lt_def]
      obtain ⟨i, hi⟩ := Function.ne_iff.mp hx
      exact ⟨fun i => conjugate_nonneg (h i).le _,
        i, conjugate_pos (h _) (isRegular_of_ne_zero hi)⟩⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ diagonal d *ᵥ x

Tactic:
refine Fintype.sum_pos ?_

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
⊢ 0 < fun i => star x i * (diagonal d *ᵥ x) i

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
⊢ (0 ≤ fun i => star x i * d i * x i) ∧ ∃ i, 0 i < star x i * d i * x i

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp hx

Result:
case intro
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
i : n
hi : x i ≠ 0 i
⊢ (0 ≤ fun i => star x i * d i * x i) ∧ ∃ i, 0 i < star x i * d i * x i

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
⊢ 0 < fun i => star x i * (diagonal d *ᵥ x) i

Tactic:
simp_rw [mulVec_diagonal, ← mul_assoc, Pi.lt_def]

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
⊢ (0 ≤ fun i => star x i * d i * x i) ∧ ∃ i, 0 i < star x i * d i * x i

Proof state:
case intro
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n → R
hx : x ≠ 0
i : n
hi : x i ≠ 0 i
⊢ (0 ≤ fun i => star x i * d i * x i) ∧ ∃ i, 0 i < star x i * d i * x i

Tactic:
exact ⟨fun i => conjugate_nonneg (h i).le _,
  i, conjugate_pos (h _) (isRegular_of_ne_zero hi)⟩

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem intCoe_mul [Ring R] {f g : ArithmeticFunction ℤ} :
    (↑(f * g) : ArithmeticFunction R) = ↑f * g

Proof state:
case h
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
⊢ ↑(f * g) = ↑f * ↑g

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem divp_eq_one_iff_eq {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = u :=
  (Units.mul_left_inj u).symm.trans <| by rw [divp_mul_cancel, one_mul]

Proof state:
α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a /ₚ u * ↑u = 1 * ↑u ↔ a = ↑u

Tactic:
rw [divp_mul_cancel, one_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_eq_iInf : infDist x s = ⨅ y : s, dist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ⊤

Tactic:
exact fun _ ↦ edist_ne_top _ _

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x s = ⨅ y, dist x ↑y

Tactic:
rw [infDist, infEdist, iInf_subtype', ENNReal.toReal_iInf]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ⨅ i, (edist x ↑i).toReal = ⨅ y, dist x ↑y

α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ∀ (i : Subtype (Membership.mem s)), edist x ↑i ≠ ⊤

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ⨅ i, (edist x ↑i).toReal = ⨅ y, dist x ↑y

Tactic:
simp only [dist_edist]

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem one_bits : Nat.bits 1 = [true]

Proof state:
case h.e'_3.h.e'_3

⊢ [] = bits 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ bits 1 = [true]

Tactic:
convert bit1_bits 0

Result:
case h.e'_3.h.e'_3

⊢ [] = bits 0
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_add [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f₁ f₂ : M₁ →SL[σ₁₂] M₂) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
⊢ g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g.comp (f₁ + f₂)) x✝ = (g.comp f₁ + g.comp f₂) x✝

Proof state:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g.comp (f₁ + f₂)) x✝ = (g.comp f₁ + g.comp f₂) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_zero [∀ i, Zero (β i)] (p : ι → Prop) [DecidablePred p] :
    (0 : Π₀ i, β i).filter p = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
i✝ : ι
⊢ (filter p 0) i✝ = 0 i✝

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
i✝ : ι
⊢ (filter p 0) i✝ = 0 i✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem finset_sup_apply_le {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {a : ℝ} (ha : 0 ≤ a)
    (h : ∀ i, i ∈ s → p i x ≤ a) : s.sup p x ≤ a

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup fun i => ⟨(p i) x, ⋯⟩) ≤ a

Tactic:
exact Finset.sup_le h

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i) x ≤ a
⊢ (s.sup p) x ≤ a

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup p) x ≤ ↑a

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup p) x ≤ ↑a

Tactic:
rw [finset_sup_apply, NNReal.coe_le_coe]

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup fun i => ⟨(p i) x, ⋯⟩) ≤ a
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem constr_basis (f : ι → M') (i : ι) : (constr (M' := M') b S f : M → M') (b i) = f i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ ((b.constr S) f) (b i) = f i

Tactic:
simp [Basis.constr_apply, b.repr_self]

Result:
no goals