harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (a ᵥ* γ)`. -/
lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ : SL(2, ℤ)) :
    v ᵥ* γ ∈ gammaSet N (a ᵥ* γ)

Proof state:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Tactic:
have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v

Result:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    (Int.castRingHom (ZMod N)) ((v ᵥ* ↑γ) i) =
      (⇑(Int.castRingHom (ZMod N)) ∘ v ᵥ* (↑γ).map ⇑(Int.castRingHom (ZMod N))) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Proof state:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Tactic:
simp_rw [Function.comp_def, this, hv.1]

Result:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i
⊢ (fun x => (a ᵥ* (↑γ).map fun x => ↑x) x) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Proof state:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
⊢ v ᵥ* ↑γ ∈ gammaSet N (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

Tactic:
refine ⟨?_, hv.2.vecMulSL γ⟩

Result:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Proof state:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i
⊢ (fun x => (a ᵥ* (↑γ).map fun x => ↑x) x) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Tactic:
simp

Result:
no goals

Proof state:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    (Int.castRingHom (ZMod N)) ((v ᵥ* ↑γ) i) =
      (⇑(Int.castRingHom (ZMod N)) ∘ v ᵥ* (↑γ).map ⇑(Int.castRingHom (ZMod N))) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Tactic:
simp only [eq_intCast, Int.coe_castRingHom] at this

Result:
N : ℕ
a : Fin 2 → ZMod N
v : Fin 2 → ℤ
hv : v ∈ gammaSet N a
γ : SL(2, ℤ)
this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
-- Mathlib/Data/List/Cycle.lean
theorem nontrivial_reverse_iff {s : Cycle α} : s.reverse.Nontrivial ↔ s.Nontrivial

Proof state:
α : Type u_1
s : Cycle α
⊢ s.reverse.Nontrivial ↔ s.Nontrivial

Tactic:
simp [Nontrivial]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inl_mul_inr [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
    (a : A) : ((inl r : Unitization R A) * a) = ↑(r • a) :=
  ext (mul_zero r) <|
    show r • a + (0 : R) • (0 : A) + 0 * a = r • a by
      rw [smul_zero, add_zero, zero_mul, add_zero]

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ r • a + 0 • 0 + 0 * a = r • a

Tactic:
rw [smul_zero, add_zero, zero_mul, add_zero]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Coherence.lean
lemma insert_id_rhs {C : Type*} [Category C] {X Y : C} (f g : X ⟶ Y) (w : f = g ≫ 𝟙 _) :
    f = g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive] lemma eq_inv_smul_iff : a = g⁻¹ • b ↔ g • a = b :=
  ⟨fun h ↦ by rw [h, smul_inv_smul], fun h ↦ by rw [← h, inv_smul_smul]⟩

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • b

Tactic:
rw [← h, inv_smul_smul]

Result:
no goals

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • a = b

Tactic:
rw [h, smul_inv_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    get? (insertMany m l) k = get? m k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ get? (insertMany m l) k = get? m k

Tactic:
simp_to_raw using Raw₀.Const.get?_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_lt_ofReal_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :
    ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Proof state:
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccOrder.lean
lemma Iic.succ_eq_of_not_isMax
    [SuccOrder J] {j : J} {i : Set.Iic j} (hi : ¬ IsMax i) :
    Order.succ i = ⟨Order.succ i.1, by
      rw [← coe_succ_of_not_isMax hi]
      apply Subtype.coe_prop⟩

Proof state:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = ↑⟨Order.succ ↑i, ⋯⟩

Tactic:
simp only [coe_succ_of_not_isMax hi]

Result:
no goals

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) ∈ Iic j

Tactic:
apply Subtype.coe_prop

Result:
no goals

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ i = ⟨Order.succ ↑i, ⋯⟩

Tactic:
ext

Result:
case a
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = ↑⟨Order.succ ↑i, ⋯⟩

Proof state:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j

Tactic:
rw [← coe_succ_of_not_isMax hi]

Result:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) ∈ Iic j
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_X_pow_char_pow_sub_C (q : ℕ) [ExpChar F q] (n : ℕ) (y : F) :
    (X ^ q ^ n - C y).natSepDegree = 1

Proof state:
F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ (X ^ q ^ n - C y).natSepDegree = 1

Tactic:
rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
/-- The group of group homomorphims from a finite cyclic group `G` of order `n` into the
group of units of a ring `M` with all roots of unity is isomorphic to `G` -/
lemma IsCyclic.monoidHom_equiv_self (G M : Type*) [CommGroup G] [Finite G]
    [IsCyclic G] [CommMonoid M] [HasEnoughRootsOfUnity M (Nat.card G)] :
    Nonempty ((G →* Mˣ) ≃* G)

Proof state:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
have hord := HasEnoughRootsOfUnity.natCard_rootsOfUnity M (Nat.card G)

Result:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩

Result:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Proof state:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
e : (G →* Mˣ) ≃* ↥(rootsOfUnity (Nat.card G) Mˣ) := ⋯.some
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
exact ⟨e.trans (rootsOfUnityUnitsMulEquiv M (Nat.card G)) |>.trans (mulEquivOfCyclicCardEq hord)⟩

Result:
no goals

Proof state:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
let e := (IsCyclic.monoidHom_mulEquiv_rootsOfUnity G Mˣ).some

Result:
G : Type u_1
M : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : Finite G
inst✝² : IsCyclic G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Nat.card G)
this : NeZero (Nat.card G)
hord : Nat.card ↥(rootsOfUnity (Nat.card G) M) = Nat.card G
e : (G →* Mˣ) ≃* ↥(rootsOfUnity (Nat.card G) Mˣ) := ⋯.some
⊢ Nonempty ((G →* Mˣ) ≃* G)
-- Mathlib/Data/Finset/Prod.lean
theorem offDiag_singleton : ({a} : Finset α).offDiag = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.offDiag = ∅

Tactic:
simp [← Finset.card_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem set_getElem_succ_eraseIdx_succ
    {l : Vector α n} {i : Nat} (h : i + 1 < n) :
    (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i + 1 < n
⊢ (l.eraseIdx (i + 1) h).set i l[i + 1] ⋯ = l.eraseIdx i ⋯

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
l : Array α
h : i + 1 < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx (i + 1) h).set i { toArray := l, size_toArray := ⋯ }[i + 1] ⋯ =
    { toArray := l, size_toArray := ⋯ }.eraseIdx i ⋯

Proof state:
case mk
α : Type u_1
i : Nat
l : Array α
h : i + 1 < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx (i + 1) h).set i { toArray := l, size_toArray := ⋯ }[i + 1] ⋯ =
    { toArray := l, size_toArray := ⋯ }.eraseIdx i ⋯

Tactic:
simp [List.set_getElem_succ_eraseIdx_succ, *]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem disjoint_frontier_iff_isOpen : Disjoint (frontier s) s ↔ IsOpen s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ Disjoint (frontier s) s ↔ IsOpen s

Tactic:
rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
  frontier_compl, subset_compl_iff_disjoint_right]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_eq_compl_sInter_compl (S : Set (Set α)) : ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Proof state:
α : Type u_1
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋃₀ S), compl_sUnion]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_pred_of_le (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0)
    (hi := Fin.ne_of_gt <| Fin.lt_of_lt_of_le (Fin.pos_iff_ne_zero.2 hp) h) :
  (pred p hp).predAbove i = pred i hi

Proof state:
n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
hi : optParam (i ≠ 0) ⋯
⊢ (p.pred hp).predAbove i = i.pred hi

Tactic:
rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_of_infinite' (α β : Type u) [Nonempty α] [Zero β] [Infinite β] :
    #(α →₀ β) = max #α #β

Proof state:
α β : Type u
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = #α ⊔ #β

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mod_right (x z : Nat) : (x + z) % z = x % z

Proof state:
x z : Nat
⊢ (x + z) % z = x % z

Tactic:
rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/Hom.lean
theorem ext_of_ring {f g : R →ₐc[R] A} (h : f 1 = g 1) : f = g :=
  coe_linearMap_injective (by ext; assumption)

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ ((fun x => ↑x) f) 1 = ((fun x => ↑x) g) 1

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ (fun x => ↑x) f = (fun x => ↑x) g

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : CoalgebraStruct R A
f g : R →ₐc[R] A
h : f 1 = g 1
⊢ ((fun x => ↑x) f) 1 = ((fun x => ↑x) g) 1
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_eq_center' : inversion c R x = c ↔ x = c ∨ R = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
by_cases hR : R = 0 <;> simp [inversion_eq_center, hR]

Result:
no goals
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem map_nhds_eq : map φ.leftFun (𝓝 φ.pt) = 𝓝 (φ.leftFun φ.pt) :=
  show map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1 by
    rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : CompleteSpace E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : CompleteSpace F
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
φ : ImplicitFunctionData 𝕜 E F G
⊢ map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1

Tactic:
rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
@[reassoc]
lemma p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi (Karoubi C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f

Tactic:
simpa only [hom_ext_iff, comp_f] using p_comm f

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
@[simp]
lemma volume_ball_fin_three (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ) :
    volume (ball x r) = .ofReal r ^ 3 * .ofReal (π * 4 / 3)

Proof state:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ Module.finrank ℝ (EuclideanSpace ℝ (Fin 3)) = 2 * 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
x : EuclideanSpace ℝ (Fin 3)
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (π * 4 / 3)

Tactic:
norm_num [InnerProductSpace.volume_ball_of_dim_odd (k := 1) (by simp) x]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem le_sum_schlomilch (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (hu : Monotone u) (n : ℕ) :
    (∑ k ∈ range (u n), f k) ≤
      ∑ k ∈ range (u 0), f k + ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ range (u n), f k ≤ ∑ k ∈ range (u 0), f k + ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)

Tactic:
convert add_le_add_left (le_sum_schlomilch' hf h_pos hu n) (∑ k ∈ range (u 0), f k)

Result:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ range (u n), f k = ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k

Proof state:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
⊢ ∑ k ∈ range (u n), f k = ∑ k ∈ range (u 0), f k + ∑ k ∈ Ico (u 0) (u n), f k

Tactic:
rw [← sum_range_add_sum_Ico _ (hu n.zero_le)]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem addOrderOf_div_of_gcd_eq_one {m n : ℕ} (hn : 0 < n) (h : m.gcd n = 1) :
    addOrderOf (↑(↑m / ↑n * p) : AddCircle p) = n

Proof state:
case h.e'_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = m.gcd n * addOrderOf ↑(↑m / ↑n * p)

Tactic:
rw [h, one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
convert gcd_mul_addOrderOf_div_eq p m hn

Result:
case h.e'_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : m.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = m.gcd n * addOrderOf ↑(↑m / ↑n * p)
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem range_pullback_to_base_of_left :
    Set.range (pullback.fst f g ≫ f).base =
      Set.range f.base ∩ Set.range g.base

Proof state:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.fst f g ≫ f).base) =
    Set.range ⇑(ConcreteCategory.hom f.base) ∩ Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rw [pullback.condition, Scheme.comp_base, TopCat.coe_comp, Set.range_comp,
  range_pullback_snd_of_left, Opens.carrier_eq_coe, Opens.map_obj, Opens.coe_mk,
  Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIdIso_hom_fst :
    (pullbackDiagonalMapIdIso f g i).hom ≫ pullback.fst _ _ =
      pullback.snd _ _ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      fst f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem nonempty_iff_ne_bot (Q : AffineSubspace k P) : (Q : Set P).Nonempty ↔ Q ≠ ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ (↑Q).Nonempty ↔ Q ≠ ⊥

Tactic:
rw [nonempty_iff_ne_empty]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥

Tactic:
exact not_congr Q.coe_eq_bot_iff

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_iff_pointwise_add_subset :
    StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hA : StarConvex 𝕜 u s
v : E
hv : v ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => a • x) u) ((fun x => b • x) v) ∈ s

Tactic:
exact hA hv ha hb hab

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s

Tactic:
rintro hA a b ha hb hab w ⟨au, ⟨u, rfl : u = x, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hA : StarConvex 𝕜 u s
v : E
hv : v ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => a • x) u) ((fun x => b • x) v) ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s

Tactic:
refine
  ⟨?_, fun h y hy a b ha hb hab =>
    h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ StarConvex 𝕜 x s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s