harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn_map [Monad m] [LawfulMonad m]
    (l : Vector α n) (g : α → β) (f : β → γ → m (ForInStep γ)) :
    forIn (l.map g) init f = forIn l init fun a y => f (g a) y

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → γ → m (ForInStep γ)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ forIn (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) init f =
    forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a y => f (g a) y

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
g : α → β
f : β → γ → m (ForInStep γ)
⊢ forIn (map g l) init f = forIn l init fun a y => f (g a) y

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → γ → m (ForInStep γ)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ forIn (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) init f =
    forIn { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a y => f (g a) y
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_rel₂ {R : L.Relations 2} {t₁ t₂ : L.Term _} :
    (R.boundedFormula₂ t₁ t₂).Realize v xs ↔
      RelMap R ![t₁.realize (Sum.elim v xs), t₂.realize (Sum.elim v xs)]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Tactic:
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : L.Term (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0

Tactic:
simp only [Matrix.cons_val_zero]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub (hf : HasFPowerSeriesAt f p x) :
    (fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓝 (x, x)] fun y =>
      ‖y - (x, x)‖ * ‖y.1 - y.2‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesWithinAt f p univ x
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simpa using hf.isBigO_image_sub_norm_mul_norm_sub

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesWithinAt f p univ x
⊢ (fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions antivary iff the rearrangement inequality holds. -/
lemma antivary_iff_mul_rearrangement :
    Antivary f g ↔ ∀ i j, f i * g i + f j * g j ≤ f i * g j + f j * g i

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
⊢ Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i

Tactic:
simp only [smul_eq_mul, antivary_iff_smul_rearrangement]

Result:
no goals
-- Mathlib/FieldTheory/Galois/GaloisClosure.lean
theorem adjoin_simple_map_algHom [IsGalois k K] (f : K →ₐ[k] K) (x : K) :
    adjoin k {f x} = adjoin k {x}

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
f : K →ₐ[k] K
x : K
⊢ adjoin k {f x} = adjoin k {x}

Tactic:
simpa only [Set.image_singleton] using adjoin_map f { x }

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹

Tactic:
rw [mul_assoc, mul_inv_cancel₀ ha, mul_one]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹

Tactic:
rw [← zpow_add_one₀ ha, Int.sub_add_cancel]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem lt_nmul_iff₃' : d < a ⨳ (b ⨳ c) ↔ ∃ a' < a, ∃ b' < b, ∃ c' < c,
    d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤
      a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c')

Proof state:
a b c d : Ordinal.{u}
⊢ d < a ⨳ (b ⨳ c) ↔
    ∃ a' < a,
      ∃ b' < b,
        ∃ c' < c,
          d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤
            a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c')

Tactic:
simpa using nmul_le_iff₃'.not

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_comp_rpow_Ioi_of_pos {g : ℝ → E} {p : ℝ} (hp : 0 < p) :
    (∫ x in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p)) = ∫ y in Ioi 0, g y

Proof state:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
x✝ : ℝ
⊢ p = |p|

Tactic:
rw [abs_of_nonneg hp.le]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, (p * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y

Tactic:
convert integral_comp_rpow_Ioi g hp.ne'

Result:
case h.e'_2.h.e'_7.h.h.e'_5.h.e'_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : 0 < p
x✝ : ℝ
⊢ p = |p|
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_image {s : Set α} {f : β → M} {g : α → β} (hg : Injective g) {x : α} :
    mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x

Tactic:
rw [← mulIndicator_comp_right, preimage_image_eq _ hg]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem boundedBy_apply (s : Set α) :
    boundedBy m s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t),
                      ∑' n, ⨆ _ : (t n).Nonempty, m (t n)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
⊢ (boundedBy m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (t n)

Tactic:
simp [boundedBy, ofFunction_apply]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
protected lemma SupClosed.infClosure (hs : SupClosed s) : SupClosed (infClosure s)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i => id i.1 ⊔ id i.2) ∈ infClosure s

Tactic:
exact finsetInf'_mem_infClosure _
  fun i hi ↦ hs (hts (mem_product.1 hi).1) (hus (mem_product.1 hi).2)

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
⊢ SupClosed (infClosure s)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ t.inf' ht id ⊔ u.inf' hu id ∈ infClosure s

Tactic:
rw [inf'_sup_inf']

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : SupClosed s
t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ s
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
⊢ ((t ×ˢ u).inf' ⋯ fun i => id i.1 ⊔ id i.2) ∈ infClosure s
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
@[simp] lemma ad_apply_eq_zero_iff (x : L) : ad R L x = 0 ↔ x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
⊢ (ad R L) x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : (ad R L) x = 0
⊢ x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : x = 0
⊢ (ad R L) x = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
x : L
h : (ad R L) x = 0
⊢ x = 0

Tactic:
rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h

Result:
no goals
-- Mathlib/Data/FinEnum.lean
theorem nodup_toList [FinEnum α] : List.Nodup (toList α)

Proof state:
α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup

Tactic:
apply List.Nodup.map <;> [apply Equiv.injective; apply List.nodup_finRange]

Result:
no goals

Proof state:
α : Type u
inst✝ : FinEnum α
⊢ (toList α).Nodup

Tactic:
simp [toList]

Result:
α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem eqRec_heq_self {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
    (x : motive a rfl) {a' : α} (e : a = a') :
    HEq (@Eq.rec α a motive x a' e) x

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
⊢ HEq (⋯ ▸ x) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
a' : α
e : a = a'
⊢ HEq (e ▸ x) x

Tactic:
subst e

Result:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
⊢ HEq (⋯ ▸ x) x
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is strictly positive, then
`f` is a strictly monotone function. -/
lemma strictAnti_of_hasDerivAt_neg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x)
    (hf' : ∀ x, f' x < 0) : StrictAnti f :=
  strictAnti_of_deriv_neg fun x ↦ by rw [(hf _).deriv]; exact hf' _

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0

Tactic:
exact hf' _

Result:
no goals

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ deriv f x < 0

Tactic:
rw [(hf _).deriv]

Result:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0
-- Mathlib/SetTheory/Game/PGame.lean
/-- `-(x + y)` has exactly the same moves as `-x + -y`. -/
protected lemma neg_add (x y : PGame) : -(x + y) = -x + -y :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR => by
    refine ext rfl rfl ?_ ?_ <;>
    · rintro (i | i) _ ⟨rfl⟩
      · exact PGame.neg_add _ _
      · simpa [Equiv.refl, mk_add_moveLeft, mk_add_moveRight] using PGame.neg_add _ _
  termination_by (x, y)

Proof state:
case refine_2.inl.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
β : Type u_1
⊢ (-(mk xl xr xL xR + mk yl yr yL yR)).moveRight (Sum.inl i) = (-mk xl xr xL xR + -mk yl yr yL yR).moveRight (Sum.inl i)

Tactic:
exact PGame.neg_add _ _

Result:
no goals

Proof state:
case refine_2
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ ∀ (i : (-(mk xl xr xL xR + mk yl yr yL yR)).RightMoves) (j : (-mk xl xr xL xR + -mk yl yr yL yR).RightMoves),
    HEq i j → (-(mk xl xr xL xR + mk yl yr yL yR)).moveRight i = (-mk xl xr xL xR + -mk yl yr yL yR).moveRight j

Tactic:
rintro (i | i) _ ⟨rfl⟩

Result:
case refine_2.inl.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : xl
β : Type u_1
⊢ (-(mk xl xr xL xR + mk yl yr yL yR)).moveRight (Sum.inl i) = (-mk xl xr xL xR + -mk yl yr yL yR).moveRight (Sum.inl i)

case refine_2.inr.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : yl
β : Type u_1
⊢ (-(mk xl xr xL xR + mk yl yr yL yR)).moveRight (Sum.inr i) = (-mk xl xr xL xR + -mk yl yr yL yR).moveRight (Sum.inr i)

Proof state:
case refine_2.inr.refl
x y : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
i : yl
β : Type u_1
⊢ (-(mk xl xr xL xR + mk yl yr yL yR)).moveRight (Sum.inr i) = (-mk xl xr xL xR + -mk yl yr yL yR).moveRight (Sum.inr i)

Tactic:
simpa [Equiv.refl, mk_add_moveLeft, mk_add_moveRight] using PGame.neg_add _ _

Result:
no goals
-- Mathlib/Algebra/Algebra/Defs.lean
theorem left_comm (x : A) (r : R) (y : A) :
    x * (algebraMap R A r * y) = algebraMap R A r * (x * y)

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)

Tactic:
rw [← mul_assoc, ← commutes, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem eq_bot_of_equiv [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] (⊥ : Submodule R₂ M₂)) : p = ⊥

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ e ⟨b, hb⟩ = 0

Tactic:
apply Submodule.eq_zero_of_bot_submodule

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ b = 0

Tactic:
rw [← p.mk_eq_zero hb, ← e.map_eq_zero_iff]

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ e ⟨b, hb⟩ = 0

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
⊢ p = ⊥

Tactic:
refine bot_unique (SetLike.le_def.2 fun b hb => (Submodule.mem_bot R).2 ?_)

Result:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁴ : Semiring R
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
module_M : Module R M
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p : Submodule R M
inst✝ : Module R₂ M₂
e : ↥p ≃ₛₗ[σ₁₂] ↥⊥
b : M
hb : b ∈ p
⊢ b = 0
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_top_of_localization_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized' (Rₚ P) P.primeCompl (f P) = ⊤) :
    N = ⊤ :=
  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP ↦ by simpa using h P

Proof state:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized' (Rₚ P) P.primeCompl (f P) N = ⊤
P : Ideal R
hP : P.IsMaximal
⊢ localized' (Rₚ P) P.primeCompl (f P) N = localized' (Rₚ P) P.primeCompl (f P) ⊤

Tactic:
simpa using h P

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_X_pow (n : ℕ) : (X ^ n).toFinsupp = Finsupp.single n (1 : R)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).toFinsupp = Finsupp.single n 1

Tactic:
rw [X_pow_eq_monomial, toFinsupp_monomial]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean
lemma shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) :
    (shiftIso L G M F' e' n a a' ha').hom.app (L.obj X) =
      (F' a).map ((L.commShiftIso n).inv.app X) ≫
        (e' a).hom.app (X⟦n⟧) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X :=
  (NatTrans.congr_app (((whiskeringLeft C D A).obj L).map_preimage _) X).trans (by simp)

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{u_7, u_1} C
inst✝⁸ : Category.{u_6, u_2} D
inst✝⁷ : Category.{u_5, u_3} A
L : C ⥤ D
G : C ⥤ A
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n a a' : M
ha' : n + a = a'
X : C
⊢ ((L.associator (shiftFunctor D n) (F' a)).symm ≪≫
            isoWhiskerRight (L.commShiftIso n).symm (F' a) ≪≫
              (shiftFunctor C n).associator L (F' a) ≪≫
                isoWhiskerLeft (shiftFunctor C n) (e' a) ≪≫ G.shiftIso n a a' ha' ≪≫ (e' a').symm).hom.app
      X =
    (F' a).map ((L.commShiftIso n).inv.app X) ≫
      (e' a).hom.app ((shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
@[simp]
lemma card_inter_add_card_sdiff (s t : Finset α) :
    #(s ∩ t) + #(s \ t) = #s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s \ t) = #s

Tactic:
rw [Nat.add_comm, card_sdiff_add_card_inter]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValInt_dvd_iff (n : ℕ) (a : ℤ) : (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Tactic:
rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff, ← Int.natCast_dvd, Int.natCast_pow]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma map_comp_cotangentComplex (f : Hom P P') :
    CotangentSpace.map f ∘ₗ P.cotangentComplex =
      P'.cotangentComplex.restrictScalars S ∘ₗ Cotangent.map f

Proof state:
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
⊢ CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Cotangent.map f

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : P.Cotangent
⊢ (CotangentSpace.map f ∘ₗ P.cotangentComplex) x = (↑S P'.cotangentComplex ∘ₗ Cotangent.map f) x

Proof state:
case h
R : Type u
S : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁶ : CommRing R'
inst✝⁵ : CommRing S'
inst✝⁴ : Algebra R' S'
P' : Extension R' S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : Algebra R S'
inst✝ : IsScalarTower R R' S'
f : P.Hom P'
x : P.Cotangent
⊢ (CotangentSpace.map f ∘ₗ P.cotangentComplex) x = (↑S P'.cotangentComplex ∘ₗ Cotangent.map f) x

Tactic:
exact map_cotangentComplex f x

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_mul_const_iff [ContinuousMul β] {c : β} (hc0 : c ≠ 0) :
    (SuperpolynomialDecay l k fun n => f n * c) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h => (h.mul_const c⁻¹).congr fun x => by simp [mul_assoc, mul_inv_cancel₀ hc0], fun h =>
    h.mul_const c⟩

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => f n * c
x : α
⊢ f x * c * c⁻¹ = f x

Tactic:
simp [mul_assoc, mul_inv_cancel₀ hc0]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_norm_spectrum [Nontrivial A] (a : A) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
a : A
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖x‖) '' σ 𝕜 a) ‖a‖

Tactic:
simpa only [cfc_id 𝕜 a] using IsGreatest.norm_cfc (id : 𝕜 → 𝕜) a

Result:
no goals