harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_cos_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₃ p₂ / Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ dist p₃ p₂ / (∡ p₂ p₃ p₁).cos = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  dist_div_cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inr (right_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem surjOn_iff_exists_map_subtype :
    SurjOn f s t ↔ ∃ (t' : Set β) (g : s → t'), t ⊆ t' ∧ Surjective g ∧ ∀ x : s, f x = g x :=
  ⟨fun h =>
    ⟨_, (mapsTo_image f s).restrict f s _, h, surjective_mapsTo_image_restrict _ _, fun _ => rfl⟩,
    fun ⟨t', g, htt', hg, hfg⟩ y hy =>
    let ⟨x, hx⟩ := hg ⟨y, htt' hy⟩
    ⟨x, x.2, by rw [hfg, hx, Subtype.coe_mk]⟩⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ t' g, t ⊆ t' ∧ Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
y : β
hy : y ∈ t
t' : Set β
g : ↑s → ↑t'
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : ↑s), f ↑x = ↑(g x)
x : ↑s
hx : g x = ⟨y, ⋯⟩
⊢ f ↑x = y

Tactic:
rw [hfg, hx, Subtype.coe_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_mkVector {a : α} {b : β} {n : Nat} :
    zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
n : Nat
⊢ zipWith f (mkVector n a) (mkVector n b) = mkVector n (f a b)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
n i✝ : Nat
x✝ : i✝ < n
⊢ (zipWith f (mkVector n a) (mkVector n b))[i✝] = (mkVector n (f a b))[i✝]

Proof state:
case h
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : α → β → α✝
a : α
b : β
n i✝ : Nat
x✝ : i✝ < n
⊢ (zipWith f (mkVector n a) (mkVector n b))[i✝] = (mkVector n (f a b))[i✝]

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma measurable_singularPart_fun_right (κ η : Kernel α γ) (a : α) :
    Measurable (fun x : γ ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x)
      - Real.toNNReal (1 - rnDerivAux κ (κ + η) a x) * rnDeriv κ η a x)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable fun x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x

Tactic:
change Measurable ((Function.uncurry fun a b ↦
  ENNReal.ofReal (rnDerivAux κ (κ + η) a b)
  - ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a b) * rnDeriv κ η a b) ∘ (fun b ↦ (a, b)))

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable
    ((Function.uncurry fun a b =>
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b) ∘
      fun b => (a, b))

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable
    ((Function.uncurry fun a b =>
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b) ∘
      fun b => (a, b))

Tactic:
exact (measurable_singularPart_fun κ η).comp measurable_prod_mk_left

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp] lemma map₂_bot_right (f : α → β → γ) (a) : map₂ f a ⊥ = ⊥

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
⊢ map₂ f a ⊥ = ⊥

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_one  : toFin (1 : BitVec w) = 1

Proof state:
w : Nat
⊢ toFin 1 = 1

Tactic:
rw [toFin_inj]

Result:
w : Nat
⊢ 1 = { toFin := 1 }

Proof state:
w : Nat
⊢ 1 = { toFin := 1 }

Tactic:
simp only [ofNat_eq_ofNat, ofFin_ofNat]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_equiv {P P' Q Q' : Fin 3 → R} (hP : P ≈ P') (hQ : Q ≈ Q') :
    W'.add P Q ≈ W'.add P' Q'

Proof state:
case intro.intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun m => m • P') u) ((fun m => m • Q') v) ≈ W'.add P' Q'

Tactic:
exact add_smul_equiv P' Q' u.isUnit v.isUnit

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P P' Q Q' : Fin 3 → R
hP : P ≈ P'
hQ : Q ≈ Q'
⊢ W'.add P Q ≈ W'.add P' Q'

Tactic:
rcases hP, hQ with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩

Result:
case intro.intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun m => m • P') u) ((fun m => m • Q') v) ≈ W'.add P' Q'
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem arsinh_zero : arsinh 0 = 0

Proof state:
⊢ arsinh 0 = 0

Tactic:
simp [arsinh]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem graph_map_snd_eq_range (f : E →ₗ.[R] F) :
    f.graph.map (LinearMap.snd R E F) = LinearMap.range f.toFun

Proof state:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x✝ : F
⊢ x✝ ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x✝ ∈ LinearMap.range f.toFun

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.snd R E F) f.graph = LinearMap.range f.toFun

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x✝ : F
⊢ x✝ ∈ Submodule.map (LinearMap.snd R E F) f.graph ↔ x✝ ∈ LinearMap.range f.toFun
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
@[simp] lemma eHolderNorm_eq_top : eHolderNorm r f = ∞ ↔ ¬ MemHolder r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = ⊤ ↔ ¬MemHolder r f

Tactic:
rw [← eHolderNorm_ne_top, not_not]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem range_eq_map (f : M →[L] N) : f.range = map f ⊤

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ f.range = Substructure.map f ⊤

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ Substructure.map f ⊤

Proof state:
case h
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ Substructure.map f ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem exists_isCompact_not_null [Regular μ] : (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.Regular
⊢ (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0

Tactic:
simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
  ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ico_add_one_add_one_eq_Ioc (a b : α) : Ico (a + 1) (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_single (n : ℕ) (r : R) : (⟨Finsupp.single n r⟩ : R[X]) = monomial n r

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ { toFinsupp := Finsupp.single n r } = (monomial n) r

Tactic:
simp [monomial]

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Proof state:
α : Type u
σ : Type v
M : NFA α σ
x : List α
⊢ x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_const_smul {f : α → F} (c : 𝕜) (hq_pos : 0 < q) :
    eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ

Tactic:
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul]
  using eLpNorm'_const_smul_le (c := c⁻¹) (f := c • f) hq_pos

Result:
no goals

Proof state:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm' (0 • f) q μ = ‖0‖ₑ * eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm, hq_pos]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
hq_pos : 0 < q
⊢ eLpNorm' (0 • f) q μ = ‖0‖ₑ * eLpNorm' f q μ

case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_

Result:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma ι_snd : ι f g ≫ biprod.snd = kernel.ι (f ≫ g) ≫ f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ ι f g ≫ biprod.snd = kernel.ι (f ≫ g) ≫ f

Tactic:
simp [ι]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem pi_top (I : Set η) : (pi I fun i => (⊤ : Subgroup (f i))) = ⊤ :=
  ext fun x => by simp [mem_pi]

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
I : Set η
x : (i : η) → f i
⊢ (x ∈ pi I fun i => ⊤) ↔ x ∈ ⊤

Tactic:
simp [mem_pi]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_one_left (i : ℤ) : lcm 1 i = natAbs i

Proof state:
i : ℤ
⊢ lcm 1 i = i.natAbs

Tactic:
rw [Int.lcm]

Result:
i : ℤ
⊢ (natAbs 1).lcm i.natAbs = i.natAbs

Proof state:
i : ℤ
⊢ (natAbs 1).lcm i.natAbs = i.natAbs

Tactic:
apply Nat.lcm_one_left

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_eq_pi_iff {θ : Angle} : θ.toReal = π ↔ θ = π

Proof state:
θ : Angle
⊢ θ.toReal = π ↔ θ = ↑π

Tactic:
rw [← toReal_inj, toReal_pi]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem IsDiag.add [AddZeroClass α] {A B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
    (A + B).IsDiag

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A + B) i j = 0

Tactic:
simp [ha h, hb h]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
⊢ (A + B).IsDiag

Tactic:
intro i j h

Result:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A + B) i j = 0
-- Mathlib/Data/Fin/Basic.lean
theorem heq_fun_iff {α : Sort*} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} :
    HEq f g ↔ ∀ i : Fin k, f i = g ⟨(i : ℕ), h ▸ i.2⟩

Proof state:
α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Tactic:
subst h

Result:
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Proof state:
α : Sort u_1
k : ℕ
f g : Fin k → α
⊢ HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem continuous_iSup_dom {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[iSup t₁, t₂] f ↔ ∀ i, Continuous[t₁ i, t₂] f

Proof state:
α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : ι → TopologicalSpace α
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ (i : ι), Continuous f

Tactic:
simp only [continuous_iff_le_induced, iSup_le_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrable_finset_sum {ι} (s : Finset ι) {f : ι → X → E}
    (hf : ∀ i ∈ s, LocallyIntegrable (f i) μ) : LocallyIntegrable (fun a ↦ ∑ i ∈ s, f i a) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
ι : Type u_6
s : Finset ι
f : ι → X → E
hf : ∀ i ∈ s, LocallyIntegrable (f i) μ
⊢ LocallyIntegrable (fun a => ∑ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.sum_apply] using locallyIntegrable_finset_sum' s hf

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subsingleton {α β : Type*} [CommMonoid β] [Subsingleton α] [Fintype α] (f : α → β)
    (a : α) : ∏ x : α, f x = f a

Proof state:
α : Type u_9
β : Type u_10
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
this : Unique α
⊢ ∏ x : α, f x = f a

Tactic:
rw [prod_unique f, Subsingleton.elim default a]

Result:
no goals

Proof state:
α : Type u_9
β : Type u_10
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
⊢ ∏ x : α, f x = f a

Tactic:
have : Unique α := uniqueOfSubsingleton a

Result:
α : Type u_9
β : Type u_10
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
this : Unique α
⊢ ∏ x : α, f x = f a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem shiftRight_congr (m n : Nat) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m)
    (rhs' : BitVec n) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs >>> rhs = lhs' >>> rhs'

Proof state:
m n : Nat
lhs : BitVec m
rhs : BitVec n
lhs' : BitVec m
rhs' : BitVec n
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs >>> rhs = lhs' >>> rhs'

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma forall_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∀ a, p a) ↔ ∀ b, q b :=
  e.forall_congr_left.trans (by simp [h])

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_eq_iInf_biSup_of_nat {p : ℕ → Prop} {u : ℕ → α} :
    blimsup u atTop p = ⨅ i, ⨆ (j) (_ : p j ∧ i ≤ j), u j

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j

Tactic:
simp only [atTop_basis.blimsup_eq_iInf_iSup, @and_comm (p _), iSup_and, mem_Ici, iInf_true]

Result:
no goals
-- Mathlib/RingTheory/Presentation.lean
@[simp]
lemma localizationAway_dimension_zero : (localizationAway S r).dimension = 0

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (localizationAway S r).dimension = 0

Tactic:
simp [Presentation.dimension, localizationAway, Generators.localizationAway_vars]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/FunctionSeries.lean
theorem tendstoUniformly_tsum {f : α → β → F} (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) :
    TendstoUniformly (fun t : Finset α => fun x => ∑ n ∈ t, f n x)
      (fun x => ∑' n, f n x) atTop

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop univ

Tactic:
exact tendstoUniformlyOn_tsum hu fun n x _ => hfu n x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop

Tactic:
rw [← tendstoUniformlyOn_univ]

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (fun t x => ∑ n ∈ t, f n x) (fun x => ∑' (n : α), f n x) atTop univ
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma descOpcycles_comp {A A' : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j)
    (hk : K.d j i ≫ k = 0) (α : A ⟶ A') :
    K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj
      (by rw [reassoc_of% hk, zero_comp])

Proof state:
C : Type u_1
inst✝² : Category.{?u.62287, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A A' : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
⊢ K.d j i ≫ k ≫ α = 0

Tactic:
rw [reassoc_of% hk, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A A' : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
⊢ K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj ⋯

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_descOpcycles_assoc, p_descOpcycles]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem image_coe_mem_of_mem_comap {f : Filter α} {U : Set α} (h : U ∈ f) {W : Set U}
    (W_in : W ∈ comap ((↑) : U → α) f) : (↑) '' W ∈ f :=
  image_mem_of_mem_comap (by simp [h]) W_in

Proof state:
α : Type u_1
f : Filter α
U : Set α
h : U ∈ f
W : Set ↑U
W_in : W ∈ comap Subtype.val f
⊢ range Subtype.val ∈ f

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem Indep.ssubset_ground [h : RankPos M✶] (hI : M.Indep I) : I ⊂ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
⊢ I ⊂ M.E

Tactic:
obtain ⟨B, hB⟩ := hI.exists_isBase_superset

Result:
case intro
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Proof state:
case intro
α : Type u_1
M : Matroid α
I : Set α
h : M✶.RankPos
hI : M.Indep I
B : Set α
hB : M.IsBase B ∧ I ⊆ B
⊢ I ⊂ M.E

Tactic:
exact hB.2.trans_ssubset hB.1.ssubset_ground

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_zero_le {x : PGame} : x ⧏ 0 ↔ ∃ j, x.moveRight j ≤ 0

Proof state:
x : PGame
⊢ x ⧏ 0 ↔ ∃ j, x.moveRight j ≤ 0

Tactic:
rw [lf_iff_exists_le]

Result:
x : PGame
⊢ ((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, x.moveRight j ≤ 0) ↔ ∃ j, x.moveRight j ≤ 0

Proof state:
x : PGame
⊢ ((∃ i, x ≤ moveLeft 0 i) ∨ ∃ j, x.moveRight j ≤ 0) ↔ ∃ j, x.moveRight j ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem mul_inv_cancel (x : K) (hx : x ≠ 0) : x * IsFractionRing.inv A x = 1

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x *
      (mk' K ↑(sec (nonZeroDivisors A) x).2 ⟨(sec (nonZeroDivisors A) x).1, ⋯⟩ *
        (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) =
    (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩

Tactic:
rw [mk'_spec, ← eq_mk'_iff_mul_eq]

Result:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x = mk' K (↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) (sec (nonZeroDivisors A) x).2

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x = mk' K (↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) (sec (nonZeroDivisors A) x).2

Tactic:
exact (mk'_sec _ x).symm

Result:
no goals

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1

Tactic:
rw [IsFractionRing.inv, dif_neg hx, ←
  IsUnit.mul_left_inj
    (map_units K
      ⟨(sec _ x).1,
        mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
          hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
  one_mul, mul_assoc]

Result:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x *
      (mk' K ↑(sec (nonZeroDivisors A) x).2 ⟨(sec (nonZeroDivisors A) x).1, ⋯⟩ *
        (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) =
    (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t

Proof state:
α : Type u_1
b : Bool
t e : α
⊢ (bif !b then t else e) = bif b then e else t

Tactic:
cases b <;> rfl

Result:
no goals