harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FermatPsp.lean
theorem a_id_helper {a b : ℕ} (ha : 2 ≤ a) (hb : 2 ≤ b) : 2 ≤ (a ^ b - 1) / (a - 1)

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ a < a ^ b

Tactic:
exact lt_self_pow₀ (Nat.lt_of_succ_le ha) hb

Result:
no goals

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ a - 1 ∣ a ^ b - 1

Tactic:
simpa only [one_pow] using nat_sub_dvd_pow_sub_pow a 1 b

Result:
no goals

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ 2 ≤ (a ^ b - 1) / (a - 1)

Tactic:
change 1 < _

Result:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ 1 < (a ^ b - 1) / (a - 1)

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
⊢ 1 < (a ^ b - 1) / (a - 1)

Tactic:
have h₁ : a - 1 ∣ a ^ b - 1 := by simpa only [one_pow] using nat_sub_dvd_pow_sub_pow a 1 b

Result:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ 1 < (a ^ b - 1) / (a - 1)

Proof state:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ 1 < (a ^ b - 1) / (a - 1)

Tactic:
rw [Nat.lt_div_iff_mul_lt' h₁, mul_one, tsub_lt_tsub_iff_right (Nat.le_of_succ_le ha)]

Result:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
h₁ : a - 1 ∣ a ^ b - 1
⊢ a < a ^ b
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem AEEqFun.eLpNorm_compMeasurePreserving {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] E)
    (hf : MeasurePreserving f μ ν) :
    eLpNorm (g.compMeasurePreserving f hf) p μ = eLpNorm g p ν

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν

Tactic:
rw [eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑g ∘ f) p μ = eLpNorm (↑g) p ν

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_6
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑g ∘ f) p μ = eLpNorm (↑g) p ν

Tactic:
exact eLpNorm_comp_measurePreserving g.aestronglyMeasurable hf

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem map_eq_zero_iff_eq_one : f x = 0 ↔ x = 1 :=
  ⟨eq_one_of_map_eq_zero _, by
    rintro rfl
    exact map_one_eq_zero _⟩

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
⊢ f 1 = 0

Tactic:
exact map_one_eq_zero _

Result:
no goals

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → f x = 0

Tactic:
rintro rfl

Result:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
⊢ f 1 = 0
-- Mathlib/RingTheory/PolynomialAlgebra.lean
lemma evalRingHom_mapMatrix_comp_polyToMatrix :
    (evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (evalRingHom 0)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommSemiring S
f : S →+* Matrix n n R
⊢ (evalRingHom 0).mapMatrix.comp f.polyToMatrix = f.comp (evalRingHom 0)

Tactic:
ext <;> simp [RingHom.polyToMatrix, ← AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive "All triangles are isosceles in an ultrametric normed additive group."]
lemma norm_div_eq_max_of_norm_div_ne_norm_div (x y z : S) (h : ‖x / y‖ ≠ ‖y / z‖) :
    ‖x / z‖ = max ‖x / y‖ ‖y / z‖

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y z : S
h : ‖x / y‖ ≠ ‖y / z‖
⊢ ‖x / z‖ = ‖x / y‖ ⊔ ‖y / z‖

Tactic:
simpa only [div_mul_div_cancel] using norm_mul_eq_max_of_norm_ne_norm h

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma eq_of_mem_uIoc_of_mem_uIoc : a ∈ Ι b c → b ∈ Ι a c → a = b

Proof state:
case inr.intro.inr.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

Tactic:
assumption

Result:
no goals

Proof state:
case inr.intro.inl.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
exact le_trans ‹_› (le_of_lt ‹_›)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
simp_rw [mem_uIoc]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b

Proof state:
case inl.intro.inl.intro.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
exact le_of_lt ‹_›

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b

Tactic:
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;> apply le_antisymm <;>
first |assumption|exact le_of_lt ‹_›|exact le_trans ‹_› (le_of_lt ‹_›)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma comap_sectL (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) :
    comap (sectL κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const)

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (((κ.sectL b).comap f hf) d) s = ((κ.comap (fun d => (f d, b)) ⋯) d) s

Tactic:
rw [comap_apply, sectL_apply, comap_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
⊢ (κ.sectL b).comap f hf = κ.comap (fun d => (f d, b)) ⋯

Tactic:
ext d s

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
b : β
f : δ → α
hf : Measurable f
d : δ
s : Set γ
a✝ : MeasurableSet s
⊢ (((κ.sectL b).comap f hf) d) s = ((κ.comap (fun d => (f d, b)) ⋯) d) s
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mul_inv_left {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
    w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ = z ↔ w = f y * z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

Tactic:
rw [mul_comm]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ * w = z ↔ w = f ↑y * z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ * w = z ↔ w = f ↑y * z

Tactic:
exact Units.inv_mul_eq_iff_eq_mul (IsUnit.liftRight (f.restrict S) h y)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq]

Proof state:
n : Nat
⊢ n ≤ 0 ↔ n = 0

Tactic:
rw [le_zero_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y

Proof state:
p : Prop
inst✝ : Decidable p
x : p → Prop
y : Prop
⊢ ((if h : p then x h else y) ↔ y) ↔ ∀ (h : p), x h ↔ y

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem smulAux'_im (g : GL(2, ℝ)⁺) (z : ℍ) :
    (smulAux' g z).im = det ↑ₘg * z.im / Complex.normSq (denom g z)

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (smulAux' g z).im = (↑↑g).det * z.im / Complex.normSq (denom g z)

Tactic:
simp only [smulAux', num, denom, Complex.div_im, Complex.add_im, Complex.mul_im,
  Complex.ofReal_re, coe_im, Complex.ofReal_im, coe_re, zero_mul, add_zero, Complex.add_re,
  Complex.mul_re, sub_zero, ← sub_div, g.1.1.det_fin_two]

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (↑↑g 0 0 * z.im * (↑↑g 1 0 * z.re + ↑↑g 1 1) - (↑↑g 0 0 * z.re + ↑↑g 0 1) * (↑↑g 1 0 * z.im)) /
      Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0) * z.im / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (↑↑g 0 0 * z.im * (↑↑g 1 0 * z.re + ↑↑g 1 1) - (↑↑g 0 0 * z.re + ↑↑g 0 1) * (↑↑g 1 0 * z.im)) /
      Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0) * z.im / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))

Tactic:
ring

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addY (u • P) (v • Q) = (u * v) ^ 2 * W'.addY P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addY (u • P) (v • Q) = (u * v) ^ 2 * W'.addY P Q

Tactic:
simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_smul]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -((u * v) ^ 2 * W'.negAddY P Q) - W'.a₁ * ((u * v) ^ 2 * W'.addX P Q) - W'.a₃ * ((u * v) ^ 2 * W'.addZ P Q) =
    (u * v) ^ 2 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -((u * v) ^ 2 * W'.negAddY P Q) - W'.a₁ * ((u * v) ^ 2 * W'.addX P Q) - W'.a₃ * ((u * v) ^ 2 * W'.addZ P Q) =
    (u * v) ^ 2 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_singleton {l : Multiset α} {a : α} : Disjoint l {a} ↔ a ∉ l

Proof state:
α : Type u_1
l : Multiset α
a : α
⊢ _root_.Disjoint l {a} ↔ a ∉ l

Tactic:
rw [_root_.disjoint_comm, singleton_disjoint]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
lemma coevaluation_evaluation'' :
    Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙.hom

Tactic:
convert coevaluation_evaluation X Y <;> simp [monoidalComp]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
  eq_of_forall_ge_iff fun b => by
    rw [← not_lt, ← not_lt, not_iff_not, lt_ceil]
    obtain hb | hb := le_or_lt n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : α), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
    · exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

Result:
no goals

Proof state:
case inl.intro
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) < a + ↑n ↔ n + d < ⌈a⌉₊ + n

Tactic:
rw [Nat.cast_add, add_comm n, add_comm (n : α), add_lt_add_iff_right, add_lt_add_iff_right,
  lt_ceil]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
obtain hb | hb := le_or_lt n b

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

case inr
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
⊢ ⌈a + ↑n⌉₊ ≤ b ↔ ⌈a⌉₊ + n ≤ b

Tactic:
rw [← not_lt, ← not_lt, not_iff_not, lt_ceil]

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le hb

Result:
case inl.intro
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) < a + ↑n ↔ n + d < ⌈a⌉₊ + n
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma δ_leftUnshift {a n' : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n')
    (m m' : ℤ) (hm' : m + a = m') :
    δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'

Tactic:
simp only [leftUnshift_leftShift, γ'.δ_leftShift a n' m' hn m hm', leftUnshift_units_smul,
  smul_smul, Int.units_mul_self, one_smul]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
⊢ δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

Tactic:
obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m (((leftShiftAddEquiv K L n a n' hn) γ').leftUnshift n hn) =
    a.negOnePow • (δ n' m' ((leftShiftAddEquiv K L n a n' hn) γ')).leftUnshift m hm'

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m (((leftShiftAddEquiv K L n a n' hn) γ').leftUnshift n hn) =
    a.negOnePow • (δ n' m' ((leftShiftAddEquiv K L n a n' hn) γ')).leftUnshift m hm'

Tactic:
dsimp

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_neg (f : R[X]) (N : ℕ) : reflect N (-f) = -reflect N f

Proof state:
R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (-f) = -reflect N f

Tactic:
rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_right_distrib_sub (x y z : PGame) : (⟦(y - z) * x⟧ : Game) = ⟦y * x⟧ - ⟦z * x⟧

Proof state:
x y z : PGame
⊢ ⟦(y - z) * x⟧ = ⟦y * x⟧ - ⟦z * x⟧

Tactic:
change (⟦(y + -z) * x⟧ : Game) = ⟦y * x⟧ + -⟦z * x⟧

Result:
x y z : PGame
⊢ ⟦(y + -z) * x⟧ = ⟦y * x⟧ + -⟦z * x⟧

Proof state:
x y z : PGame
⊢ ⟦(y + -z) * x⟧ = ⟦y * x⟧ + -⟦z * x⟧

Tactic:
rw [quot_right_distrib, quot_neg_mul]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_succ : Ico a.succ b.succ = Ioc a b

Proof state:
a b : ℕ
⊢ Ico a.succ b.succ = Ioc a b

Tactic:
ext x

Result:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b.succ ↔ x ∈ Ioc a b

Proof state:
case h
a b x : ℕ
⊢ x ∈ Ico a.succ b.succ ↔ x ∈ Ioc a b

Tactic:
rw [mem_Ico, mem_Ioc, succ_le_iff, Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem lexOrder_zero : lexOrder (0 : MvPowerSeries σ R) = ⊤

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ lexOrder 0 = ⊤

Tactic:
unfold lexOrder

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ (if h : 0 = 0 then ⊤
    else
      let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support 0) ne)) =
    ⊤

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ (if h : 0 = 0 then ⊤
    else
      let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support 0) ne)) =
    ⊤

Tactic:
rw [dif_pos rfl]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem inf_equiv_inf {a₁ b₁ a₂ b₂ : CauSeq α abs} (ha : a₁ ≈ a₂) (hb : b₁ ≈ b₂) :
    a₁ ⊓ b₁ ≈ a₂ ⊓ b₂

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
exact
  ⟨ai ⊔ bi, fun i hi =>
    (abs_min_sub_min_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
      (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊓ b₁ ≈ a₂ ⊓ b₂

Tactic:
intro ε ε0

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_segment_singleton (a b c : E) :
    convexJoin 𝕜 (segment 𝕜 a b) {c} = convexHull 𝕜 {a, b, c}

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b c : E
⊢ convexJoin 𝕜 (segment 𝕜 a b) {c} = (convexHull 𝕜) {a, b, c}

Tactic:
rw [← pair_eq_singleton, ← convexJoin_segments, segment_same, pair_eq_singleton]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_filter_eq_zero_iff {p : α → Prop} [DecidablePred p] :
    #(s.filter p) = 0 ↔ ∀ x ∈ s, ¬ p x

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = 0 ↔ ∀ x ∈ s, ¬p x

Tactic:
rw [card_eq_zero, filter_eq_empty_iff]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem len_lt_of_mono {Δ' Δ : SimplexCategory} (i : Δ' ⟶ Δ) [hi : Mono i] (hi' : Δ ≠ Δ') :
    Δ'.len < Δ.len

Proof state:
case a
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ Δ.len = Δ'.len

Tactic:
exact h.symm

Result:
no goals

Proof state:
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ Δ = Δ'

Tactic:
ext

Result:
case a
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ Δ.len = Δ'.len

Proof state:
case inl
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len < Δ.len
⊢ Δ'.len < Δ.len

Tactic:
exact h

Result:
no goals

Proof state:
case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ Δ'.len < Δ.len

Tactic:
exfalso

Result:
case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ False

Proof state:
case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ False

Tactic:
exact hi' (by ext; exact h.symm)

Result:
no goals

Proof state:
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
⊢ Δ'.len < Δ.len

Tactic:
rcases lt_or_eq_of_le (len_le_of_mono hi) with (h | h)

Result:
case inl
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len < Δ.len
⊢ Δ'.len < Δ.len

case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : Δ'.len = Δ.len
⊢ Δ'.len < Δ.len
-- Mathlib/Order/Filter/Pi.lean
theorem hasBasis_pi {ι' : ι → Type*} {s : ∀ i, ι' i → Set (α i)} {p : ∀ i, ι' i → Prop}
    (h : ∀ i, (f i).HasBasis (p i) (s i)) :
    (pi f).HasBasis (fun If : Set ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i))
      fun If : Set ι × ∀ i, ι' i => If.1.pi fun i => s i <| If.2 i

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
ι' : ι → Type u_3
s : (i : ι) → ι' i → Set (α i)
p : (i : ι) → ι' i → Prop
h : ∀ (i : ι), (f i).HasBasis (p i) (s i)
⊢ (pi f).HasBasis (fun If => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If => If.1.pi fun i => s i (If.2 i)

Tactic:
simpa [Set.pi_def] using hasBasis_iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem continuousAt_log_iff : ContinuousAt log x ↔ x ≠ 0

Proof state:
x : ℝ
⊢ ContinuousAt log x → x ≠ 0

Tactic:
rintro h rfl

Result:
h : ContinuousAt log 0
⊢ False

Proof state:
x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_log⟩

Result:
x : ℝ
⊢ ContinuousAt log x → x ≠ 0

Proof state:
h : ContinuousAt log 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsWithin_zero _
  (h.tendsto.mono_left inf_le_left)

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_sum {f : X ⊕ Y → Z} :
    IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X ⊕ Y → Z
⊢ IsOpenMap f ↔ (IsOpenMap fun a => f (inl a)) ∧ IsOpenMap fun b => f (inr b)

Tactic:
simp only [isOpenMap_iff_nhds_le, Sum.forall, nhds_inl, nhds_inr, Filter.map_map, comp_def]

Result:
no goals