harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Submonoid.lean
/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
and an element of `M` is contained in the additive closure of `M`. -/
lemma mul_right_mem_add_closure (ha : a ∈ closure (S : Set R)) (hb : b ∈ S) :
    a * b ∈ closure (S : Set R)

Proof state:
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
hb : b ∈ S
⊢ a * b ∈ closure ↑S

Tactic:
induction ha using closure_induction with
| mem r hr => exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
| one => simp only [zero_mul, zero_mem _]
| mul r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs

Result:
no goals

Proof state:
case mem
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r : R
hr : r ∈ ↑S
⊢ r * b ∈ closure ↑S

Tactic:
exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)

Result:
no goals

Proof state:
case mul
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
r s : R
hx✝ : r ∈ closure ↑S
hy✝ : s ∈ closure ↑S
hr : r * b ∈ closure ↑S
hs : s * b ∈ closure ↑S
⊢ (r + s) * b ∈ closure ↑S

Tactic:
simpa only [add_mul] using add_mem hr hs

Result:
no goals

Proof state:
case one
M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
hb : b ∈ S
⊢ 0 * b ∈ closure ↑S

Tactic:
simp only [zero_mul, zero_mem _]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem edist_triangle_right (x y z : α) : edist x y ≤ edist x z + edist y z

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y

Tactic:
apply edist_triangle

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z

Tactic:
rw [edist_comm y]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem b_pos : 0 < b

Proof state:
b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt.iter_sq_le (n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n

Proof state:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ n / guess

Tactic:
apply Nat.le_of_add_le_add_left (a := guess)

Result:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess + guess ≤ guess + n / guess

Proof state:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
simpa only [next, dif_pos h] using sqrt.iter_sq_le n next

Result:
no goals

Proof state:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess * guess ≤ n

Tactic:
apply Nat.mul_le_of_le_div

Result:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ n / guess

Proof state:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess + guess ≤ guess + n / guess

Tactic:
rw [← Nat.mul_two, ← le_div_iff_mul_le]

Result:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ (guess + n / guess) / 2

case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ 0 < 2

Proof state:
n guess : ℕ
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
let next := (guess + n / guess) / 2

Result:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Proof state:
n guess : ℕ
⊢ iter n guess * iter n guess ≤ n

Tactic:
unfold sqrt.iter

Result:
n guess : ℕ
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Proof state:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ ((let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) *
      let next := (guess + n / guess) / 2;
      if _h : next < guess then iter n next else guess) ≤
    n

Tactic:
simp only [next, dif_neg h]

Result:
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess * guess ≤ n

Proof state:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ guess ≤ (guess + n / guess) / 2

Tactic:
exact Nat.le_of_not_lt h

Result:
no goals

Proof state:
case h
n guess : ℕ
next : ℕ := (guess + n / guess) / 2
h : ¬next < guess
⊢ 0 < 2

Tactic:
exact Nat.zero_lt_two

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem subgroupOf_normalizer_eq {H N : Subgroup G} (h : H.normalizer ≤ N) :
    H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer

Proof state:
case hf
G : Type u_1
inst✝ : Group G
H N : Subgroup G
h : H.normalizer ≤ N
⊢ Injective ⇑N.subtype

Tactic:
exact Subtype.coe_injective

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H N : Subgroup G
h : H.normalizer ≤ N
⊢ H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer

Tactic:
apply comap_normalizer_eq_of_injective_of_le_range

Result:
case hf
G : Type u_1
inst✝ : Group G
H N : Subgroup G
h : H.normalizer ≤ N
⊢ Injective ⇑N.subtype

case h
G : Type u_1
inst✝ : Group G
H N : Subgroup G
h : H.normalizer ≤ N
⊢ H.normalizer ≤ N.subtype.range

Proof state:
case h
G : Type u_1
inst✝ : Group G
H N : Subgroup G
h : H.normalizer ≤ N
⊢ H.normalizer ≤ N.subtype.range

Tactic:
simpa

Result:
no goals
-- Mathlib/Order/DirectedInverseSystem.lean
theorem induction₃
    {C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop}
    (ih : ∀ i x y z, C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧) (x y z : DirectLimit F f) : C x y z

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
x y z : DirectLimit F f
⊢ C x y z

Tactic:
obtain ⟨_, _, _, _, rfl, rfl, rfl⟩ := exists_eq_mk₃ f x y z

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
w✝³ : ι
w✝² w✝¹ w✝ : F w✝³
⊢ C ⟦⟨w✝³, w✝²⟩⟧ ⟦⟨w✝³, w✝¹⟩⟧ ⟦⟨w✝³, w✝⟩⟧

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
w✝³ : ι
w✝² w✝¹ w✝ : F w✝³
⊢ C ⟦⟨w✝³, w✝²⟩⟧ ⟦⟨w✝³, w✝¹⟩⟧ ⟦⟨w✝³, w✝⟩⟧

Tactic:
apply ih

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_mk (a : Array α) (h : a.size = n) :
    (Vector.mk a h).reverse = Vector.mk a.reverse (by simp [h]) := rfl

Proof state:
α : Type ?u.13517
n : Nat
a : Array α
h : a.size = n
⊢ a.reverse.size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀)
    (hom : ∀ i j, C.X i ⟶ D.X j) :
    (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
dsimp only [nullHomotopicMap]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem lift_fac (H : Set.range g.base ⊆ Set.range f.base) : lift f g H ≫ f = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g

Tactic:
exact pullback.condition

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g

Tactic:
rw [IsIso.inv_comp_eq]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ lift f g H ≫ f = g

Tactic:
erw [Category.assoc]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := fun x ↦ by
  rw [← not_imp_not, nmem_support]
  exact fderiv_of_not_mem_tsupport _

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ x ∉ tsupport f → fderiv 𝕜 f x = 0

Tactic:
exact fderiv_of_not_mem_tsupport _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ x ∈ support (fderiv 𝕜 f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, nmem_support]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ x ∉ tsupport f → fderiv 𝕜 f x = 0
-- Mathlib/Algebra/Ring/Idempotent.lean
lemma add_sub_mul_of_commute (h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
    IsIdempotentElem (a + b - a * b)

Proof state:
R : Type u_1
inst✝ : Ring R
a b : R
h : Commute a b
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ Commute (1 - a) (1 - b)

Tactic:
simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : Ring R
a b : R
h : Commute a b
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ a + b - a * b = 1 - (1 - a) * (1 - b)

Tactic:
simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
a b : R
h : Commute a b
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ IsIdempotentElem (a + b - a * b)

Tactic:
convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1

Result:
case h.e'_3
R : Type u_1
inst✝ : Ring R
a b : R
h : Commute a b
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ a + b - a * b = 1 - (1 - a) * (1 - b)

R : Type u_1
inst✝ : Ring R
a b : R
h : Commute a b
hp : IsIdempotentElem a
hq : IsIdempotentElem b
⊢ Commute (1 - a) (1 - b)
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.equivFun_ofEquivFun [Finite ι] (e : M ≃ₗ[R] ι → R) :
    (Basis.ofEquivFun e).equivFun = e

Proof state:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ (ofEquivFun e).equivFun j x✝ = e j x✝

Tactic:
simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
⊢ (ofEquivFun e).equivFun = e

Tactic:
ext j

Result:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x✝ : ι
⊢ (ofEquivFun e).equivFun j x✝ = e j x✝
-- Mathlib/Topology/Homotopy/Path.lean
theorem hcomp_half (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (t : I) :
    F.hcomp G (t, ⟨1 / 2, by norm_num, by norm_num⟩) = x₁ :=
  show ite _ _ _ = _ by norm_num

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 1 / 2 ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ x₂ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
t : ↑I
⊢ (if ↑(t, ⟨1 / 2, ⋯⟩).2 ≤ 1 / 2 then (F.eval (t, ⟨1 / 2, ⋯⟩).1).extend (2 * ↑(t, ⟨1 / 2, ⋯⟩).2)
    else (G.eval (t, ⟨1 / 2, ⋯⟩).1).extend (2 * ↑(t, ⟨1 / 2, ⋯⟩).2 - 1)) =
    x₁

Tactic:
norm_num

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_natural_whiskerRight (f : A ⟶ A') :
    F.map (f ▷ B) ≫ prodComparison F A' B =
      prodComparison F A B ≫ (F.map f ▷ F.obj B)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ prodComparison F A B ≫ (F.map f ⊗ 𝟙 (F.obj B)) = prodComparison F A B ≫ F.map f ▷ F.obj B

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B

Tactic:
rw [← tensorHom_id, prodComparison_natural, Functor.map_id]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ prodComparison F A B ≫ (F.map f ⊗ 𝟙 (F.obj B)) = prodComparison F A B ≫ F.map f ▷ F.obj B
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f

Proof state:
case succ
n : Nat
ih : ∀ (f : Fin n → UInt8), (ofFn f).data = Array.ofFn f
f : Fin (n + 1) → UInt8
⊢ (ofFn f).data = Array.ofFn f

Tactic:
simp [ofFn_succ, Array.ofFn_succ, ih, Fin.last]

Result:
no goals

Proof state:
case zero
f : Fin 0 → UInt8
⊢ (ofFn f).data = Array.ofFn f

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
f : Fin n → UInt8
⊢ (ofFn f).data = Array.ofFn f

Tactic:
induction n with
| zero => rfl
| succ n ih => simp [ofFn_succ, Array.ofFn_succ, ih, Fin.last]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp] lemma mem_graphOn : x ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : α × β
⊢ x ∈ graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2

Tactic:
aesop (add simp graphOn)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Defs.lean
theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio

Proof state:
⊢ (range ofNNReal).OrdConnected

Tactic:
rw [range_coe']

Result:
⊢ (Iio ⊤).OrdConnected

Proof state:
⊢ (Iio ⊤).OrdConnected

Tactic:
exact ordConnected_Iio

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma max_left_comm (a b c : ℕ) : max a (max b c) = max b (max a c)

Proof state:
a b c : ℕ
⊢ max a (max b c) = max b (max a c)

Tactic:
rw [← Nat.max_assoc, ← Nat.max_assoc, b.max_comm]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_const_bot {f : Filter β} : limsup (fun _ : β => (⊥ : α)) f = (⊥ : α)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥

Tactic:
exact sInf_le (Eventually.of_forall fun _ => le_rfl)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x => ⊥) f = ⊥

Tactic:
rw [limsup_eq, eq_bot_iff]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
-- Mathlib/Data/Real/Irrational.lean
theorem div_nat (h : Irrational x) {m : ℕ} (hm : m ≠ 0) : Irrational (x / m) :=
  h.div_int <| by rwa [Int.natCast_ne_zero]

Proof state:
x : ℝ
h : Irrational x
m : ℕ
hm : m ≠ 0
⊢ ↑m ≠ 0

Tactic:
rwa [Int.natCast_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem foldr_toList (o : Option β) (a : α) (f : β → α → α) :
    o.toList.foldr f a = o.elim a (fun b => f b a)

Proof state:
β : Type u_1
α : Type u_2
o : Option β
a : α
f : β → α → α
⊢ List.foldr f a o.toList = o.elim a fun b => f b a

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Rank.lean
theorem IsWellFounded.rank_eq_typein (r) [IsWellOrder α r] : rank r = Ordinal.typein r

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ rank r = ⇑(Ordinal.typein r).toRelEmbedding

Tactic:
classical
letI := linearOrderOfSTO r
ext a
exact InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
  fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
⊢ rank r = ⇑(Ordinal.typein r).toRelEmbedding

Tactic:
ext a

Result:
case h
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
a : α
⊢ rank r a = (Ordinal.typein r).toRelEmbedding a

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ rank r = ⇑(Ordinal.typein r).toRelEmbedding

Tactic:
letI := linearOrderOfSTO r

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
⊢ rank r = ⇑(Ordinal.typein r).toRelEmbedding

Proof state:
case h
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
a : α
⊢ rank r a = (Ordinal.typein r).toRelEmbedding a

Tactic:
exact InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
  fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.exists_eq_add_of_fderiv_eq (hs : IsOpen s) (hs' : IsPreconnected s)
    (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s)
    (hf' : s.EqOn (fderiv 𝕜 f) (fderiv 𝕜 g)) : ∃ a, s.EqOn f (g · + a)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (fun x => f x - g x) x = 0 x

Tactic:
rw [fderiv_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
  hf' hx, sub_self, Pi.zero_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ a, ∀ ⦃x : E⦄, x ∈ s → f x - g x = a

Tactic:
refine hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
⊢ fderiv 𝕜 (fun x => f x - g x) x = 0 x

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ a, EqOn f (fun x => g x + a) s

Tactic:
simp_rw [Set.EqOn, ← sub_eq_iff_eq_add']

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ a, ∀ ⦃x : E⦄, x ∈ s → f x - g x = a
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
lemma pow_cpow_nat_inv {x : ℂ} {n : ℕ} (h₀ : n ≠ 0) (hlt : -(π / n) < x.arg) (hle : x.arg ≤ π / n) :
    (x ^ n) ^ (n⁻¹ : ℂ) = x

Proof state:
case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π

Tactic:
rwa [← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)]

Result:
no goals

Proof state:
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]

Result:
case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

case hle
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ ↑n * x.arg ≤ π

Proof state:
case hlt
x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ -π < ↑n * x.arg

Tactic:
rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]

Result:
no goals