harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_mk' (x) (y : S) : f.map hy k (f.mk' x y) = k.mk' (g x) ⟨g y, hy y⟩

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k.toMap (g x) = k.mk' (g ↑y * g x) ⟨g ↑y, ⋯⟩

Tactic:
exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
rw [map, lift_mk', mul_inv_left]

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMap.comp g) x = (k.toMap.comp g) ↑y * k.mk' (g x) ⟨g ↑y, ⋯⟩

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k.toMap (g x) = k.toMap (g ↑y) * k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
rw [mul_mk'_eq_mk'_of_mul]

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k.toMap (g x) = k.mk' (g ↑y * g x) ⟨g ↑y, ⋯⟩

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMap.comp g) x = (k.toMap.comp g) ↑y * k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
show k.toMap (g x) = k.toMap (g y) * _

Result:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k.toMap (g x) = k.toMap (g ↑y) * k.mk' (g x) ⟨g ↑y, ⋯⟩
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem transcendental_iff_ker_eq_bot {x : A} :
    Transcendental R x ↔ RingHom.ker (aeval (R := R) x) = ⊥

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
⊢ Transcendental R x ↔ RingHom.ker (aeval x) = ⊥

Tactic:
rw [transcendental_iff_injective, RingHom.injective_iff_ker_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Basic.lean
theorem toNonneg_le {a : α} {b : { x : α // 0 ≤ x }} : toNonneg a ≤ b ↔ a ≤ b

Proof state:
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ ⟨b, hb⟩ ↔ a ≤ ↑⟨b, hb⟩

Tactic:
simp [toNonneg, hb]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a : α
b : { x // 0 ≤ x }
⊢ toNonneg a ≤ b ↔ a ≤ ↑b

Tactic:
obtain ⟨b, hb⟩ := b

Result:
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : SemilatticeSup α
a b : α
hb : 0 ≤ b
⊢ toNonneg a ≤ ⟨b, hb⟩ ↔ a ≤ ↑⟨b, hb⟩
-- Mathlib/Computability/Tape.lean
theorem proj_map_nth {ι : Type*} {Γ : ι → Type*} [∀ i, Inhabited (Γ i)] (i : ι) (L n) :
    (ListBlank.map (@proj ι Γ _ i) L).nth n = L.nth n i

Proof state:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (ListBlank.map (proj i) L).nth n = L.nth n i

Tactic:
rw [ListBlank.nth_map]

Result:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i

Proof state:
ι : Type u_1
Γ : ι → Type u_2
inst✝ : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (proj i).f (L.nth n) = L.nth n i

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem AddContent.extend_eq (hC : IsSetSemiring C) (m : AddContent C) (hs : s ∈ C) :
    m.extend hC s = m s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent C
hs : s ∈ C
⊢ (AddContent.extend hC m) s = m s

Tactic:
rwa [m.extend_eq_extend, extend_eq]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mkOfObjOfMapSucc_arrow (i : ℕ) (hi : i < n

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
i : ℕ
hi : autoParam (i < n) _auto✝
⊢ ((mkOfObjOfMapSucc obj mapSucc).arrow i hi).hom = eqToHom ⋯ ≫ (mk₁ (mapSucc ⟨i, hi⟩)).hom ≫ eqToHom ⋯

Tactic:
simpa using mkOfObjOfMapSucc_map_succ obj mapSucc i hi

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_mul_right [IsMulLeftInvariant μ] (g : G) :
    QuasiMeasurePreserving (fun h : G => h * g) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => h * g) μ μ

Tactic:
refine ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → (map (fun h => h * g) μ) s = 0

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0

Tactic:
exact id

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → (map (fun h => h * g) μ) s = 0

Tactic:
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem smtSDiv_zero {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n then 1#n else (allOnes n)

Proof state:
n : Nat
x : BitVec n
⊢ x.smtSDiv 0#n = if x.slt 0#n = true then 1#n else allOnes n

Tactic:
rcases hx : x.msb <;> simp [smtSDiv, slt_zero_iff_msb_cond, hx, ← negOne_eq_allOnes]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma mod_two_add_add_odd_mod_two (m : ℕ) {n : ℕ} (hn : Odd n) : m % 2 + (m + n) % 2 = 1 :=
  ((even_or_odd m).elim fun hm ↦ by rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]) fun hm ↦ by
    rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]

Proof state:
m n : ℕ
hn : Odd n
hm : Odd m
⊢ m % 2 + (m + n) % 2 = 1

Tactic:
rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]

Result:
no goals

Proof state:
m n : ℕ
hn : Odd n
hm : Even m
⊢ m % 2 + (m + n) % 2 = 1

Tactic:
rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]

Result:
no goals
-- Mathlib/Topology/Connected/LocallyConnected.lean
theorem locallyConnectedSpace_of_connected_bases {ι : Type*} (b : α → ι → Set α) (p : α → ι → Prop)
    (hbasis : ∀ x, (𝓝 x).HasBasis (p x) (b x))
    (hconnected : ∀ x i, p x i → IsPreconnected (b x i)) : LocallyConnectedSpace α

Proof state:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id

Tactic:
exact fun x =>
  (hbasis x).to_hasBasis
    (fun i hi => ⟨b x i, ⟨(hbasis x).mem_of_mem hi, hconnected x i hi⟩, subset_rfl⟩) fun s hs =>
    ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_connected_basis]

Result:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ ∀ (x : α), (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPreconnected s) id
-- Mathlib/Algebra/Group/Conj.lean
theorem conj_pow {i : ℕ} {a b : α} : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Proof state:
case succ
α : Type u
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹

Tactic:
simp [pow_succ, hi]

Result:
no goals

Proof state:
α : Type u
inst✝ : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
induction' i with i hi

Result:
case zero
α : Type u
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ 0 = a * b ^ 0 * a⁻¹

case succ
α : Type u
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹

Proof state:
case zero
α : Type u
inst✝ : Group α
a b : α
⊢ (a * b * a⁻¹) ^ 0 = a * b ^ 0 * a⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_filterMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Option β)) :
    toList <$> a.filterMapM f = a.toList.filterMapM f

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Option β)
⊢ toList <$> List.toArray <$> List.filterMapM f a.toList = List.filterMapM f a.toList

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Option β)
⊢ toList <$> filterMapM f a = List.filterMapM f a.toList

Tactic:
rw [List.filterMapM_toArray]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Option β)
⊢ toList <$> List.toArray <$> List.filterMapM f a.toList = List.filterMapM f a.toList
-- Mathlib/Data/Set/Functor.lean
theorem image_image_val_eq_restrict_image {δ : Type*} {f : α → δ} : f '' γ = β.restrict f '' γ

Proof state:
case h
α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' (Subtype.val '' γ) ↔ x✝ ∈ β.restrict f '' γ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
⊢ f '' (Subtype.val '' γ) = β.restrict f '' γ

Tactic:
ext

Result:
case h
α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' (Subtype.val '' γ) ↔ x✝ ∈ β.restrict f '' γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_nonneg_of_nonpos {a : Int} (h : a ≤ 0) : 0 ≤ -a

Proof state:
a : Int
h : a ≤ 0
this : -0 ≤ -a
⊢ 0 ≤ -a

Tactic:
rwa [Int.neg_zero] at this

Result:
no goals

Proof state:
a : Int
h : a ≤ 0
⊢ 0 ≤ -a

Tactic:
have : -0 ≤ -a := Int.neg_le_neg h

Result:
a : Int
h : a ≤ 0
this : -0 ≤ -a
⊢ 0 ≤ -a
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.linear_preimage {s : Set F} (f : E →ₗ[𝕜] F) (hs : StarConvex 𝕜 (f x) s) :
    StarConvex 𝕜 x (f ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 (f x) s
⊢ StarConvex 𝕜 x (⇑f ⁻¹' s)

Tactic:
intro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 (f x) s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Tactic:
exact hs hy ha hb hab

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebra_le [Nonempty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1

Proof state:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
m : ι → A
⊢ ‖∏ i : ι, m i‖ ≤ ∏ i : ι, ‖m i‖

Tactic:
exact norm_prod_le' _ univ_nonempty _

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1

Tactic:
refine opNorm_le_bound zero_le_one fun m => ?_

Result:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
m : ι → A
⊢ ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) m‖ ≤ 1 * ∏ i : ι, ‖m i‖

Proof state:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
m : ι → A
⊢ ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) m‖ ≤ 1 * ∏ i : ι, ‖m i‖

Tactic:
simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]

Result:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
m : ι → A
⊢ ‖∏ i : ι, m i‖ ≤ ∏ i : ι, ‖m i‖
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem aeSeq_eq_mk_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α}
    (hx : x ∈ aeSeqSet hf p) (i : ι) : aeSeq hf p i x = (hf i).mk (f i) x

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
simp only [aeSeq, hx, if_true]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ {r}

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
⊢ (fun x => r) '' spectrum R 0 ⊆ {r}

Tactic:
rintro - ⟨x, -, rfl⟩

Result:
case intro.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r x : R
⊢ (fun x => r) x ∈ {r}

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r x : R
⊢ (fun x => r) x ∈ {r}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
⊢ spectrum R ((algebraMap R A) r) ⊆ {r}

Tactic:
rw [← cfc_const r 0 (cfc_predicate_zero R),
  cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
⊢ (fun x => r) '' spectrum R 0 ⊆ {r}
-- Mathlib/CategoryTheory/Quotient.lean
@[reassoc]
lemma comp_natTransLift {F G H : Quotient r ⥤ D}
    (τ : Quotient.functor r ⋙ F ⟶ Quotient.functor r ⋙ G)
    (τ' : Quotient.functor r ⋙ G ⟶ Quotient.functor r ⋙ H) :
    natTransLift r τ ≫ natTransLift r τ' =  natTransLift r (τ ≫ τ')

Proof state:
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} D
F G H : Quotient r ⥤ D
τ : functor r ⋙ F ⟶ functor r ⋙ G
τ' : functor r ⋙ G ⟶ functor r ⋙ H
⊢ natTransLift r τ ≫ natTransLift r τ' = natTransLift r (τ ≫ τ')

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_eq_iff_eq_replicate {l : List α} :
    Chain' (· = ·) l ↔ ∀ a ∈ l.head?, l = replicate l.length a :=
  match l with
  | [] => by simp
  | a :: l => by simp [Chain', chain_eq_iff_eq_replicate, replicate_succ]

Proof state:
α : Type u
l✝ : List α
a : α
l : List α
⊢ Chain' (fun x1 x2 => x1 = x2) (a :: l) ↔ ∀ (a_1 : α), a_1 ∈ (a :: l).head? → a :: l = replicate (a :: l).length a_1

Tactic:
simp [Chain', chain_eq_iff_eq_replicate, replicate_succ]

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ Chain' (fun x1 x2 => x1 = x2) [] ↔ ∀ (a : α), a ∈ [].head? → [] = replicate [].length a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem _root_.Function.leftInvOn_invFunOn_of_subset_image_image [Nonempty α]
    (h : s ⊆ (invFunOn f s) '' (f '' s)) : LeftInvOn (invFunOn f s) f s :=
  fun x hx ↦ by
    obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
    rw [invFunOn_apply_eq (f := f) hx']

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' (f '' s)
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)

Tactic:
rw [invFunOn_apply_eq (f := f) hx']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' (f '' s)
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) = x

Tactic:
obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝ : Nonempty α
h : s ⊆ invFunOn f s '' (f '' s)
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_eq_zero_of_not_injective (v : ι → M) (hv : ¬Function.Injective v) : f v = 0

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ f v = 0

Tactic:
exact f.map_eq_zero_of_eq v heq hne

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬Injective v
⊢ f v = 0

Tactic:
rw [Function.Injective] at hv

Result:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ f v = 0

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ∃ a₁ a₂, v a₁ = v a₂ ∧ a₁ ≠ a₂
⊢ f v = 0

Tactic:
rcases hv with ⟨i₁, i₂, heq, hne⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ f v = 0

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ f v = 0

Tactic:
push_neg at hv

Result:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ∃ a₁ a₂, v a₁ = v a₂ ∧ a₁ ≠ a₂
⊢ f v = 0
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem isCoatom_comap_or_eq_top (f : F) {p : Submodule R₂ M₂} (hp : IsCoatom p) :
    IsCoatom (comap f p) ∨ comap f p = ⊤ :=
  or_iff_not_imp_right.mpr fun h ↦ ⟨h, fun q lt ↦ by
    rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]
    simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_le⟩

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p

Tactic:
simpa only [right_lt_sup, map_le_iff_le_comap] using lt.not_le

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ q = ⊤

Tactic:
rw [← comap_map_sup_of_comap_le lt.le, hp.2 (map f q ⊔ p), comap_top]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p : Submodule R₂ M₂
hp : IsCoatom p
h : ¬comap f p = ⊤
q : Submodule R M
lt : comap f p < q
⊢ p < map f q ⊔ p
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive]
lemma _root_.Cardinal.mk_div_le : #(s / t) ≤ #s * #t

Proof state:
M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(image2 Div.div s t) ≤ #↑s * #↑t

Tactic:
exact Cardinal.mk_image2_le

Result:
no goals

Proof state:
M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(s / t) ≤ #↑s * #↑t

Tactic:
rw [← image2_div]

Result:
M : Type u_2
inst✝ : DivInvMonoid M
s t : Set M
⊢ #↑(image2 Div.div s t) ≤ #↑s * #↑t