harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma factorization_ceilRoot (n a : ℕ) :
    (ceilRoot n a).factorization = a.factorization ⌈/⌉ n

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Tactic:
refine prod_pow_factorization_eq_self fun p hp ↦ ?_

Result:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p

Proof state:
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p ∧ p ∣ a ∧ ¬a = 0

Tactic:
simpa using support_ceilDiv_subset hp

Result:
no goals

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
⊢ Prime p

Tactic:
have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp

Result:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Proof state:
n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Tactic:
split_ifs with h

Result:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n

case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
⊢ ((a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Proof state:
n a : ℕ
⊢ (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n

Tactic:
rw [ceilRoot_def]

Result:
n a : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2).factorization = a.factorization ⌈/⌉ n

Proof state:
case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n

Tactic:
obtain rfl | rfl := h <;> simp

Result:
no goals

Proof state:
case neg
n a : ℕ
h : ¬(n = 0 ∨ a = 0)
p : ℕ
hp : p ∈ (a.factorization ⌈/⌉ n).support
this : Prime p ∧ p ∣ a ∧ ¬a = 0
⊢ Prime p

Tactic:
exact this.1

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_add_eq_right (h : p.supDegree D < q.supDegree D) :
    (p + q).supDegree D = q.supDegree D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D p < supDegree D q
⊢ supDegree D (p + q) = supDegree D q

Tactic:
rw [add_comm, supDegree_add_eq_left h]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
@[reassoc]
lemma toRightDerivedZero'_naturality {C} [Category C] [Abelian C] {X Y : C} (f : X ⟶ Y)
    (P : InjectiveResolution X) (Q : InjectiveResolution Y)
    (φ : P.cocomplex ⟶ Q.cocomplex) (comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0)
    (F : C ⥤ D) [F.Additive] :
    F.map f ≫ Q.toRightDerivedZero' F =
      P.toRightDerivedZero' F ≫
        HomologicalComplex.cyclesMap ((F.mapHomologicalComplex _).map φ) 0

Proof state:
D : Type u_1
inst✝⁴ : Category.{u_4, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
φ : P.cocomplex ⟶ Q.cocomplex
comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map f ≫ Q.toRightDerivedZero' F =
    P.toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0

Tactic:
simp only [← cancel_mono (HomologicalComplex.iCycles _ _),
  Functor.mapHomologicalComplex_obj_X, assoc, toRightDerivedZero'_comp_iCycles,
  CochainComplex.single₀_obj_zero, HomologicalComplex.cyclesMap_i,
  Functor.mapHomologicalComplex_map_f, toRightDerivedZero'_comp_iCycles_assoc,
  ← F.map_comp, comm]

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem map_ciSup (hf : LeftOrdContinuous f) {g : ι → α} (hg : BddAbove (range g)) :
    f (⨆ i, g i) = ⨆ i, f (g i)

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]

Result:
α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun i => f (g i))

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun i => f (g i))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_add_zsmul' (a b : α) (m : ℤ) :
    toIocDiv hp (a + m • p) b = toIocDiv hp a b - m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - m

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc _ ?_

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)

Tactic:
simpa using sub_toIocDiv_zsmul_mem_Ioc hp a b

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem of_ne_one (a : α) : of a ≠ 1

Proof state:
α : Type u_1
a : α
h : of a = 1
this : (of a).length = length 1
⊢ False

Tactic:
simp only [length_of, length_one, Nat.succ_ne_self] at this

Result:
no goals

Proof state:
α : Type u_1
a : α
⊢ of a ≠ 1

Tactic:
intro h

Result:
α : Type u_1
a : α
h : of a = 1
⊢ False

Proof state:
α : Type u_1
a : α
h : of a = 1
⊢ False

Tactic:
have := congrArg FreeMonoid.length h

Result:
α : Type u_1
a : α
h : of a = 1
this : (of a).length = length 1
⊢ False
-- Mathlib/Data/TypeVec.lean
theorem const_nil {β} (x : β) (α : TypeVec 0) : TypeVec.const x α = nilFun

Proof state:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun

Tactic:
ext i : 1

Result:
case a
β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i

Proof state:
case a
β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i

Tactic:
cases i

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.fg_adjoin_singleton [Algebra R B] {x : B} (hx : IsIntegral R x) :
    (Algebra.adjoin R {x}).toSubmodule.FG

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
hx : IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R {x})).FG

Tactic:
rcases hx with ⟨f, hfm, hfx⟩

Result:
case intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R {x})).FG

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ (aeval x) f = 0

Tactic:
rwa [aeval_def]

Result:
no goals

Proof state:
case h
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
f : R[X]
hfm : f.Monic
hfx : eval₂ (algebraMap R B) x f = 0
⊢ span R ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})

Tactic:
exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem covBy_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a)

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom ⟨b, h⟩

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem isSplittingField_iff_intermediateField : p.IsSplittingField K L ↔
    p.Splits (algebraMap K L) ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔ Splits (algebraMap K L) p ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤

Tactic:
rw [← IntermediateField.toSubalgebra_injective.eq_iff,
    IntermediateField.adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔ Splits (algebraMap K L) p ∧ Algebra.adjoin K (p.rootSet L) = ⊤.toSubalgebra

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
⊢ IsSplittingField K L p ↔ Splits (algebraMap K L) p ∧ Algebra.adjoin K (p.rootSet L) = ⊤.toSubalgebra

Tactic:
exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean
/-- There are `n.totient` Dirichlet characters mod `n` with values in a ring that has enough
roots of unity. -/
lemma card_eq_totient_of_hasEnoughRootsOfUnity :
    Nat.card (DirichletCharacter R n) = n.totient

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = n.totient

Tactic:
rw [← ZMod.card_units_eq_totient n, ← Nat.card_eq_fintype_card]

Result:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Tactic:
exact Nat.card_congr (mulEquiv_units R n).some.toEquiv

Result:
no goals
-- Mathlib/GroupTheory/Commensurable.lean
theorem refl (H : Subgroup G) : Commensurable H H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Commensurable H H

Tactic:
simp [Commensurable]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_lt_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal ↔ a < b

Proof state:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal < (↑b).toReal ↔ ↑a < ↑b

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal < b.toReal ↔ ↑a < b

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal < (↑b).toReal ↔ ↑a < ↑b

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a.toReal < b.toReal ↔ a < b

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal < b.toReal ↔ ↑a < b
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem vanishingIdeal_iUnion {γ : Sort*} (t : γ → Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal (⋃ i, t i) = ⨅ i, vanishingIdeal (t i) :=
  HomogeneousIdeal.toIdeal_injective <| by
    convert (gc_ideal 𝒜).u_iInf; exact HomogeneousIdeal.toIdeal_iInf _

Proof state:
case h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (⨅ i, vanishingIdeal (t i)).toIdeal = ⨅ i, (vanishingIdeal (t i)).toIdeal

Tactic:
exact HomogeneousIdeal.toIdeal_iInf _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (⋃ i, t i)).toIdeal = (⨅ i, vanishingIdeal (t i)).toIdeal

Tactic:
convert (gc_ideal 𝒜).u_iInf

Result:
case h.e'_3
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ (⨅ i, vanishingIdeal (t i)).toIdeal = ⨅ i, (vanishingIdeal (t i)).toIdeal
-- Mathlib/LinearAlgebra/Charpoly/Basic.lean
lemma charpoly_natDegree [Nontrivial R] [StrongRankCondition R] :
    natDegree (charpoly f) = finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
inst✝¹ : Nontrivial R
inst✝ : StrongRankCondition R
⊢ f.charpoly.natDegree = finrank R M

Tactic:
rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]

Result:
no goals
-- Mathlib/Data/Complex/BigOperators.lean
@[simp, norm_cast]
lemma ofReal_balance [Fintype α] (f : α → ℝ) (a : α) :
    ((balance f a : ℝ) : ℂ) = balance ((↑) ∘ f) a

Proof state:
α : Type u_1
inst✝ : Fintype α
f : α → ℝ
a : α
⊢ ↑(balance f a) = balance (ofReal ∘ f) a

Tactic:
simp [balance]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_lt_rpow_iff (hx : 0 ≤ x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Proof state:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

Tactic:
rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, lt_irrefl, (zero_lt_one' ℝ).not_lt]

Result:
no goals

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Result:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 1 < 0 ^ y ↔ 1 < 0 ∧ 0 < y ∨ 0 < 0 ∧ 0 < 1 ∧ y < 0

case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Proof state:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

Tactic:
simp [one_lt_rpow_iff_of_pos hx, hx]

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem direction_perpBisector (p₁ p₂ : P) :
    (perpBisector p₁ p₂).direction = (ℝ ∙ (p₂ -ᵥ p₁))ᗮ

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
x : V
⊢ x ∈ LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) ↔ x ∈ (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ

Tactic:
exact Submodule.mem_orthogonal_singleton_iff_inner_right.symm

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ

Tactic:
ext x

Result:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
x : V
⊢ x ∈ LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) ↔ x ∈ (Submodule.span ℝ {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
⊢ (perpBisector p₁ p₂).direction = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ

Tactic:
erw [perpBisector, comap_symm, map_direction, Submodule.map_id,
  Submodule.toAffineSubspace_direction]

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
⊢ LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_eq_right_iff {x y : P} : midpoint R x y = y ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = y ↔ x = y

Tactic:
rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β → β} :
    (Const.modify m k f).getKeyD k fallback = if m.contains k then k else fallback

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k fallback : α
f : β → β
⊢ (modify m k f).getKeyD k fallback = if m.contains k = true then k else fallback

Tactic:
simp_to_model [Const.modify] using List.Const.getKeyD_modifyKey_self

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
lemma IsNilpotent.not_isUnit [Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) :
    ¬ IsUnit x :=
  mt IsUnit.not_isNilpotent (by simpa only [not_not] using hx)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsNilpotent x
⊢ ¬¬IsNilpotent x

Tactic:
simpa only [not_not] using hx

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem measure_preimage {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞)
    (hu : IsUniform X s ℙ μ) {A : Set E} (hA : MeasurableSet A) :
    ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ⊤
hu : IsUniform X s ℙ μ
A : Set E
hA : MeasurableSet A
⊢ ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s

Tactic:
rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
  ENNReal.div_eq_inv_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem w {A B : Over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Over X
f : A ⟶ B
⊢ f.left ≫ B.hom = A.hom

Tactic:
have := f.w

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Over X
f : A ⟶ B
this : (𝟭 T).map f.left ≫ B.hom = A.hom ≫ (Functor.fromPUnit X).map f.right
⊢ f.left ≫ B.hom = A.hom

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
A B : Over X
f : A ⟶ B
this : (𝟭 T).map f.left ≫ B.hom = A.hom ≫ (Functor.fromPUnit X).map f.right
⊢ f.left ≫ B.hom = A.hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow {f g : ℕ → E}
    (hf : f =O[atTop] fun n ↦ (n : ℝ) ^ a) (hg : g =O[atTop] fun n ↦ (n : ℝ) ^ b)
    (h : a + b ≤ c) :
    (f * g) =O[atTop] fun n ↦ (n : ℝ) ^ c

Proof state:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ↑t ^ (a + b) ≤ ↑t ^ c

Tactic:
exact Real.rpow_le_rpow_of_exponent_le ht h

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Tactic:
rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
  (zero_le_one.trans ht) (a + b))]

Result:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ↑t ^ (a + b) ≤ ↑t ^ c

Proof state:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Tactic:
replace ht : 1 ≤ (t : ℝ) := Nat.one_le_cast.mpr ht

Result:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ ↑t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Proof state:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑x ^ a * ↑x ^ b‖ ≤ ↑x ^ c

Tactic:
filter_upwards [eventually_ge_atTop 1] with t ht

Result:
case h
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
t : ℕ
ht : 1 ≤ t
⊢ ‖↑t ^ a * ↑t ^ b‖ ≤ ↑t ^ c

Proof state:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun n => ↑n ^ c

Tactic:
refine (hf.mul hg).trans (Eventually.isBigO ?_)

Result:
E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℕ → E
hf : f =O[atTop] fun n => ↑n ^ a
hg : g =O[atTop] fun n => ↑n ^ b
h : a + b ≤ c
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑x ^ a * ↑x ^ b‖ ≤ ↑x ^ c
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma mk_eq_mk_iff_crossProduct_eq_zero {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) :
    mk F v hv = mk F w hw ↔ crossProduct v w = 0

Proof state:
F : Type u_1
inst✝ : Field F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ mk F v hv = mk F w hw ↔ (crossProduct v) w = 0

Tactic:
rw [← not_iff_not, mk_eq_mk_iff', not_exists, ← LinearIndependent.pair_iff' hw,
  ← crossProduct_ne_zero_iff_linearIndependent, ← cross_anticomm, neg_ne_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma comp_apply {M N O : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ O) (r : M) :
    (f ≫ g) r = g (f r)

Proof state:
M N O : SemiNormedGrp₁
f : M ⟶ N
g : N ⟶ O
r : M.carrier
⊢ ↑(Hom.hom (f ≫ g)) r = ↑(Hom.hom g) (↑(Hom.hom f) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/CastCard.lean
lemma cast_card_sdiff [AddGroupWithOne R] (h : s ⊆ t) : (#(t \ s) : R) = #t - #s

Proof state:
α : Type u_1
R : Type u_3
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
h : s ⊆ t
⊢ ↑(#(t \ s)) = ↑(#t) - ↑(#s)

Tactic:
rw [card_sdiff h, Nat.cast_sub (card_mono h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty = true → get? m a = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.isEmpty = true → get? m a = none

Tactic:
simp_to_raw using Raw₀.Const.get?_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma coe_fwdDiffₗ_pow (n : ℕ) : ↑(fwdDiffₗ M G h ^ n) = (fwdDiff h)^[n]

Proof state:
case h.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝

Tactic:
rw [LinearMap.pow_apply, coe_fwdDiffₗ]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
⊢ ⇑(fwdDiffₗ M G h ^ n) = Δ_[h]^[n]

Tactic:
ext

Result:
case h.h
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
n : ℕ
x✝¹ : M → G
x✝ : M
⊢ (fwdDiffₗ M G h ^ n) x✝¹ x✝ = Δ_[h]^[n] x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∧ b) = b

Proof state:
a b : Prop
h : a = True
⊢ (a ∧ b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem stronglyMeasurableAt_bot {f : α → β} : StronglyMeasurableAtFilter f ⊥ μ :=
  ⟨∅, mem_bot, by simp⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : TopologicalSpace β
μ : Measure α
f : α → β
⊢ AEStronglyMeasurable f (μ.restrict ∅)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_cons_self_replicate (n) (a : α) :
    dropLast (a :: replicate n a) = replicate n a

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (a :: replicate n a).dropLast = replicate n a

Tactic:
rw [← replicate_succ, dropLast_replicate, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_subtype (p : α → Prop) : IsEmpty (Subtype p) ↔ ∀ x, ¬p x

Proof state:
α : Sort u_1
p : α → Prop
⊢ IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x

Tactic:
simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

Result:
no goals