harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
theorem preservesColimitIso_inv_comp_desc (t : Cocone F) :
    (preservesColimitIso G F).inv ≫ G.map (colimit.desc _ t) =
    colimit.desc _ (G.mapCocone t)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)

Proof state:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝² : Category.{w', w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F G
inst✝ : HasColimit F
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)

Tactic:
simp [← G.map_comp]

Result:
no goals
-- Mathlib/Data/Pi/Interval.lean
lemma card_Ioi : #(Ioi a) = ∏ i, #(Ici (a i)) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
a : (i : ι) → α i
⊢ #(Ioi a) = ∏ i : ι, #(Ici (a i)) - 1

Tactic:
rw [card_Ioi_eq_card_Ici_sub_one, card_Ici]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem OneHom.cancel_left [One M] [One N] [One P] {g : OneHom N P} {f₁ f₂ : OneHom M N}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => OneHom.ext fun x => hg <| by rw [← OneHom.comp_apply, h, OneHom.comp_apply],
    fun h => h ▸ rfl⟩

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← OneHom.comp_apply, h, OneHom.comp_apply]

Result:
no goals
-- Mathlib/Order/Height.lean
theorem chainHeight_eq_top_iff : s.chainHeight = ⊤ ↔ ∀ n, ∃ l ∈ s.subchain, length l = n

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
⊢ s.chainHeight = ⊤ ↔ ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n

Tactic:
refine ⟨fun h n ↦ le_chainHeight_iff.1 (le_top.trans_eq h.symm), fun h ↦ ?_⟩

Result:
α : Type u_1
inst✝ : LT α
s : Set α
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
⊢ s.chainHeight = ⊤

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
h : s.chainHeight ≠ ⊤
⊢ ∃ n, ∀ l ∈ s.subchain, l.length ≠ n

Tactic:
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.1 h

Result:
case intro
α : Type u_1
inst✝ : LT α
s : Set α
h : s.chainHeight ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight
⊢ ∃ n, ∀ l ∈ s.subchain, l.length ≠ n

Proof state:
case intro
α : Type u_1
inst✝ : LT α
s : Set α
h : s.chainHeight ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight
⊢ ∃ n, ∀ l ∈ s.subchain, l.length ≠ n

Tactic:
exact ⟨n + 1, fun l hs ↦ (Nat.lt_succ_iff.2 <| Nat.cast_le.1 <|
  (length_le_chainHeight_of_mem_subchain hs).trans_eq hn.symm).ne⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
h : ∀ (n : ℕ), ∃ l ∈ s.subchain, l.length = n
⊢ s.chainHeight = ⊤

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝ : LT α
s : Set α
h : s.chainHeight ≠ ⊤
⊢ ∃ n, ∀ l ∈ s.subchain, l.length ≠ n
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_eq' (absorbs : Absorbent ℝ s) (a : ℝ) :
    { x | gauge s x < a } = ⋃ (r : ℝ) (_ : 0 < r) (_ : r < a), r • s

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s

Tactic:
exact
  ⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
    (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
⊢ {x | gauge s x < a} = ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s

Tactic:
ext

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r, ⋃ (_ : 0 < r), ⋃ (_ : r < a), r • s

Tactic:
simp_rw [mem_setOf, mem_iUnion, exists_prop]

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_inv : SameCycle f⁻¹ x y ↔ SameCycle f x y :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [SameCycle]

Proof state:
α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f⁻¹ ^ (Equiv.symm (Equiv.neg ℤ)) b) x = y) ↔ f.SameCycle x y

Tactic:
simp [SameCycle]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
lemma commute_of_mem_adjoin_of_forall_mem_commute {a b : A} {s : Set A}
    (hb : b ∈ adjoin R s) (h : ∀ b ∈ s, Commute a b) (h_star : ∀ b ∈ s, Commute a (star b)) :
    Commute a b :=
  NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute hb fun b hb ↦
    hb.elim (h b) (by simpa using h_star (star b))

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
a b✝ : A
s : Set A
hb✝ : b✝ ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
h_star : ∀ b ∈ s, Commute a (star b)
b : A
hb : b ∈ s ∪ star s
⊢ b ∈ star s → Commute a b

Tactic:
simpa using h_star (star b)

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem geom_series_mul_one_add (x : R) (h : ‖x‖ < 1) :
    (1 + x) * ∑' i : ℕ, x ^ i = 2 * ∑' i : ℕ, x ^ i - 1

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

Tactic:
rw [add_mul, one_mul, geom_series_mul_shift x h, geom_series_succ x h, two_mul, add_sub_assoc]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
private lemma lipschitzWith_one_equiv_prod_aux : LipschitzWith 1 (equiv (E × F)) :=
  AddMonoidHomClass.lipschitz_of_bound_nnnorm (linearEquiv ℂ (E × F)) 1 <| by
    simpa using norm_equiv_le_norm_prod

Proof state:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul Aᵐᵒᵖ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul Aᵐᵒᵖ F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
⊢ ∀ (x : C⋆ᵐᵒᵈ (E × F)), ‖(linearEquiv ℂ (E × F)) x‖₊ ≤ 1 * ‖x‖₊

Tactic:
simpa using norm_equiv_le_norm_prod

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblZ_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.dblZ P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblZ P = 0

Tactic:
rw [dblZ, hPz, zero_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/
lemma isEquivalence_of_comp_right {E : Type*} [Category E] (F : C ⥤ D) (G : D ⥤ E)
    [IsEquivalence G] [IsEquivalence (F ⋙ G)] : IsEquivalence F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence

Tactic:
exact ((F ⋙ G).asEquivalence.trans G.asEquivalence.symm).isEquivalence_functor

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatMap_id (l : Array (Array α)) : l.flatMap id = l.flatten

Proof state:
α : Type u_1
l : Array (Array α)
⊢ flatMap id l = l.flatten

Tactic:
simp [flatMap_def]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma lintegral_condKernel (hf : Measurable f) (a : α) :
    ∫⁻ b, ∫⁻ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a) = ∫⁻ x, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [Kernel.lintegral_compProd _ _ _ hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂(κ.fst ⊗ₖ κ.condKernel) a
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem resolventSet_of_subsingleton [Subsingleton A] (a : A) : resolventSet R a = Set.univ

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ

Tactic:
simp_rw [resolventSet, Subsingleton.elim (algebraMap R A _ - a) 1, isUnit_one, Set.setOf_true]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictMono.mem_upperBounds_image (hf : StrictMono f) :
    f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ f a ∈ upperBounds (f '' s) ↔ a ∈ upperBounds s

Tactic:
simp [upperBounds, hf.le_iff_le]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ici_eq_Ici_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
    (has_least_elem : (⨅ i, f i) ∈ range f) : ⋃ i : ι, Ici (f i) = Ici (⨅ i, f i)

Proof state:
ι : Sort u
R : Type u_1
inst✝ : CompleteLinearOrder R
f : ι → R
has_least_elem : ⨅ i, f i ∈ range f
⊢ ⋃ i, Ici (f i) = Ici (⨅ i, f i)

Tactic:
simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
  iUnion_exists, iUnion_iUnion_eq']

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
lemma toFinset_card_eq_one_iff (s : Multiset α) :
    #s.toFinset = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a : α, s = Multiset.card s • {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #s.toFinset = 1 ↔ s.card ≠ 0 ∧ ∃ a, s = s.card • {a}

Tactic:
simp_rw [Finset.card_eq_one, Multiset.toFinset_eq_singleton_iff, exists_and_left]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
@[simp] lemma LieModuleEquiv.range_coe {M' : Type*}
    [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') :
    LieModuleHom.range (e : M →ₗ⁅R,L⁆ M') = ⊤

Proof state:
R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective ⇑e.toLieModuleHom

Tactic:
exact e.surjective

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤

Tactic:
rw [LieModuleHom.range_eq_top]

Result:
R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ Function.Surjective ⇑e.toLieModuleHom
-- Mathlib/MeasureTheory/Measure/Restrict.lean
lemma comap_restrict (μ : Measure β) (s : Set β) :
    (μ.restrict s).comap f = (μ.comap f).restrict (f ⁻¹' s)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ Measure.comap f (μ.restrict s) = (Measure.comap f μ).restrict (f ⁻¹' s)

Tactic:
ext t ht

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
⊢ (Measure.comap f (μ.restrict s)) t = ((Measure.comap f μ).restrict (f ⁻¹' s)) t

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
⊢ (Measure.comap f (μ.restrict s)) t = ((Measure.comap f μ).restrict (f ⁻¹' s)) t

Tactic:
rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,
  Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Zero.lean
lemma isNilpotent_iff_charpoly (φ : End R M) :
    IsNilpotent φ ↔ charpoly φ = X ^ finrank R M :=
  ⟨IsNilpotent.charpoly_eq_X_pow_finrank,
    fun h ↦ ⟨finrank R M, by rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]⟩⟩

Proof state:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : charpoly φ = X ^ finrank R M
⊢ φ ^ finrank R M = 0

Tactic:
rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]

Result:
no goals
-- Mathlib/Algebra/Field/Defs.lean
theorem smul_one_eq_cast (A : Type*) [DivisionRing A] (m : ℚ) : m • (1 : A) = ↑m

Proof state:
A : Type u_2
inst✝ : DivisionRing A
m : ℚ
⊢ m • 1 = ↑m

Tactic:
rw [Rat.smul_def, mul_one]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasFDerivAt.inner (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) :
    HasFDerivAt (fun t => ⟪f t, g t⟫) ((fderivInnerCLM 𝕜 (f x, g x)).comp <| f'.prod g') x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
f' g' : G →L[ℝ] E
x : G
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (fun t => Inner.inner (f t) (g t)) ((fderivInnerCLM 𝕜 (f x, g x)).comp (f'.prod g')) x

Tactic:
exact isBoundedBilinearMap_inner (𝕜 := 𝕜) (E := E)
  |>.hasFDerivAt (f x, g x) |>.comp x (hf.prod hg)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
    k ∈ m.alter k f ↔ (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
⊢ k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

Tactic:
rw [mem_iff_contains, contains_alter_self]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem comap_zero : comap (0 : M →ₛₗ[σ₁₂] M₂) q = ⊤ :=
  ext <| by simp

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ ∀ (x : M), x ∈ comap 0 q ↔ x ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.inj {f} (H : IsNormal f) {a b} : f a = f b ↔ a = b

Proof state:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
a b : Ordinal.{u_4}
⊢ f a = f b ↔ a = b

Tactic:
simp only [le_antisymm_iff, H.le_iff]

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem noncommPiCoprod_mulSingle [DecidableEq ι]
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y}(i : ι) (y : H i) :
    noncommPiCoprod hcomm (Pi.mulSingle i y) = y

Proof state:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i : ι
y : ↥(H i)
⊢ (noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y

Tactic:
apply MonoidHom.noncommPiCoprod_mulSingle

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel`. -/
lemma inv_mul_le_one : a⁻¹ * a ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a : α
⊢ a⁻¹ * a ≤ 1

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem disjoint_principal_left {f : Filter α} {s : Set α} : Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Proof state:
α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint (𝓟 s) f ↔ sᶜ ∈ f

Tactic:
rw [disjoint_comm, disjoint_principal_right]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iSup₂ (f : ∀ i, κ i → LowerSet α) :
    (↑(⨆ (i) (j), f i j) : Set α) = ⋃ (i) (j), f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → LowerSet α
⊢ ↑(⨆ i, ⨆ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)

Tactic:
simp_rw [coe_iSup]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma iIndepFun_zero_right {β : ι → Type*} {m : ∀ x : ι, MeasurableSpace (β x)}
    {f : ∀ x : ι, Ω → β x} : iIndepFun m f κ 0

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
⊢ iIndepFun m f κ 0

Tactic:
simp [iIndepFun]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem r_one_pow (k : ℕ) : (r 1 : DihedralGroup n) ^ k = r k

Proof state:
n k : ℕ
⊢ r 1 ^ k = r ↑k

Tactic:
simp only [r_pow, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[simp]
lemma map_add_hom_app (a b : A) (X : C) :
    F.map ((add hF s i a b).hom.app X) =
      (i (a + b)).hom.app X ≫ (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
        ((i a).inv.app X)⟦b⟧' ≫ (i b).inv.app ((s a).obj X)

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((i (a + b)).hom.app X ≫
          (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
            𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X))) ≫
              (shiftFunctor D b).map ((i a).inv.app X) ≫
                𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X))) ≫
                  (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
dsimp [add]

Result:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((i (a + b)).hom.app X ≫
          (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
            𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X))) ≫
              (shiftFunctor D b).map ((i a).inv.app X) ≫
                𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X))) ≫
                  (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_eq_mk_iff {a c : M} {b d : S} : mk a b = mk c d ↔ r S ⟨a, b⟩ ⟨c, d⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a c : M
b d : ↥S
⊢ (∃ u v, u • c = v • a ∧ ↑u * ↑d = v * ↑b) ↔ (OreLocalization.oreEqv S M) (a, b) (c, d)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a c : M
b d : ↥S
⊢ mk a b = mk c d ↔ (r S) (a, b) (c, d)

Tactic:
rw [mk, mk, OreLocalization.oreDiv_eq_iff, r_iff_oreEqv_r]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
a c : M
b d : ↥S
⊢ (∃ u v, u • c = v • a ∧ ↑u * ↑d = v * ↑b) ↔ (OreLocalization.oreEqv S M) (a, b) (c, d)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_smul (c : ℝ) (x : mixedSpace K) :
    convexBodySumFun (c • x) = |c| * convexBodySumFun x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ convexBodySumFun (c • x) = |c| * convexBodySumFun x

Tactic:
simp_rw [convexBodySumFun, normAtPlace_smul, ← mul_assoc, mul_comm, Finset.mul_sum, mul_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem R_mul {G : Type*} [Semigroup G] [TopologicalSpace G] [ChartedSpace H G] [ContMDiffMul I ∞ G]
    (g h : G) : 𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g)

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑹 I (g * h)) x✝ = ((𝑹 I h).comp (𝑹 I g)) x✝

Tactic:
simp only [ContMDiffMap.comp_apply, R_apply, mul_assoc]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h : G
⊢ 𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑹 I (g * h)) x✝ = ((𝑹 I h).comp (𝑹 I g)) x✝