harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma singularPart_eq_self [μ.HaveLebesgueDecomposition ν] : μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Tactic:
refine ⟨fun h ↦ ?_, fun  h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = μ
⊢ μ ⟂ₘ ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ μ.singularPart ν = μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = μ
⊢ μ ⟂ₘ ν

Tactic:
rw [← h]

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = μ
⊢ μ.singularPart ν ⟂ₘ ν

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ μ.singularPart ν = μ

Tactic:
conv_rhs => rw [h_dec]

Result:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = μ
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

Tactic:
simp [mem_iff_contains, contains_insertIfNew h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem nonzeroMinimum_le {xs : List Nat} (m : a ∈ xs) (h : a ≠ 0) : xs.nonzeroMinimum ≤ a

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h✝ : ¬a = 0
m? : Option Nat
h : (filter (fun x => decide (x ≠ 0)) xs).min? = m?
w : 0 < m?.getD 0
⊢ m? = some (m?.getD 0)

Tactic:
match m?, w with
| some m?, _ => rfl

Result:
no goals

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h✝ : ¬a = 0
m?✝ : Option Nat
w : 0 < m?✝.getD 0
m? : Nat
x✝ : 0 < (some m?).getD 0
h : (filter (fun x => decide (x ≠ 0)) xs).min? = some m?
⊢ some m? = some ((some m?).getD 0)

Tactic:
rfl

Result:
no goals

Proof state:
case a
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ a ∈ xs ∧ ¬a = 0

Tactic:
exact ⟨m, h⟩

Result:
no goals

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
w : 0 < xs.nonzeroMinimum
⊢ (filter (fun x => decide (x ≠ 0)) xs).min? = some xs.nonzeroMinimum

Tactic:
dsimp [nonzeroMinimum] at *

Result:
a : Nat
xs : List Nat
m : a ∈ xs
h : ¬a = 0
w : 0 < (filter (fun x => decide ¬x = 0) xs).min?.getD 0
⊢ (filter (fun x => decide ¬x = 0) xs).min? = some ((filter (fun x => decide ¬x = 0) xs).min?.getD 0)

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this : (filter (fun x => decide (x ≠ 0)) xs).min? = some xs.nonzeroMinimum
⊢ xs.nonzeroMinimum ≤ a

Tactic:
rw [min?_eq_some_iff''] at this

Result:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ xs.nonzeroMinimum ≤ a

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ xs.nonzeroMinimum ≤ a

Tactic:
apply this.2

Result:
case a
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ a ∈ filter (fun x => decide (x ≠ 0)) xs

Proof state:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
⊢ (filter (fun x => decide (x ≠ 0)) xs).min? = some xs.nonzeroMinimum

Tactic:
have w := nonzeroMinimum_pos m h

Result:
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
w : 0 < xs.nonzeroMinimum
⊢ (filter (fun x => decide (x ≠ 0)) xs).min? = some xs.nonzeroMinimum

Proof state:
case a
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ a ∈ filter (fun x => decide (x ≠ 0)) xs

Tactic:
simp [List.mem_filter]

Result:
case a
a : Nat
xs : List Nat
m : a ∈ xs
h : a ≠ 0
this :
  xs.nonzeroMinimum ∈ filter (fun x => decide (x ≠ 0)) xs ∧
    ∀ (b : Nat), b ∈ filter (fun x => decide (x ≠ 0)) xs → xs.nonzeroMinimum ≤ b
⊢ a ∈ xs ∧ ¬a = 0
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image_diff {t : Set α} (h : s.InjOn f) : f '' (s \ t) = f '' s \ f '' (s ∩ t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)

Tactic:
rw [← image_union, inter_union_diff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' (s \ t) = f '' s \ f '' (s ∩ t)

Tactic:
refine subset_antisymm (subset_diff.2 ⟨image_subset f diff_subset, ?_⟩)
  (diff_subset_iff.2 (by rw [← image_union, inter_union_diff]))

Result:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))

Tactic:
exact Disjoint.image disjoint_sdiff_inter h diff_subset inter_subset_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
    (h2 : ∀ j (hji : j ≤ i), ¬p (xs[j]'(Nat.lt_of_le_of_lt hji h))) : i < xs.findIdx p

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : ¬i < findIdx p xs
⊢ False

Tactic:
simp only [Nat.not_lt] at f

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : findIdx p xs ≤ i
⊢ False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : findIdx p xs ≤ i
⊢ False

Tactic:
exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)

Result:
no goals

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ ¬i < findIdx p xs → False

Tactic:
intro f

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : ¬i < findIdx p xs
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ i < findIdx p xs

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ ¬i < findIdx p xs → False
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem indicator_ae_eq_restrict_compl (hs : MeasurableSet s) :
    indicator s f =ᵐ[μ.restrict sᶜ] 0

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
exact piecewise_ae_eq_restrict_compl hs

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict sᶜ)] 0

Tactic:
classical exact piecewise_ae_eq_restrict_compl hs

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem floor_def' (a : ℚ) : a.floor = a.num / a.den

Proof state:
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den

Tactic:
split

Result:
case isTrue
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den

case isFalse
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den

Proof state:
a : ℚ
⊢ a.floor = a.num / ↑a.den

Tactic:
rw [Rat.floor]

Result:
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den

Proof state:
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den

Tactic:
next => rfl

Result:
no goals

Proof state:
case isTrue
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den

Tactic:
next h => simp [h]

Result:
no goals

Proof state:
a : ℚ
h : a.den = 1
⊢ a.num = a.num / ↑a.den

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp 1100, norm_cast]
lemma nnnorm_nnratCast (q : ℚ≥0) : ‖(q : ℝ)‖₊ = q

Proof state:
q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
simp [nnnorm, -norm_eq_abs]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem submodule_map_mul_reverse (p q : Submodule R (CliffordAlgebra Q)) :
    (p * q).map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      q.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) *
        p.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.map reverse (p * q) = Submodule.map reverse q * Submodule.map reverse p

Tactic:
simp_rw [reverse, Submodule.map_comp, Submodule.map_mul, Submodule.map_unop_mul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem swap_mul_swap_same_mem_closure_three_cycles {a b c : α} (ab : a ≠ b) (ac : a ≠ c) :
    swap a b * swap a c ∈ closure { σ : Perm α | IsThreeCycle σ }

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : ¬b = c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

Tactic:
exact subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab ac : a ≠ b
⊢ swap a b * swap a b ∈ closure {σ | σ.IsThreeCycle}

Tactic:
simp [one_mem]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

Tactic:
by_cases bc : b = c

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b = c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : ¬b = c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b = c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

Tactic:
subst bc

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab ac : a ≠ b
⊢ swap a b * swap a b ∈ closure {σ | σ.IsThreeCycle}
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_orderOf_iff {H : Type*} [Monoid H] {y : H} :
    orderOf x = orderOf y ↔ ∀ n : ℕ, x ^ n = 1 ↔ y ^ n = 1

Proof state:
G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Tactic:
simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Resolution.lean
lemma essSurj_of_hasRightResolutions [Φ.HasRightResolutions] : (Φ.functor ⋙ L₂).EssSurj where
  mem_essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have := Localization.essSurj L₂ W₂

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have R : Φ.RightResolution (L₂.objPreimage X₂) := Classical.arbitrary _

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
this : L₂.EssSurj
R : Φ.RightResolution (L₂.objPreimage X₂)
⊢ (Φ.functor ⋙ L₂).essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
X₂ : D₂
this : L₂.EssSurj
R : Φ.RightResolution (L₂.objPreimage X₂)
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
exact ⟨R.X₁, ⟨(Localization.isoOfHom L₂ W₂ _ R.hw).symm ≪≫ L₂.objObjPreimageIso X₂⟩⟩

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_δ_snd (X Y : C) : (δ (prod' F G) X Y).2 = δ G X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).2 = δ G X Y

Tactic:
change G.map (𝟙 _) ≫ _ = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ G.map (𝟙 ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ G.map (𝟙 ((diag C).obj (X ⊗ Y)).2) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Tactic:
rw [Functor.map_id, Category.id_comp]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma slope_lt_of_hasDerivWithinAt (hfc : StrictConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hfd : HasDerivWithinAt f f' S x) :
    slope f x y < f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hfd : HasDerivWithinAt f f' S x
⊢ slope f x y < f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
  neg_lt_neg (hfc.neg.lt_slope_of_hasDerivWithinAt hx hy hxy hfd.neg)

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem Topology.IsEmbedding.separableSpace
    [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) :
    TopologicalSpace.SeparableSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
this : SecondCountableTopology α
⊢ SeparableSpace α

Tactic:
exact SecondCountableTopology.to_separableSpace

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
⊢ SeparableSpace α

Tactic:
have := hf.secondCountableTopology

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
this : SecondCountableTopology α
⊢ SeparableSpace α
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
lemma apply_eq_apply_of_inseparable {F : Type*} [FunLike F M N] [AddMonoidHomClass F M N] (f : F)
    (hf : ∀ x, ‖x‖ = 0 → f x = 0) : ∀ x y, Inseparable x y → f x = f y :=
  fun x y h ↦ eq_of_sub_eq_zero <| by
    rw [← map_sub]
    rw [Metric.inseparable_iff, dist_eq_norm] at h
    exact hf (x - y) h

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f (x - y) = 0

Tactic:
rw [Metric.inseparable_iff, dist_eq_norm] at h

Result:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : ‖x - y‖ = 0
⊢ f (x - y) = 0

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f x - f y = 0

Tactic:
rw [← map_sub]

Result:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : Inseparable x y
⊢ f (x - y) = 0

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
F : Type u_3
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
x y : M
h : ‖x - y‖ = 0
⊢ f (x - y) = 0

Tactic:
exact hf (x - y) h

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) : n ! * n ^ (m - n) ≤ m !

Proof state:
n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !

Tactic:
calc
  _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
  _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Result:
no goals

Proof state:
n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !

Tactic:
simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
/-- See `isUnit_iff_exists_and_exists` for a similar lemma with two existentials. -/
@[to_additive "See `isAddUnit_iff_exists_and_exists` for a similar lemma with two existentials."]
lemma isUnit_iff_exists [Monoid M] {x : M} : IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x✝ : IsUnit ↑u
⊢ ∃ b, ↑u * b = 1 ∧ b * ↑u = 1

Tactic:
exact ⟨u.inv, u.val_inv, u.inv_val⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : IsUnit x
u : Mˣ
hu : ↑u = x
⊢ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
subst x

Result:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x✝ : IsUnit ↑u
⊢ ∃ b, ↑u * b = 1 ∧ b * ↑u = 1

Proof state:
M : Type u_1
inst✝ : Monoid M
x : M
⊢ IsUnit x ↔ ∃ b, x * b = 1 ∧ b * x = 1

Tactic:
refine ⟨fun ⟨u, hu⟩ => ?_, fun ⟨b, h1b, h2b⟩ => ⟨⟨x, b, h1b, h2b⟩, rfl⟩⟩

Result:
M : Type u_1
inst✝ : Monoid M
x : M
x✝ : IsUnit x
u : Mˣ
hu : ↑u = x
⊢ ∃ b, x * b = 1 ∧ b * x = 1
-- Mathlib/Tactic/Ring/Basic.lean
theorem smul_eq_cast {a : ℕ} (_ : ((a : ℕ) : R) = a') (_ : a' * b = c) : a • b = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a' b c : R
a : ℕ
x✝¹ : ↑a = a'
x✝ : a' * b = c
⊢ a • b = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
b : R
a : ℕ
⊢ a • b = ↑a * b

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b : R
a : ℕ
⊢ a • b = ↑a * b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
/-- In `Fin n`, all elements are even for odd `n`,
otherwise an element is even iff its `Fin.val` value is even. -/
lemma even_iff {n : ℕ} {k : Fin n} : Even k ↔ (Odd n ∨ Even k.val)

Proof state:
n : ℕ
k : Fin n
hk : Even k
⊢ Even n → Even ↑k

Tactic:
exact fun hn ↦ (even_iff_of_even hn).mp hk

Result:
no goals

Proof state:
n : ℕ
k : Fin n
hk : Even k
⊢ Odd n ∨ Even ↑k

Tactic:
rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]

Result:
n : ℕ
k : Fin n
hk : Even k
⊢ Even n → Even ↑k
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_induction_right {s : Set M} {p : (m : M) → m ∈ closure s → Prop}
    (one : p 1 (one_mem _))
    (mul_right : ∀ x hx, ∀ (y) (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
    {x : M} (h : x ∈ closure s) : p x h :=
  closure_induction_left (s := MulOpposite.unop ⁻¹' s)
    (p := fun m hm => p m.unop <| by rwa [← op_closure] at hm)
    one
    (fun _x hx _y _ => mul_right _ _ _ hx)
    (by rwa [← op_closure])

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), p x hx → p (x * y) ⋯
x : M
h : x ∈ closure s
⊢ { unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)

Tactic:
rwa [← op_closure]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), p x hx → p (x * y) ⋯
x : M
h : x ∈ closure s
m : Mᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
rwa [← op_closure] at hm

Result:
no goals