harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_finset_sum {ι : Type*} (s : Finset ι) (x y : R) (f : ι → R[X][Y]) :
    (∑ i ∈ s, f i).evalEval x y = ∑ i ∈ s, (f i).evalEval x y

Proof state:
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
s : Finset ι
x y : R
f : ι → R[X][Y]
⊢ evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, evalEval x y (f i)

Tactic:
simp only [evalEval, eval_finset_sum]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_iff_exists_bit1 : Odd a ↔ ∃ b, a = 2 * b + 1 := exists_congr fun b ↦ by rw [two_mul]

Proof state:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ a = 2 * b + 1 ↔ a = 2 * b + 1

Tactic:
rw [two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
    (s ++ t).set i x = s.set i x ++ t

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h : i < n
⊢ (s ++ t).set i x ⋯ = s.set i x h ++ t

Tactic:
simp [set_append, h]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_limit {a b : Ordinal} (ha : a ≠ 0) (hb : IsLimit b) :
    a ^ b = ⨆ x : Iio b, a ^ x.1

Proof state:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : b.IsLimit
⊢ a ^ b = ⨆ x, a ^ ↑x

Tactic:
simp_rw [opow_of_ne_zero ha, limitRecOn_limit _ _ _ _ hb]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem continuousAt_of_tendsto_nhds [TopologicalSpace Y] [T1Space Y] {f : X → Y} {x : X} {y : Y}
    (h : Tendsto f (𝓝 x) (𝓝 y)) : ContinuousAt f x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x

Tactic:
rwa [ContinuousAt, eq_of_tendsto_nhds h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_one_div_add_atTop_nhds_zero_nat :
    Tendsto (fun n : ℕ ↦ 1 / ((n : ℝ) + 1)) atTop (𝓝 0) :=
  suffices Tendsto (fun n : ℕ ↦ 1 / (↑(n + 1) : ℝ)) atTop (𝓝 0) by simpa
  (tendsto_add_atTop_iff_nat 1).2 (_root_.tendsto_const_div_atTop_nhds_zero_nat 1)

Proof state:
this : Tendsto (fun n => 1 / ↑(n + 1)) atTop (𝓝 0)
⊢ Tendsto (fun n => 1 / (↑n + 1)) atTop (𝓝 0)

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem coe_neLocus : ↑(f.neLocus g) = { x | f x ≠ g x }

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ ↑(f.neLocus g) = {x | f x ≠ g x}

Tactic:
ext

Result:
case h
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(f.neLocus g) ↔ x✝ ∈ {x | f x ≠ g x}

Proof state:
case h
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
x✝ : α
⊢ x✝ ∈ ↑(f.neLocus g) ↔ x✝ ∈ {x | f x ≠ g x}

Tactic:
exact mem_neLocus

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem HasIntegral.mcShane_of_forall_isLittleO (B : ι →ᵇᵃ[I] ℝ) (hB0 : ∀ J, 0 ≤ B J)
    (g : ι →ᵇᵃ[I] F) (H : ∀ (_ : ℝ≥0), ∀ x ∈ Box.Icc I, ∀ ε > (0 : ℝ), ∃ δ > 0, ∀ J ≤ I,
      Box.Icc J ⊆ Metric.closedBall x δ → dist (vol J (f x)) (g J) ≤ ε * B J) :
    HasIntegral I McShane f vol (g I) :=
  (HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (l := McShane) rfl B hB0 g ∅ countable_empty
      (fun ⟨_x, hx⟩ => hx.elim) fun _ _ hx => hx.2.elim) <| by
    simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, diff_empty] using H

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
H :
  ℝ≥0 →
    ∀ x ∈ Box.Icc I, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J
⊢ ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ ∅,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (McShane.bHenstock = true → x ∈ Box.Icc J) →
                (McShane.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J

Tactic:
simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, diff_empty] using H

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_eq_append (x : α) (xs : Fin n → α) :
    cons x xs = append (cons x Fin.elim0) xs ∘ Fin.cast (Nat.add_comm ..)

Proof state:
case h
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons x xs i = (append (cons x elim0) xs ∘ Fin.cast ⋯) i

Tactic:
simp [append_left_eq_cons]

Result:
no goals

Proof state:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
⊢ cons x xs = append (cons x elim0) xs ∘ Fin.cast ⋯

Tactic:
funext i

Result:
case h
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons x xs i = (append (cons x elim0) xs ∘ Fin.cast ⋯) i
-- Mathlib/CategoryTheory/Quotient.lean
theorem lift_map_functor_map {X Y : C} (f : X ⟶ Y) :
    (lift r F H).map ((functor r).map f) = F.map f

Proof state:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) = F.map f

Tactic:
rw [← NatIso.naturality_1 (lift.isLift r F H)]

Result:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) =
    (lift.isLift r F H).inv.app X ≫ (functor r ⋙ lift r F H).map f ≫ (lift.isLift r F H).hom.app Y

Proof state:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (lift r F H).map ((functor r).map f) =
    (lift.isLift r F H).inv.app X ≫ (functor r ⋙ lift r F H).map f ≫ (lift.isLift r F H).hom.app Y

Tactic:
dsimp [lift, functor]

Result:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (Quot.mk (CompClosure r) f).liftOn (fun f => F.map f) ⋯ =
    𝟙 (F.obj X) ≫ (Quot.mk (CompClosure r) f).liftOn (fun f => F.map f) ⋯ ≫ 𝟙 (F.obj Y)

Proof state:
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (Quot.mk (CompClosure r) f).liftOn (fun f => F.map f) ⋯ =
    𝟙 (F.obj X) ≫ (Quot.mk (CompClosure r) f).liftOn (fun f => F.map f) ⋯ ≫ 𝟙 (F.obj Y)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_permCongr (e : α ≃ β) (p : Perm α) : sign (e.permCongr p) = sign p :=
  sign_eq_sign_of_equiv _ _ e.symm (by simp)

Proof state:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
e : α ≃ β
p : Perm α
⊢ ∀ (x : β), e.symm ((e.permCongr p) x) = p (e.symm x)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toIocMod_toReal (θ : Angle) : toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

Proof state:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝

Tactic:
exact toIocMod_toIocMod _ _ _ _

Result:
no goals

Proof state:
θ : Angle
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal

Proof state:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal

Tactic:
rw [toReal_coe]

Result:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem nilpotencyLength_eq_one_iff [Nontrivial M] :
    nilpotencyLength L M = 1 ↔ IsTrivial L M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Nontrivial M
⊢ nilpotencyLength L M = 1 ↔ IsTrivial L M

Tactic:
rw [nilpotencyLength_eq_succ_iff ℤ, ← trivial_iff_lower_central_eq_bot]

Result:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Nontrivial M
⊢ IsTrivial L M ∧ lowerCentralSeries ℤ L M 0 ≠ ⊥ ↔ IsTrivial L M

Proof state:
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : Nontrivial M
⊢ IsTrivial L M ∧ lowerCentralSeries ℤ L M 0 ≠ ⊥ ↔ IsTrivial L M

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/CompTypeclasses.lean
theorem comp_apply_eq₂ {x : R₂} : σ (σ' x) = x

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂) x = x

Tactic:
simp

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ σ (σ' x) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq₂]

Result:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂) x = x
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.mem_convexHull {s : Finset E} {x : E} : x ∈ convexHull R (s : Set E) ↔
    ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
⊢ x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x

Tactic:
rw [Finset.convexHull_eq, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
@[simp]
lemma piecewise_univ [∀ i, Decidable (i ∈ (univ : Finset ι))] (f g : ∀ i, π i) :
    univ.piecewise f g = f

Proof state:
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Decidable (i ∈ univ)
f g : (i : ι) → π i
⊢ univ.piecewise f g = f

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Decidable (i ∈ univ)
f g : (i : ι) → π i
i : ι
⊢ univ.piecewise f g i = f i

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Decidable (i ∈ univ)
f g : (i : ι) → π i
i : ι
⊢ univ.piecewise f g i = f i

Tactic:
simp [piecewise]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem one_le_iff_pos [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero (1 : α)]
    [SuccAddOrder α] : 1 ≤ x ↔ 0 < x

Proof state:
α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ x ↔ 0 < x

Tactic:
rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma not_isFiniteMeasure_iff : ¬IsFiniteMeasure μ ↔ μ univ = ∞

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ¬IsFiniteMeasure μ ↔ μ univ = ⊤

Tactic:
simp [isFiniteMeasure_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_neg_one (x : ℝ≥0) : x ^ (-1 : ℝ) = x⁻¹

Proof state:
x : ℝ≥0
⊢ x ^ (-1) = x⁻¹

Tactic:
simp [rpow_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
    Lex r₂ s₂ x y

Proof state:
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
x y : α✝ ⊕ β✝
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
h : Lex r₁ s₁ x y
⊢ Lex r₂ s₂ x y

Tactic:
cases h

Result:
case inl
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
a₁✝ a₂✝ : α✝
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)

case inr
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
b₁✝ b₂✝ : β✝
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)

case sep
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
a✝ : α✝
b✝ : β✝
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)

Proof state:
case inr
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
b₁✝ b₂✝ : β✝
h✝ : s₁ b₁✝ b₂✝
⊢ Lex r₂ s₂ (inr b₁✝) (inr b₂✝)

Tactic:
exact Lex.inr (hs _ _ ‹_›)

Result:
no goals

Proof state:
case inl
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
a₁✝ a₂✝ : α✝
h✝ : r₁ a₁✝ a₂✝
⊢ Lex r₂ s₂ (inl a₁✝) (inl a₂✝)

Tactic:
exact Lex.inl (hr _ _ ‹_›)

Result:
no goals

Proof state:
case sep
α✝ : Type u_1
r₁ r₂ : α✝ → α✝ → Prop
β✝ : Type u_2
s₁ s₂ : β✝ → β✝ → Prop
hr : ∀ (a b : α✝), r₁ a b → r₂ a b
hs : ∀ (a b : β✝), s₁ a b → s₂ a b
a✝ : α✝
b✝ : β✝
⊢ Lex r₂ s₂ (inl a✝) (inr b✝)

Tactic:
exact Lex.sep _ _

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem mem_divisors {m : ℕ} : n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0

Proof state:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m

Tactic:
exact le_of_dvd hm.bot_lt

Result:
no goals

Proof state:
n m : ℕ
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Result:
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Proof state:
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

Tactic:
simp [divisors]

Result:
no goals

Proof state:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
  mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]

Result:
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma congr_φH {γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φH = γ₂.φH

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem oangle_rotation_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) :
    o.oangle (o.rotation θ x) y = o.oangle x y - θ

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ o.oangle ((o.rotation θ) x) y = o.oangle x y - θ

Tactic:
simp only [oangle, o.kahler_rotation_left']

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑(-θ).toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

Proof state:
case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(-θ).toCircle ≠ 0

Tactic:
exact Circle.coe_ne_zero _

Result:
no goals

Proof state:
case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0

Tactic:
exact o.kahler_ne_zero hx hy

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

Tactic:
abel

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑(-θ).toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(-θ).toCircle ≠ 0

case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_prod_left_iff {t : Finset ι} {s : ι → ℕ} {x : ℕ} :
    Coprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, Coprime (s i) x

Proof state:
ι : Type u_1
t : Finset ι
s : ι → ℕ
x : ℕ
⊢ (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x

Tactic:
simpa using coprime_multiset_prod_left_iff (m := t.val.map s)

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, n ^ k ≤ n.ascFactorial k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]
    exact Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

Proof state:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k

Tactic:
exact Nat.mul_le_mul (Nat.le_refl n)
  (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

Result:
no goals

Proof state:
n k : ℕ
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]

Result:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k

Proof state:
n : ℕ
⊢ n ^ 0 ≤ n.ascFactorial 0

Tactic:
rw [ascFactorial_zero, Nat.pow_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_ne_zero {P : Nat → Prop} : (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1) :=
  ⟨fun ⟨n, h, w⟩ => by cases n with | zero => simp at h | succ n => exact ⟨n, w⟩,
    fun ⟨n, w⟩ => ⟨n + 1, by simp, w⟩⟩

Proof state:
case zero
P : Nat → Prop
x✝ : ∃ n, ¬n = 0 ∧ P n
h : ¬0 = 0
w : P 0
⊢ ∃ n, P (n + 1)

Tactic:
simp at h

Result:
no goals

Proof state:
P : Nat → Prop
x✝ : ∃ n, P (n + 1)
n : Nat
w : P (n + 1)
⊢ ¬n + 1 = 0

Tactic:
simp

Result:
no goals

Proof state:
P : Nat → Prop
x✝ : ∃ n, ¬n = 0 ∧ P n
n : Nat
h : ¬n = 0
w : P n
⊢ ∃ n, P (n + 1)

Tactic:
cases n with | zero => simp at h | succ n => exact ⟨n, w⟩

Result:
no goals

Proof state:
case succ
P : Nat → Prop
x✝ : ∃ n, ¬n = 0 ∧ P n
n : Nat
h : ¬n + 1 = 0
w : P (n + 1)
⊢ ∃ n, P (n + 1)

Tactic:
exact ⟨n, w⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem exact_sat (r : Int) (t : Int) : (exact r).sat t = decide (r = t)

Proof state:
r t : Int
⊢ (exact r).sat t = decide (r = t)

Tactic:
simp only [sat, exact, Option.all_some, decide_eq_true_eq, decide_eq_decide]

Result:
r t : Int
⊢ r ≤ t ∧ t ≤ r ↔ r = t

Proof state:
r t : Int
⊢ r ≤ t ∧ t ≤ r ↔ r = t

Tactic:
exact Int.eq_iff_le_and_ge.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α}
    {v : β k} :
    (m.insert k v).getKey! k = k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).getKey! k = k

Tactic:
simp_to_raw using Raw₀.getKey!_insert_self

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem rank_eq_one_iff : Module.rank F K = 1 ↔ K = ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ Module.rank F ↥K = 1 ↔ K = ⊥

Tactic:
rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
  bot_toSubalgebra]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem frespects_eq {σ₁ σ₂} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} {a₂ b₂} (h : f₂ a₂ = f₂ b₂) :
    ∀ {b₁}, FRespects f₂ tr a₂ b₁ ↔ FRespects f₂ tr b₂ b₁
  | some _ => reaches₁_eq h
  | none => by unfold FRespects; rw [h]

Proof state:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none

Tactic:
rw [h]

Result:
no goals

Proof state:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ FRespects f₂ tr a₂ none ↔ FRespects f₂ tr b₂ none

Tactic:
unfold FRespects

Result:
σ₁ : Type u_1
σ₂ : Type u_2
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₂ b₂ : σ₂
h : f₂ a₂ = f₂ b₂
⊢ (match none with
    | some b₁ => Reaches₁ f₂ a₂ (tr b₁)
    | none => f₂ a₂ = none) ↔
    match none with
    | some b₁ => Reaches₁ f₂ b₂ (tr b₁)
    | none => f₂ b₂ = none
-- Mathlib/Data/Finset/Insert.lean
theorem ne_insert_of_not_mem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ≠ insert a t

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_pf_right (b₁ : R) (b₂) (_ : a * b₃ = c) :
    a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Tactic:
rw [mul_left_comm]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
lemma iterate_add_eq_iterate (hf : Injective f) : f^[m + n] a = f^[n] a ↔ f^[m] a = a :=
  Iff.trans (by rw [← iterate_add_apply, Nat.add_comm]) (hf.iterate n).eq_iff

Proof state:
α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
rw [← iterate_add_apply, Nat.add_comm]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
lemma radical_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
    (hs : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) :
    (s.inf f).radical = (f i).radical

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ (⇑radicalInfTopHom ∘ f) = (f i).radical

Tactic:
exact Finset.inf'_eq_of_forall _ _ hs

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical

Tactic:
rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]

Result:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ s.inf' ⋯ (⇑radicalInfTopHom ∘ f) = (f i).radical