harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem min?_mem {t : RBNode α} (h : t.min? = some a) : a ∈ t

Proof state:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u_1
a : α
t : RBNode α
h : t.min? = some a
⊢ a ∈ t

Tactic:
rw [min?_eq_toList_head?] at h

Result:
α : Type u_1
a : α
t : RBNode α
h : t.toList.head? = some a
⊢ a ∈ t

Proof state:
α : Type u_1
a : α
t : RBNode α
h : t.toList.head? = some a
⊢ a ∈ t

Tactic:
rw [← mem_toList]

Result:
α : Type u_1
a : α
t : RBNode α
h : t.toList.head? = some a
⊢ a ∈ t.toList

Proof state:
α : Type u_1
a : α
t : RBNode α
h : t.toList.head? = some a
⊢ a ∈ t.toList

Tactic:
revert h

Result:
α : Type u_1
a : α
t : RBNode α
⊢ t.toList.head? = some a → a ∈ t.toList

Proof state:
α : Type u_1
a : α
t : RBNode α
⊢ t.toList.head? = some a → a ∈ t.toList

Tactic:
cases toList t <;> rintro ⟨⟩

Result:
case cons.refl
α : Type u_1
a : α
t : RBNode α
tail✝ : List α
⊢ a ∈ a :: tail✝
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma map_comp_ιMulti_family {I : Type*} [LinearOrder I] (v : I → M) (f : M →ₗ[R] N) :
    (map n f) ∘ (ιMulti_family R n v) = ιMulti_family R n (f ∘ v)

Proof state:
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
⊢ ⇑(map n f) ∘ ιMulti_family R n v = ιMulti_family R n (⇑f ∘ v)

Tactic:
ext ⟨s, hs⟩

Result:
case h.mk.a
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s.card = n
⊢ ↑((⇑(map n f) ∘ ιMulti_family R n v) ⟨s, hs⟩) = ↑(ιMulti_family R n (⇑f ∘ v) ⟨s, hs⟩)

Proof state:
case h.mk.a
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s.card = n
⊢ ↑((ιMulti R n) (⇑f ∘ fun i => v ↑((s.orderIsoOfFin ⋯) i))) = ↑((ιMulti R n) fun i => f (v ↑((s.orderIsoOfFin ⋯) i)))

Tactic:
rfl

Result:
no goals

Proof state:
case h.mk.a
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s.card = n
⊢ ↑((⇑(map n f) ∘ ιMulti_family R n v) ⟨s, hs⟩) = ↑(ιMulti_family R n (⇑f ∘ v) ⟨s, hs⟩)

Tactic:
simp only [ιMulti_family, Function.comp_apply, map_apply_ιMulti]

Result:
case h.mk.a
R : Type u
inst✝⁵ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
I : Type u_4
inst✝ : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s.card = n
⊢ ↑((ιMulti R n) (⇑f ∘ fun i => v ↑((s.orderIsoOfFin ⋯) i))) = ↑((ιMulti R n) fun i => f (v ↑((s.orderIsoOfFin ⋯) i)))
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
theorem finite_biUnion_mem_iff {is : Set β} {s : β → Set α} (his : is.Finite) :
    (⋃ i ∈ is, s i) ∈ f ↔ ∃ i ∈ is, s i ∈ f

Proof state:
α : Type u
β : Type v
f : Ultrafilter α
is : Set β
s : β → Set α
his : is.Finite
⊢ ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f

Tactic:
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), exists_mem_image]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem multiset_Ico_map_mod (n a : ℕ) :
    (Multiset.Ico n (n + a)).map (· % a) = Multiset.range a

Proof state:
n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a

Tactic:
convert congr_arg Finset.val (image_Ico_mod n a)

Result:
case h.e'_2
n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val

Proof state:
case h.e'_2
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y

Tactic:
exact mod_injOn_Ico _ _

Result:
no goals

Proof state:
case h.e'_2
n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val

Tactic:
refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm

Result:
case h.e'_2
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem refl_restr_source (s : Set α) : ((PartialEquiv.refl α).restr s).source = s

Proof state:
α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).source = s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
theorem toAffineEquiv_injective : Injective (toAffineEquiv : (P₁ ≃ᵃL[k] P₂) → P₁ ≃ᵃ[k] P₂)

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
⊢ Injective toAffineEquiv

Tactic:
rintro ⟨e, econt, einv_cont⟩ ⟨e', e'cont, e'inv_cont⟩ H

Result:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᵃ[k] P₂
econt : Continuous e.toFun
einv_cont : Continuous e.invFun
e' : P₁ ≃ᵃ[k] P₂
e'cont : Continuous e'.toFun
e'inv_cont : Continuous e'.invFun
H :
  { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont }.toAffineEquiv =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }.toAffineEquiv
⊢ { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont } =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }

Proof state:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : Module k V₁
inst✝⁵ : AddTorsor V₁ P₁
inst✝⁴ : TopologicalSpace P₁
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₂ P₂
inst✝ : TopologicalSpace P₂
e : P₁ ≃ᵃ[k] P₂
econt : Continuous e.toFun
einv_cont : Continuous e.invFun
e' : P₁ ≃ᵃ[k] P₂
e'cont : Continuous e'.toFun
e'inv_cont : Continuous e'.invFun
H :
  { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont }.toAffineEquiv =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }.toAffineEquiv
⊢ { toAffineEquiv := e, continuous_toFun := econt, continuous_invFun := einv_cont } =
    { toAffineEquiv := e', continuous_toFun := e'cont, continuous_invFun := e'inv_cont }

Tactic:
congr

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem iInter_Ioi_coe_nat : ⋂ n : ℕ, Ioi (n : ℝ≥0∞) = {∞}

Proof state:
⊢ ⋂ n, Ioi ↑n = {⊤}

Tactic:
simp only [← compl_Iic, ← compl_iUnion, iUnion_Iic_coe_nat, compl_compl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
lemma mkDerivation_one_eq_derivative (f : R[X]) : mkDerivation R (1 : R[X]) f = derivative f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ((mkDerivation R) 1) f = derivative f

Tactic:
rw [mkDerivation_one_eq_derivative']

Result:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ derivative' f = derivative f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ derivative' f = derivative f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[local simp] lemma emod_two_ne_zero : ¬n % 2 = 0 ↔ n % 2 = 1

Proof state:
n : ℤ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

Tactic:
rcases emod_two_eq_zero_or_one n with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonpos_iff_pos_imp_nonpos : a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
simp only [neg_pos, neg_nonneg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.hasDerivAt_convolution_left [IsNegInvariant μ]
    (hcf : HasCompactSupport f₀) (hf : ContDiff 𝕜 1 f₀) (hg : LocallyIntegrable g₀ μ) (x₀ : 𝕜) :
    HasDerivAt (f₀ ⋆[L, μ] g₀) ((deriv f₀ ⋆[L, μ] g₀) x₀) x₀

Proof state:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : SFinite μ
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt (f₀ ⋆[L, μ] g₀) ((deriv f₀ ⋆[L, μ] g₀) x₀) x₀

Tactic:
simp (config := { singlePass := true }) only [← convolution_flip]

Result:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : SFinite μ
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt (g₀ ⋆[L.flip, μ] f₀) ((g₀ ⋆[L.flip, μ] deriv f₀) x₀) x₀

Proof state:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : SFinite μ
inst✝ : μ.IsNegInvariant
hcf : HasCompactSupport f₀
hf : ContDiff 𝕜 1 f₀
hg : LocallyIntegrable g₀ μ
x₀ : 𝕜
⊢ HasDerivAt (g₀ ⋆[L.flip, μ] f₀) ((g₀ ⋆[L.flip, μ] deriv f₀) x₀) x₀

Tactic:
exact hcf.hasDerivAt_convolution_right L.flip hg hf x₀

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Defs.lean
@[aesop safe apply (rule_sets := [SetLike])]
lemma ratCast_mem (s : S) (q : ℚ) : (q : K) ∈ s

Proof state:
K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ
⊢ ↑q ∈ s

Tactic:
simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den)

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma analyticWithinAt_pi_iff :
    AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e ↔ ∀ i, AnalyticWithinAt 𝕜 (f i) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e ↔ ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e

Tactic:
refine ⟨fun h i ↦ ?_, fun h ↦ .pi h⟩

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
h : AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
h : AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e
i : ι
⊢ AnalyticWithinAt 𝕜 (f i) s e

Tactic:
exact ((ContinuousLinearMap.proj (R := 𝕜) i).analyticAt _).comp_analyticWithinAt h

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Defs.lean
@[aesop safe apply (rule_sets := [SetLike])]
lemma qsmul_mem (s : S) (q : ℚ) (hx : x ∈ s) : q • x ∈ s

Proof state:
K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
x : K
s : S
q : ℚ
hx : x ∈ s
⊢ q • x ∈ s

Tactic:
simpa only [Rat.smul_def] using mul_mem (ratCast_mem _ _) hx

Result:
no goals
-- Mathlib/RingTheory/Regular/IsSMulRegular.lean
lemma biUnion_associatedPrimes_eq_compl_regular [IsNoetherianRing R] :
    ⋃ p ∈ associatedPrimes R M, p = { r : R | IsSMulRegular M r }ᶜ :=
  Eq.trans (biUnion_associatedPrimes_eq_zero_divisors R M) <| by
    simp_rw [Set.compl_setOf, isSMulRegular_iff_smul_eq_zero_imp_eq_zero,
      not_forall, exists_prop, and_comm]

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {r | IsSMulRegular M r}ᶜ

Tactic:
simp_rw [Set.compl_setOf, isSMulRegular_iff_smul_eq_zero_imp_eq_zero,
  not_forall, exists_prop, and_comm]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.mem_nhds_iff {x : α} {s : Set α} : s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
rw [nhds_eq_comap_uniformity, mem_comap]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
simp_rw [ball]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem apply_mem_of_equiv_iff {I : Ideal R} {f : R ≃+* S} {x : R} :
    f x ∈ I.map f ↔ x ∈ I

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
x : R
⊢ f x ∈ map f I ↔ x ∈ I

Tactic:
rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem direction_mongePlane {n : ℕ} (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} :
    (s.mongePlane i₁ i₂).direction =
      (ℝ ∙ s.points i₁ -ᵥ s.points i₂)ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (s.mongePlane i₁ i₂).direction = (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
  direction_affineSpan]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem mul_inverse_cancel_left (x y : M₀) (h : IsUnit x) : x * (inverse x * y) = y

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x * (inverse x * y) = y

Tactic:
rw [← mul_assoc, mul_inverse_cancel x h, one_mul]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_sub_partitions (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F)
    {π₁ π₂ : TaggedPrepartition I} (h₁ : π₁.IsPartition) (h₂ : π₂.IsPartition) :
    integralSum f vol π₁ - integralSum f vol π₂ =
      ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        (vol J (f <| (π₁.infPrepartition π₂.toPrepartition).tag J) -
          vol J (f <| (π₂.infPrepartition π₁.toPrepartition).tag J))

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ ∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
      ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) =
    ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₁.infPrepartition π₂.toPrepartition).tag x)) -
      ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₂.infPrepartition π₁.toPrepartition).tag x))

Tactic:
simp only [infPrepartition_toPrepartition, inf_comm]

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ integralSum f vol π₁ - integralSum f vol π₂ =
    ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
        (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))

Tactic:
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁,
  integralSum, integralSum, Finset.sum_sub_distrib]

Result:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ ∑ J ∈ (π₁.infPrepartition π₂.toPrepartition).boxes, (vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) -
      ∑ J ∈ (π₂.infPrepartition π₁.toPrepartition).boxes, (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)) =
    ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₁.infPrepartition π₂.toPrepartition).tag x)) -
      ∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, (vol x) (f ((π₂.infPrepartition π₁.toPrepartition).tag x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_flatMap (f : β → γ) (g : α → Array β) (l : Array α) :
     (l.flatMap g).map f = l.flatMap fun a => (g a).map f

Proof state:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
g : α → Array β
l : List α
⊢ map f (flatMap g { toList := l }) = flatMap (fun a => map f (g a)) { toList := l }

Tactic:
simp [List.map_flatMap]

Result:
no goals

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
g : α → Array β
l : Array α
⊢ map f (flatMap g l) = flatMap (fun a => map f (g a)) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
g : α → Array β
l : List α
⊢ map f (flatMap g { toList := l }) = flatMap (fun a => map f (g a)) { toList := l }
-- Mathlib/Data/Finset/Image.lean
theorem fin_map {n} {s : Finset ℕ} : (s.fin n).map Fin.valEmbedding = s.filter (· < n)

Proof state:
n : ℕ
s : Finset ℕ
⊢ map Fin.valEmbedding (Finset.fin n s) = filter (fun x => x < n) s

Tactic:
simp [Finset.fin, Finset.map_map]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
lemma LSeriesSummable_zetaMul (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    LSeriesSummable χ.zetaMul s

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖(toArithmeticFunction fun x => χ ↑x) n‖ ≤ 1

Tactic:
simpa only [toArithmeticFunction, coe_mk, hn, ↓reduceIte]
using norm_le_one χ _

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑χ.zetaMul) s

Tactic:
refine ArithmeticFunction.LSeriesSummable_mul (LSeriesSummable_zeta_iff.mpr hs) <|
  LSeriesSummable_of_bounded_of_one_lt_re (m := 1) (fun n hn ↦ ?_) hs

Result:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖(toArithmeticFunction fun x => χ ↑x) n‖ ≤ 1
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isInt_ratCast {R : Type*} [DivisionRing R] : {q : ℚ} → {n : ℤ} →
    IsInt q n → IsInt (q : R) n
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CharP/Quotient.lean
theorem quotient_iff_le_ker_natCast {R : Type*} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) :
    CharP (R ⧸ I) n ↔ I.comap (Nat.castRingHom R) ≤ RingHom.ker (Nat.castRingHom R)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)

Tactic:
rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]

Result:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate_of_length_pos (h : 0 < n) : find? p (replicate n a) = if p a then some a else none

Proof state:
n : Nat
α✝ : Type u_1
p : α✝ → Bool
a : α✝
h : 0 < n
⊢ find? p (replicate n a) = if p a = true then some a else none

Tactic:
simp [find?_replicate, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem subtypeVal_nil {α : TypeVec.{u} 0} (ps : α ⟹ «repeat» 0 Prop) :
    TypeVec.subtypeVal ps = nilFun :=
  funext <| by rintro ⟨⟩

Proof state:
α : TypeVec.{u} 0
ps : α ⟹ «repeat» 0 Prop
⊢ ∀ (x : Fin2 0), subtypeVal ps x = nilFun x

Tactic:
rintro ⟨⟩

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem zero_not_mem_iff {a : A} : (0 : R) ∉ σ a ↔ IsUnit a

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ 0 ∉ σ a ↔ IsUnit a

Tactic:
rw [zero_mem_iff, Classical.not_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n

Proof state:
m n : Nat
⊢ n.gcd (m * n) = n

Tactic:
rw [gcd_comm, gcd_mul_left_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
theorem cross_orthogonal_right {v w : ℙ F (Fin 3 → F)} (h : v ≠ w) :
    (cross v w).orthogonal w

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (w.cross v).orthogonal w

Tactic:
exact cross_orthogonal_left h.symm

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal w

Tactic:
rw [cross_comm]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (w.cross v).orthogonal w
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem card_support_mul_le : #(p * q).support ≤ #p.support * #q.support

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p * q).support ≤ #p.support * #q.support

Tactic:
calc #(p * q).support
 _ = #(p.toFinsupp * q.toFinsupp).support := by rw [← support_toFinsupp, toFinsupp_mul]
 _ ≤ #(p.toFinsupp.support + q.toFinsupp.support) :=
  Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
 _ ≤ #p.support * #q.support := Finset.card_image₂_le ..

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p * q).support = #(p.toFinsupp * q.toFinsupp).support

Tactic:
rw [← support_toFinsupp, toFinsupp_mul]

Result:
no goals