harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
@[simp]
lemma direction_smul (ha : a ≠ 0) (s : AffineSubspace k V) : (a • s).direction = s.direction

Proof state:
case h
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
x✝ : V
⊢ (DistribMulAction.toLinearMap k V a) x✝ = (a • LinearMap.id) x✝

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ (a • s).direction = s.direction

Tactic:
have : DistribMulAction.toLinearMap k V a = a • LinearMap.id := by
  ext; simp

Result:
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
this : DistribMulAction.toLinearMap k V a = a • LinearMap.id
⊢ (a • s).direction = s.direction

Proof state:
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ DistribMulAction.toLinearMap k V a = a • LinearMap.id

Tactic:
ext

Result:
case h
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
x✝ : V
⊢ (DistribMulAction.toLinearMap k V a) x✝ = (a • LinearMap.id) x✝

Proof state:
k : Type u_2
V : Type u_3
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
this : DistribMulAction.toLinearMap k V a = a • LinearMap.id
⊢ (a • s).direction = s.direction

Tactic:
simp [smul_eq_map, map_direction, this, Submodule.map_smul, ha]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
lemma mk_lt_mk_iff_of_comm {X A₁ A₂ : C} {i₁ : A₁ ⟶ X} {i₂ : A₂ ⟶ X} [Mono i₁] [Mono i₂]
    (f : A₁ ⟶ A₂) (fac : f ≫ i₂ = i₁) :
    Subobject.mk i₁ < Subobject.mk i₂ ↔ ¬ IsIso f :=
  ⟨fun h hf ↦ by simp only [mk_eq_mk_of_comm i₁ i₂ (asIso f) fac, lt_self_iff_false] at h,
    mk_lt_mk_of_comm f fac⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
h : mk i₁ < mk i₂
hf : IsIso f
⊢ False

Tactic:
simp only [mk_eq_mk_of_comm i₁ i₂ (asIso f) fac, lt_self_iff_false] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_inj_right {f : α → β} (w : ∀ x y, f x = f y → x = y) : map f l = map f l' ↔ l = l'

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ f a = f a' ↔ a = a'

Tactic:
constructor

Result:
case cons.cons.mp
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ f a = f a' → a = a'

case cons.cons.mpr
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ a = a' → f a = f a'

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
⊢ f a :: map f l = map f [] ↔ a :: l = []

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
⊢ f a :: map f l = map f (a' :: l') ↔ a :: l = a' :: l'

Tactic:
simp only [map_cons, cons.injEq, ih, and_congr_left_iff]

Result:
case cons.cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
⊢ l = l' → (f a = f a' ↔ a = a')

Proof state:
case cons.cons.mpr
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ a = a' → f a = f a'

Tactic:
simp +contextual

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
l' : List α
⊢ map f [] = map f l' ↔ [] = l'

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
⊢ l = l' → (f a = f a' ↔ a = a')

Tactic:
intro h

Result:
case cons.cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ f a = f a' ↔ a = a'

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
l' : List α
⊢ map f (a :: l) = map f l' ↔ a :: l = l'

Tactic:
simp only [map_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
l' : List α
⊢ f a :: map f l = map f l' ↔ a :: l = l'

Proof state:
case cons.cons.mp
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
l : List α
ih : ∀ {l' : List α}, map f l = map f l' ↔ l = l'
a' : α
l' : List α
h : l = l'
⊢ f a = f a' → a = a'

Tactic:
apply w

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualRestrict_comp_dualLift (W : Subspace K V) : W.dualRestrict.comp W.dualLift = 1

Proof state:
case h.h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K ↥W
x : ↥W
⊢ ((dualRestrict W ∘ₗ W.dualLift) φ) x = (1 φ) x

Tactic:
simp

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualRestrict W ∘ₗ W.dualLift = 1

Tactic:
ext φ x

Result:
case h.h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K ↥W
x : ↥W
⊢ ((dualRestrict W ∘ₗ W.dualLift) φ) x = (1 φ) x
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_monomial (N n : ℕ) : reflect N ((X : R[X]) ^ n) = X ^ revAt N n

Proof state:
R : Type u_1
inst✝ : Semiring R
N n : ℕ
⊢ reflect N (X ^ n) = X ^ (revAt N) n

Tactic:
rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_dirac {a : α} (f : α → ℝ≥0∞) (s : Set α) [MeasurableSingletonClass α]
    [Decidable (a ∈ s)] : ∫⁻ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Proof state:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

Tactic:
exact lintegral_dirac _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫⁻ (x : α), f x ∂dirac a = f a

case neg
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ ∫⁻ (x : α) in s, f x ∂dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac]

Result:
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
⊢ (∫⁻ (x : α), f x ∂if a ∈ s then dirac a else 0) = if a ∈ s then f a else 0

Proof state:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
a : α
f : α → ℝ≥0∞
s : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫⁻ (x : α), f x ∂0 = 0

Tactic:
exact lintegral_zero_measure _

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_bij_iff_rTensor_bij :
    Function.Bijective (lTensor M f) ↔ Function.Bijective (rTensor M f)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
⊢ Function.Bijective ⇑(lTensor M f) ↔ Function.Bijective ⇑(rTensor M f)

Tactic:
simp [← comm_comp_rTensor_comp_comm_eq]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivWithinAt.hasMFDerivAt (h : HasMFDerivWithinAt I I' f s x f') (hs : s ∈ 𝓝 x) :
    HasMFDerivAt I I' f x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
hs : s ∈ 𝓝 x
⊢ HasMFDerivAt I I' f x f'

Tactic:
rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findSomeRevM?_eq_findSomeM?_reverse
    [Monad m] [LawfulMonad m] (f : α → m (Option β)) (as : Array α) :
    as.findSomeRevM? f = as.reverse.findSomeM? f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
as : Array α
⊢ findSomeRevM? f as = findSomeM? f as.reverse

Tactic:
cases as

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toList✝ : List α
⊢ findSomeRevM? f { toList := toList✝ } = findSomeM? f { toList := toList✝ }.reverse

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toList✝ : List α
⊢ List.findSomeM? f toList✝.reverse = findSomeM? f { toList := toList✝ }.reverse

Tactic:
simp

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toList✝ : List α
⊢ findSomeRevM? f { toList := toList✝ } = findSomeM? f { toList := toList✝ }.reverse

Tactic:
rw [List.findSomeRevM?_toArray]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
toList✝ : List α
⊢ List.findSomeM? f toList✝.reverse = findSomeM? f { toList := toList✝ }.reverse
-- Mathlib/Analysis/Complex/Convex.lean
/-- A version of `convexHull_prod` for `Set.reProdIm`. -/
lemma convexHull_reProdIm (s t : Set ℝ) :
    convexHull ℝ (s ×ℂ t) = convexHull ℝ s ×ℂ convexHull ℝ t :=
  calc
    convexHull ℝ (equivRealProdLm ⁻¹' (s ×ˢ t)) = equivRealProdLm ⁻¹' convexHull ℝ (s ×ˢ t)

Proof state:
s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) s ×ˢ (convexHull ℝ) t = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

Tactic:
rfl

Result:
no goals

Proof state:
s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

Tactic:
rw [convexHull_prod]

Result:
s t : Set ℝ
⊢ ⇑equivRealProdLm ⁻¹' (convexHull ℝ) s ×ˢ (convexHull ℝ) t = (convexHull ℝ) s ×ℂ (convexHull ℝ) t

Proof state:
s t : Set ℝ
⊢ (convexHull ℝ) (⇑equivRealProdLm ⁻¹' s ×ˢ t) = ⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t)

Tactic:
simpa only [← LinearEquiv.image_symm_eq_preimage]
  using ((equivRealProdLm.symm.toLinearMap).image_convexHull (s ×ˢ t)).symm

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_union_add_inter' (hs : MeasurableSet s) (t : Set α) :
    μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_smul_left_self (x : V) {r : ℝ} : (2 : ℤ) • o.oangle (r • x) x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
⊢ 2 • o.oangle (r • x) x = 0

Tactic:
rcases lt_or_le r 0 with (h | h) <;> simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_insert_congr (he : e ∈ M.closure (insert f X) \ M.closure X) :
    M.closure (insert e X) = M.closure (insert f X)

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)

Tactic:
have hf := closure_exchange he

Result:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (insert e X) = M.closure (insert f X)

Tactic:
rw [eq_comm, ← closure_closure, ← insert_eq_of_mem he.1, closure_insert_closure_eq_closure_insert,
  insert_comm, ← closure_closure, ← closure_insert_closure_eq_closure_insert,
  insert_eq_of_mem hf.1, closure_closure, closure_closure]

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma IsWeaklyRegular.isWeaklyRegular_rTensor [Module.Flat R M₂]
    {rs : List R} (h : IsWeaklyRegular M rs) :
    IsWeaklyRegular (M ⊗[R] M₂) rs

Proof state:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (QuotSMulTop r N ⊗[R] M₂) rs'
e : QuotSMulTop r N ⊗[R] M₂ ≃ₗ[R] QuotSMulTop r (N ⊗[R] M₂) := quotSMulTopTensorEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')

Tactic:
exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module.Flat R M₂
rs : List R
h : IsWeaklyRegular M rs
⊢ IsWeaklyRegular (M ⊗[R] M₂) rs

Tactic:
induction h with
| nil N => exact nil R (N ⊗[R] M₂)
| @cons N _ _ r rs' h1 _ ih =>
  let e := quotSMulTopTensorEquivQuotSMulTop r M₂ N
  exact ((e.isWeaklyRegular_congr rs').mp ih).cons (h1.rTensor M₂)

Result:
no goals

Proof state:
case nil
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsWeaklyRegular (N ⊗[R] M₂) []

Tactic:
exact nil R (N ⊗[R] M₂)

Result:
no goals

Proof state:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (QuotSMulTop r N ⊗[R] M₂) rs'
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')

Tactic:
let e := quotSMulTopTensorEquivQuotSMulTop r M₂ N

Result:
case cons
R : Type u_1
M : Type u_3
M₂ : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module.Flat R M₂
rs : List R
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r : R
rs' : List R
h1 : IsSMulRegular N r
h2✝ : IsWeaklyRegular (QuotSMulTop r N) rs'
ih : IsWeaklyRegular (QuotSMulTop r N ⊗[R] M₂) rs'
e : QuotSMulTop r N ⊗[R] M₂ ≃ₗ[R] QuotSMulTop r (N ⊗[R] M₂) := quotSMulTopTensorEquivQuotSMulTop r M₂ N
⊢ IsWeaklyRegular (N ⊗[R] M₂) (r :: rs')
-- Mathlib/GroupTheory/Exponent.lean
theorem ExponentExists.of_finite : ExponentExists G

Proof state:
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩

Result:
case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf

case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1

Proof state:
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ ExponentExists G

Tactic:
let _inst := Fintype.ofFinite G

Result:
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ExponentExists G

Proof state:
case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf

Tactic:
simpa [pos_iff_ne_zero, Finset.lcm_eq_zero_iff] using fun x => (_root_.orderOf_pos x).ne'

Result:
no goals

Proof state:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, lcm_orderOf_eq_exponent]

Result:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G

Proof state:
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ExponentExists G

Tactic:
simp only [Monoid.ExponentExists]

Result:
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1

Proof state:
case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ orderOf g ∣ exponent G

Tactic:
exact order_dvd_exponent g

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma wInner_cWeight_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ : AddChar G R
⊢ wInner cWeight ⇑ψ ⇑ψ = 1

Tactic:
simp [wInner_cWeight_eq_expect, ψ.norm_apply, RCLike.conj_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem countP_attach (l : List α) (p : α → Bool) :
    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ countP (fun a => p a.val) l.attach = countP p l

Tactic:
simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attach_map_subtype_val]

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_prod (s : Finset ι) (f : ι → G → R) :
    conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i)

Proof state:
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
⊢ conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i)

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, conjneg (f i)) x✝

Proof state:
case h
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, conjneg (f i)) x✝

Tactic:
simp

Result:
no goals
-- 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 ∧ LiftPropWithinAt 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
h : ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
h1 : ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e.symm.symm x)
this : ContinuousAt (↑f) ((g ∘ ↑e.symm) (↑e x))
⊢ ContinuousWithinAt (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
exact this.comp_continuousWithinAt h1

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem pred_le_self (o) : pred o ≤ o

Proof state:
o : Ordinal.{u_4}
h : ¬∃ a, o = succ a
⊢ o.pred ≤ o

Tactic:
rw [pred, dif_neg h]

Result:
no goals

Proof state:
o : Ordinal.{u_4}
h : ∃ a, o = succ a
a : Ordinal.{u_4}
e : o = succ a
⊢ a ≤ succ a

Tactic:
exact le_succ a

Result:
no goals

Proof state:
o : Ordinal.{u_4}
h : ∃ a, o = succ a
a : Ordinal.{u_4}
e : o = succ a
⊢ o.pred ≤ o

Tactic:
rw [e, pred_succ]

Result:
o : Ordinal.{u_4}
h : ∃ a, o = succ a
a : Ordinal.{u_4}
e : o = succ a
⊢ a ≤ succ a

Proof state:
o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
classical
exact if h : ∃ a, o = succ a then by
  let ⟨a, e⟩ := h
  rw [e, pred_succ]; exact le_succ a
else by rw [pred, dif_neg h]

Result:
no goals

Proof state:
o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
exact if h : ∃ a, o = succ a then by
  let ⟨a, e⟩ := h
  rw [e, pred_succ]; exact le_succ a
else by rw [pred, dif_neg h]

Result:
no goals

Proof state:
o : Ordinal.{u_4}
h : ∃ a, o = succ a
⊢ o.pred ≤ o

Tactic:
let ⟨a, e⟩ := h

Result:
o : Ordinal.{u_4}
h : ∃ a, o = succ a
a : Ordinal.{u_4}
e : o = succ a
⊢ o.pred ≤ o
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem abs_dist_sub_le_dist_mul_mul (a₁ a₂ b₁ b₂ : E) :
    |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

Tactic:
simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
  abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblZ_smul (P : Fin 3 → R) (u : R) : W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblZ (u • P) = u ^ 4 * W'.dblZ P

Tactic:
simp only [dblZ, negY_smul, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ u * P z * (u * P y - u * W'.negY P) ^ 3 = u ^ 4 * (P z * (P y - W'.negY P) ^ 3)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ u * P z * (u * P y - u * W'.negY P) ^ 3 = u ^ 4 * (P z * (P y - W'.negY P) ^ 3)

Tactic:
ring1

Result:
no goals
-- Mathlib/CategoryTheory/Opposites.lean
theorem op_unop {X Y : C} (f : X ≅ Y) : f.op.unop = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop = f

Tactic:
ext

Result:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom

Proof state:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop = f

Tactic:
(ext; rfl)

Result:
no goals