harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/Pi.lean
theorem splittingOfFunOnFintypeSurjective_splits [Finite α] (f : M →ₗ[R] α → R)
    (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

Tactic:
ext x y

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ ((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun i => R) x) 1 y = (id ∘ₗ single R (fun i => R) x) 1 y

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id

Tactic:
classical
ext x y
dsimp [splittingOfFunOnFintypeSurjective]
rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
  (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
rw [zero_smul]

Result:
no goals

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
rw [zero_smul]

Result:
no goals

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ ((f ∘ₗ f.splittingOfFunOnFintypeSurjective s) ∘ₗ single R (fun i => R) x) 1 y = (id ∘ₗ single R (fun i => R) x) 1 y

Tactic:
dsimp [splittingOfFunOnFintypeSurjective]

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f (((linearEquivFunOnFinite R R α).symm (Pi.single x 1)).sum fun x r => r • ⋯.choose) y = Pi.single x 1 y

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f (((linearEquivFunOnFinite R R α).symm (Pi.single x 1)).sum fun x r => r • ⋯.choose) y = Pi.single x 1 y

Tactic:
rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
  (s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_4
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Ioo_add_bij : BijOn (· + d) (Ioo a b) (Ioo (a + d) (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioo a b) (Ioo (a + d) (b + d))

Tactic:
rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))

Tactic:
exact
  (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx =>
    lt_of_add_lt_add_right hx.2

Result:
no goals
-- Mathlib/Data/Nat/PSub.lean
theorem pred_eq_ppred (n : ℕ) : pred n = (ppred n).getD 0

Proof state:
n : ℕ
⊢ n.pred = n.ppred.getD 0

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_iff_injective_get {l : List α} :
    Nodup l ↔ Function.Injective l.get

Proof state:
α : Type u
l : List α
⊢ (Injective fun i => l[↑i]) ↔ Injective l.get

Tactic:
change _ ↔ Injective (fun i => l.get i)

Result:
α : Type u
l : List α
⊢ (Injective fun i => l[↑i]) ↔ Injective fun i => l.get i

Proof state:
α : Type u
l : List α
⊢ (Injective fun i => l[↑i]) ↔ Injective fun i => l.get i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ l.Nodup ↔ Injective l.get

Tactic:
rw [nodup_iff_injective_getElem]

Result:
α : Type u
l : List α
⊢ (Injective fun i => l[↑i]) ↔ Injective l.get
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.sInter {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) :
    MeasurableSet (⋂₀ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂₀ s)

Tactic:
rw [sInter_eq_biInter]

Result:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)

Tactic:
exact MeasurableSet.biInter hs h

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_nil : π [] = 1

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.wordProd [] = 1

Tactic:
simp [wordProd]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma one_product_one [One β] : (1 ×ˢ 1 : Finset (α × β)) = 1

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
a✝ : α × β
⊢ a✝ ∈ 1 ×ˢ 1 ↔ a✝ ∈ 1

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
a✝ : α × β
⊢ a✝ ∈ 1 ×ˢ 1 ↔ a✝ ∈ 1

Tactic:
simp [Prod.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem MonoidHom.map_mulIndicator {M N : Type*} [MulOneClass M] [MulOneClass N] (f : M →* N)
    (s : Set α) (g : α → M) (x : α) : f (s.mulIndicator g x) = s.mulIndicator (f ∘ g) x

Proof state:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
s : Set α
g : α → M
x : α
⊢ f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x

Tactic:
simp [Set.mulIndicator_comp_of_one]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma support_nonempty {p : MvPolynomial σ R} : p.support.Nonempty ↔ p ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv_symm_apply {n : ℤ} (f : ShiftedHom (Opposite.op Y) (Opposite.op X) n) :
    (opEquiv n).symm f =
      ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫ f.unop⟦n⟧'

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
n : ℤ
f : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ (opEquiv n).symm f =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫ (shiftFunctor C n).map (Quiver.Hom.unop f)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_inv_app_left :
    (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.left = iX.inv

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem exists_norm_eq_iInf_of_complete_subspace (h : IsComplete (↑K : Set E)) :
    ∀ u : E, ∃ v ∈ K, ‖u - v‖ = ⨅ w : (K : Set E), ‖u - w‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
let K' : Submodule ℝ E := Submodule.restrictScalars ℝ K

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
exact exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete ↑K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_neg : cosh (-x) = cosh x

Proof state:
x : ℂ
⊢ cosh (-x) = cosh x

Tactic:
simp [add_comm, cosh, exp_neg]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousAt_update_same [DecidableEq α] {y : β} :
    ContinuousAt (Function.update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

Tactic:
rw [← continuousWithinAt_univ, continuousWithinAt_update_same, compl_eq_univ_diff]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_eq (μ : Measure Ω) [IsFiniteMeasure μ] [h : Nonempty Ω]
    (m : MeasurableSpace Ω) :
    condExpKernel (mΩ := mΩ) μ m = Kernel.comap (@condDistrib Ω Ω Ω mΩ _ _ mΩ (m ⊓ mΩ) id id μ _) id
      (measurable_id'' (inf_le_left : m ⊓ mΩ ≤ m))

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
m : MeasurableSpace Ω
⊢ condExpKernel μ m = (condDistrib id id μ).comap id ⋯

Tactic:
simp [condExpKernel, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem mem_of_mem_eraseP {l : Array α} : a ∈ l.eraseP p → a ∈ l

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ a ∈ { toList := l }.eraseP p → a ∈ { toList := l }

Tactic:
simpa using List.mem_of_mem_eraseP

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
⊢ a ∈ l.eraseP p → a ∈ l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ a ∈ { toList := l }.eraseP p → a ∈ { toList := l }
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem natDegree_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquiv R n f).natDegree = degreeOf 0 f

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
by_cases c : f = 0

Result:
case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ((finSuccEquiv R n) f).natDegree = degreeOf 0 f

Tactic:
rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem succ_zero_eq_one' [NeZero n] : Fin.succ (0 : Fin n) = 1

Proof state:
case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

Tactic:
exact (NeZero.ne 0 rfl).elim

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ succ 0 = 1

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Enum.lean
theorem forall_mem_zipIdx {l : List α} {n : ℕ} {p : α × ℕ → Prop} :
    (∀ x ∈ l.zipIdx n, p x) ↔ ∀ (i : ℕ) (_ : i < length l), p (l[i], n + i)

Proof state:
α : Type u_1
l : List α
n : ℕ
p : α × ℕ → Prop
⊢ (∀ (x : α × ℕ), x ∈ l.zipIdx n → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], n + i)

Tactic:
simp only [forall_mem_iff_getElem, getElem_zipIdx, length_zipIdx]

Result:
no goals
-- Mathlib/Logic/Function/FiberPartition.lean
lemma mem_iff_eq_image (f : Y → Z) (y : Y) (a : Fiber f) : y ∈ a.val ↔ f y = a.image :=
  ⟨fun h ↦ a.map_eq_image _ ⟨y, h⟩, fun h ↦ by rw [a.eq_fiber_image]; exact h⟩

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ f ⁻¹' {image f a}

Tactic:
exact h

Result:
no goals

Proof state:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ ↑a

Tactic:
rw [a.eq_fiber_image]

Result:
Y : Type u_2
Z : Type u_3
f : Y → Z
y : Y
a : Fiber f
h : f y = image f a
⊢ y ∈ f ⁻¹' {image f a}
-- Mathlib/Data/Finset/Max.lean
@[simp]
protected lemma max_eq_top [OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s :=
  Finset.sup_eq_top_iff.trans <| by simp

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Finset α
⊢ (∃ b ∈ s, ↑b = ⊤) ↔ ⊤ ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.pow {p a : α} (hp : Prime p)
    (hfin : FiniteMultiplicity p a) {k : ℕ} : FiniteMultiplicity p (a ^ k) :=
  match k, hfin with
  | 0, _ => ⟨0, by simp [mt isUnit_iff_dvd_one.2 hp.2.1]⟩
  | k + 1, ha => by rw [_root_.pow_succ']; exact hp.finiteMultiplicity_mul ha (ha.pow hp)

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k : ℕ
x✝ : FiniteMultiplicity p a
⊢ ¬p ^ (0 + 1) ∣ a ^ 0

Tactic:
simp [mt isUnit_iff_dvd_one.2 hp.2.1]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)

Tactic:
exact hp.finiteMultiplicity_mul ha (ha.pow hp)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
rw [_root_.pow_succ']

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)
-- Mathlib/Order/Cofinal.lean
theorem IsCofinal.trans {s : Set α} {t : Set s} (hs : IsCofinal s) (ht : IsCofinal t) :
    IsCofinal (Subtype.val '' t)

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
⊢ IsCofinal (Subtype.val '' t)

Tactic:
intro a

Result:
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a : α
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := ht ⟨b, hb⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a b : α
hb : b ∈ s
hb' : a ≤ b
c : ↑s
hc : c ∈ t
hc' : ⟨b, hb⟩ ≤ c
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a : α
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a b : α
hb : b ∈ s
hb' : a ≤ b
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
a b : α
hb : b ∈ s
hb' : a ≤ b
c : ↑s
hc : c ∈ t
hc' : ⟨b, hb⟩ ≤ c
⊢ ∃ y ∈ Subtype.val '' t, a ≤ y

Tactic:
exact ⟨c, Set.mem_image_of_mem _ hc, hb'.trans hc'⟩

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
theorem MonoidHom.id_commMonCat_comp {G : Type u} [CommMonoid G] {H : CommMonCat.{u}} (f : G →* H) :
    MonoidHom.comp (CommMonCat.Hom.hom (𝟙 H)) f = f

Proof state:
G : Type u
inst✝ : CommMonoid G
H : CommMonCat
f : G →* ↑H
⊢ (CommMonCat.Hom.hom (𝟙 H)).comp f = f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_neg (x : ℝ) : log⁺ (-x) = log⁺ x

Proof state:
x : ℝ
⊢ log⁺ (-x) = log⁺ x

Tactic:
simp [posLog]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_add : ∀ m n, ((m + n : ℤ) : R) = m + n
  | (m : ℕ), (n : ℕ) => by simp [-Int.natCast_add, ← Int.ofNat_add]
  | (m : ℕ), -[n+1] => by erw [cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
  | -[m+1], (n : ℕ) => by
    erw [cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add, add_assoc,
      eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
  | -[m+1], -[n+1] =>
    show (-[m + n + 1+1] : R) = _ by
      rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
        Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[m + n + 1+1] = ↑-[m+1] + ↑-[n+1]

Tactic:
rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
  Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n

Tactic:
erw [cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add, add_assoc,
  eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]

Tactic:
erw [cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n

Tactic:
simp [-Int.natCast_add, ← Int.ofNat_add]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem denom_mul_dvd (x y : RatFunc K) : denom (x * y) ∣ denom x * denom y

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x * y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
refine ⟨x.num * y.num, ?_⟩

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)

Tactic:
rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, num_div_denom, num_div_denom]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ (x * y).denom ∣ x.denom * y.denom

Tactic:
rw [denom_dvd (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))]

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
⊢ ∃ p, x * y = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
/--
Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
Then the centralizer of `A ⊗ 1 ⊆ A ⊗ B` is `C(A) ⊗ B` where `C(A)` is the center of `A`.
-/
lemma centralizer_coe_range_includeLeft_eq_center_tensorProduct [Module.Free R B] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.includeLeft : A →ₐ[R] A ⊗[R] B).range =
    (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = (Algebra.TensorProduct.map (center R A).val (AlgHom.id R B)).range

Tactic:
rw [← centralizer_univ, ← Algebra.coe_top (R := R) (A := A),
  ← centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = centralizer R ↑(map includeLeft ⊤)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = centralizer R ↑(map includeLeft ⊤)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
x✝ : A ⊗[R] B
⊢ x✝ ∈ centralizer R ↑includeLeft.range ↔ x✝ ∈ centralizer R ↑(map includeLeft ⊤)

Proof state:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
x✝ : A ⊗[R] B
⊢ x✝ ∈ centralizer R ↑includeLeft.range ↔ x✝ ∈ centralizer R ↑(map includeLeft ⊤)

Tactic:
simp [includeLeft, includeLeftRingHom, Set.range_comp]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma neg_add {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊤) (h2 : x ≠ ⊤ ∨ y ≠ ⊥) :
    - (x + y) = - x - y

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

Tactic:
rw [← coe_add, ← coe_neg, ← coe_neg, ← coe_sub, neg_add']

Result:
no goals

Proof state:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊤
h2 : x ≠ ⊤ ∨ y ≠ ⊥
⊢ -(x + y) = -x - y

Tactic:
induction x <;> induction y <;> try tauto

Result:
case h_real.h_real
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ -(↑a✝¹ + ↑a✝) = -↑a✝¹ - ↑a✝

Proof state:
case h_top.h_top
h1 : ⊤ ≠ ⊥ ∨ ⊤ ≠ ⊤
h2 : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊥
⊢ -(⊤ + ⊤) = -⊤ - ⊤

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem coe_unit_eq_one (u : (Associates M)ˣ) : (u : Associates M) = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
u : (Associates M)ˣ
⊢ ↑u = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem lt_def {p q : ℚ≥0} : p < q ↔ p.num * q.den < q.num * p.den

Proof state:
p q : ℚ≥0
⊢ p < q ↔ p.num * q.den < q.num * p.den

Tactic:
rw [← NNRat.coe_lt_coe, Rat.lt_def]

Result:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den

Proof state:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den < (↑q).num * ↑(↑p).den ↔ p.num * q.den < q.num * p.den

Tactic:
norm_cast

Result:
no goals