harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subtype {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ x, x ∈ s ↔ p x)
    (f : α → β) : ∏ a ∈ s, f a = ∏ a : Subtype p, f a

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
F : Fintype { x // x ∈ s }
h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x
⊢ ∏ a ∈ s, f a = ∏ a : { x // x ∈ s }, f ↑a

Tactic:
rw [← prod_coe_sort]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
F : Fintype { x // x ∈ s }
h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x
⊢ ∏ i : { x // x ∈ s }, f ↑i = ∏ a : { x // x ∈ s }, f ↑a

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
p : α → Prop
F : Fintype (Subtype p)
s : Finset α
h : ∀ (x : α), x ∈ s ↔ p x
f : α → β
this : (fun x => x ∈ s) = p
⊢ ∏ a ∈ s, f a = ∏ a : Subtype p, f ↑a

Tactic:
subst p

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
F : Fintype { x // x ∈ s }
h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x
⊢ ∏ a ∈ s, f a = ∏ a : { x // x ∈ s }, f ↑a

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
F : Fintype { x // x ∈ s }
h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x
⊢ ∏ i : { x // x ∈ s }, f ↑i = ∏ a : { x // x ∈ s }, f ↑a

Tactic:
congr!

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem _root_.Algebra.adjoin_range_eq_range_aeval :
    Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Algebra.adjoin R (range f) = (aeval f).range

Tactic:
simp only [← Algebra.map_top, ← MvPolynomial.adjoin_range_X, AlgHom.map_adjoin, ← Set.range_comp,
  Function.comp_def, MvPolynomial.aeval_X]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_biUnion₀ {s : Set β} {f : β → Set α} (hs : s.Countable)
    (hd : s.Pairwise (AEDisjoint μ on f)) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
    μ (⋃ b ∈ s, f b) = ∑' p : s, μ (f p)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

Tactic:
haveI := hs.toEncodable

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ x, f ↑x) = ∑' (p : ↑s), μ (f ↑p)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable ↑s
⊢ μ (⋃ x, f ↑x) = ∑' (p : ↑s), μ (f ↑p)

Tactic:
exact measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ioc_iff_Ioi (h : a < b) :
    ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIciTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioc a b) a ↔ ContinuousWithinAt f (Ioi a) a

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsGT h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem comp_symm_mem_uniformity_sets {s : Set (α × α)} (hs : s ∈ 𝓤 α) :
    ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ w ○ w

Tactic:
gcongr

Result:
no goals

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s

Tactic:
calc symmetrizeRel w ○ symmetrizeRel w
  _ ⊆ w ○ w := by gcongr
  _ ⊆ s     := w_sub

Result:
no goals

Proof state:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s

Tactic:
have : symmetrizeRel w ⊆ w := symmetrizeRel_subset_self w

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : symmetrizeRel w ⊆ w
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s

Proof state:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s

Tactic:
use symmetrizeRel w, symmetrize_mem_uniformity w_in, symmetric_symmetrizeRel w

Result:
case right
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ symmetrizeRel w ○ symmetrizeRel w ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s

Tactic:
obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs

Result:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s
-- Mathlib/Computability/Primrec.lean
theorem add : Nat.Primrec (unpaired (· + ·)) :=
  (prec .id ((Primrec.succ.comp right).comp right)).of_eq fun p => by
    simp; induction p.unpair.2 <;> simp [*, Nat.add_assoc]

Proof state:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH => IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2

Tactic:
induction p.unpair.2 <;> simp [*, Nat.add_assoc]

Result:
no goals

Proof state:
p : ℕ
⊢ unpaired (fun z n => Nat.rec (id z) (fun y IH => (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.succ) n) p =
    unpaired (fun x1 x2 => x1 + x2) p

Tactic:
simp

Result:
p : ℕ
⊢ Nat.rec (unpair p).1 (fun y IH => IH + 1) (unpair p).2 = (unpair p).1 + (unpair p).2
-- Mathlib/Data/Fin/Parity.lean
lemma even_of_val {n : ℕ} {k : Fin n} (h : Even k.val) : Even k

Proof state:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even k

Tactic:
rw [← Fin.cast_val_eq_self k]

Result:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even ↑↑k

Proof state:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even ↑↑k

Tactic:
exact h.natCast

Result:
no goals

Proof state:
n : ℕ
k : Fin n
h : Even ↑k
⊢ Even k

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩

Result:
n : ℕ
k : Fin n
h : Even ↑k
this : NeZero n
⊢ Even k
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem mono_of_source_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : Mono f :=
  ⟨fun {Z} g h _ => by rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
x✝ : g ≫ f = h ≫ f
⊢ g = h

Tactic:
rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem finsuppTotal_apply_eq_of_fintype [Fintype ι] (f : ι →₀ I) :
    finsuppTotal ι M I v f = ∑ i, (f i : R) • v i

Proof state:
case h
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0

Tactic:
exact fun _ => zero_smul _ _

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = ∑ i : ι, ↑(f i) • v i

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_fintype]

Result:
case h
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem cone_iso_of_hom_iso {K : J ⥤ C} {c d : Cone K} (f : c ⟶ d) [i : IsIso f.hom] : IsIso f :=
  ⟨⟨{   hom := inv f.hom
        w := fun j => (asIso f.hom).inv_comp_eq.2 (f.w j).symm }, by aesop_cat⟩⟩

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
K : J ⥤ C
c d : Cone K
f : c ⟶ d
i : IsIso f.hom
⊢ f ≫ { hom := inv f.hom, w := ⋯ } = 𝟙 c ∧ { hom := inv f.hom, w := ⋯ } ≫ f = 𝟙 d

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[simp]
lemma genEigenspace_zero {f : End R M} {μ : R} :
    f.genEigenspace μ 0 = ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) 0 = ⊥

Tactic:
ext

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x✝ : M
⊢ x✝ ∈ (f.genEigenspace μ) 0 ↔ x✝ ∈ ⊥

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x✝ : M
⊢ x✝ ∈ (f.genEigenspace μ) 0 ↔ x✝ ∈ ⊥

Tactic:
apply mem_genEigenspace_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_filterMapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.filterMapₘ f).1 where
  buckets_hash_self := isHashSelf_filterMapₘ h
  size_eq

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
h : Raw.WFImp m.val
⊢ (m.filterMapₘ f).val.size = (toListModel (m.filterMapₘ f).val.buckets).length

Tactic:
simp [filterMapₘ]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
protected lemma empty : Absorbs M s ∅

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
⊢ Absorbs M s ∅

Tactic:
simp [Absorbs]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Ideal.lean
theorem ker_evalRingHom (x : R) : RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - C x}

Tactic:
simp [Ideal.mem_span_singleton, dvd_iff_isRoot, RingHom.mem_ker]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ RingHom.ker (evalRingHom x) = Ideal.span {X - C x}

Tactic:
ext y

Result:
case h
R : Type u_1
inst✝ : CommRing R
x : R
y : R[X]
⊢ y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - C x}
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem mk_arrow (P : Subobject X) : mk P.arrow = P :=
  Quotient.inductionOn' P fun Q => by
    obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q
    exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
Q : MonoOver X
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
obtain ⟨e⟩ := @Quotient.mk_out' _ (isIsomorphicSetoid _) Q

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
Q : MonoOver X
e : (Quotient.mk'' Q).out ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
Q : MonoOver X
e : (Quotient.mk'' Q).out ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]?

Proof state:
case succ.cons
α : Type u_1
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝ → (take n✝ l)[m]? = l[m]?
m : Nat
h : m < n✝ + 1
hd : α
tl : List α
⊢ (take (n✝ + 1) (hd :: tl))[m]? = (hd :: tl)[m]?

Tactic:
cases m

Result:
case succ.cons.zero
α : Type u_1
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝ → (take n✝ l)[m]? = l[m]?
hd : α
tl : List α
h : 0 < n✝ + 1
⊢ (take (n✝ + 1) (hd :: tl))[0]? = (hd :: tl)[0]?

case succ.cons.succ
α : Type u_1
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝¹ → (take n✝¹ l)[m]? = l[m]?
hd : α
tl : List α
n✝ : Nat
h : n✝ + 1 < n✝¹ + 1
⊢ (take (n✝¹ + 1) (hd :: tl))[n✝ + 1]? = (hd :: tl)[n✝ + 1]?

Proof state:
case succ.cons.succ
α : Type u_1
n✝¹ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝¹ → (take n✝¹ l)[m]? = l[m]?
hd : α
tl : List α
n✝ : Nat
h : n✝ + 1 < n✝¹ + 1
⊢ (take (n✝¹ + 1) (hd :: tl))[n✝ + 1]? = (hd :: tl)[n✝ + 1]?

Tactic:
simpa using hn (Nat.lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
case succ.cons.zero
α : Type u_1
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝ → (take n✝ l)[m]? = l[m]?
hd : α
tl : List α
h : 0 < n✝ + 1
⊢ (take (n✝ + 1) (hd :: tl))[0]? = (hd :: tl)[0]?

Tactic:
simp

Result:
no goals

Proof state:
case zero
α : Type u_1
l : List α
m : Nat
h : m < 0
⊢ (take 0 l)[m]? = l[m]?

Tactic:
exact absurd h (Nat.not_lt_of_le m.zero_le)

Result:
no goals

Proof state:
case succ.nil
α : Type u_1
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, m < n✝ → (take n✝ l)[m]? = l[m]?
m : Nat
h : m < n✝ + 1
⊢ (take (n✝ + 1) [])[m]? = [][m]?

Tactic:
simp only [take_nil]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem eq_zero_of_sameRay_self_neg [NoZeroSMulDivisors R M] (h : SameRay R x (-x)) : x = 0

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)

Tactic:
rwa [neg_one_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0

Tactic:
refine eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) ?_

Result:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
⊢ x = 0

Tactic:
nontriviality M

Result:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
⊢ x = 0

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
⊢ x = 0

Tactic:
haveI : Nontrivial R := Module.nontrivial R M

Result:
R : Type u_1
inst✝³ : StrictOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
a✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0
-- Mathlib/Data/Multiset/AddSub.lean
theorem add_cons (a : α) (s t : Multiset α) : s + a ::ₘ t = a ::ₘ (s + t)

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ s + a ::ₘ t = a ::ₘ (s + t)

Tactic:
rw [Multiset.add_comm, cons_add, Multiset.add_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Icc_sub_one_right_eq_Ico_of_not_isMin (hb : ¬ IsMin b) (a : α) : Icc a (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico_of_not_isMin hb a

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem exists_smul_eq (hH : Nat.Coprime (Nat.card H) H.index) (α β : H.QuotientDiff) :
    ∃ h : H, h • α = β :=
  Quotient.inductionOn' α
    (Quotient.inductionOn' β fun β α =>
      Exists.imp (fun _ => Quotient.sound')
        ⟨(powCoprime hH).symm (diff (MonoidHom.id H) β α),
          (diff_inv _ _ _).symm.trans
            (inv_eq_one.mpr
              ((smul_diff' β α ((powCoprime hH).symm (diff (MonoidHom.id H) β α))⁻¹).trans
                (by rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel])))⟩)

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ β✝ : H.QuotientDiff
β α : H.LeftTransversal
⊢ diff (MonoidHom.id ↥H) β α * ((powCoprime hH).symm (diff (MonoidHom.id ↥H) β α))⁻¹ ^ H.index = 1

Tactic:
rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem tendsto_const_mul_pow_nhds_iff {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) :
    Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Tactic:
simp [tendsto_const_mul_pow_nhds_iff', hc]

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem mul_and_mul_iff [Mul R] [IsScalarTower R R M] :
    IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Proof state:
case refine_1.intro
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
exact ⟨ba.of_mul, ab.of_mul⟩

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
rintro ⟨ha, hb⟩

Result:
case refine_2.intro
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Proof state:
case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rintro ⟨ab, ba⟩

Result:
case refine_1.intro
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Proof state:
case refine_2.intro
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean
lemma nnnorm_rpow (a : A) {r : ℝ} (hr : 0 < r) (ha : 0 ≤ a

Proof state:
case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

Tactic:
simpa

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
r : ℝ
hr : 0 < r
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a ^ r‖₊ = ‖a‖₊ ^ r

Tactic:
lift r to ℝ≥0 using hr.le

Result:
case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ ‖a ^ ↑r‖₊ = ‖a‖₊ ^ ↑r

Proof state:
case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

Tactic:
all_goals simpa

Result:
no goals

Proof state:
case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ ‖a ^ ↑r‖₊ = ‖a‖₊ ^ ↑r

Tactic:
rw [← nnrpow_eq_rpow, ← nnnorm_nnrpow a]

Result:
case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r

case intro
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : autoParam (0 ≤ a) _auto✝
r : ℝ≥0
hr : 0 < ↑r
⊢ 0 < r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂

Proof state:
α : Type u_1
l₁ l₂ l : List α
h : l <+ l₁ ++ l₂
a : α
⊢ l <+ l₁ ++ a :: l₂

Tactic:
rw [sublist_append_iff] at h

Result:
α : Type u_1
l₁ l₂ l : List α
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
a : α
⊢ l <+ l₁ ++ a :: l₂

Proof state:
case intro.intro.intro.intro
α : Type u_1
l₁ l₂ : List α
a : α
l₁' l₂' : List α
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₁ ++ a :: l₂

Tactic:
exact Sublist.append h₁ (h₂.cons a)

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l : List α
h : ∃ l₁_1 l₂_1, l = l₁_1 ++ l₂_1 ∧ l₁_1 <+ l₁ ∧ l₂_1 <+ l₂
a : α
⊢ l <+ l₁ ++ a :: l₂

Tactic:
obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h

Result:
case intro.intro.intro.intro
α : Type u_1
l₁ l₂ : List α
a : α
l₁' l₂' : List α
h₁ : l₁' <+ l₁
h₂ : l₂' <+ l₂
⊢ l₁' ++ l₂' <+ l₁ ++ a :: l₂