harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions monovary iff the rearrangement inequality holds. -/
lemma monovaryOn_iff_mul_rearrangement :
    MonovaryOn f g s ↔
      ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
s : Set ι
⊢ MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j

Tactic:
simp only [smul_eq_mul, monovaryOn_iff_smul_rearrangement]

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem ker_toSpanSingleton_isMaximal {m : M} (hm : m ≠ 0) :
    Ideal.IsMaximal (ker (toSpanSingleton R M m))

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Ideal.IsMaximal (ker (toSpanSingleton R M m))

Tactic:
rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]

Result:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsSimpleModule R (R ⧸ ker (toSpanSingleton R M m))

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ IsSimpleModule R (R ⧸ ker (toSpanSingleton R M m))

Tactic:
exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropPrefix?_append_of_beq [BEq α] {l₁ l₂ : List α} (p : List α) (h : l₁ == l₂) :
    dropPrefix? (l₁ ++ p) l₂ = some p

Proof state:
α : Type u_1
inst✝ : BEq α
l₁ l₂ p : List α
h : (l₁ == l₂) = true
⊢ (l₁ ++ p).dropPrefix? l₂ = some p

Tactic:
simp [dropPrefix?_eq_some_iff, h]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem le_sup_inf_aux (a b c : α) : (a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c) :=
  calc
    (a + b + a * b) * (a + c + a * c) =
        a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) +
          (a * b * c + a * a * b * c)

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) =
    a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a * a + b * c + a * (b * c) + (a * b + a * a * b) + (a * c + a * a * c) + (a * b * c + a * a * b * c) =
    a + b * c + a * (b * c)

Tactic:
simp only [mul_self, add_self, add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_push [BEq α] {as : Vector α n} {a : α} {p : α → Bool} :
    (as.push a).all p = (as.all p && p a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
p : α → Bool
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).all p = ({ toArray := as, size_toArray := ⋯ }.all p && p a)

Tactic:
simp [Array.all_push]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
as : Vector α n
a : α
p : α → Bool
⊢ (as.push a).all p = (as.all p && p a)

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
p : α → Bool
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).all p = ({ toArray := as, size_toArray := ⋯ }.all p && p a)
-- Mathlib/Logic/Encodable/Basic.lean
theorem decode₂_encode [Encodable α] (a : α) : decode₂ α (encode a) = some a

Proof state:
α : Type u_1
inst✝ : Encodable α
a : α
⊢ decode₂ α (encode a) = some a

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : Encodable α
a a✝ : α
⊢ a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a

Proof state:
case a
α : Type u_1
inst✝ : Encodable α
a a✝ : α
⊢ a✝ ∈ decode₂ α (encode a) ↔ a✝ ∈ some a

Tactic:
simp [mem_decode₂, eq_comm, decode₂_eq_some]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem mem_offDiag : x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
simp [offDiag, and_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiableAt_prod_module_iff (f : M → F₁ × F₂) :
    MDifferentiableAt I 𝓘(𝕜, F₁ × F₂) f x ↔
      MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x
      ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDifferentiableAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f x ↔
    MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x

Tactic:
exact mdifferentiableAt_prod_iff f

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDifferentiableAt I 𝓘(𝕜, F₁ × F₂) f x ↔
    MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
x : M
f : M → F₁ × F₂
⊢ MDifferentiableAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f x ↔
    MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x
-- Mathlib/RingTheory/Localization/Basic.lean
theorem IsLocalization.map_units_map_submonoid (y : M) : IsUnit (algebraMap R Sₘ y)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
Sₘ : Type u_5
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap R Sₘ) ↑y)

Tactic:
rw [IsScalarTower.algebraMap_apply _ S]

Result:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
Sₘ : Type u_5
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap S Sₘ) ((algebraMap R S) ↑y))

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
Sₘ : Type u_5
inst✝³ : CommRing Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap S Sₘ) ((algebraMap R S) ↑y))

Tactic:
exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
@[simp] lemma map_smul {f : Ω → Ω'} (c : ℝ≥0) (ν : FiniteMeasure Ω) :
    (c • ν).map f = c • (ν.map f)

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
⊢ (c • ν).map f = c • ν.map f

Tactic:
ext s _

Result:
case h
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
s : Set Ω'
a✝ : MeasurableSet s
⊢ ↑((c • ν).map f) s = ↑(c • ν.map f) s

Proof state:
case h
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
s : Set Ω'
a✝ : MeasurableSet s
⊢ ↑((c • ν).map f) s = ↑(c • ν.map f) s

Tactic:
simp [toMeasure_smul]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_zero [IsProbabilityMeasure μ] : mgf X μ 0 = 1

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
⊢ mgf X μ 0 = 1

Tactic:
simp only [mgf_zero', measure_univ, ENNReal.one_toReal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
  match h₁, h₂ with
  | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
    ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩

Proof state:
a b c : Nat
h₁ : a ∣ b
h₂ : b ∣ c
d : Nat
h₃ : b = a * d
e : Nat
h₄ : c = b * e
⊢ c = a * (d * e)

Tactic:
simp[h₃,h₄, Nat.mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_eq_shiftFunctorAdd (i j : A) :
    shiftFunctorAdd' C i j (i+j) rfl = shiftFunctorAdd C i j

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorAdd' C i j (i + j) ⋯ = shiftFunctorAdd C i j

Tactic:
ext1

Result:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorAdd' C i j (i + j) ⋯).hom = (shiftFunctorAdd C i j).hom

Proof state:
case w
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
i j : A
⊢ (shiftFunctorAdd' C i j (i + j) ⋯).hom = (shiftFunctorAdd C i j).hom

Tactic:
apply Category.id_comp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem den_smul_val (f : HomogeneousLocalization 𝒜 x) :
    f.den • f.val = algebraMap _ _ f.num

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num

Tactic:
exact IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ f.den • f.val = (algebraMap A (at x)) f.num

Tactic:
rw [eq_num_div_den, Localization.mk_eq_mk', IsLocalization.smul_mk']

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem abs_det_adjustToOrientation (v : ι → E) :
    |(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
v : ι → E
⊢ |(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|

Tactic:
simp [toBasis_adjustToOrientation]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_mul_X_pow : degree (p * X ^ n) = degree p + n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
⊢ (p * X ^ n).degree = p.degree + ↑n

Tactic:
simp [(monic_X_pow n).degree_mul]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_le_iff_left : a \ b ≤ b ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b ≤ b ↔ a ≤ b

Tactic:
rw [sdiff_le_iff, sup_idem]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem Ioi_eq_finset_subtype : Ioi a = (Ioc (a : ℕ) n).fin n

Proof state:
n : ℕ
a : Fin n
⊢ Ioi a = Finset.fin n (Ioc (↑a) n)

Tactic:
ext

Result:
case h
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ Ioi a ↔ a✝ ∈ Finset.fin n (Ioc (↑a) n)

Proof state:
case h
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ Ioi a ↔ a✝ ∈ Finset.fin n (Ioc (↑a) n)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    Real.tan (∠ p₂ p₃ p₁) = dist 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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.tan (∠ p₂ p₃ p₁) = dist 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
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, tan_angle_add_of_inner_eq_zero h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.length

Proof state:
case cons
α : Type u_1
head✝ : α
l : List α
h : (head✝ :: l).tail ≠ []
⊢ 1 < (head✝ :: l).length

Tactic:
simp only [tail_cons, ne_eq] at h

Result:
case cons
α : Type u_1
head✝ : α
l : List α
h : ¬l = []
⊢ 1 < (head✝ :: l).length

Proof state:
case nil
α : Type u_1
h : [].tail ≠ []
⊢ 1 < [].length

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ 1 < l.length

Tactic:
cases l with
| nil => simp at h
| cons _ l =>
  simp only [tail_cons, ne_eq] at h
  exact Nat.lt_add_of_pos_left (length_pos.mpr h)

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : α
l : List α
h : ¬l = []
⊢ 1 < (head✝ :: l).length

Tactic:
exact Nat.lt_add_of_pos_left (length_pos.mpr h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_flatMap {L : List α} {f : α → List β} :
    (L.flatMap f).getLast? = L.reverse.findSome? fun a => (f a).getLast?

Proof state:
α : Type u_1
β : Type u_2
L : List α
f : α → List β
⊢ (flatMap f L).getLast? = findSome? (fun a => (f a).getLast?) L.reverse

Tactic:
simp only [← head?_reverse, reverse_flatMap]

Result:
α : Type u_1
β : Type u_2
L : List α
f : α → List β
⊢ (flatMap (reverse ∘ f) L.reverse).head? = findSome? (fun a => (f a).reverse.head?) L.reverse

Proof state:
α : Type u_1
β : Type u_2
L : List α
f : α → List β
⊢ (flatMap (reverse ∘ f) L.reverse).head? = findSome? (fun a => (f a).reverse.head?) L.reverse

Tactic:
rw [head?_flatMap]

Result:
α : Type u_1
β : Type u_2
L : List α
f : α → List β
⊢ findSome? (fun a => ((reverse ∘ f) a).head?) L.reverse = findSome? (fun a => (f a).reverse.head?) L.reverse

Proof state:
α : Type u_1
β : Type u_2
L : List α
f : α → List β
⊢ findSome? (fun a => ((reverse ∘ f) a).head?) L.reverse = findSome? (fun a => (f a).reverse.head?) L.reverse

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_right_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle x (r • x) = 0

Proof state:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle x (r • x) = 0

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle x (r • x) = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
⊢ o.oangle x (r • x) = 0

Tactic:
rcases hr.lt_or_eq with (h | h)

Result:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle x (r • x) = 0

case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle x (r • x) = 0
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem generator_map_dvd_of_mem {N : Submodule R M} (ϕ : M →ₗ[R] R) [(N.map ϕ).IsPrincipal] {x : M}
    (hx : x ∈ N) : generator (N.map ϕ) ∣ ϕ x

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (map ϕ N) ∣ ϕ x

Tactic:
rw [← mem_iff_generator_dvd, Submodule.mem_map]

Result:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y ∈ N, ϕ y = ϕ x

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y ∈ N, ϕ y = ϕ x

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equiv_some_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1] :=
  equiv_of_X_eq_of_Y_eq hPz one_ne_zero
    (by linear_combination (norm := (matrix_simp; ring1)) -P x * div_self (pow_ne_zero 2 hPz))
    (by linear_combination (norm := (matrix_simp; ring1)) -P y * div_self (pow_ne_zero 3 hPz))

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 3 + -P y * 1 -
      (![P x / P z ^ 2, P y / P z ^ 3, 1] y * P z ^ 3 + -P y * (P z ^ 3 / P z ^ 3)) =
    0

Tactic:
matrix_simp

Result:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 ^ 3 + -P y * 1 - (P y / P z ^ 3 * P z ^ 3 + -P y * (P z ^ 3 / P z ^ 3)) = 0

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 ^ 3 + -P y * 1 - (P y / P z ^ 3 * P z ^ 3 + -P y * (P z ^ 3 / P z ^ 3)) = 0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 2 = ![P x / P z ^ 2, P y / P z ^ 3, 1] x * P z ^ 2

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P x * div_self (pow_ne_zero 2 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 2 + -P x * 1 -
      (![P x / P z ^ 2, P y / P z ^ 3, 1] x * P z ^ 2 + -P x * (P z ^ 2 / P z ^ 2)) =
    0

Tactic:
matrix_simp

Result:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 ^ 2 + -P x * 1 - (P x / P z ^ 2 * P z ^ 2 + -P x * (P z ^ 2 / P z ^ 2)) = 0

Proof state:
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * ![P x / P z ^ 2, P y / P z ^ 3, 1] z ^ 3 = ![P x / P z ^ 2, P y / P z ^ 3, 1] y * P z ^ 3

Tactic:
linear_combination (norm := (matrix_simp; ring1)) -P y * div_self (pow_ne_zero 3 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 ^ 2 + -P x * 1 - (P x / P z ^ 2 * P z ^ 2 + -P x * (P z ^ 2 / P z ^ 2)) = 0

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
lemma not_eq_iff : ∀ {a b : Bool}, !a = b ↔ a ≠ b

Proof state:
⊢ ∀ {a b : Bool}, (!decide (a = b)) = true ↔ a ≠ b

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
lemma part_eq_of_mem (ht : t ∈ P.parts) (hat : a ∈ t) : P.part a = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
a : α
ht : t ∈ P.parts
hat : a ∈ t
⊢ P.part a = t

Tactic:
apply P.eq_of_mem_parts (P.part_mem _) ht (P.mem_part _) hat <;> exact mem_of_subset (P.le ht) hat

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem smul_nonneg {f : ι → Ω → F} {c : ℝ} (hc : 0 ≤ c) (hf : Supermartingale f ℱ μ) :
    Supermartingale (c • f) ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
⊢ Supermartingale (c • f) ℱ μ

Tactic:
refine ⟨hf.1.smul c, fun i j hij => ?_, fun i => (hf.2.2 i).smul c⟩

Result:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j|↑ℱ i] ≤ᶠ[ae μ] (c • f) i

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j|↑ℱ i] ≤ᶠ[ae μ] (c • f) i

Tactic:
filter_upwards [condExp_smul c (f j) (ℱ i), hf.2.1 i j hij] with ω hω hle

Result:
case h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
ω : Ω
hω : (μ[c • f j|↑ℱ i]) ω = (c • μ[f j|↑ℱ i]) ω
hle : (μ[f j|↑ℱ i]) ω ≤ f i ω
⊢ (μ[(c • f) j|↑ℱ i]) ω ≤ (c • f) i ω

Proof state:
case h
Ω : Type u_1
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝³ : NormedLatticeAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : OrderedSMul ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
ω : Ω
hω : (μ[c • f j|↑ℱ i]) ω = (c • μ[f j|↑ℱ i]) ω
hle : (μ[f j|↑ℱ i]) ω ≤ f i ω
⊢ (μ[(c • f) j|↑ℱ i]) ω ≤ (c • f) i ω

Tactic:
simpa only [hω, Pi.smul_apply] using smul_le_smul_of_nonneg_left hle hc

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem isConnected_setOf_sameRay_and_ne_zero {x : E} (hx : x ≠ 0) :
    IsConnected { y | SameRay ℝ x y ∧ y ≠ 0 }

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | SameRay ℝ x y ∧ y ≠ 0}

Tactic:
simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected {y | ∃ r, 0 < r ∧ r • x = y}

Tactic:
exact isConnected_Ioi.image _ (continuous_id.smul continuous_const).continuousOn

Result:
no goals