harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Support.lean
theorem ne_and_ne_of_swap_mul_apply_ne_self {f : Perm α} {x y : α} (hy : (swap x (f x) * f) y ≠ y) :
    f y ≠ y ∧ y ≠ x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (swap x (f x) * f) y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *

Result:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
by_cases h : f y = x

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : f y = x
⊢ f y ≠ y ∧ y ≠ x

case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : ¬f y = x
⊢ f y ≠ y ∧ y ≠ x

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : f y = x
⊢ f y ≠ y ∧ y ≠ x

Tactic:
constructor <;> intro <;> simp_all only [if_true, eq_self_iff_true, not_true, Ne]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
h : ¬f y = x
⊢ f y ≠ y ∧ y ≠ x

Tactic:
split_ifs at hy with h <;> try { simp [*] at * }

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
h✝ : ¬f y = x
h : ¬y = x
hy : f y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
simp [*] at *

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma product_pow [Monoid β] (s : Finset α) (t : Finset β) : ∀ n, (s ×ˢ t) ^ n = (s ^ n) ×ˢ (t ^ n)
  | 0 => by simp
  | n + 1 => by simp [pow_succ, product_pow _ _ n]

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ s ×ˢ t ^ 0 = (s ^ 0) ×ˢ (t ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Finset α
t : Finset β
n : ℕ
⊢ s ×ˢ t ^ (n + 1) = (s ^ (n + 1)) ×ˢ (t ^ (n + 1))

Tactic:
simp [pow_succ, product_pow _ _ n]

Result:
no goals
-- Mathlib/Data/Matrix/DMatrix.lean
theorem map_add [∀ i j, AddMonoid (α i j)] {β : m → n → Type w} [∀ i j, AddMonoid (β i j)]
    (f : ∀ ⦃i j⦄, α i j →+ β i j) (M N : DMatrix m n α) :
    ((M + N).map fun i j => @f i j) = (M.map fun i j => @f i j) + N.map fun i j => @f i j

Proof state:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M + N).map (fun i j => ⇑f) i✝ j✝ = ((M.map fun i j => ⇑f) + N.map fun i j => ⇑f) i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M + N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) + N.map fun i j => ⇑f

Tactic:
ext

Result:
case a
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M + N).map (fun i j => ⇑f) i✝ j✝ = ((M.map fun i j => ⇑f) + N.map fun i j => ⇑f) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffix_replicate_iff {n} {a : α} {l : List α} :
    l <:+ List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l.reverse.length ≤ n ∧ l.reverse = replicate l.reverse.length a ↔ l.length ≤ n ∧ l = replicate l.length a

Tactic:
simp [reverse_eq_iff]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l <:+ replicate n a ↔ l.length ≤ n ∧ l = replicate l.length a

Tactic:
rw [← reverse_prefix, reverse_replicate, isPrefix_replicate_iff]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l.reverse.length ≤ n ∧ l.reverse = replicate l.reverse.length a ↔ l.length ≤ n ∧ l = replicate l.length a
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_indep_chart [HasGroupoid M G] [HasGroupoid M' G']
    (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source) (hf : f ∈ G'.maximalAtlas M')
    (xf : g x ∈ f.source) :
    LiftPropWithinAt P g s x ↔
    ContinuousWithinAt g s x ∧ P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
⊢ ContinuousWithinAt g s x ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
exact and_congr_right <|
  hG.liftPropWithinAt_indep_chart_aux (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) he xe
    (chart_mem_maximalAtlas _ _) (mem_chart_source _ _) hf xf

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
⊢ LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
simp only [liftPropWithinAt_iff']

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : PartialHomeomorph M H
f : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
inst✝¹ : HasGroupoid M G
inst✝ : HasGroupoid M' G'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
⊢ ContinuousWithinAt g s x ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_le_iff : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

Tactic:
rw [abs_le, neg_le_sub_iff_le_add, sub_le_iff_le_add', and_comm, sub_le_iff_le_add']

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
lemma IsPointwiseRightKanExtensionAt.isIso_hom_app
    {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
    IsIso (E.hom.app X)

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
X : C
h : E.IsPointwiseRightKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso (E.hom.app X)

Tactic:
simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem isSome_symm_get (f : α ≃. β) {a : α} (h : isSome (f a)) :
    isSome (f.symm (Option.get _ h)) :=
  isSome_iff_exists.2 ⟨a, by rw [f.eq_some_iff, some_get]⟩

Proof state:
α : Type u
β : Type v
f : α ≃. β
a : α
h : (f a).isSome = true
⊢ f.symm ((f a).get h) = some a

Tactic:
rw [f.eq_some_iff, some_get]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, rclike_simps, norm_cast]
lemma norm_nnratCast (q : ℚ≥0) : ‖(q : K)‖ = q

Proof state:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑q‖ = ↑q

Tactic:
rw [← ofReal_nnratCast]

Result:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑↑q‖ = ↑q

Proof state:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑↑q‖ = ↑q

Tactic:
exact norm_of_nonneg q.cast_nonneg

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
@[simp] lemma pos_nilpotencyClass_iff [Nontrivial R] :
    0 < nilpotencyClass x ↔ IsNilpotent x

Proof state:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : x ^ nilpotencyClass x = 0
⊢ False

Tactic:
rw [hx', pow_zero] at hx

Result:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : 1 = 0
⊢ False

Proof state:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx : IsNilpotent x
hx' : nilpotencyClass x = 0
⊢ False

Tactic:
replace hx := pow_nilpotencyClass hx

Result:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : x ^ nilpotencyClass x = 0
⊢ False

Proof state:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx' : nilpotencyClass x = 0
hx : 1 = 0
⊢ False

Tactic:
exact one_ne_zero hx

Result:
no goals

Proof state:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x

Tactic:
refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩

Result:
R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hx : IsNilpotent x
hx' : nilpotencyClass x = 0
⊢ False
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma even_card_aut_of_not_isUnramifiedIn [IsGalois k K] [FiniteDimensional k K]
    {w : InfinitePlace k} (hw : ¬ w.IsUnramifiedIn K) :
    Even (Fintype.card <| K ≃ₐ[k] K)

Proof state:
case intro
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (card (K ≃ₐ[k] K))

Tactic:
exact even_card_aut_of_not_isUnramified hw

Result:
no goals

Proof state:
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
⊢ Even (card (K ≃ₐ[k] K))

Tactic:
obtain ⟨v, rfl⟩ := comap_surjective (K := K) w

Result:
case intro
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
v : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x => x.comap (algebraMap k K)) v)
⊢ Even (card (K ≃ₐ[k] K))

Proof state:
case intro
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
v : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x => x.comap (algebraMap k K)) v)
⊢ Even (card (K ≃ₐ[k] K))

Tactic:
rw [isUnramifiedIn_comap] at hw

Result:
case intro
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra k K
inst✝¹ : IsGalois k K
inst✝ : FiniteDimensional k K
v : InfinitePlace K
hw : ¬IsUnramified k v
⊢ Even (card (K ≃ₐ[k] K))
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_eq_sum {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} (hp : p ≠ ∞)
    [∀ i, SeminormedAddCommGroup (β i)] (f : PiLp p β) :
    ‖f‖₊ = (∑ i, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ‖f‖₊ = (∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
ext

Result:
case a
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal))

Proof state:
case a
ι : Type u_2
inst✝² : Fintype ι
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_5
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal))

Tactic:
simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitIsoLimitCurryCompLim_inv_π {j} {k} :
    (limitIsoLimitCurryCompLim G).inv ≫ limit.π _ (j, k) =
      (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) =
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom]

Result:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) =
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem _root_.Memℓp.infty_mul {f g : ∀ i, B i} (hf : Memℓp f ∞) (hg : Memℓp g ∞) :
    Memℓp (f * g) ∞

Proof state:
case intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)

Tactic:
refine ⟨Cf * Cg, ?_⟩

Result:
case intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ Cf * Cg ∈ upperBounds (Set.range fun i => ‖(f * g) i‖)

Proof state:
case intro.intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
i : I
⊢ (fun i => ‖(f * g) i‖) i ≤ Cf * Cg

Tactic:
calc
  ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le (f i) (g i)
  _ ≤ Cf * Cg :=
    mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)
      ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))

Result:
no goals

Proof state:
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)

Tactic:
obtain ⟨⟨Cf, hCf⟩, ⟨Cg, hCg⟩⟩ := hf.bddAbove, hg.bddAbove

Result:
case intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)

Proof state:
case intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ Cf * Cg ∈ upperBounds (Set.range fun i => ‖(f * g) i‖)

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case intro.intro.intro
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
i : I
⊢ (fun i => ‖(f * g) i‖) i ≤ Cf * Cg

Proof state:
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ Memℓp (f * g) ⊤

Tactic:
rw [memℓp_infty_iff]

Result:
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem exp_inl (x : R) : exp 𝕜 (inl x : tsze R M) = inl (exp 𝕜 x)

Proof state:
case hx
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ MulOpposite.op (inl x).fst • (inl x).snd = (inl x).fst • (inl x).snd

Tactic:
rw [snd_inl, fst_inl, smul_zero, smul_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ exp 𝕜 (inl x) = inl (exp 𝕜 x)

Tactic:
rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]

Result:
case hx
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ MulOpposite.op (inl x).fst • (inl x).snd = (inl x).fst • (inl x).snd
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) (x : K) :
    a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Tactic:
have : discrim a b c = 0 * 0 := by rw [h, mul_zero]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Tactic:
rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ discrim a b c = 0 * 0

Tactic:
rw [h, mul_zero]

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
theorem smul_diff_smul (g : G) : diff ϕ (g • S) (g • T) = diff ϕ S T :=
  let _ := H.fintypeQuotientOfFiniteIndex
  Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun _ ↦ by
    simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
      inv_mul_cancel_left, toPerm_symm_apply]

Proof state:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
S T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
x✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex
x✝ : G ⧸ H
⊢ ϕ ⟨(↑(⋯.leftQuotientEquiv x✝))⁻¹ * ↑(⋯.leftQuotientEquiv x✝), ⋯⟩ =
    ϕ ⟨(↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x✝)))⁻¹ * ↑(⋯.leftQuotientEquiv ((Equiv.symm (toPerm g)) x✝)), ⋯⟩

Tactic:
simp only [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
  inv_mul_cancel_left, toPerm_symm_apply]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem germ_ext (F : X.Presheaf C) {U V : Opens X} {x : X} {hxU : x ∈ U} {hxV : x ∈ V}
    (W : Opens X) (hxW : x ∈ W) (iWU : W ⟶ U) (iWV : W ⟶ V)
    {sU : ToType (F.obj (op U))} {sV : ToType (F.obj (op V))}
    (ih : F.map iWU.op sU = F.map iWV.op sV) :
      F.germ _ x hxU sU = F.germ _ x hxV sV

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : ToType (F.obj (op U))
sV : ToType (F.obj (op V))
ih : (ConcreteCategory.hom (F.map iWU.op)) sU = (ConcreteCategory.hom (F.map iWV.op)) sV
⊢ (ConcreteCategory.hom (F.germ U x hxU)) sU = (ConcreteCategory.hom (F.germ V x hxV)) sV

Tactic:
rw [← F.germ_res iWU x hxW, ← F.germ_res iWV x hxW, ConcreteCategory.comp_apply,
  ConcreteCategory.comp_apply, ih]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem S_two_mul_complex_cos (n : ℤ) : (S ℂ n).eval (2 * cos θ) * sin θ = sin ((n + 1) * θ)

Proof state:
θ : ℂ
n : ℤ
⊢ eval (2 * cos θ) (S ℂ n) * sin θ = sin ((↑n + 1) * θ)

Tactic:
simp [S_eq_U_comp_half_mul_X]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem completeSpace_iff_ultrafilter :
    CompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x

Proof state:
α : Type u
uniformSpace : UniformSpace α
⊢ CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ 𝓝 x

Tactic:
simp [completeSpace_iff_isComplete_univ, isComplete_iff_ultrafilter]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem le_one_of_mul_le_right [MulLeftReflectLE α] {a b : α} (h : a * b ≤ a) :
    b ≤ 1 :=
  le_of_mul_le_mul_left' (a := a) <| by simpa only [mul_one]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulLeftReflectLE α
a b : α
h : a * b ≤ a
⊢ a * b ≤ a * 1

Tactic:
simpa only [mul_one]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem continuousAt_infty {Y : Type*} [TopologicalSpace Y] {f : OnePoint X → Y} :
    ContinuousAt f ∞ ↔
      ∀ s ∈ 𝓝 (f ∞), ∃ t : Set X, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ (↑)) tᶜ s :=
  continuousAt_infty'.trans <| by simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ s ∈ 𝓝 (f ∞), ∃ t, IsClosed t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s

Tactic:
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]

Result:
no goals