harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem _root_.Set.smul_mem_centralizer {s : Set A} (r : R) {a : A} (ha : a ∈ s.centralizer) :
    r • a ∈ s.centralizer :=
  fun x hx => by rw [mul_smul_comm, smul_mul_assoc, ha x hx]

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
⊢ x * r • a = r • a * x

Tactic:
rw [mul_smul_comm, smul_mul_assoc, ha x hx]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
@[to_additive existing (attr := simp) pow_addLeft]
lemma pow_mulLeft (n : ℕ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

Proof state:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

Tactic:
ext

Result:
case H
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝

Proof state:
case H
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝

Tactic:
simp [Perm.coe_pow]

Result:
no goals
-- Mathlib/Topology/Basic.lean
lemma nhdsWithin_neBot : (𝓝[s] x).NeBot ↔ ∀ ⦃t⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
rw [nhdsWithin, inf_neBot_iff]

Result:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
exact forall₂_congr fun U _ ↦
  ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).reverse = p.reverse.copy hv hu

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).reverse = p.reverse.copy hv hu

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).reverse = p.reverse.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_le_pow_iff_mem_span_pow (x : ℤ_[p]) (n : ℕ) :
    ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p])

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n

Tactic:
exact mod_cast Nat.zero_le _

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
subst hx

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖0‖ ≤ ↑p ^ (-↑n) ↔ 0 ∈ Ideal.span {↑p ^ n}

Tactic:
simp only [norm_zero, zpow_neg, zpow_natCast, inv_nonneg, iff_true, Submodule.zero_mem]

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ ↑p ^ n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
by_cases hx : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_real :
    a.toBasis.det b = 1 ∨ a.toBasis.det b = -1

Proof state:
ι : Type u_1
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ a.toBasis.det ⇑b ^ 2 = 1

Tactic:
simpa [unitary, sq] using Matrix.det_of_mem_unitary (a.toMatrix_orthonormalBasis_mem_unitary b)

Result:
no goals

Proof state:
ι : Type u_1
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1

Tactic:
rw [← sq_eq_one_iff]

Result:
ι : Type u_1
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι ℝ F
⊢ a.toBasis.det ⇑b ^ 2 = 1
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
    preserves finite products. -/
lemma preservesProduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesLimit (Discrete.functor f) F where
  preserves hc :=
    ⟨IsLimit.ofIsoLimit
        ((IsLimit.postcomposeInvEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
          (isBilimitOfPreserves F (biconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
      Cones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Proof state:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
as✝ : J
⊢ ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
      { as := as✝ } =
    (Iso.refl
          ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
      (F.mapCone c✝).π.app { as := as✝ }

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
⊢ ∀ (j : Discrete J),
    ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
        j =
      (Iso.refl
            ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
                (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
        (F.mapCone c✝).π.app j

Tactic:
rintro ⟨⟩

Result:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
as✝ : J
⊢ ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
      { as := as✝ } =
    (Iso.refl
          ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
      (F.mapCone c✝).π.app { as := as✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_append {p : ι → Prop} (f : ∀ a : ι, p a → α) (l₁ l₂ : List ι)
    (h : ∀ a ∈ l₁ ++ l₂, p a) :
    (l₁ ++ l₂).pmap f h =
      (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
        l₂.pmap f fun a ha => h a (mem_append_right l₁ ha)

Proof state:
case cons
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : List ι
head✝ : ι
tail✝ : List ι
ih : ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a), pmap f (tail✝ ++ l₂) h = pmap f tail✝ ⋯ ++ pmap f l₂ ⋯
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ pmap f (head✝ :: tail✝ ++ l₂) h = pmap f (head✝ :: tail✝) ⋯ ++ pmap f l₂ ⋯

Tactic:
dsimp only [pmap, cons_append]

Result:
case cons
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : List ι
head✝ : ι
tail✝ : List ι
ih : ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a), pmap f (tail✝ ++ l₂) h = pmap f tail✝ ⋯ ++ pmap f l₂ ⋯
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ f head✝ ⋯ :: pmap f (tail✝ ++ l₂) ⋯ = f head✝ ⋯ :: (pmap f tail✝ ⋯ ++ pmap f l₂ ⋯)

Proof state:
case cons
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : List ι
head✝ : ι
tail✝ : List ι
ih : ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a), pmap f (tail✝ ++ l₂) h = pmap f tail✝ ⋯ ++ pmap f l₂ ⋯
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ f head✝ ⋯ :: pmap f (tail✝ ++ l₂) ⋯ = f head✝ ⋯ :: (pmap f tail✝ ⋯ ++ pmap f l₂ ⋯)

Tactic:
rw [ih]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
⊢ pmap f (l₁ ++ l₂) h = pmap f l₁ ⋯ ++ pmap f l₂ ⋯

Tactic:
induction l₁ with
| nil => rfl
| cons _ _ ih =>
  dsimp only [pmap, cons_append]
  rw [ih]

Result:
no goals

Proof state:
case nil
ι : Type u_1
α : Type u_2
p : ι → Prop
f : (a : ι) → p a → α
l₂ : List ι
h : ∀ (a : ι), a ∈ [] ++ l₂ → p a
⊢ pmap f ([] ++ l₂) h = pmap f [] ⋯ ++ pmap f l₂ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem map_uniformity_set_coe {s : Set α} [UniformSpace α] :
    map (Prod.map (↑) (↑)) (𝓤 s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Proof state:
α : Type ua
s : Set α
inst✝ : UniformSpace α
⊢ map (Prod.map Subtype.val Subtype.val) (𝓤 ↑s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Tactic:
rw [uniformity_setCoe, map_comap, range_prod_map, Subtype.range_val]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_mul_X_pow (p : R[X]) (n : ℕ) : reverse (p * X ^ n) = reverse p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X ^ n).reverse = p.reverse

Tactic:
induction n with
| zero => simp
| succ n ih => rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (p * X ^ 0).reverse = p.reverse

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ (p * X ^ (n + 1)).reverse = p.reverse

Tactic:
rw [pow_succ, ← mul_assoc, reverse_mul_X, ih]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.Coprime m n

Proof state:
m n : ℕ
⊢ IsCoprime ↑m ↑n ↔ m.Coprime n

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem mk' (h_meas : NullMeasurableSet s μ) (h_exists : ∀ x : α, ∃! g : G, g • x ∈ s) :
    IsFundamentalDomain G s μ where
  nullMeasurableSet := h_meas
  ae_covers := Eventually.of_forall fun x => (h_exists x).exists
  aedisjoint a b hab := Disjoint.aedisjoint <| disjoint_left.2 fun x hxa hxb => by
    rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
    exact hab (inv_injective <| (h_exists x).unique hxa hxb)

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : x ∈ (fun g => g • s) a
hxb : x ∈ (fun g => g • s) b
⊢ False

Tactic:
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb

Result:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False

Tactic:
exact hab (inv_injective <| (h_exists x).unique hxa hxb)

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem card_nthRoots_one {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
    Multiset.card (nthRoots n (1 : R)) = n

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (nthRoots n 1).card = n

Tactic:
rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma pairing_smul_root_eq (k : ι) (hij : P.reflection_perm i = P.reflection_perm j) :
    P.pairing k i • P.root i = P.pairing k j • P.root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
h : (P.reflection i) (P.root k) = (P.reflection j) (P.root k)
⊢ P.pairing k i • P.root i = P.pairing k j • P.root j

Tactic:
simpa only [reflection_apply_root, sub_right_inj] using h

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
⊢ (P.reflection i) (P.root k) = (P.reflection j) (P.root k)

Tactic:
simp only [← root_reflection_perm, hij]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
⊢ P.pairing k i • P.root i = P.pairing k j • P.root j

Tactic:
have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by
  simp only [← root_reflection_perm, hij]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
h : (P.reflection i) (P.root k) = (P.reflection j) (P.root k)
⊢ P.pairing k i • P.root i = P.pairing k j • P.root j
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem contractNth_apply_of_eq (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (h : (k : ℕ) = j) : contractNth j op g k = op (g (Fin.castSucc k)) (g k.succ)

Proof state:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)

Result:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Proof state:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
h : ↑k = ↑j
this : ¬↑k < ↑j
⊢ j.contractNth op g k = op (g k.castSucc) (g k.succ)

Tactic:
rw [contractNth, if_neg this, if_pos h]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem IsClosedMap.mapClusterPt_iff_lift'_closure
    {F : Filter X} (f_closed : IsClosedMap f) (f_cont : Continuous f) {y : Y} :
    MapClusterPt y F f ↔ ((F.lift' closure) ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous f
y : Y
⊢ MapClusterPt y F f ↔ (F.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
rw [MapClusterPt, clusterPt_iff_lift'_closure', f_closed.lift'_closure_map_eq f_cont,
    ← comap_principal, ← map_neBot_iff f, Filter.push_pull, principal_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
lemma IsInvertedBy.map_iff {C₁ C₂ C₃ : Type*} [Category C₁] [Category C₂] [Category C₃]
    (W : MorphismProperty C₁) (F : C₁ ⥤ C₂) (G : C₂ ⥤ C₃) :
    (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{u_4, u_1} C₁
inst✝¹ : Category.{u_5, u_2} C₂
inst✝ : Category.{u_6, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
⊢ (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G)

Tactic:
simp only [IsInvertedBy.iff_map_le_isomorphisms, map_map]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.sum (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) :
    IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g

Proof state:
case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith (C i + ∑ i ∈ s, C i) l (fun x => A i x + ∑ i ∈ s, A i x) g

Tactic:
exact h.1.add (IH h.2)

Result:
no goals

Proof state:
case empty
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ ∅, C i) l (fun x => ∑ i ∈ ∅, A i x) g

Tactic:
simp only [isBigOWith_zero', Finset.sum_empty, forall_true_iff]

Result:
no goals

Proof state:
case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g
h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g
⊢ IsBigOWith (∑ i ∈ Finset.cons i s is, C i) l (fun x => ∑ i ∈ Finset.cons i s is, A i x) g

Tactic:
simp only [is, Finset.sum_cons, Finset.forall_mem_cons] at h ⊢

Result:
case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g
h : IsBigOWith (C i) l (A i) g ∧ ∀ x ∈ s, IsBigOWith (C x) l (A x) g
⊢ IsBigOWith (C i + ∑ i ∈ s, C i) l (fun x => A i x + ∑ i ∈ s, A i x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g

Tactic:
induction s using Finset.cons_induction with
| empty => simp only [isBigOWith_zero', Finset.sum_empty, forall_true_iff]
| cons i s is IH =>
  simp only [is, Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
  exact h.1.add (IH h.2)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
/-- See also `EReal.sub_lt_of_lt_add`. -/
lemma sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) : a - b < c :=
  sub_lt_of_lt_add <| by rwa [add_comm]

Proof state:
a b c : EReal
h : a < b + c
⊢ a < c + b

Tactic:
rwa [add_comm]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem idxOf_append_of_not_mem {a : α} (h : a ∉ l₁) :
    idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Proof state:
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : ¬a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Tactic:
induction' l₁ with d₁ t₁ ih

Result:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : ¬a ∈ []
⊢ idxOf a ([] ++ l₂) = [].length + idxOf a l₂

case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : ¬a ∈ t₁ → idxOf a (t₁ ++ l₂) = t₁.length + idxOf a l₂
h : ¬a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: t₁ ++ l₂) = (d₁ :: t₁).length + idxOf a l₂

Proof state:
case nil
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : ¬a ∈ []
⊢ idxOf a ([] ++ l₂) = [].length + idxOf a l₂

Tactic:
rw [List.nil_append, List.length, Nat.zero_add]

Result:
no goals

Proof state:
case cons
α : Type u
l₁ l₂ : List α
inst✝ : DecidableEq α
a d₁ : α
t₁ : List α
ih : ¬a ∈ t₁ → idxOf a (t₁ ++ l₂) = t₁.length + idxOf a l₂
h : ¬a ∈ d₁ :: t₁
⊢ idxOf a (d₁ :: t₁ ++ l₂) = (d₁ :: t₁).length + idxOf a l₂

Tactic:
rw [List.cons_append, idxOf_cons_ne _ (ne_of_not_mem_cons h).symm, List.length,
  ih (not_mem_of_not_mem_cons h), Nat.succ_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem natDegree_mul_mirror : (p * p.mirror).natDegree = 2 * p.natDegree

Proof state:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
rw [hp, zero_mul, natDegree_zero, mul_zero]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem image_mul_left' : (a⁻¹ * ·) '' t = (a * ·) ⁻¹' t

Proof state:
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x => a⁻¹ * x) '' t = (fun x => a * x) ⁻¹' t

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConvexOn.pow (hf : ConvexOn 𝕜 s f) (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) :
    ∀ n, ConvexOn 𝕜 s (f ^ n)
  | 0 => by simpa using convexOn_const 1 hf.1
  | n + 1 => by
    rw [pow_succ']
    exact hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <|
      (monovaryOn_self f s).pow_right₀ hf₀ n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : LinearOrderedCommRing 𝕜
inst✝⁴ : LinearOrderedCommRing E
inst✝³ : Module 𝕜 E
s : Set 𝕜
inst✝² : OrderedSMul 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : 𝕜 → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f * f ^ n)

Tactic:
exact hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <|
  (monovaryOn_self f s).pow_right₀ hf₀ n

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : LinearOrderedCommRing 𝕜
inst✝⁴ : LinearOrderedCommRing E
inst✝³ : Module 𝕜 E
s : Set 𝕜
inst✝² : OrderedSMul 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : 𝕜 → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
⊢ ConvexOn 𝕜 s (f ^ 0)

Tactic:
simpa using convexOn_const 1 hf.1

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : LinearOrderedCommRing 𝕜
inst✝⁴ : LinearOrderedCommRing E
inst✝³ : Module 𝕜 E
s : Set 𝕜
inst✝² : OrderedSMul 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : 𝕜 → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f ^ (n + 1))

Tactic:
rw [pow_succ']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : LinearOrderedCommRing 𝕜
inst✝⁴ : LinearOrderedCommRing E
inst✝³ : Module 𝕜 E
s : Set 𝕜
inst✝² : OrderedSMul 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : 𝕜 → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f * f ^ n)