harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem one_le_tprod (h : ∀ i, 1 ≤ g i) : 1 ≤ ∏' i, g i

Proof state:
case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

Tactic:
rw [tprod_eq_one_of_not_multipliable hg]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏' (i : ι), g i

Tactic:
by_cases hg : Multipliable g

Result:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

case neg
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

Proof state:
case pos
ι : Type u_1
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

Tactic:
exact hg.hasProd.one_le h

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem normNoninc_iff_norm_le_one : f.NormNoninc ↔ ‖f‖ ≤ 1

Proof state:
case refine_1
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
v : V
⊢ ‖f v‖ ≤ 1 * ‖v‖

Tactic:
simpa [one_mul] using h v

Result:
no goals

Proof state:
case refine_2
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ ‖f v‖ ≤ ‖v‖

Tactic:
simpa using le_of_opNorm_le f h v

Result:
no goals

Proof state:
case refine_1
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
⊢ ‖f‖ ≤ 1

Tactic:
refine opNorm_le_bound _ zero_le_one fun v => ?_

Result:
case refine_1
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
v : V
⊢ ‖f v‖ ≤ 1 * ‖v‖

Proof state:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
⊢ f.NormNoninc ↔ ‖f‖ ≤ 1

Tactic:
refine ⟨fun h => ?_, fun h => fun v => ?_⟩

Result:
case refine_1
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : f.NormNoninc
⊢ ‖f‖ ≤ 1

case refine_2
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ ‖f v‖ ≤ ‖v‖
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma maximumClique_card_eq_cliqueNum [Fintype α] (s : Finset α) (sm : G.IsMaximumClique s) :
    #s = G.cliqueNum

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sm : G.IsMaximumClique s
⊢ #s = G.cliqueNum

Tactic:
obtain ⟨sc, sm⟩ := sm

Result:
case mk
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
⊢ #s = G.cliqueNum

Proof state:
case mk.intro.mk
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ #s = G.cliqueNum

Tactic:
exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ ¬#s < G.cliqueNum

Tactic:
simp [← tcard, sm t tc]

Result:
no goals

Proof state:
case mk
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
⊢ #s = G.cliqueNum

Tactic:
obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum

Result:
case mk.intro.mk
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
sc : G.IsClique ↑s
sm : ∀ (t : Finset α), G.IsClique ↑t → #t ≤ #s
t : Finset α
tc : G.IsClique ↑t
tcard : #t = G.cliqueNum
⊢ #s = G.cliqueNum
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_le_iff {a : A} (ha : p a) {f g : C(σₙ R a, R)₀} :
    cfcₙHom ha f ≤ cfcₙHom ha g ↔ f ≤ g

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.1057402) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f g : C(↑(σₙ R a), R)₀
⊢ (cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g

Tactic:
rw [← sub_nonneg, ← map_sub, cfcₙHom_nonneg_iff, sub_nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
theorem comp_distTriang_mor_zero₃₁ (T : Triangle C) (H : T ∈ distTriang C) :
    T.mor₃ ≫ T.mor₁⟦1⟧' = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0

Tactic:
have H₂ := rot_of_distTriang T.rotate (rot_of_distTriang T H)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : T.rotate.rotate ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : T.rotate.rotate ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0

Tactic:
simpa using comp_distTriang_mor_zero₁₂ T.rotate.rotate H₂

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_lt_of_forall_lt_add (hf : Continuous f) {z : ℝ} (hz : ∀ x, f x < x + z) :
    τ f < z

Proof state:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f ≤ f x - x

Tactic:
apply translationNumber_le_of_le_add

Result:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ ∀ (x_1 : ℝ), f x_1 ≤ x_1 + (f x - x)

Proof state:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ ∀ (x_1 : ℝ), f x_1 ≤ x_1 + (f x - x)

Tactic:
simp only [← sub_le_iff_le_add']

Result:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ ∀ (x_1 : ℝ), f x_1 - x_1 ≤ f x - x

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
⊢ τ f < z

Tactic:
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
  isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 zero_le_one)
    (hf.sub continuous_id).continuousOn

Result:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f < z

Proof state:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f < z

Tactic:
refine lt_of_le_of_lt ?_ (sub_lt_iff_lt_add'.2 <| hz x)

Result:
case intro.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ τ f ≤ f x - x

Proof state:
case intro.intro.hz
f : CircleDeg1Lift
hf : Continuous ⇑f
z : ℝ
hz : ∀ (x : ℝ), f x < x + z
x : ℝ
hx : ∀ y ∈ Icc 0 1, f y - y ≤ f x - x
⊢ ∀ (x_1 : ℝ), f x_1 - x_1 ≤ f x - x

Tactic:
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma of_comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g]
    [IsOpenImmersion (f ≫ g)] : IsOpenImmersion f :=
  haveI (x : X) : IsIso (f.stalkMap x) :=
    haveI : IsIso (g.stalkMap (f.base x) ≫ f.stalkMap x)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ IsIso (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x)

Tactic:
rw [← Scheme.stalkMap_comp]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion g
inst✝ : IsOpenImmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ IsIso (Scheme.Hom.stalkMap (f ≫ g) x)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioo_top (x : ℝ) : Real.toEReal ⁻¹' Ioo x ⊤ = Ioi x

Proof state:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ⊤ = Ioi x

Tactic:
rw [← Ioi_inter_Iio]

Result:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
/--
Given a vertex with one edge in a graph of cycles this gives the other edge incident
to the same vertex.
-/
lemma IsCycles.other_adj_of_adj (h : G.IsCycles) (hadj : G.Adj v w) :
    ∃ w', w ≠ w' ∧ G.Adj v w'

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
obtain ⟨w', hww'⟩ := (G.neighborSet v).exists_ne_of_one_lt_ncard (by omega) w

Result:
case intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
w' : V
hww' : w' ∈ G.neighborSet v ∧ w' ≠ w
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
have := h ⟨w, hadj⟩

Result:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
w' : V
hww' : w' ∈ G.neighborSet v ∧ w' ≠ w
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Tactic:
exact ⟨w', ⟨hww'.2.symm, hww'.1⟩⟩

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : G.Adj v w
⊢ ∃ w', w ≠ w' ∧ G.Adj v w'

Tactic:
simp_rw [← SimpleGraph.mem_neighborSet] at hadj ⊢

Result:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
⊢ ∃ w', w ≠ w' ∧ w' ∈ G.neighborSet v

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.IsCycles
hadj : w ∈ G.neighborSet v
this : (G.neighborSet v).ncard = 2
⊢ 1 < (G.neighborSet v).ncard

Tactic:
omega

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma ideal_biInf {ι : Type*} (I : ι → IdealSheafData X) {s : Set ι} (hs : s.Finite) :
    (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal

Proof state:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal

Tactic:
refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_

Result:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s✝ : Set ι
hs✝ : s✝.Finite
i : ι
s : Set ι
his : i ∉ s
hs : s.Finite
e : (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal
⊢ (⨅ i_1 ∈ insert i s, I i_1).ideal = ⨅ i_1 ∈ insert i s, (I i_1).ideal

Proof state:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s✝ : Set ι
hs✝ : s✝.Finite
i : ι
s : Set ι
his : i ∉ s
hs : s.Finite
e : (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal
⊢ (⨅ i_1 ∈ insert i s, I i_1).ideal = ⨅ i_1 ∈ insert i s, (I i_1).ideal

Tactic:
simp only [iInf_insert, e, ideal_inf]

Result:
no goals

Proof state:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ (⨅ i ∈ ∅, I i).ideal = ⨅ i ∈ ∅, (I i).ideal

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec_add : npowRec (m + n) a = npowRec m a * npowRec n a

Proof state:
case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a

Tactic:
induction n with
| zero => simp only [Nat.zero_add, npowRec, ha]
| succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]

Result:
no goals

Proof state:
case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

Tactic:
exact (hn rfl).elim

Result:
no goals

Proof state:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec (m + (n + 1 + 1)) a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]

Result:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a

Proof state:
case succ.succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
ih : n + 1 ≠ 0 → npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
hn : n + 1 + 1 ≠ 0
⊢ npowRec m a * npowRec (n + 1) a * a = npowRec m a * npowRec (n + 1 + 1) a

Tactic:
simp only [npowRec, mul_assoc]

Result:
no goals

Proof state:
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a

Tactic:
obtain _ | n := n

Result:
case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a

Proof state:
case succ.zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 + 1 ≠ 0
⊢ npowRec (m + (0 + 1)) a = npowRec m a * npowRec (0 + 1) a

Tactic:
simp only [Nat.zero_add, npowRec, ha]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem iff_forall_not_isBadSeq (r : α → α → Prop) (s : Set α) :
    s.PartiallyWellOrderedOn r ↔ ∀ f, ¬IsBadSeq r s f :=
  forall_congr' fun f => by simp [IsBadSeq]

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f

Tactic:
simp [IsBadSeq]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem martingale_const_fun [OrderBot ι] (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMeasure μ]
    {f : Ω → E} (hf : StronglyMeasurable[ℱ ⊥] f) (hfint : Integrable f μ) :
    Martingale (fun _ => f) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
i j : ι
x✝ : i ≤ j
⊢ μ[(fun x => f) j|↑ℱ i] =ᶠ[ae μ] (fun x => f) i

Tactic:
rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
⊢ Martingale (fun x => f) ℱ μ

Tactic:
refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : OrderBot ι
ℱ : Filtration ι m0
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → E
hf : StronglyMeasurable f
hfint : Integrable f μ
i j : ι
x✝ : i ≤ j
⊢ μ[(fun x => f) j|↑ℱ i] =ᶠ[ae μ] (fun x => f) i
-- Mathlib/Algebra/Group/Basic.lean
/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/
@[to_additive]
lemma hom_coe_pow {F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id)
    (hmul : ∀ f g, c (f * g) = c f ∘ c g) (f : F) : ∀ n, c (f ^ n) = (c f)^[n]
  | 0 => by
    rw [pow_zero, h1]
    rfl
  | n + 1 => by rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]

Proof state:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
n : ℕ
⊢ c (f ^ (n + 1)) = (c f)^[n + 1]

Tactic:
rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]

Result:
no goals

Proof state:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ c (f ^ 0) = (c f)^[0]

Tactic:
rw [pow_zero, h1]

Result:
M : Type u_4
F : Type u_5
inst✝ : Monoid F
c : F → M → M
h1 : c 1 = id
hmul : ∀ (f g : F), c (f * g) = c f ∘ c g
f : F
⊢ id = (c f)^[0]
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.contDiffOn (hm : m ≤ n) (h' : m = ∞ → n = ω)
    (h : ContDiffWithinAt 𝕜 n f s x) :
    ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
hm : m ≤ n
h' : m = ∞ → n = ω
h : ContDiffWithinAt 𝕜 n f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Tactic:
obtain ⟨_u, uo, xu, h⟩ := h.contDiffOn' hm h'

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
hm : m ≤ n
h' : m = ∞ → n = ω
h✝ : ContDiffWithinAt 𝕜 n f s x
_u : Set E
uo : IsOpen _u
xu : x ∈ _u
h : ContDiffOn 𝕜 m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m n : WithTop ℕ∞
hm : m ≤ n
h' : m = ∞ → n = ω
h✝ : ContDiffWithinAt 𝕜 n f s x
_u : Set E
uo : IsOpen _u
xu : x ∈ _u
h : ContDiffOn 𝕜 m f (insert x s ∩ _u)
⊢ ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u

Tactic:
exact ⟨_, inter_mem_nhdsWithin _ (uo.mem_nhds xu), inter_subset_left, h⟩

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem card_image₂_singleton_left (hf : Injective (f a)) : #(image₂ f {a} t) = #t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image₂ f {a} t) = #t

Tactic:
rw [image₂_singleton_left, card_image_of_injective _ hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_zero {x : BitVec w} : x ||| 0#w = x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| 0#w).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x ||| 0#w = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ||| 0#w).getLsbD i = x.getLsbD i
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem const_equiv {q r : ℚ} : const (padicNorm p) q ≈ const (padicNorm p) r ↔ q = r :=
  ⟨fun heq ↦ eq_of_sub_eq_zero <| const_limZero.1 heq, fun heq ↦ by
    rw [heq]⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ const (padicNorm p) q ≈ const (padicNorm p) r

Tactic:
rw [heq]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem prime_iff_card_units (p : ℕ) [Fintype (ZMod p)ˣ] :
    p.Prime ↔ Fintype.card (ZMod p)ˣ = p - 1

Proof state:
inst✝ : Fintype (ZMod 0)ˣ
this : Fintype.card ℤˣ ≠ 0
⊢ ¬Fintype.card ℤˣ = 0

Tactic:
convert this

Result:
no goals

Proof state:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0

Tactic:
suffices Fintype.card ℤˣ ≠ 0 by convert this

Result:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0

Proof state:
case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rw [ZMod.card_units_eq_totient, Nat.totient_eq_iff_prime <| NeZero.pos p]

Result:
no goals

Proof state:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Fintype.card ℤˣ ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rcases eq_zero_or_neZero p with hp | hp

Result:
case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

case inr
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : NeZero p
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Proof state:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1

Tactic:
simp only [ZMod, not_prime_zero, false_iff, zero_tsub]

Result:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ ¬Fintype.card ℤˣ = 0

Proof state:
case inl
p : ℕ
inst✝ : Fintype (ZMod p)ˣ
hp : p = 0
⊢ Prime p ↔ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
subst hp

Result:
case inl
inst✝ : Fintype (ZMod 0)ˣ
⊢ Prime 0 ↔ Fintype.card (ZMod 0)ˣ = 0 - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
    (x ∈ if p then none else l) ↔ ¬ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Option α
⊢ (x ∈ if p then none else l) ↔ ¬p ∧ x ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_inv_mul_left (g : ℝ → F) (a : ℝ) :
    (∫ x : ℝ, g (a⁻¹ * x)) = |a| • ∫ y : ℝ, g y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y

Tactic:
simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, Module.finrank_self, pow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty → m.contains a = false

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
⊢ m.isEmpty = true → m.contains a = false

Tactic:
simp_to_raw using Raw₀.contains_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive (attr := simp)]
lemma smul_one_mul {M N} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) :
    x • (1 : N) * y = x • y

Proof state:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y

Tactic:
rw [smul_mul_assoc, one_mul]

Result:
no goals