harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_add [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α]
    (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (c + x)) = ∏ x ∈ Ico (a + c) (b + c), f x

Proof state:
case h.e'_2.a
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (c + x) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
convert prod_Ico_add' f a b c using 2

Result:
case h.e'_2.a
α : Type u_1
M : Type u_2
inst✝³ : CommMonoid M
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)
-- Mathlib/Algebra/Ring/Parity.lean
lemma two_mul_div_two_add_one_of_odd (h : Odd n) : 2 * (n / 2) + 1 = n

Proof state:
n : ℕ
h : Odd n
⊢ 2 * (n / 2) + 1 = n

Tactic:
rw [← odd_iff.mp h, div_add_mod]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem IsIntegral.minpoly_splits_tower_top [Algebra K L] [Algebra R L] [IsScalarTower R K L]
    (int : IsIntegral R x) (h : Splits (algebraMap R L) (minpoly R x)) :
    Splits (algebraMap K L) (minpoly K x)

Proof state:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : Splits (algebraMap R L) (minpoly R x)
⊢ Splits (algebraMap K L) (minpoly K x)

Tactic:
rw [IsScalarTower.algebraMap_eq R K L] at h

Result:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : Splits ((algebraMap K L).comp (algebraMap R K)) (minpoly R x)
⊢ Splits (algebraMap K L) (minpoly K x)

Proof state:
R : Type u_1
K : Type u_2
L : Type u_3
M : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : CommRing M
inst✝⁶ : Algebra R K
inst✝⁵ : Algebra R M
inst✝⁴ : Algebra K M
inst✝³ : IsScalarTower R K M
x : M
inst✝² : Algebra K L
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
int : IsIntegral R x
h : Splits ((algebraMap K L).comp (algebraMap R K)) (minpoly R x)
⊢ Splits (algebraMap K L) (minpoly K x)

Tactic:
exact int.minpoly_splits_tower_top' h

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_isClosed (s : Set E) : IsClosed (X := WeakBilin B.flip) (B.polar s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (B.polar s)

Tactic:
rw [polar_eq_biInter_preimage]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1)

Tactic:
exact isClosed_biInter
  fun _ _ ↦ Metric.isClosed_closedBall.preimage (WeakBilin.eval_continuous B.flip _)

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih₁₂ (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₁ x₂ y

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ IH24 x₁ x₂ y

Tactic:
rw [IH24]

Result:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)

Proof state:
case refine_3
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption y
⊢ CutExpand IsOption (Args.P24 x₁ x₂ z).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Tactic:
exact (cutExpand_add_left {x₁}).2 (cutExpand_pair_right h)

Result:
no goals

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ ∀ ⦃z : PGame⦄, (z.IsOption x₁ → P24 z x₂ y) ∧ (z.IsOption x₂ → P24 x₁ z y) ∧ (z.IsOption y → P24 x₁ x₂ z)

Tactic:
refine fun z ↦ ⟨?_, ?_, ?_⟩ <;>
  refine fun h ↦ ih' (Args.P24 _ _ _) (TransGen.single ?_)

Result:
case refine_1
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption x₁
⊢ CutExpand IsOption (Args.P24 z x₂ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption x₂
⊢ CutExpand IsOption (Args.P24 x₁ z y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

case refine_3
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption y
⊢ CutExpand IsOption (Args.P24 x₁ x₂ z).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Proof state:
case refine_2
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption x₂
⊢ CutExpand IsOption (Args.P24 x₁ z y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Tactic:
exact (cutExpand_add_left {x₁}).2 (cutExpand_pair_left h)

Result:
no goals

Proof state:
case refine_1
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
z : PGame
h : z.IsOption x₁
⊢ CutExpand IsOption (Args.P24 z x₂ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Tactic:
exact (cutExpand_add_right {y}).2 (cutExpand_pair_left h)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_def {o : ONote} {x} (e : fundamentalSequence o = x) :
    fastGrowing o =
      match
        (motive := (x : Option ONote ⊕ (ℕ → ONote)) → FundamentalSequenceProp o x → ℕ → ℕ)
        x, e ▸ fundamentalSequence_has_prop o with
      | Sum.inl none, _ => Nat.succ
      | Sum.inl (some a), _ =>
        fun i => (fastGrowing a)^[i] i
      | Sum.inr f, _ => fun i =>
        fastGrowing (f i) i

Proof state:
o : ONote
x : Option ONote ⊕ (ℕ → ONote)
e : o.fundamentalSequence = x
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) x, ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
    | Sum.inr f, x => fun i => (f i).fastGrowing i

Tactic:
subst x

Result:
o : ONote
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
    | Sum.inr f, x => fun i => (f i).fastGrowing i

Proof state:
o : ONote
⊢ o.fastGrowing =
    match (motive := (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → ℕ → ℕ) o.fundamentalSequence,
      ⋯ with
    | Sum.inl none, x => Nat.succ
    | Sum.inl (some a), x => fun i => a.fastGrowing^[i] i
    | Sum.inr f, x => fun i => (f i).fastGrowing i

Tactic:
rw [fastGrowing]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem single_lt_prod' {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j)
    (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < ∏ k ∈ s, f k :=
  calc
    f i = ∏ k ∈ {i}, f k

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
f : ι → M
s : Finset ι
i j : ι
hij : j ≠ i
hi : i ∈ s
hj : j ∈ s
hlt : 1 < f j
hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k
⊢ f i = ∏ k ∈ {i}, f k

Tactic:
rw [prod_singleton]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
lemma IsAtomic.realize_comp_of_injective {φ : L.BoundedFormula α n} (hA : φ.IsAtomic)
    [L.HomClass F M N] {f : F} (hInj : Function.Injective f) {v : α → M} {xs : Fin n → M} :
    φ.Realize v xs → φ.Realize (f ∘ v) (f ∘ xs)

Proof state:
case rel
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (RelMap R fun i => Term.realize (Sum.elim v xs) (ts i)) → RelMap R fun i => f (Term.realize (Sum.elim v xs) (ts i))

Tactic:
exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → φ.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
induction hA with
| equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
  imp_self]
| rel R ts =>
  simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
  exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))

Result:
no goals

Proof state:
case equal
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
t₁ t₂ : L.Term (α ⊕ Fin n)
⊢ (t₁ =' t₂).Realize v xs → (t₁ =' t₂).Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
imp_self]

Result:
no goals

Proof state:
case rel
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (R.boundedFormula ts).Realize v xs → (R.boundedFormula ts).Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]

Result:
case rel
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝³ : L.Structure M
N : Type u_2
inst✝² : L.Structure N
F : Type u_3
inst✝¹ : FunLike F M N
φ : L.BoundedFormula α n
inst✝ : L.HomClass F M N
f : F
hInj : Function.Injective ⇑f
v : α → M
xs : Fin n → M
l✝ : ℕ
R : L.Relations l✝
ts : Fin l✝ → L.Term (α ⊕ Fin n)
⊢ (RelMap R fun i => Term.realize (Sum.elim v xs) (ts i)) → RelMap R fun i => f (Term.realize (Sum.elim v xs) (ts i))
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem fderiv_inv : fderiv 𝕜 (fun x => x⁻¹) x = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (-(x ^ 2)⁻¹)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ fderiv 𝕜 (fun x => x⁻¹) x = smulRight 1 (-(x ^ 2)⁻¹)

Tactic:
rw [← deriv_fderiv, deriv_inv]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ioo_left [NoMinOrder α] (b : α) : ⋃ a, Ioo a b = Iio b

Proof state:
α : Type v
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
b : α
⊢ ⋃ a, Ioo a b = Iio b

Tactic:
simp only [← Ioi_inter_Iio, ← iUnion_inter, iUnion_Ioi, univ_inter]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Tendsto.const_mul {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞}
    (hm : Tendsto m f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ∞) : Tendsto (fun b => a * m b) f (𝓝 (a * b)) :=
  by_cases (fun (this : a = 0) => by simp [this, tendsto_const_nhds]) fun ha : a ≠ 0 =>
    ENNReal.Tendsto.mul tendsto_const_nhds (Or.inl ha) hm hb

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 b)
hb : b ≠ 0 ∨ a ≠ ⊤
this : a = 0
⊢ Tendsto (fun b => a * m b) f (𝓝 (a * b))

Tactic:
simp [this, tendsto_const_nhds]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem integrable_iff_integrableAtFilter_cocompact :
    Integrable f μ ↔ (IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ)

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ Integrable f μ

Tactic:
rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ

Tactic:
refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩

Result:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
⊢ Integrable f μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
⊢ Integrable f μ

Tactic:
obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ Integrable f μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
s : Set X
hsc : s ∈ cocompact X
hs : IntegrableOn f s μ
hloc : LocallyIntegrable f μ
t : Set X
htc : IsCompact t
ht : sᶜ ⊆ t
⊢ IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ

Tactic:
exact ⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_concat_iff {l₁ l₂ : List α} {a : α} :
    l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ l₁ <+: l₂ ++ [a] ↔ l₁ = l₂ ++ [a] ∨ l₁ <+: l₂

Tactic:
simp only [← reverse_suffix, reverse_concat, suffix_cons_iff]

Result:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ l₁.reverse = a :: l₂.reverse ∨ l₁.reverse <:+ l₂.reverse ↔ l₁ = l₂ ++ [a] ∨ l₁.reverse <:+ l₂.reverse

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ l₁.reverse = a :: l₂.reverse ∨ l₁.reverse <:+ l₂.reverse ↔ l₁ = l₂ ++ [a] ∨ l₁.reverse <:+ l₂.reverse

Tactic:
simp only [concat_eq_append, ← reverse_concat, reverse_eq_iff, reverse_reverse]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for
stronger assumptions on `B`. -/
@[simp]
lemma ker_aeval_eq_span_minpoly :
    RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x

Proof state:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
⊢ RingHom.ker (Polynomial.aeval x) = Submodule.span A[X] {minpoly A x}

Tactic:
ext p

Result:
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval x) ↔ p ∈ Submodule.span A[X] {minpoly A x}

Proof state:
case h
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval x) ↔ p ∈ Submodule.span A[X] {minpoly A x}

Tactic:
simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
  dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isLeftDescent_iff_not_isLeftDescent_mul {w : W} {i : B} :
    cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (s i * w) i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1

Tactic:
tauto

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i

Tactic:
rw [isLeftDescent_iff, not_isLeftDescent_iff, simple_mul_simple_cancel_left]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_closedBall (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
    c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

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

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)

Tactic:
simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
exact smul_closedBall' hc x r

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma le_induce_union : G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')

Proof state:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts

Tactic:
simp only [verts_sup, induce_verts, Set.Subset.rfl]

Result:
no goals

Proof state:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄,
    v ∈ s ∧ w ∈ s ∧ G'.Adj v w ∨ v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w → (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Tactic:
rintro v w (h | h) <;> simp [h]

Result:
no goals

Proof state:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w

Tactic:
simp only [sup_adj, induce_adj, Set.mem_union]

Result:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄,
    v ∈ s ∧ w ∈ s ∧ G'.Adj v w ∨ v ∈ s' ∧ w ∈ s' ∧ G'.Adj v w → (v ∈ s ∨ v ∈ s') ∧ (w ∈ s ∨ w ∈ s') ∧ G'.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')

Tactic:
constructor

Result:
case left
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.induce s ⊔ G'.induce s').verts ⊆ (G'.induce (s ∪ s')).verts

case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ ∀ ⦃v w : V⦄, (G'.induce s ⊔ G'.induce s').Adj v w → (G'.induce (s ∪ s')).Adj v w
-- Mathlib/ModelTheory/DirectLimit.lean
theorem Equiv_isup_symm_inclusion_apply {i : ι} (x : S i) :
    (Equiv_iSup S).symm (Substructure.inclusion (le_iSup _ _) x)
    = of L ι _ (fun _ _ h ↦ Substructure.inclusion (S.monotone h)) i x

Proof state:
case a
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Equiv_iSup S) ((Equiv_iSup S).symm ((Substructure.inclusion ⋯) x)) =
    (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)

Tactic:
simp only [Equiv.apply_symm_apply]

Result:
case a
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Substructure.inclusion ⋯) x =
    (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)

Proof state:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Equiv_iSup S).symm ((Substructure.inclusion ⋯) x) =
    (of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x

Tactic:
apply (Equiv_iSup S).injective

Result:
case a
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Equiv_iSup S) ((Equiv_iSup S).symm ((Substructure.inclusion ⋯) x)) =
    (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)

Proof state:
case a
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
i : ι
x : ↥(S i)
⊢ (Substructure.inclusion ⋯) x =
    (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem trans_induction_on {P : ∀ {a b : α}, TransGen r a b → Prop} {a b : α} (h : TransGen r a b)
    (base : ∀ {a b} (h : r a b), P (single h))
    (ih : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) :
    P h

Proof state:
α : Type u_1
r : α → α → Prop
P : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
base : ∀ {a b : α} (h : r a b), P ⋯
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P ⋯
⊢ P h

Tactic:
induction h with
| single h => exact base h
| tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P ⋯
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P ⋯
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : P hab
⊢ P ⋯

Tactic:
exact ih hab (single hbc) h_ih (base hbc)

Result:
no goals

Proof state:
case single
α : Type u_1
r : α → α → Prop
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P ⋯
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P ⋯
b✝ : α
h : r a b✝
⊢ P ⋯

Tactic:
exact base h

Result:
no goals
-- Mathlib/Order/Part.lean
lemma Antitone.partSeq (hf : Antitone f) (hg : Antitone g) : Antitone fun x ↦ f x <*> g x

Proof state:
α : Type u_1
inst✝ : Preorder α
β γ : Type u_4
f : α → Part (β → γ)
g : α → Part β
hf : Antitone f
hg : Antitone g
⊢ Antitone fun x => f x <*> g x

Tactic:
simpa only [seq_eq_bind_map] using hf.partBind <| Antitone.of_apply₂ fun _ ↦ hg.partMap

Result:
no goals