harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean
theorem op_adjoin (s : Set A) :
    (Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)

Tactic:
apply toSubsemiring_injective

Result:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Algebra.adjoin R s).op.toSubsemiring = (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)).toSubsemiring

Proof state:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ x ∈ MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ↔ x ∈ Set.range ⇑(algebraMap R Aᵐᵒᵖ)

Tactic:
simp_rw [Set.mem_preimage, Set.mem_range, MulOpposite.algebraMap_apply]

Result:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, MulOpposite.op ((algebraMap R A) y) = x

Proof state:
case a.e_s.e_a.h.a.h.e'_2.h.a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x✝ : R
⊢ (algebraMap R A) x✝ = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A) x✝) = x

Tactic:
rw [← MulOpposite.op_injective.eq_iff (b := x.unop), MulOpposite.op_unop]

Result:
no goals

Proof state:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subsemiring.closure (MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ∪ MulOpposite.unop ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)

Tactic:
congr with x

Result:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ x ∈ MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ↔ x ∈ Set.range ⇑(algebraMap R Aᵐᵒᵖ)

Proof state:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ (Algebra.adjoin R s).op.toSubsemiring = (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)).toSubsemiring

Tactic:
simp_rw [Algebra.adjoin, op_toSubsemiring, Subsemiring.op_closure, Set.preimage_union]

Result:
case a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subsemiring.closure (MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ∪ MulOpposite.unop ⁻¹' s) =
    Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)

Proof state:
case a.e_s.e_a.h
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
⊢ (∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, MulOpposite.op ((algebraMap R A) y) = x

Tactic:
congr!

Result:
case a.e_s.e_a.h.a.h.e'_2.h.a
R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x : Aᵐᵒᵖ
x✝ : R
⊢ (algebraMap R A) x✝ = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A) x✝) = x
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inr_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (m₁ m₂ : M) :
    (inr m₁ * inr m₂ : tsze R M) = 0 :=
  ext (mul_zero _) <|
    show (0 : R) •> m₂ + m₁ <• (0 : R) = 0 by rw [zero_smul, zero_add, op_zero, zero_smul]

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 •> m₂ + m₁ <• 0 = 0

Tactic:
rw [zero_smul, zero_add, op_zero, zero_smul]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iio_insert [DecidableEq α] (b : α) : insert b (Iio b) = Iic b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b

Tactic:
ext

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b

Tactic:
simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem tprod_eq_one_iff (hf : Multipliable f) : ∏' i, f i = 1 ↔ ∀ x, f x = 1

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

Tactic:
rw [← hasProd_one_iff, hf.hasProd_iff]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem tail_init_eq_init_tail {β : Sort*} (q : Fin (n + 2) → β) :
    tail (init q) = init (tail q)

Proof state:
case h
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
i : Fin n
⊢ tail (init q) i = init (tail q) i

Tactic:
simp [tail, init, castSucc_fin_succ]

Result:
no goals

Proof state:
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
⊢ tail (init q) = init (tail q)

Tactic:
ext i

Result:
case h
n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
i : Fin n
⊢ tail (init q) i = init (tail q) i
-- Mathlib/Analysis/Complex/TaylorSeries.lean
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball. -/
lemma taylorSeries_eq_on_ball' {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) :
    ∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Proof state:
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert taylorSeries_eq_on_ball hf hz using 3 with n

Result:
case h.e'_2.h.e'_5.h
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Proof state:
case h.e'_2.h.e'_5.h
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma iSup_add [Nonempty ι] (f : ι → ℕ∞) : (⨆ i, f i) + a = ⨆ i, f i + a

Proof state:
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + a

Tactic:
simp [add_comm, add_iSup]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_div_iff_comm : a / b = c / d ↔ b / a = d / c :=
  inv_inj.symm.trans <| by simp only [inv_div]

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b c d : α
⊢ (a / b)⁻¹ = (c / d)⁻¹ ↔ b / a = d / c

Tactic:
simp only [inv_div]

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem eq_toGHSpace_iff {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X]
    {p : NonemptyCompacts ℓ_infty_ℝ} :
    ⟦p⟧ = toGHSpace X ↔ ∃ Ψ : X → ℓ_infty_ℝ, Isometry Ψ ∧ range Ψ = p

Proof state:
case refine_1.intro
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p

Tactic:
use fun x => f x, isometry_subtype_coe.comp f.isometry

Result:
case right
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
h : IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ (range fun x => ↑(f x)) = ↑p

Proof state:
case refine_2.intro.intro
X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤)
Ψ : X → ↥(lp (fun n => ℝ) ⊤)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
E : (↑(range Ψ) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding X)) = (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))
⊢ IsometryRel.setoid p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
exact ⟨cast E f⟩

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem append_prod {i j k l} {w₁ : NeWord M i j} {hne : j ≠ k} {w₂ : NeWord M k l} :
    (append w₁ hne w₂).prod = w₁.prod * w₂.prod

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ (w₁.append hne w₂).prod = w₁.prod * w₂.prod

Tactic:
simp [toWord, prod, Word.prod]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem s_as_blocks : S l R = Matrix.fromBlocks 1 0 0 (-1)

Proof state:
l : Type u_4
R : Type u₂
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ S l R = fromBlocks 1 0 0 (-1)

Tactic:
rw [← Matrix.diagonal_one, Matrix.diagonal_neg, Matrix.fromBlocks_diagonal]

Result:
l : Type u_4
R : Type u₂
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ S l R = diagonal (Sum.elim (fun x => 1) fun i => -1)

Proof state:
l : Type u_4
R : Type u₂
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ S l R = diagonal (Sum.elim (fun x => 1) fun i => -1)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_map_snd (n) (l : Array α) : map Prod.snd (zipIdx l n) = range' n l.size

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ map Prod.snd ({ toList := toList✝ }.zipIdx n) = range' n { toList := toList✝ }.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Array α
⊢ map Prod.snd (l.zipIdx n) = range' n l.size

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ map Prod.snd ({ toList := toList✝ }.zipIdx n) = range' n { toList := toList✝ }.size
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem neg_apply [ContinuousNeg M] (x : M) :
    neg R x = -x

Proof state:
R : Type u_3
inst✝⁴ : Semiring R
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousNeg M
x : M
⊢ (neg R) x = -x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
@[simp]
lemma Away.val_mk {d : ι} (n : ℕ) (hf : f ∈ 𝒜 d) (x : A) (hx : x ∈ 𝒜 (n • d)) :
    (Away.mk 𝒜 hf n x hx).val = Localization.mk x ⟨f ^ n, by use n⟩ :=
  rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x✝¹ : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x✝ : A
hx✝ : x✝ = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
x : A
hx : x ∈ 𝒜 (n • d)
⊢ f ^ n ∈ Submonoid.powers f

Tactic:
use n

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_mul (x₁ x₂ : M) (y₁ y₂ : S) : f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂ :=
  (mul_inv_left f.map_units _ _ _).2 <|
    show _ = _ * (_ * _ * (_ * _)) by
      rw [← mul_assoc, ← mul_assoc, mul_inv_right f.map_units, mul_assoc, mul_assoc,
          mul_comm _ (f.toMap x₂), ← mul_assoc, ← mul_assoc, mul_inv_right f.map_units,
          Submonoid.coe_mul, f.toMap.map_mul, f.toMap.map_mul]
      ac_rfl

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.toMap (x₁ * x₂) =
    f.toMap ↑(y₁ * y₂) *
      (f.toMap x₁ * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y₁)⁻¹ *
        (f.toMap x₂ * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) y₂)⁻¹))

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_inv_right f.map_units, mul_assoc, mul_assoc,
    mul_comm _ (f.toMap x₂), ← mul_assoc, ← mul_assoc, mul_inv_right f.map_units,
    Submonoid.coe_mul, f.toMap.map_mul, f.toMap.map_mul]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.toMap x₁ * f.toMap x₂ * f.toMap ↑y₂ * f.toMap ↑y₁ = f.toMap ↑y₁ * f.toMap ↑y₂ * f.toMap x₁ * f.toMap x₂

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.toMap x₁ * f.toMap x₂ * f.toMap ↑y₂ * f.toMap ↑y₁ = f.toMap ↑y₁ * f.toMap ↑y₂ * f.toMap x₁ * f.toMap x₂

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_inv (hc : 0 < c) : IsBigOWith c⁻¹ l f g ↔ ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hc : 0 < c
⊢ IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
simp only [IsBigOWith_def, ← div_eq_inv_mul, le_div_iff₀' hc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_mul_C_of_leadingCoeff_mul_eq_one {b : R} (hp : p.leadingCoeff * b = 1) :
    Monic (p * C b)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ (p * C b).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (p * C b).Monic

Tactic:
unfold Monic

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (p * C b).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (p * C b).leadingCoeff = 1

Tactic:
nontriviality

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ (p * C b).leadingCoeff = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α}
    {v : β} : getValue k (insertEntry k v l) containsKey_insertEntry_self = v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
k : α
v : β
⊢ getValue k (insertEntry k v l) ⋯ = v

Tactic:
simp [getValue_insertEntry]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem sSup_apply {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {l : E →ₗ.[R] F}
    (hl : l ∈ c) (x : l.domain) :
    (LinearPMap.sSup c hc) ⟨x, (LinearPMap.le_sSup hc hl).1 x.2⟩ = l x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
l : E →ₗ.[R] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩ = ↑l x

Tactic:
symm

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
l : E →ₗ.[R] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑l x = ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
l : E →ₗ.[R] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑l x = ↑(LinearPMap.sSup c hc) ⟨↑x, ⋯⟩

Tactic:
apply (Classical.choose_spec (sSup_aux c hc) hl).2

Result:
case _h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
l : E →ₗ.[R] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑x = ↑⟨↑x, ⋯⟩

Proof state:
case _h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
c : Set (E →ₗ.[R] F)
hc : DirectedOn (fun x1 x2 => x1 ≤ x2) c
l : E →ₗ.[R] F
hl : l ∈ c
x : ↥l.domain
⊢ ↑x = ↑⟨↑x, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem sSup_atoms_le_eq (b : α) : sSup { a : α | IsAtom a ∧ a ≤ b } = b

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
b : α
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b

Tactic:
rcases eq_sSup_atoms b with ⟨s, rfl, hs⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ a ∈ s, IsAtom a
⊢ sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ a ∈ s, IsAtom a
⊢ sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s

Tactic:
exact le_antisymm (sSup_le fun _ => And.right) (sSup_le_sSup fun a ha => ⟨hs a ha, le_sSup ha⟩)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Monotone.measure_iInter [Preorder ι] [IsDirected ι (· ≥ ·)]
    [(atBot : Filter ι).IsCountablyGenerated] {s : ι → Set α} (hs : Monotone s)
    (hsm : ∀ i, NullMeasurableSet (s i) μ) (hfin : ∃ i, μ (s i) ≠ ∞) :
    μ (⋂ i, s i) = ⨅ i, μ (s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)

Tactic:
rcases exists_seq_antitone_tendsto_atTop_atBot ι with ⟨x, hxm, hx⟩

Result:
case intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem iteratedPDeriv_succ_right {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E, F)) :
    iteratedPDeriv 𝕜 m f = iteratedPDeriv 𝕜 (Fin.init m) (pderivCLM 𝕜 (m (Fin.last n)) f)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.init (Fin.tail m))) ((pderivCLM 𝕜 (Fin.tail m (Fin.last n))) f)) =
    (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Tactic:
simp only [hmtail, iteratedPDeriv_succ_left, hmzero, Fin.tail_init_eq_init_tail]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
IH :
  ∀ (m : Fin (n + 1) → E), (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last n))) f)
m : Fin (n + 1 + 1) → E
hmzero : Fin.init m 0 = m 0
hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ)
⊢ (iteratedPDeriv 𝕜 m) f = (iteratedPDeriv 𝕜 (Fin.init m)) ((pderivCLM 𝕜 (m (Fin.last (n + 1)))) f)

Tactic:
calc
  _ = pderivCLM 𝕜 (m 0) (iteratedPDeriv 𝕜 _ f) := iteratedPDeriv_succ_left _ _ _
  _ = pderivCLM 𝕜 (m 0) ((iteratedPDeriv 𝕜 _) ((pderivCLM 𝕜 _) f)) := by
    congr 1
    exact IH _
  _ = _ := by
    simp only [hmtail, iteratedPDeriv_succ_left, hmzero, Fin.tail_init_eq_init_tail]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_mul {m n : ℕ} (hmn : m.Coprime n) :
    Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ (∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n

Tactic:
refine forall₂_congr fun p hp => ?_

Result:
m n : ℕ
hmn : m.Coprime n
p : ℕ
hp : Prime p
⊢ ¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n

Tactic:
simp only [squarefree_iff_prime_squarefree, ← sq, ← forall_and]

Result:
m n : ℕ
hmn : m.Coprime n
⊢ (∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n

Proof state:
m n : ℕ
hmn : m.Coprime n
p : ℕ
hp : Prime p
⊢ ¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n

Tactic:
simp only [hmn.isPrimePow_dvd_mul (hp.isPrimePow.pow two_ne_zero), not_or]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivative_X : d⁄dX R (X : R⟦X⟧) = 1

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (coeff R n✝) ((d⁄dX R) X) = (coeff R n✝) 1

Tactic:
rw [coeff_derivative, coeff_one, coeff_X, boole_mul]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (if n✝ + 1 = 1 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (if n✝ = 0 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
h : n✝ = 0
⊢ ↑n✝ + 1 = 1

case neg
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
h : ¬n✝ = 0
⊢ 0 = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
h : n✝ = 0
⊢ ↑n✝ + 1 = 1

Tactic:
rw [h, cast_zero, zero_add]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (if n✝ + 1 = 1 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0

Tactic:
simp_rw [add_left_eq_self]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (if n✝ = 0 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0

Proof state:
case neg
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
h : ¬n✝ = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (d⁄dX R) X = 1

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
⊢ (coeff R n✝) ((d⁄dX R) X) = (coeff R n✝) 1