harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem alternization_map_eq_zero_of_eq_aux (m : MultilinearMap R (fun _ : ι => M) N')
    (v : ι → M) (i j : ι) (i_ne_j : i ≠ j) (hv : v i = v j) :
    (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ) 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_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ∑ a : Perm ι, (Perm.sign a • domDomCongr a m) v = 0

Tactic:
exact
  Finset.sum_involution (fun σ _ => swap i j * σ)
    (fun σ _ => by simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv, -Equiv.Perm.sign_swap'])
    (fun σ _ _ => (not_congr swap_mul_eq_iff).mpr i_ne_j) (fun σ _ => Finset.mem_univ _)
    fun σ _ => swap_mul_involutive i j σ

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_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
σ : Perm ι
x✝ : σ ∈ Finset.univ
⊢ (Perm.sign σ • domDomCongr σ m) v +
      (Perm.sign ((fun σ x => swap i j * σ) σ x✝) • domDomCongr ((fun σ x => swap i j * σ) σ x✝) m) v =
    0

Tactic:
simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv, -Equiv.Perm.sign_swap']

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_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ (∑ σ : Perm ι, Perm.sign σ • domDomCongr σ m) v = 0

Tactic:
rw [sum_apply]

Result:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ ∑ a : Perm ι, (Perm.sign a • domDomCongr a m) v = 0
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_rotate (a b c : G) : a * b * c = b * c * a

Proof state:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = b * c * a

Tactic:
simp only [mul_left_comm, mul_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem mem_const_vsub_affineSegment {x y z : P} (p : P) :
    p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_const_vsub_image, (vsub_right_injective p).mem_set_image]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem res_length (x : ℕ → α) (n : ℕ) : (res x n).length = n

Proof state:
α : Type u_2
x : ℕ → α
n : ℕ
⊢ (res x n).length = n

Tactic:
induction n <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
theorem bijective_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] :
    Function.Bijective f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso ⇑(hom f)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Function.Bijective ⇑(hom f)

Tactic:
rw [← isIso_iff_bijective]

Result:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso ⇑(hom f)
-- Mathlib/Data/Vector/Basic.lean
theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f i

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).toList.get (Fin.cast ⋯ i) = (List.ofFn f).get ⟨↑i, ⋯⟩

Tactic:
congr <;> simp [Fin.heq_ext_iff]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).get i = (List.ofFn f).get ⟨↑i, ⋯⟩

Tactic:
simp only [get_eq_get_toList]

Result:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).toList.get (Fin.cast ⋯ i) = (List.ofFn f).get ⟨↑i, ⋯⟩

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ ↑i < (List.ofFn f).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).get i = f i

Tactic:
conv_rhs => erw [← List.get_ofFn f ⟨i, by simp⟩]

Result:
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ (ofFn f).get i = (List.ofFn f).get ⟨↑i, ⋯⟩
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem Finset.analyticAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A]
    {f : α → E → A} {c : E} (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
    AnalyticAt 𝕜 (fun z ↦ ∏ n ∈ N, f n z) c

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
⊢ AnalyticAt 𝕜 (fun z => ∏ n ∈ N, f n z) c

Tactic:
simp_rw [← analyticWithinAt_univ] at h ⊢

Result:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt 𝕜 (fun z => ∏ n ∈ N, f n z) Set.univ c

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) Set.univ c
⊢ AnalyticWithinAt 𝕜 (fun z => ∏ n ∈ N, f n z) Set.univ c

Tactic:
exact N.analyticWithinAt_prod h

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem mul_tsub {a b c : α}
    (h : AddLECancellable (a * c)) : a * (b - c) = a * b - a * c

Proof state:
case inl
α : Type u
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
a b c : α
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c

Tactic:
rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]

Result:
no goals

Proof state:
case inr
α : Type u
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
a b c : α
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c

Tactic:
apply h.eq_tsub_of_add_eq

Result:
case inr
α : Type u
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
a b c : α
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b

Proof state:
case inr
α : Type u
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : PartialOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
a b c : α
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b

Tactic:
rw [← mul_add, tsub_add_cancel_of_le hcb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_sub_iff_add_eq {x y z : BitVec w} : x = z - y ↔ x + y = z

Proof state:
w : Nat
x y z : BitVec w
⊢ x = z - y ↔ x + y = z

Tactic:
apply Iff.intro <;> intro h

Result:
case mp
w : Nat
x y z : BitVec w
h : x = z - y
⊢ x + y = z

case mpr
w : Nat
x y z : BitVec w
h : x + y = z
⊢ x = z - y

Proof state:
case mpr
w : Nat
x y z : BitVec w
h : x + y = z
⊢ x = z - y

Tactic:
simp [←h, add_sub_cancel]

Result:
no goals

Proof state:
case mp
w : Nat
x y z : BitVec w
h : x = z - y
⊢ x + y = z

Tactic:
simp [h, sub_add_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem iInter_of_antitone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    [(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α}
    (hsm : Antitone s) (hs : ∀ i, MeasurableSet (s i)) : MeasurableSet (⋂ i, s i)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋂ i, s i)

Tactic:
rw [← compl_iff, compl_iInter]

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, (s i)ᶜ)

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
ι : Type u_6
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hsm : Antitone s
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ MeasurableSet (⋃ i, (s i)ᶜ)

Tactic:
exact .iUnion_of_monotone (compl_anti.comp hsm) fun i ↦ (hs i).compl

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem lt_iff_re_im : z < w ↔ re z < re w ∧ im z = im w

Proof state:
case mp.intro.intro
K : Type u_1
inst✝ : RCLike K
z w : K
heq : z ≠ w
hr : re z ≤ re w
hi : im z = im w
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z < w ↔ re z < re w ∧ im z = im w

Tactic:
simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]

Result:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Proof state:
case mpr.intro.intro
K : Type u_1
inst✝ : RCLike K
z w : K
hi : im z = im w
hr : re z ≤ re w
hrn : re z ≠ re w
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w

Tactic:
exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
constructor

Result:
case mp
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w → (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

case mpr
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w → (re z ≤ re w ∧ im z = im w) ∧ z ≠ w

Proof state:
case mp
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w → (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
rintro ⟨⟨hr, hi⟩, heq⟩

Result:
case mp.intro.intro
K : Type u_1
inst✝ : RCLike K
z w : K
heq : z ≠ w
hr : re z ≤ re w
hi : im z = im w
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Proof state:
case mpr
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w → (re z ≤ re w ∧ im z = im w) ∧ z ≠ w

Tactic:
rintro ⟨⟨hr, hrn⟩, hi⟩

Result:
case mpr.intro.intro
K : Type u_1
inst✝ : RCLike K
z w : K
hi : im z = im w
hr : re z ≤ re w
hrn : re z ≠ re w
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w
-- Mathlib/LinearAlgebra/Dual.lean
theorem LinearMap.dualMap_injective_of_surjective {f : M₁ →ₗ[R] M₂} (hf : Function.Surjective f) :
    Function.Injective f.dualMap

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
⊢ Function.Injective ⇑f.dualMap

Tactic:
intro φ ψ h

Result:
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
⊢ φ = ψ

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
x : M₂
⊢ φ x = ψ x

Tactic:
obtain ⟨y, rfl⟩ := hf x

Result:
case h.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
y : M₁
⊢ φ (f y) = ψ (f y)

Proof state:
case h.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
y : M₁
⊢ φ (f y) = ψ (f y)

Tactic:
exact congr_arg (fun g : Module.Dual R M₁ => g y) h

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
⊢ φ = ψ

Tactic:
ext x

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
φ ψ : Dual R M₂
h : f.dualMap φ = f.dualMap ψ
x : M₂
⊢ φ x = ψ x
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem Tendsto.prod_atBot [Preorder α] [Preorder γ] {f g : α → γ}
    (hf : Tendsto f atBot atBot) (hg : Tendsto g atBot atBot) :
    Tendsto (Prod.map f g) atBot atBot

Proof state:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Result:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot

Proof state:
α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot

Tactic:
exact hf.prod_map_prod_atBot hg

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformGroup.mk' {α} [UniformSpace α] [Group α]
    (h₁ : UniformContinuous fun p : α × α => p.1 * p.2) (h₂ : UniformContinuous fun p : α => p⁻¹) :
    UniformGroup α :=
  ⟨by simpa only [div_eq_mul_inv] using
    h₁.comp (uniformContinuous_fst.prod_mk (h₂.comp uniformContinuous_snd))⟩

Proof state:
α : Type u_3
inst✝¹ : UniformSpace α
inst✝ : Group α
h₁ : UniformContinuous fun p => p.1 * p.2
h₂ : UniformContinuous fun p => p⁻¹
⊢ UniformContinuous fun p => p.1 / p.2

Tactic:
simpa only [div_eq_mul_inv] using
h₁.comp (uniformContinuous_fst.prod_mk (h₂.comp uniformContinuous_snd))

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_characterModule_injective [Small.{v} R] :
    Flat R M ↔ Module.Injective R (CharacterModule M)

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v, u} R
⊢ Flat R M ↔ Injective R (CharacterModule M)

Tactic:
rw [injective_characterModule_iff_rTensor_preserves_injective_linearMap,
  iff_rTensor_preserves_injective_linearMap']

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_lt_toPartENat_iff {n : ℕ} {c : Cardinal} :
    ↑n < toPartENat c ↔ ↑n < c

Proof state:
n : ℕ
c : Cardinal.{u_1}
⊢ ↑n < toPartENat c ↔ ↑n < c

Tactic:
simp only [← not_le, Cardinal.toPartENat_le_natCast_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
lemma tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ p) :
    a ⊗ₜ[R] m ∈ p.baseChange A

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : A
m : M
hm : m ∈ p
⊢ a • 1 ⊗ₜ[R] m ∈ baseChange A p

Tactic:
exact smul_mem (baseChange A p) a (subset_span ⟨m, hm, rfl⟩)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : A
m : M
hm : m ∈ p
⊢ a ⊗ₜ[R] m ∈ baseChange A p

Tactic:
rw [← mul_one a, ← smul_eq_mul, ← smul_tmul']

Result:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : A
m : M
hm : m ∈ p
⊢ a • 1 ⊗ₜ[R] m ∈ baseChange A p
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorZero_hom_app_shift (n : A) :
    (shiftFunctorZero C A).hom.app (X⟦n⟧) =
    (shiftFunctorComm C n 0).hom.app X ≫ ((shiftFunctorZero C A).hom.app X)⟦n⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    (shiftFunctorComm C n 0).hom.app X ≫ (shiftFunctor C n).map ((shiftFunctorZero C A).hom.app X)

Tactic:
rw [← shiftFunctorAdd'_zero_add_inv_app n X, shiftFunctorComm_eq C n 0 n (add_zero n)]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    ((shiftFunctorAdd' C n 0 n ⋯).symm ≪≫ shiftFunctorAdd' C 0 n n ⋯).hom.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).inv.app X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    ((shiftFunctorAdd' C n 0 n ⋯).inv.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).hom.app X) ≫
      (shiftFunctorAdd' C 0 n n ⋯).inv.app X

Tactic:
rw [Category.assoc, Iso.hom_inv_id_app, Category.comp_id, shiftFunctorAdd'_add_zero_inv_app]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    ((shiftFunctorAdd' C n 0 n ⋯).symm ≪≫ shiftFunctorAdd' C 0 n n ⋯).hom.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).inv.app X

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    ((shiftFunctorAdd' C n 0 n ⋯).inv.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).hom.app X) ≫
      (shiftFunctorAdd' C 0 n n ⋯).inv.app X
-- Mathlib/Probability/Kernel/WithDensity.lean
lemma withDensity_add_right [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞}
    (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) :
    withDensity κ (f + g) = withDensity κ f + withDensity κ g

Proof state:
case h.h.hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (Function.uncurry (f + g))

Tactic:
exact hf.add hg

Result:
no goals

Proof state:
case h.h.hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (g a)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
⊢ κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity (f + g)) a) s✝ = ((κ.withDensity f + κ.withDensity g) a) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity (f + g)) a) s✝ = ((κ.withDensity f + κ.withDensity g) a) s✝

Tactic:
rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg,
  Kernel.withDensity_apply, Pi.add_apply, MeasureTheory.withDensity_add_right]

Result:
case h.h.hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (g a)

case h.h.hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ Measurable (Function.uncurry (f + g))
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tag_mem_smul_span (ν : ι → ℤ) :
    tag n ν ∈ (n : ℝ)⁻¹ • L

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ (algebraMap ℤ ℝ) (ν i + 1) = ↑n * tag n ν i

Tactic:
rw [tag_apply, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel_of_invertible, one_mul, map_add,
  map_one, eq_intCast]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ tag n ν ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))

Tactic:
refine mem_smul_span_iff.mpr fun i ↦ ⟨ν i + 1, ?_⟩

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ (algebraMap ℤ ℝ) (ν i + 1) = ↑n * tag n ν i
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isShortNF : W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * 0 ^ 3 * W.a₆ + 16 * 0 ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * 0 * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
rw [Δ_of_isCharNeTwoNF, a₂_of_isShortNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * 0 ^ 3 * W.a₆ + 16 * 0 ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * 0 * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)