harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp]
lemma absorbs_neg_neg {s t : Set E} : Absorbs M (-s) (-t) ↔ Absorbs M s t

Proof state:
M : Type u_1
E : Type u_2
inst✝³ : Monoid M
inst✝² : AddGroup E
inst✝¹ : DistribMulAction M E
inst✝ : Bornology M
s t : Set E
⊢ Absorbs M (-s) (-t) ↔ Absorbs M s t

Tactic:
simp [Absorbs]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The two-variable Jacobi theta function is even in `z`. -/
@[simp]
lemma jacobiTheta₂_neg_left (z τ : ℂ) : jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ (-z) τ = jacobiTheta₂ z τ

Tactic:
conv_lhs => rw [jacobiTheta₂, ← Equiv.tsum_eq (Equiv.neg ℤ)]

Result:
z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ) c) (-z) τ = jacobiTheta₂ z τ

Proof state:
z τ : ℂ
⊢ ∑' (c : ℤ), jacobiTheta₂_term ((Equiv.neg ℤ) c) (-z) τ = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Result:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term ((Equiv.neg ℤ) n) (-z) τ = jacobiTheta₂_term n z τ

Proof state:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term ((Equiv.neg ℤ) n) (-z) τ = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, Equiv.neg_apply, Int.cast_neg, neg_sq, mul_assoc, neg_mul_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
    as.contains a = true → a ∈ as

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true → a ∈ { toArray := as, size_toArray := ⋯ }

Tactic:
simp [Array.mem_of_contains_eq_true]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Vector α n
⊢ as.contains a = true → a ∈ as

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.contains a = true → a ∈ { toArray := as, size_toArray := ⋯ }
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_const_const_iff {c : E''} {c' : F''} (l : Filter α) [l.NeBot] :
    ((fun _x : α => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0

Proof state:
case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
hc' : c' ≠ 0
⊢ ((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0

Tactic:
simp [hc', isBigO_const_const _ hc']

Result:
no goals

Proof state:
case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x => c) =O[l] fun _x => 0) ↔ 0 = 0 → c = 0

Tactic:
simp [EventuallyEq]

Result:
no goals

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0

Tactic:
rcases eq_or_ne c' 0 with (rfl | hc')

Result:
case inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
l : Filter α
inst✝ : l.NeBot
⊢ ((fun _x => c) =O[l] fun _x => 0) ↔ 0 = 0 → c = 0

case inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
c : E''
c' : F''
l : Filter α
inst✝ : l.NeBot
hc' : c' ≠ 0
⊢ ((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_eq_iff (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Proof state:
d₁ d₂ : Nat
n₁ n₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

Tactic:
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_eq_iff]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_inv_natural_whiskerRight (f : A ⟶ A') [IsIso (prodComparison F A' B)] :
    inv (prodComparison F A B) ≫ F.map (f ▷ B) =
      (F.map f ▷ F.obj B) ≫ inv (prodComparison F A' B)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ inv (prodComparison F A B) ≫ F.map (f ▷ B) = F.map f ▷ F.obj B ≫ inv (prodComparison F A' B)

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_inv : (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
@[simp]
lemma findAtom_bot : findAtom (⊥ : α) = ⊥

Proof state:
case h
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ Order.pred ⊥ = ⊥

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ findAtom ⊥ = ⊥

Tactic:
apply Function.iterate_fixed

Result:
case h
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
⊢ Order.pred ⊥ = ⊥
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_le_card_of_rightTotal_unique (h₁ : RightTotal r) (h₂ : RightUnique r) :
    Fintype.card β ≤ Fintype.card α :=
  card_le_card_of_forall_subsingleton' r (by simpa using h₁) fun _ _ _ ha₁ _ ha₂ ↦ h₂ ha₁.2 ha₂.2

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
r : α → β → Prop
h₁ : RightTotal r
h₂ : RightUnique r
⊢ ∀ b ∈ univ, ∃ a ∈ univ, r a b

Tactic:
simpa using h₁

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_eq_of_ne {x y : ∀ n, E n} (h : x ≠ y) : dist x y = (1 / 2 : ℝ) ^ firstDiff x y

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ dist x y = (1 / 2) ^ firstDiff x y

Tactic:
simp [dist, h]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem liftHom_eq_algHom (f : R[X]) (ϕ : AdjoinRoot f →ₐ[R] S) :
    liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ) = ϕ

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯) = ⊤

Tactic:
rw [eq_top_iff, ← adjoinRoot_eq_top, Algebra.adjoin_le_iff, Set.singleton_subset_iff]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
this : AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯) = ⊤
⊢ liftHom f (ϕ (root f)) ⋯ = ϕ

Tactic:
exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ liftHom f (ϕ (root f)) ⋯ = ϕ

Tactic:
suffices AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ)) = ⊤ by
  exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯) = ⊤

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯))

Tactic:
exact (@lift_root _ _ _ _ _ _ _ (aeval_algHom_eq_zero f ϕ)).symm

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem blsub_eq_blsub {ι : Type u} (r r' : ι → ι → Prop) [IsWellOrder ι r] [IsWellOrder ι r']
    (f : ι → Ordinal.{max u v}) :
    blsub.{_, v} _ (bfamilyOfFamily' r f) = blsub.{_, v} _ (bfamilyOfFamily' r' f)

Proof state:
ι : Type u
r r' : ι → ι → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι r'
f : ι → Ordinal.{max u v}
⊢ (type r).blsub (bfamilyOfFamily' r f) = (type r').blsub (bfamilyOfFamily' r' f)

Tactic:
rw [blsub_eq_lsub', blsub_eq_lsub']

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_sub_left (hf : IntervalIntegrable f volume a b) (c : ℝ) :
    IntervalIntegrable (fun x => f (c - x)) volume (c - a) (c - b)

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (c - x)) volume (c - a) (c - b)

Tactic:
simpa only [neg_sub, ← sub_eq_add_neg] using iff_comp_neg.mp (hf.comp_add_left c)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_antiperiodic : Function.Antiperiodic cos π

Proof state:
⊢ Function.Antiperiodic cos π

Tactic:
simp [cos_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff {g : Perm α}
    {x :α} {m : ℤ} {c : g.cycleFactorsFinset} :
    (g ^ m) x ∈ (c : Perm α).support ↔ x ∈ (c : Perm α).support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
m : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
⊢ (g ^ m) x ∈ (↑c).support ↔ x ∈ (↑c).support

Tactic:
rw [← g.eq_cycleOf_of_mem_cycleFactorsFinset_iff _ c.prop, cycleOf_self_apply_zpow,
  eq_cycleOf_of_mem_cycleFactorsFinset_iff _ _ c.prop]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
lemma integral_indicator₂ {β : Type*} (f : β → α → G) (s : Set β) (b : β) :
    ∫ y, s.indicator (f · y) b ∂μ = s.indicator (fun x ↦ ∫ y, f x y ∂μ) b

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
⊢ ∫ (y : α), s.indicator (fun x => f x y) b ∂μ = s.indicator (fun x => ∫ (y : α), f x y ∂μ) b

Tactic:
by_cases hb : b ∈ s <;> simp [hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k

Proof state:
k x y : Nat
Hk : 0 < k
⊢ ¬y ≤ x / k ↔ ¬y * k ≤ x

Tactic:
exact not_congr (le_div_iff_mul_le Hk)

Result:
no goals

Proof state:
k x y : Nat
Hk : 0 < k
⊢ x / k < y ↔ x < y * k

Tactic:
rw [← Nat.not_le, ← Nat.not_le]

Result:
k x y : Nat
Hk : 0 < k
⊢ ¬y ≤ x / k ↔ ¬y * k ≤ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem get_ite' {p : Prop} [Decidable p] (h) :
    (if p then none else some b).get h = b

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
h : (if p then none else some b).isSome = true
⊢ (if h : p then none else some ((fun x => b) h)).isSome = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α✝ : Type u_1
b : α✝
p : Prop
inst✝ : Decidable p
h : (if p then none else some b).isSome = true
⊢ (if p then none else some b).get h = b

Tactic:
simpa using get_dite' (p := p) (fun _ => b) (by simpa using h)

Result:
no goals
-- Mathlib/Algebra/Order/Star/Conjneg.lean
@[simp] lemma conjneg_nonneg : 0 ≤ conjneg f ↔ 0 ≤ f :=
  (Equiv.neg _).forall_congr' <| by simp [starRingEnd_apply]

Proof state:
G : Type u_1
R : Type u_2
inst✝³ : AddGroup G
inst✝² : OrderedCommSemiring R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ ∀ (b : G), 0 ((Equiv.symm (Equiv.neg G)) b) ≤ conjneg f ((Equiv.symm (Equiv.neg G)) b) ↔ 0 b ≤ f b

Tactic:
simp [starRingEnd_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a

Proof state:
a b : Int
H1 : 0 ≤ a
H2 : a < b
⊢ a.fmod b = a

Tactic:
rw [fmod_eq_emod _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]

Result:
no goals
-- Mathlib/FieldTheory/Galois/GaloisClosure.lean
lemma val_injective : Function.Injective (toIntermediateField (k := k) (K := K))

Proof state:
case mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
toIntermediateField✝¹ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥toIntermediateField✝¹
isGalois✝¹ : IsGalois k ↥toIntermediateField✝¹
toIntermediateField✝ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥toIntermediateField✝
isGalois✝ : IsGalois k ↥toIntermediateField✝
eq : (mk toIntermediateField✝¹).toIntermediateField = (mk toIntermediateField✝).toIntermediateField
⊢ mk toIntermediateField✝¹ = mk toIntermediateField✝

Tactic:
simpa only [mk.injEq] using eq

Result:
no goals

Proof state:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ Function.Injective toIntermediateField

Tactic:
rintro ⟨⟩ ⟨⟩ eq

Result:
case mk.mk
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
toIntermediateField✝¹ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥toIntermediateField✝¹
isGalois✝¹ : IsGalois k ↥toIntermediateField✝¹
toIntermediateField✝ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥toIntermediateField✝
isGalois✝ : IsGalois k ↥toIntermediateField✝
eq : (mk toIntermediateField✝¹).toIntermediateField = (mk toIntermediateField✝).toIntermediateField
⊢ mk toIntermediateField✝¹ = mk toIntermediateField✝
-- Mathlib/Data/Seq/WSeq.lean
theorem map_ret (f : α → β) (a) : map f (ret a) = ret (f a)

Proof state:
α : Type u
β : Type v
f : α → β
a : α
⊢ map f (ret a) = ret (f a)

Tactic:
simp [ret]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.negAddY P Q / W.addZ P Q =
      W.toAffine.negAddY (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))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.negAddY P Q / W.addZ P Q =
    (toAffine W).negAddY (P x / P z) (Q x / Q z) (P y / P z)
      ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [negAddY_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
  toAffine_negAddY_of_ne hPz hQz <| sub_ne_zero.mpr hx]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
theorem finrank_sup_eq_finrank_right_mul_finrank_of_free :
    finrank R ↥(A ⊔ B) = finrank R B * finrank B (Algebra.adjoin B (A : Set S))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥B * finrank ↥B ↥(Algebra.adjoin ↥B ↑A)

Tactic:
rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleMap_sub_center (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ - c = circleMap 0 R θ

Proof state:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ - c = circleMap 0 R θ

Tactic:
simp [circleMap]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_univ_range_eq {m₂ : β → δ} :
    (univ : Set α) ×ˢ range m₂ = range fun p : α × β => (p.1, m₂ p.2) :=
  ext <| by simp [range]

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p => (p.1, m₂ p.2)

Tactic:
simp [range]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_left_eq_neg (x y : V) :
    (o.oangle (y - x) y).sign = -(o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (y - x) y).sign = -(o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_sub_left x y 1, one_smul]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
/-- A bounded above function `u` is in particular eventually bounded above. -/
lemma _root_.BddAbove.isBoundedUnder_of_range (hu : BddAbove (Set.range u)) :
    f.IsBoundedUnder (· ≤ ·) u := BddAbove.isBoundedUnder (s := univ) f.univ_mem (by simpa)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
hu : BddAbove (range u)
⊢ BddAbove (u '' univ)

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_X_pow (n : ℕ) : order ((X : R⟦X⟧) ^ n) = n

Proof state:
case h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).order = ↑n

Tactic:
rw [X_pow_eq, order_monomial_of_ne_zero]

Result:
case h
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ 1 ≠ 0
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_eq_zero_of_dvd_aeval_eq_zero [CommSemiring S] [CommSemiring T] [Algebra S T]
    {p q : S[X]} (h₁ : p ∣ q) {a : T} (h₂ : aeval a p = 0) : aeval a q = 0

Proof state:
S : Type v
T : Type w
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0

Tactic:
exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂

Result:
no goals

Proof state:
S : Type v
T : Type w
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : (aeval a) p = 0
⊢ (aeval a) q = 0

Tactic:
rw [aeval_def, ← eval_map] at h₂ ⊢

Result:
S : Type v
T : Type w
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_flip {n : ℕ} (f : ℕ → β) :
    (∏ r ∈ range (n + 1), f (n - r)) = ∏ k ∈ range (n + 1), f k

Proof state:
case succ
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
⊢ (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ

Tactic:
simp [← ih]

Result:
no goals

Proof state:
case succ
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
⊢ ∏ r ∈ range (n + 1 + 1), f (n + 1 - r) = ∏ k ∈ range (n + 1 + 1), f k

Tactic:
rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]

Result:
case succ
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
⊢ (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ

Proof state:
β : Type u_4
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k

Tactic:
induction n with
| zero => rw [prod_range_one, prod_range_one]
| succ n ih =>
  rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
  simp [← ih]

Result:
no goals

Proof state:
case zero
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ r ∈ range (0 + 1), f (0 - r) = ∏ k ∈ range (0 + 1), f k

Tactic:
rw [prod_range_one, prod_range_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0

Proof state:
n : Nat
k : Fin (n + 1)
⊢ 0 * k = 0

Tactic:
simp [Fin.ext_iff, mul_def]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma empty_isBasis_iff : M.IsBasis ∅ X ↔ X ⊆ M.closure ∅

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsBasis ∅ X ↔ X ⊆ M.closure ∅

Tactic:
rw [isBasis_iff_indep_closure, and_iff_right M.empty_indep, and_iff_left (empty_subset _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getD_eq_getElem?_getD (l) (i) (a : α) : getD l i a = (l[i]?).getD a

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ l.getD i a = l[i]?.getD a

Tactic:
simp [getD]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    (m.erase k).contains a → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ (m.erase k).contains a = true → m.contains a = true

Tactic:
simp_to_raw using Raw₀.contains_of_contains_erase

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity {r d : R}
    (hr : r ≠ 0) (hd : d ∈ normalizedFactors r) :
    emultiplicity d r =
      emultiplicity (normalizedFactorsEquivSpanNormalizedFactors hr ⟨d, hd⟩ : Ideal R)
        (Ideal.span {r})

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r d : R
hr : r ≠ 0
hd : d ∈ normalizedFactors r
⊢ emultiplicity d r = emultiplicity (↑((normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (span {r})

Tactic:
simp only [normalizedFactorsEquivSpanNormalizedFactors, emultiplicity_eq_emultiplicity_span,
  Subtype.coe_mk, Equiv.ofBijective_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_sub_le (a : Nat) {b c : Nat} (h : b ≤ c) : a + b - c = a - (c - b)

Proof state:
a b c : Nat
h : b ≤ c
p : a + b - c = a - (c - b)
⊢ a + b - c = a - (c - b)

Tactic:
exact p

Result:
no goals

Proof state:
a b c : Nat
h : b ≤ c
p : a + b - (0 + c) = a - (0 + (c - b))
⊢ a + b - c = a - (c - b)

Tactic:
simp only [Nat.zero_add] at p

Result:
a b c : Nat
h : b ≤ c
p : a + b - c = a - (c - b)
⊢ a + b - c = a - (c - b)

Proof state:
a b c : Nat
h : b ≤ c
⊢ a + b - c = a - (c - b)

Tactic:
have p := add_sub_add_le a 0 h

Result:
a b c : Nat
h : b ≤ c
p : a + b - (0 + c) = a - (0 + (c - b))
⊢ a + b - c = a - (c - b)
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem srange_eq_top_iff_surjective {f : F} :
    srange f = (⊤ : NonUnitalSubsemiring S) ↔ Function.Surjective (f : R → S) :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ

Proof state:
R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ↑(srange f) = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_srange, coe_top]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma map_add_left_Ico (a b c : α) :
    (Ico a b).map (addLeftEmbedding c) = Ico (c + a) (c + b)

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ico a b = Set.Ico (c + a) (c + b)

Tactic:
exact Set.image_const_add_Ico _ _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (addLeftEmbedding c) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [← coe_inj, coe_map, coe_Ico, coe_Ico]

Result:
α : Type u_2
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ ⇑(addLeftEmbedding c) '' Set.Ico a b = Set.Ico (c + a) (c + b)
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioo_sub_one_left_eq_Ioc (a b : α) : Ioo (a - 1) b = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioo_pred_left_eq_Ioc a b

Result:
no goals