harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_add {m n : ℤ} {x : AddCircle T} : fourier (m+n) x = fourier m x * fourier n x

Proof state:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Tactic:
simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
/-- This can't be an instance because of typeclass loops. -/
lemma BoundedLatticeHomClass.toBiheytingHomClass [BooleanAlgebra α] [BooleanAlgebra β]
    [BoundedLatticeHomClass F α β] : BiheytingHomClass F α β :=
  { ‹BoundedLatticeHomClass F α β› with
    map_himp := fun f a b => by rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]
    map_sdiff := fun f a b => by rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq] }

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
rw [sdiff_eq, sdiff_eq, map_inf, (isCompl_compl.map _).compl_eq]

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ⇨ b) = f a ⇨ f b

Tactic:
rw [himp_eq, himp_eq, map_sup, (isCompl_compl.map _).compl_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
lemma map_apply_of_aemeasurable (ν : ProbabilityMeasure Ω) {f : Ω → Ω'}
    (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) :
    (ν.map f_aemble) A = ν (f ⁻¹' A)

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
⊢ (ν.map f_aemble) A = ν (f ⁻¹' A)

Tactic:
exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <|
  ν.map_apply' f_aemble A_mble

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem findExistsOneDivLT_spec (hi : ¬s ≤[i] 0) :
    ExistsOneDivLT s i (findExistsOneDivLT s i)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)

Tactic:
rw [findExistsOneDivLT, dif_pos hi]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (Nat.find ⋯)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬s ≤[i] 0
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (Nat.find ⋯)

Tactic:
convert Nat.find_spec (existsNatOneDivLTMeasure_of_not_negative hi)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_map {l : List α} {p : β → Bool} : (l.map f).all p = l.all (p ∘ f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
p : β → Bool
⊢ (map f l).all p = l.all (p ∘ f)

Tactic:
induction l with simp | cons _ _ ih => rw [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
p : β → Bool
head✝ : α
tail✝ : List α
ih : (map f tail✝).all p = tail✝.all (p ∘ f)
⊢ (p (f head✝) && (map f tail✝).all p) = (p (f head✝) && tail✝.all (p ∘ f))

Tactic:
rw [ih]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem add_lt_ack : ∀ m n, m + n < ack m n
  | 0, n => by simp
  | m + 1, 0 => by simpa using add_lt_ack m 1
  | m + 1, n + 1 =>
    calc
      m + 1 + n + 1 ≤ m + (m + n + 2)

Proof state:
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1

Tactic:
ring_nf

Result:
no goals

Proof state:
n : ℕ
⊢ 0 + n < ack 0 n

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ m + 1 + n + 1 ≤ m + (m + n + 2)

Tactic:
omega

Result:
no goals

Proof state:
m : ℕ
⊢ m + 1 + 0 < ack (m + 1) 0

Tactic:
simpa using add_lt_ack m 1

Result:
no goals

Proof state:
m n : ℕ
⊢ m + n + 2 = (m + 1 + n).succ

Tactic:
rw [succ_eq_add_one]

Result:
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem coeff_zero_eq_aeval_zero (p : R[X]) : p.coeff 0 = aeval 0 p

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ p.coeff 0 = (aeval 0) p

Tactic:
simp [coeff_zero_eq_eval_zero]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem bot_covBy_iff : ⊥ ⋖ a ↔ IsAtom a

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a : α
⊢ ⊥ ⋖ a ↔ IsAtom a

Tactic:
simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem commutes_symm' {m : ℕ} (hm : n ≤ m) (x : TruncatedWittVector p m (ZMod p)) :
    (zmodEquivTrunc p n).symm (truncate hm x) =
      ZMod.castHom (pow_dvd_pow p hm) _ ((zmodEquivTrunc p m).symm x)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (truncate hm) ((zmodEquivTrunc p m) ((zmodEquivTrunc p m).symm x))

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n).symm ((truncate hm) x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x)

Tactic:
apply (zmodEquivTrunc p n).injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x))

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x))

Tactic:
rw [← commutes' _ _ hm]

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (truncate hm) ((zmodEquivTrunc p m) ((zmodEquivTrunc p m).symm x))
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
protected lemma mem_nonZeroDivisors_iff {P : R[X]} : P ∈ R[X]⁰ ↔ ∀ a : R, a • P = 0 → a = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0

Tactic:
simpa [not_imp_not] using (nmem_nonZeroDivisors_iff (P := P)).not

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem image_closure (h : X ≃ₜ Y) (s : Set X) : h '' closure s = closure (h '' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' closure s = closure (⇑h '' s)

Tactic:
rw [← preimage_symm, preimage_closure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
  | 0 => by simp
  | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]

Proof state:
α : Type u_1
a b : α
⊢ b ∈ replicate 0 a ↔ 0 ≠ 0 ∧ b = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a b : α
n : Nat
⊢ b ∈ replicate (n + 1) a ↔ n + 1 ≠ 0 ∧ b = a

Tactic:
simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem typein_le_typein (r : α → α → Prop) [IsWellOrder α r] {a b : α} :
    typein r a ≤ typein r b ↔ ¬r b a

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
⊢ (typein r).toRelEmbedding a ≤ (typein r).toRelEmbedding b ↔ ¬r b a

Tactic:
rw [← not_lt, typein_lt_typein]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_mem_getLast? : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ getLast? l
  | [], h => by contradiction
  | _ :: _, _ => rfl

Proof state:
α : Type u_1
h : [] ≠ []
⊢ [].getLast h ∈ [].getLast?

Tactic:
contradiction

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_image_get' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (f <| l.get ·) = (l.map f).toFinset

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun x => f (l.get x)) univ = (List.map f l).toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem ext_elem [Finite ι] {q₁ q₂ : P} (h : ∀ i, b.coord i q₁ = b.coord i q₂) : q₁ = q₂

Proof state:
case intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂

Tactic:
rw [← b.affineCombination_coord_eq_self q₁, ← b.affineCombination_coord_eq_self q₂]

Result:
case intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₂

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
⊢ q₁ = q₂

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ q₁ = q₂

Proof state:
case intro
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : Finite ι
q₁ q₂ : P
h : ∀ (i : ι), (b.coord i) q₁ = (b.coord i) q₂
val✝ : Fintype ι
⊢ ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₁) =
    (Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q₂

Tactic:
simp only [h]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
h : H ≤ K
a : ↥H
⊢ ↑((inclusion h) a) = ↑a

Tactic:
cases a

Result:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Proof state:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
H K : S
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ H
⊢ ↑((inclusion h) ⟨val✝, property✝⟩) = ↑⟨val✝, property✝⟩

Tactic:
simp only [inclusion, MonoidHom.mk'_apply]

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

Proof state:
case inr
α✝¹ : Type u_1
α✝ : Type u_2
r₁ r₂ : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s₁ s₂ : β✝¹ → β✝ → Prop
hr : ∀ (a : α✝¹) (b : α✝), r₁ a b → r₂ a b
hs : ∀ (a : β✝¹) (b : β✝), s₁ a b → s₂ a b
b✝ : β✝¹
d✝ : β✝
a✝ : s₁ b✝ d✝
⊢ LiftRel r₂ s₂ (inr b✝) (inr d✝)

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

Result:
no goals

Proof state:
case inl
α✝¹ : Type u_1
α✝ : Type u_2
r₁ r₂ : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s₁ s₂ : β✝¹ → β✝ → Prop
hr : ∀ (a : α✝¹) (b : α✝), r₁ a b → r₂ a b
hs : ∀ (a : β✝¹) (b : β✝), s₁ a b → s₂ a b
a✝¹ : α✝¹
c✝ : α✝
a✝ : r₁ a✝¹ c✝
⊢ LiftRel r₂ s₂ (inl a✝¹) (inl c✝)

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

Result:
no goals

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

Tactic:
cases h

Result:
case inl
α✝¹ : Type u_1
α✝ : Type u_2
r₁ r₂ : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s₁ s₂ : β✝¹ → β✝ → Prop
hr : ∀ (a : α✝¹) (b : α✝), r₁ a b → r₂ a b
hs : ∀ (a : β✝¹) (b : β✝), s₁ a b → s₂ a b
a✝¹ : α✝¹
c✝ : α✝
a✝ : r₁ a✝¹ c✝
⊢ LiftRel r₂ s₂ (inl a✝¹) (inl c✝)

case inr
α✝¹ : Type u_1
α✝ : Type u_2
r₁ r₂ : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s₁ s₂ : β✝¹ → β✝ → Prop
hr : ∀ (a : α✝¹) (b : α✝), r₁ a b → r₂ a b
hs : ∀ (a : β✝¹) (b : β✝), s₁ a b → s₂ a b
b✝ : β✝¹
d✝ : β✝
a✝ : s₁ b✝ d✝
⊢ LiftRel r₂ s₂ (inr b✝) (inr d✝)
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_re_symm (x y : E) : re ⟪x, y⟫ = re ⟪y, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = re ⟪y, x⟫_𝕜

Tactic:
rw [← inner_conj_symm, conj_re]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma sSup_inv (s : Set M) : sSup s⁻¹ = (sInf s)⁻¹

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹

Tactic:
exact ((OrderIso.inv M).map_sInf _).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
rw [← image_inv_eq_inv, sSup_image]

Result:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹
-- Mathlib/Algebra/Order/Invertible.lean
theorem invOf_nonpos [Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedSemiring α
a : α
inst✝ : Invertible a
⊢ ⅟a ≤ 0 ↔ a ≤ 0

Tactic:
simp only [← not_lt, invOf_pos]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_eq_top_iff : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

Tactic:
rw [mul_def]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ (if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b) = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem pred_mul (n m : Nat) : pred n * m = n * m - m

Proof state:
case succ
m n : Nat
⊢ (n + 1).pred * m = (n + 1) * m - m

Tactic:
rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]

Result:
no goals

Proof state:
n m : Nat
⊢ n.pred * m = n * m - m

Tactic:
cases n with
| zero   => simp
| succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]

Result:
no goals

Proof state:
case zero
m : Nat
⊢ pred 0 * m = 0 * m - m

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
lemma complex_exactAt_succ (n : ℕ) :
    P.complex.ExactAt (n + 1)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ ExactAt P.complex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt' P.π (n + 1) (exactAt_succ_single_obj _ _)]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt P.π (n + 1)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt P.π (n + 1)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_some {xs : Vector α n} (h : find? p xs = some a) : p a

Proof state:
α : Type
n : Nat
p : α → Bool
a : α
xs : Vector α n
h : find? p xs = some a
⊢ p a = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type
p : α → Bool
a : α
xs : Array α
h : find? p { toArray := xs, size_toArray := ⋯ } = some a
⊢ p a = true

Proof state:
case mk
α : Type
p : α → Bool
a : α
xs : Array α
h : find? p { toArray := xs, size_toArray := ⋯ } = some a
⊢ p a = true

Tactic:
simp at h

Result:
case mk
α : Type
p : α → Bool
a : α
xs : Array α
h : Array.find? p xs = some a
⊢ p a = true

Proof state:
case mk
α : Type
p : α → Bool
a : α
xs : Array α
h : Array.find? p xs = some a
⊢ p a = true

Tactic:
exact Array.find?_some h

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) :
    (a * b).val = a.val * b.val

Proof state:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ (a * b).val = a.val * b.val

Tactic:
rw [val_mul]

Result:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val

Proof state:
n : ℕ
a b : ZMod n
h : a.val * b.val < n
⊢ a.val * b.val % n = a.val * b.val

Tactic:
apply Nat.mod_eq_of_lt h

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem map_rename (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R) :
    map f (rename g p) = rename g (map f p)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : (map f) ((rename g) p) = (rename g) ((map f) p)
⊢ (map f) ((rename g) (p * X n)) = (rename g) ((map f) (p * X n))

Tactic:
simp only [hp, rename_X, map_X, map_mul]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ (map f) ((rename g) p) = (rename g) ((map f) p)

Tactic:
apply MvPolynomial.induction_on p
  (fun a => by simp only [map_C, rename_C])
  (fun p q hp hq => by simp only [hp, hq, map_add]) fun p n hp => by
  simp only [hp, rename_X, map_X, map_mul]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p q : MvPolynomial σ R
hp : (map f) ((rename g) p) = (rename g) ((map f) p)
hq : (map f) ((rename g) q) = (rename g) ((map f) q)
⊢ (map f) ((rename g) (p + q)) = (rename g) ((map f) (p + q))

Tactic:
simp only [hp, hq, map_add]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ (map f) ((rename g) (C a)) = (rename g) ((map f) (C a))

Tactic:
simp only [map_C, rename_C]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_inv (x : ℝ) : logb b x⁻¹ = -logb b x

Proof state:
b x : ℝ
⊢ logb b x⁻¹ = -logb b x

Tactic:
simp [logb, neg_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
    (replicate n a).erase b = replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a b : α
h : (!b == a) = true
⊢ (replicate n a).erase b = replicate n a

Tactic:
rw [erase_of_not_mem]

Result:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a b : α
h : (!b == a) = true
⊢ ¬b ∈ replicate n a

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a b : α
h : (!b == a) = true
⊢ ¬b ∈ replicate n a

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem valuation_lt_one_iff (a : A) : a ∈ IsLocalRing.maximalIdeal A ↔ A.valuation a < 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬A.valuation ↑a = 1 ↔ A.valuation ↑a < 1

Tactic:
exact (A.valuation_le_one a).lt_iff_ne.symm

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔ A.valuation ↑a < 1

Tactic:
rw [valuation_eq_one_iff]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬A.valuation ↑a = 1 ↔ A.valuation ↑a < 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ IsLocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1

Tactic:
rw [IsLocalRing.mem_maximalIdeal]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ nonunits ↥A ↔ A.valuation ↑a < 1

Proof state:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ nonunits ↥A ↔ A.valuation ↑a < 1

Tactic:
dsimp [nonunits]

Result:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ ¬IsUnit a ↔ A.valuation ↑a < 1
-- Mathlib/Tactic/Ring/Compare.lean
theorem lt_congr {α : Type*} [LT α] {a b c d : α} (h1 : a = b) (h2 : b < c) (h3 : d = c) :
    a < d

Proof state:
α : Type u_1
inst✝ : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
⊢ a < d

Tactic:
rwa [h1, h3]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_option (v : Option α → M) (f : Option α →₀ R) :
    linearCombination R v f =
      f none • v none + linearCombination R (v ∘ Option.some) f.some

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r => r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a => a • (v ∘ Option.some) i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (linearCombination R v) f = f none • v none + (linearCombination R (v ∘ Option.some)) f.some

Tactic:
rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : Option α → M
f : Option α →₀ R
⊢ (f none • v none + f.some.sum fun a r => r • v (Option.some a)) =
    f none • v none + f.some.sum fun i a => a • (v ∘ Option.some) i