harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/CoprodI.lean
theorem rcons_eq_smul {i} (p : Pair M i) :
    rcons p = of p.head • p.tail

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
⊢ rcons p = of p.head • p.tail

Tactic:
simp [of_smul_def]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_of_oangle_sign_eq_neg_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = -1) : p₁ ≠ p₂ :=
  left_ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

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₃).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) :=
  fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddCommMonoid α
inst✝² : Neg β
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_zero : blockDiagonal (0 : o → Matrix m n α) = 0

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal 0 i✝ j✝ = 0 i✝ j✝

Tactic:
simp [blockDiagonal_apply]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
⊢ blockDiagonal 0 = 0

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal 0 i✝ j✝ = 0 i✝ j✝
-- Mathlib/Data/Nat/Factorial/BigOperators.lean
theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i ∈ range k, (n - i)
  | 0 => rfl
  | k + 1 => by rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]

Proof state:
n k : ℕ
⊢ n.descFactorial (k + 1) = ∏ i ∈ range (k + 1), (n - i)

Tactic:
rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp] lemma algebraMap_coxeterWeightIn (S : Type*) [CommRing S] [Algebra S R] [P.IsValuedIn S]
    (i j : ι) :
    algebraMap S R (P.coxeterWeightIn S i j) = P.coxeterWeight i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra S R
inst✝ : P.IsValuedIn S
i j : ι
⊢ (algebraMap S R) (P.coxeterWeightIn S i j) = P.coxeterWeight i j

Tactic:
simp [coxeterWeightIn, coxeterWeight]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem fin_curry {n} {f : α → Fin n → σ} : Primrec f ↔ Primrec₂ f :=
  ⟨fun h => fin_app.comp (h.comp fst) snd, fun h =>
    (vector_get'.comp
          (vector_ofFn fun i => show Primrec fun a => f a i from h.comp .id (const i))).of_eq
      fun a => by funext i; simp⟩

Proof state:
case h
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ (List.Vector.ofFn fun i => f a i).get i = f a i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ (List.Vector.ofFn fun i => f a i).get = f a

Tactic:
funext i

Result:
case h
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ (List.Vector.ofFn fun i => f a i).get i = f a i
-- Mathlib/Order/Category/FinBddDistLat.lean
lemma hom_inv_apply {X Y : FinBddDistLat} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : FinBddDistLat
e : X ≅ Y
s : ↑Y.toDistLat
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem emultiplicity_pow_sub_pow_of_prime {p : R} (hp : Prime p) {x y : R}
    (hxy : p ∣ x - y) (hx : ¬p ∣ x) {n : ℕ} (hn : ¬p ∣ n) :
    emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y)

Tactic:
rw [← geom_sum₂_mul, emultiplicity_mul hp,
  emultiplicity_eq_zero.2 (not_dvd_geom_sum₂ hp hxy hx hn), zero_add]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natMod_lt {n : ℕ} (hn : n ≠ 0) : m.natMod n < n :=
  (toNat_lt' hn).2 <| emod_lt_of_pos _ <| by omega

Proof state:
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_intCast (a : Aˣ) (n : ℤ) (ha : (0 : A) ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
n : ℤ
ha : autoParam (0 ≤ ↑a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 ↑a
⊢ x✝¹ ^ ↑n = x✝¹ ^ n

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
n : ℤ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ cfc (fun x => x ^ ↑n) ↑a = cfc (fun x => x ^ n) ↑a

Tactic:
refine cfc_congr fun _ _ => ?_

Result:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
n : ℤ
ha : autoParam (0 ≤ ↑a) _auto✝
x✝¹ : ℝ≥0
x✝ : x✝¹ ∈ spectrum ℝ≥0 ↑a
⊢ x✝¹ ^ ↑n = x✝¹ ^ n

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
n : ℤ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ ↑a ^ ↑n = ↑(a ^ n)

Tactic:
rw [← cfc_zpow (R := ℝ≥0) a n, rpow_def]

Result:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : Aˣ
n : ℤ
ha : autoParam (0 ≤ ↑a) _auto✝
⊢ cfc (fun x => x ^ ↑n) ↑a = cfc (fun x => x ^ n) ↑a
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Injective cycleFactorsFinset

Tactic:
intro f g h

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f = g

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f.cycleFactorsFinset.noncommProd id ⋯ = g

Tactic:
simpa [h] using cycleFactorsFinset_noncommProd g

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f = g

Tactic:
rw [← cycleFactorsFinset_noncommProd f]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f.cycleFactorsFinset.noncommProd id ⋯ = g
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
lemma injective_add_right_of_ne_top (b : α) (h : b ≠ ⊤) : Function.Injective (fun x ↦ b + x)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x => b + x

Tactic:
simpa [add_comm] using injective_add_left_of_ne_top b h

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem half_le_symm_iff (t : I) : 1 / 2 ≤ (σ t : ℝ) ↔ (t : ℝ) ≤ 1 / 2

Proof state:
t : ↑I
⊢ 1 / 2 ≤ ↑(σ t) ↔ ↑t ≤ 1 / 2

Tactic:
rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_toAssocList (l : AssocList α β) : l.toList.toAssocList = l

Proof state:
α : Type u_1
β : Type u_2
l : AssocList α β
⊢ l.toList.toAssocList = l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Iio : (fun x => x - a) '' Iio b = Iio (b - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) '' Iio b = Iio (b - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
/-- See `List.length_flatMap` for the corresponding statement using `List.sum`. -/
@[deprecated "Use `List.length_flatMap`." (since := "2024-10-17")]
lemma length_flatMap' (l : List α) (f : α → List β) :
    length (l.flatMap f) = Nat.sum (map (length ∘ f) l)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (flatMap f l).length = Nat.sum (map (length ∘ f) l)

Tactic:
rw [List.flatMap, length_flatten', map_map]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_union' (s t : Set α) (ht : MeasurableSet t) (hs_finite : μ s ≠ ∞)
    (ht_finite : μ t ≠ ∞) (hdisj : Disjoint s t) :
    (weightedSMul μ (s ∪ t) : F →L[ℝ] F) = weightedSMul μ s + weightedSMul μ t

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ⊤
ht_finite : μ t ≠ ⊤
hdisj : Disjoint s t
x : F
⊢ (weightedSMul μ (s ∪ t)) x = (weightedSMul μ s + weightedSMul μ t) x

Tactic:
simp_rw [add_apply, weightedSMul_apply, measure_union hdisj ht,
  ENNReal.toReal_add hs_finite ht_finite, add_smul]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ⊤
ht_finite : μ t ≠ ⊤
hdisj : Disjoint s t
⊢ weightedSMul μ (s ∪ t) = weightedSMul μ s + weightedSMul μ t

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ⊤
ht_finite : μ t ≠ ⊤
hdisj : Disjoint s t
x : F
⊢ (weightedSMul μ (s ∪ t)) x = (weightedSMul μ s + weightedSMul μ t) x
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_neg (p : R[X]) : natTrailingDegree (-p) = natTrailingDegree p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).natTrailingDegree = p.natTrailingDegree

Tactic:
simp [natTrailingDegree]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem tail_zipWithAll {f : Option α → Option β → γ} :
    (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
⊢ (zipWithAll f as bs).tail = zipWithAll f as.tail bs.tail

Tactic:
cases as <;> cases bs <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
theorem toSphere_apply_univ : μ.toSphere univ = dim E * μ (ball 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1)

Tactic:
rw [toSphere_apply_univ', measure_diff_null (measure_singleton _)]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1)

Tactic:
nontriviality E

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1)
-- Mathlib/Data/Set/Card.lean
theorem encard_union_add_encard_inter (s t : Set α) :
    (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard

Proof state:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard

Tactic:
rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm,
  encard_diff_add_encard_inter]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_norm_col (v : n → α) : ‖col ι v‖ = ‖(WithLp.equiv 2 _).symm v‖

Proof state:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ (∑ x : n, ‖col ι v x default‖ ^ 2) ^ (1 / 2) = (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖ ^ 2) ^ (1 / 2)

Tactic:
simp only [col_apply, Real.rpow_two, WithLp.equiv_symm_pi_apply]

Result:
no goals

Proof state:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖col ι v‖ = ‖(WithLp.equiv 2 (n → α)).symm v‖

Tactic:
simp_rw [frobenius_norm_def, Fintype.sum_unique, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

Result:
n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ (∑ x : n, ‖col ι v x default‖ ^ 2) ^ (1 / 2) = (∑ i : n, ‖(WithLp.equiv 2 (n → α)).symm v i‖ ^ 2) ^ (1 / 2)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem induction_on {β : LocalizedModule S M → Prop} (h : ∀ (m : M) (s : S), β (mk m s)) :
    ∀ x : LocalizedModule S M, β x

Proof state:
case mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
x✝ : LocalizedModule S M
m : M
s : ↥S
⊢ β (Quot.mk ⇑(r.setoid S M) (m, s))

Tactic:
exact h m s

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
⊢ ∀ (x : LocalizedModule S M), β x

Tactic:
rintro ⟨⟨m, s⟩⟩

Result:
case mk.mk
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
β : LocalizedModule S M → Prop
h : ∀ (m : M) (s : ↥S), β (mk m s)
x✝ : LocalizedModule S M
m : M
s : ↥S
⊢ β (Quot.mk ⇑(r.setoid S M) (m, s))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i

Proof state:
xs ys : IntList
i : Nat
⊢ (match xs[i]?, ys[i]? with
        | none, none => none
        | a?, b? => some (a?.getD 0 + b?.getD 0)).getD
      0 =
    xs[i]?.getD 0 + ys[i]?.getD 0

Tactic:
cases xs[i]? <;> cases ys[i]? <;> simp

Result:
no goals

Proof state:
xs ys : IntList
i : Nat
⊢ (xs + ys).get i = xs.get i + ys.get i

Tactic:
simp only [get, add_def, List.get?_eq_getElem?, List.getElem?_zipWithAll]

Result:
xs ys : IntList
i : Nat
⊢ (match xs[i]?, ys[i]? with
        | none, none => none
        | a?, b? => some (a?.getD 0 + b?.getD 0)).getD
      0 =
    xs[i]?.getD 0 + ys[i]?.getD 0
-- Mathlib/NumberTheory/Ostrowski.lean
private lemma list_mul_sum {R : Type*} [CommSemiring R] {T : Type*} (l : List T) (y : R) (x : R) :
    (l.mapIdx fun i _ => x * y ^ i).sum = x * (l.mapIdx fun i _ => y ^ i).sum

Proof state:
case e_a
R : Type u_1
inst✝ : CommSemiring R
T : Type u_2
l : List T
y x : R
⊢ List.map (fun x_1 => x • y ^ x_1.2) l.zipIdx = List.map (fun x_1 => x • x_1) (List.map (fun x => y ^ x.2) l.zipIdx)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
T : Type u_2
l : List T
y x : R
⊢ (List.mapIdx (fun i x_1 => x * y ^ i) l).sum = x * (List.mapIdx (fun i x => y ^ i) l).sum

Tactic:
simp_rw [← smul_eq_mul, List.smul_sum, List.mapIdx_eq_zipIdx_map]

Result:
R : Type u_1
inst✝ : CommSemiring R
T : Type u_2
l : List T
y x : R
⊢ (List.map (fun x_1 => x • y ^ x_1.2) l.zipIdx).sum =
    (List.map (fun x_1 => x • x_1) (List.map (fun x => y ^ x.2) l.zipIdx)).sum

Proof state:
R : Type u_1
inst✝ : CommSemiring R
T : Type u_2
l : List T
y x : R
⊢ (List.map (fun x_1 => x • y ^ x_1.2) l.zipIdx).sum =
    (List.map (fun x_1 => x • x_1) (List.map (fun x => y ^ x.2) l.zipIdx)).sum

Tactic:
congr 1

Result:
case e_a
R : Type u_1
inst✝ : CommSemiring R
T : Type u_2
l : List T
y x : R
⊢ List.map (fun x_1 => x • y ^ x_1.2) l.zipIdx = List.map (fun x_1 => x • x_1) (List.map (fun x => y ^ x.2) l.zipIdx)
-- Mathlib/Combinatorics/Digraph/Orientation.lean
@[simp]
lemma toSimpleGraphStrict_bot : (⊥ : Digraph V).toSimpleGraphStrict = ⊥

Proof state:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

Result:
no goals

Proof state:
V : Type u_1
⊢ ⊥.toSimpleGraphStrict = ⊥

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphStrict.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Proof state:
V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphStrict.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∧ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
tauto

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem appIso_inv_app (U) :
    (f.appIso U).inv ≫ f.app (f ''ᵁ U) = X.presheaf.map (eqToHom (preimage_image_eq f U)).op :=
  (PresheafedSpace.IsOpenImmersion.invApp_app _ _).trans (by rw [eqToHom_op])

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯).op

Tactic:
rw [eqToHom_op]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isGLB_empty_iff : IsGLB ∅ a ↔ IsTop a

Proof state:
α : Type u
inst✝ : Preorder α
a : α
⊢ IsGLB ∅ a ↔ IsTop a

Tactic:
simp [IsGLB]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem exists_maximal_algebraicIndependent (s t : Set A) (hst : s ⊆ t)
    (hs : AlgebraicIndependent R ((↑) : s → A)) : ∃ u, s ⊆ u ∧
      Maximal (fun (x : Set A) ↦ AlgebraicIndependent R ((↑) : x → A) ∧ x ⊆ t) u

Proof state:
case refine_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

Result:
no goals

Proof state:
case refine_1
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent R Subtype.val

Tactic:
exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)

Result:
no goals

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
⊢ ∃ u, s ⊆ u ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ t) u

Tactic:
refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
  (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩

Result:
case refine_1
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent R Subtype.val

case refine_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndependent R Subtype.val
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_reverse {u v : V} (p : G.Walk u v) : p.reverse.reverse = p

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.reverse = p

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => simp [ih]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.reverse.reverse = p✝
⊢ (cons h✝ p✝).reverse.reverse = cons h✝ p✝

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.reverse = nil

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w ^^^ x).getLsbD i = (~~~x).getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ allOnes w ^^^ x = ~~~x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w ^^^ x).getLsbD i = (~~~x).getLsbD i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.gt_ult (x y : BitVec w) : x > y ↔ (y.ult x = true)

Proof state:
w : Nat
x y : BitVec w
⊢ x > y ↔ y.ult x = true

Tactic:
simp [BitVec.lt_ult]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem hom_ext [Ring R] {d : ℤ} (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) : f = g

Proof state:
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
⊢ f = g

Tactic:
ext ⟨x_re, x_im⟩

Result:
case a.mk
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
x_re x_im : ℤ
⊢ f { re := x_re, im := x_im } = g { re := x_re, im := x_im }

Proof state:
case a.mk
R : Type
inst✝ : Ring R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
x_re x_im : ℤ
⊢ f { re := x_re, im := x_im } = g { re := x_re, im := x_im }

Tactic:
simp [decompose, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_add_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P)
    (hQ : W.Nonsingular Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)) : toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] = toAffine W P + toAffine W Q

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = (Projective.toAffine W).negY (Q x / Q z) (Q y / Q z))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ toAffine W
      ![(Projective.toAffine W).addX (P x / P z) (Q x / Q z)
          ((Projective.toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (Projective.toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((Projective.toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    toAffine W P + toAffine W Q

Tactic:
rw [toAffine_some <| nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy, toAffine_of_Z_ne_zero hP hPz,
  toAffine_of_Z_ne_zero hQ hQz,
  Affine.Point.add_some <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]]

Result:
no goals