harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem zero_add' (x : LocalizedModule S M) : 0 + x = x :=
  induction_on
    (fun m s => by
      rw [← zero_mk s, mk_add_mk, smul_zero, zero_add, mk_eq]
      exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩)
    x

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ 1 • s • s • m = 1 • (s * s) • m

Tactic:
rw [one_smul, mul_smul, one_smul]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ 0 + mk m s = mk m s

Tactic:
rw [← zero_mk s, mk_add_mk, smul_zero, zero_add, mk_eq]

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ ∃ u, u • s • s • m = u • (s * s) • m

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : LocalizedModule S M
m : M
s : ↥S
⊢ ∃ u, u • s • s • m = u • (s * s) • m

Tactic:
exact ⟨1, by rw [one_smul, mul_smul, one_smul]⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_blockDiagonal' (v : ∀ i, Matrix (n' i) (n' i) 𝔸) :
    exp 𝕂 (blockDiagonal' v) = blockDiagonal' (exp 𝕂 v)

Proof state:
𝕂 : Type u_1
m : Type u_2
n' : m → Type u_4
𝔸 : Type u_5
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
inst✝⁷ : (i : m) → Fintype (n' i)
inst✝⁶ : (i : m) → DecidableEq (n' i)
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra 𝕂 𝔸
inst✝ : T2Space 𝔸
v : (i : m) → Matrix (n' i) (n' i) 𝔸
⊢ exp 𝕂 (blockDiagonal' v) = blockDiagonal' (exp 𝕂 v)

Tactic:
simp_rw [exp_eq_tsum, ← blockDiagonal'_pow, ← blockDiagonal'_smul, ← blockDiagonal'_tsum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_dite_none_right {x : α} [Decidable p] {l : p → Option α} :
    (x ∈ if h : p then l h else none) ↔ ∃ h : p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : p → Option α
⊢ (x ∈ if h : p then l h else none) ↔ ∃ h, x ∈ l h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem cancel_left {g : β →+* γ} {f₁ f₂ : α →+* β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => RingHom.ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
g : β →+* γ
f₁ f₂ : α →+* β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
    (g₂ : Y₂ ⟶ Z₂) : tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂

Proof state:
case hf
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) = Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)

Tactic:
apply TensorProduct.ext

Result:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (mk R ↑X₁ ↑X₂).compr₂ (Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))) =
    (mk R ↑X₁ ↑X₂).compr₂ (Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂))

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (mk R ↑X₁ ↑X₂).compr₂ (Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))) =
    (mk R ↑X₁ ↑X₂).compr₂ (Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) = Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
-- Mathlib/Probability/Kernel/Basic.lean
lemma copy_apply (a : α) : copy α a = Measure.dirac (a, a)

Proof state:
α : Type u_1
mα : MeasurableSpace α
a : α
⊢ (copy α) a = Measure.dirac (a, a)

Tactic:
simp [copy, deterministic_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : Vector α n) (l₂ : Vector β n) :
    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Proof state:
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
n : Nat
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₁ : Vector α n
l₂ : Vector β n
⊢ zipWith f (map g l₁) (map h l₂) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith f (map g { toArray := l₁, size_toArray := ⋯ }) (map h l₂) =
    zipWith (fun a b => f (g a) (h b)) { toArray := l₁, size_toArray := ⋯ } l₂

Proof state:
case mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith f (map g { toArray := l₁, size_toArray := ⋯ }) (map h l₂) =
    zipWith (fun a b => f (g a) (h b)) { toArray := l₁, size_toArray := ⋯ } l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h✝ : β → δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith f (map g { toArray := l₁, size_toArray := ⋯ }) (map h✝ { toArray := l₂, size_toArray := h }) =
    zipWith (fun a b => f (g a) (h✝ b)) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Proof state:
case mk.mk
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h✝ : β → δ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith f (map g { toArray := l₁, size_toArray := ⋯ }) (map h✝ { toArray := l₂, size_toArray := h }) =
    zipWith (fun a b => f (g a) (h✝ b)) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Tactic:
simp [Array.zipWith_map]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem prod_map_id {α β : TypeVec n} : (@TypeVec.id _ α ⊗' @TypeVec.id _ β) = id

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec.{u_1} n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) a✝.fs
⊢ id a✝ x = id a✝.fs x

Tactic:
rfl

Result:
no goals

Proof state:
case a.h
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
x : (α ⊗ β) i
⊢ (id ⊗' id) i x = id i x

Tactic:
induction i <;> simp only [TypeVec.prod.map, *, dropFun_id]

Result:
case a.h.fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) Fin2.fz
⊢ (id Fin2.fz x.1, id Fin2.fz x.2) = id Fin2.fz x

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec.{u_1} n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) a✝.fs
⊢ id a✝ x = id a✝.fs x

Proof state:
n : ℕ
α β : TypeVec.{u_1} n
⊢ (id ⊗' id) = id

Tactic:
ext i x : 2

Result:
case a.h
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
x : (α ⊗ β) i
⊢ (id ⊗' id) i x = id i x

Proof state:
case a.h.fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) Fin2.fz
⊢ (id Fin2.fz x.1, id Fin2.fz x.2) = id Fin2.fz x

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec.{u_1} n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) a✝.fs
⊢ id a✝ x = id a✝.fs x

Tactic:
cases x

Result:
case a.h.fz.mk
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
fst✝ : α.last
snd✝ : β.last
⊢ (id Fin2.fz (fst✝, snd✝).1, id Fin2.fz (fst✝, snd✝).2) = id Fin2.fz (fst✝, snd✝)

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec.{u_1} n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec.{u_1} (n✝ + 1)
x : (α ⊗ β) a✝.fs
⊢ id a✝ x = id a✝.fs x

Proof state:
case a.h.fz.mk
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
fst✝ : α.last
snd✝ : β.last
⊢ (id Fin2.fz (fst✝, snd✝).1, id Fin2.fz (fst✝, snd✝).2) = id Fin2.fz (fst✝, snd✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_coe_angle_eq_iff {x y : ℂ} : (arg x : Real.Angle) = arg y ↔ arg x = arg y

Proof state:
x y : ℂ
⊢ ↑x.arg = ↑y.arg ↔ x.arg = y.arg

Tactic:
simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Linear.lean
/-- Given a Lie module `M` of a nilpotent Lie algebra `L` with coefficients in `R`,
if a function `χ : L → R` has a simultaneous generalized eigenvector for the action of `L`
then it has a simultaneous true eigenvector, provided `M` is Noetherian and has linear weights. -/
lemma exists_forall_lie_eq_smul [LinearWeights R L M] [IsNoetherian R M] (χ : Weight R L M) :
    ∃ m : M, m ≠ 0 ∧ ∀ x : L, ⁅x, m⁆ = χ x • m

Proof state:
case intro.mk.mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights R L M
inst✝ : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial ↥(shiftedGenWeightSpace R L M ⇑χ)
m : M
property✝ : m ∈ shiftedGenWeightSpace R L M ⇑χ
hm₁✝ : ⟨m, property✝⟩ ∈ maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M ⇑χ)
hm₂ : ⟨⟨m, property✝⟩, hm₁✝⟩ ≠ 0
hm₁ : ∀ (x : L), ↑⁅x, ⟨m, property✝⟩⁆ = 0
⊢ ∀ (x : L), ⁅x, m⁆ = χ x • m

Tactic:
intro x

Result:
case intro.mk.mk
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : LinearWeights R L M
inst✝ : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial ↥(shiftedGenWeightSpace R L M ⇑χ)
m : M
property✝ : m ∈ shiftedGenWeightSpace R L M ⇑χ
hm₁✝ : ⟨m, property✝⟩ ∈ maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M ⇑χ)
hm₂ : ⟨⟨m, property✝⟩, hm₁✝⟩ ≠ 0
hm₁ : ∀ (x : L), ↑⁅x, ⟨m, property✝⟩⁆ = 0
x : L
⊢ ⁅x, m⁆ = χ x • m
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem BinaryFan.isLimit_iff_isIso_snd {X Y : C} (h : IsTerminal X) (c : BinaryFan X Y) :
    Nonempty (IsLimit c) ↔ IsIso c.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))

Tactic:
exact
  ⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
    ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.snd

Tactic:
refine Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))
-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem coe_ofIsClosedGraph (hg : IsClosed (g.graph : Set <| E × F)) :
    ↑(ContinuousLinearMap.ofIsClosedGraph hg) = g

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
x✝ : E
⊢ ↑(ofIsClosedGraph hg) x✝ = g x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
⊢ ↑(ofIsClosedGraph hg) = g

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
g : E →ₗ[𝕜] F
hg : IsClosed ↑g.graph
x✝ : E
⊢ ↑(ofIsClosedGraph hg) x✝ = g x✝
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_baseChange : finrank R (R ⊗[S] M') = finrank S M'

Proof state:
R : Type u
S : Type u'
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : StrongRankCondition R
inst✝³ : StrongRankCondition S
inst✝² : Module S M'
inst✝¹ : Free S M'
inst✝ : Algebra S R
⊢ finrank R (R ⊗[S] M') = finrank S M'

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Iic_sub_one_eq_Iio (b : α) : Iic (b - 1) = Iio b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrderBot α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio b

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem val_dvd_le : ∀ a b : R, b ∣ a → a ≠ 0 → ¬a ≺ b
  | _, b, ⟨d, rfl⟩, ha => mul_left_not_lt b (mt (by rintro rfl; exact mul_zero _) ha)

Proof state:
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0

Tactic:
exact mul_zero _

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
b d : R
ha : b * d ≠ 0
⊢ d = 0 → b * d = 0

Tactic:
rintro rfl

Result:
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.eq_node' {s l x r} (h : @Sized α (node s l x r)) : node s l x r = .node' l x r

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ node s l x r = l.node' x r

Tactic:
rw [h.1]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma nat_le_ofENat {m : ℕ} {n : ℕ∞} : (m : Cardinal) ≤ n ↔ m ≤ n

Proof state:
m : ℕ
n : ℕ∞
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.multisetProd {s : Multiset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) ~[l] (fun x ↦ (s.map (g · x)).prod)

Proof state:
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
s : Multiset ι
f g : ι → α → β
h : ∀ i ∈ s, f i ~[l] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) ~[l] fun x => (Multiset.map (fun x_1 => g x_1 x) s).prod

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Result:
case intro
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l✝ : Filter α
f g : ι → α → β
l : List ι
h : ∀ i ∈ ↑l, f i ~[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) ~[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod

Proof state:
case intro
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l✝ : Filter α
f g : ι → α → β
l : List ι
h : ∀ i ∈ ↑l, f i ~[l✝] g i
⊢ (fun x => (Multiset.map (fun x_1 => f x_1 x) ↑l).prod) ~[l✝] fun x => (Multiset.map (fun x_1 => g x_1 x) ↑l).prod

Tactic:
exact listProd h

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem IsRelPrime.mul_dvd_of_left_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z)
    (hx : IsPrimal x) : x * y ∣ z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ x * y ∣ z

Tactic:
rw [mul_comm]

Result:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z

Tactic:
exact H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem conjugate' {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (star z * x * z)

Proof state:
R : Type u_1
inst✝¹ : Semigroup R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
⊢ IsSelfAdjoint (star z * x * z)

Tactic:
simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem bagInter_consecutive (n m l : Nat) :
    @List.bagInter ℕ instBEqOfDecidableEq (Ico n m) (Ico m l) = [] :=
  (bagInter_nil_iff_inter_nil _ _).2 (by convert inter_consecutive n m l)

Proof state:
n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
convert inter_consecutive n m l

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobjectMap_arrow {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g]
    (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
    imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ sq.right

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = (imageSubobject f).arrow ≫ sq.right

Tactic:
erw [image.map_ι, ← Category.assoc, imageSubobject_arrow]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ sq.right

Tactic:
simp only [imageSubobjectMap, Category.assoc, imageSubobject_arrow']

Result:
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = (imageSubobject f).arrow ≫ sq.right
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma basicOpen_subset_freeLocus_iff [Module.FinitePresentation R M] {f : R} :
    (basicOpen f : Set (PrimeSpectrum R)) ⊆ freeLocus R M ↔
      Module.Projective (Localization.Away f) (LocalizedModule (.powers f) M)

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
f : R
⊢ ↑(basicOpen f) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule (Submonoid.powers f) M)

Tactic:
rw [← freeLocus_eq_univ_iff, freeLocus_localization,
  Set.preimage_eq_univ_iff, localization_away_comap_range _ f]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem continuousOn_iff_lower_upperSemicontinuousOn {f : α → γ} :
    ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
exact
  ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s

Tactic:
simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ (∀ x ∈ s, LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x) ↔
    LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
-- Mathlib/Data/PEquiv.lean
theorem single_trans_of_mem (a : α) {b : β} {c : γ} {f : β ≃. γ} (h : c ∈ f b) :
    (single a b).trans f = single a c

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
⊢ (single a b).trans f = single a c

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ ((single a b).trans f) x✝ ↔ a✝ ∈ (single a c) x✝

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ ((single a b).trans f) x✝ ↔ a✝ ∈ (single a c) x✝

Tactic:
dsimp [single, PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ (if x✝ = a then some b else none).bind ⇑f ↔ a✝ ∈ if x✝ = a then some c else none

Proof state:
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
x✝ : α
a✝ : γ
⊢ a✝ ∈ (if x✝ = a then some b else none).bind ⇑f ↔ a✝ ∈ if x✝ = a then some c else none

Tactic:
split_ifs <;> simp_all

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ite_one_prod (p : Prop) [Decidable p] (s : Finset α) (f : α → β) :
    (if p then 1 else (∏ x ∈ s, f x)) = ∏ x ∈ s, if p then 1 else f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
p : Prop
inst✝ : Decidable p
s : Finset α
f : α → β
⊢ (if p then 1 else ∏ x ∈ s, f x) = ∏ x ∈ s, if p then 1 else f x

Tactic:
simp only [prod_ite_irrel, prod_const_one]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.of_comp {f : α → β} {g : β → γ} (hf : UniformContinuous f)
    (hg : UniformContinuous g) (hgf : IsUniformInducing (g ∘ f)) : IsUniformInducing f

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))

Tactic:
exact comap_mono hg.le_comap

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ IsUniformInducing f

Tactic:
refine ⟨le_antisymm ?_ hf.le_comap⟩

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (fun x => (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (fun x => (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α

Tactic:
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : IsUniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem card_eq [Fintype V] [Fintype W] : Fintype.card V = Fintype.card W

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card W = Fintype.card W

Tactic:
convert rfl

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card V = Fintype.card W

Tactic:
rw [← Fintype.ofEquiv_card f.toEquiv]

Result:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ Fintype.card W = Fintype.card W