harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem of_normalize_eq {f g f' : C} {η θ : f ≅ g} (η_f : 𝟙_ C ⊗ f ≅ f') (η_g : 𝟙_ C ⊗ g ≅ f')
    (h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f)
    (h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f) : η = θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom h_η)]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
apply Iso.ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
h_η : 𝟙_ C ◁ η ≪≫ η_g = η_f
h_θ : 𝟙_ C ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom

Tactic:
calc
  η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
    simp [← reassoc_of% (congrArg Iso.hom h_η)]
  _ = θ.hom := by
    simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_smul_left {c : 𝕜} (hV : DifferentiableWithinAt 𝕜 V s x)
    (hs : UniqueDiffWithinAt 𝕜 s x) :
    lieBracketWithin 𝕜 (c • V) W s x =
      c • lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ lieBracketWithin 𝕜 (c • V) W s x = c • lieBracketWithin 𝕜 V W s x

Tactic:
simp only [lieBracketWithin, Pi.add_apply, map_add, Pi.smul_apply, map_smul, smul_sub]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ c • (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 (c • V) s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ c • (fderivWithin 𝕜 W s x) (V x) - (c • fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ c • (fderivWithin 𝕜 W s x) (V x) - (fderivWithin 𝕜 (c • V) s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)

Tactic:
rw [fderivWithin_const_smul' hs hV]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
c : 𝕜
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ c • (fderivWithin 𝕜 W s x) (V x) - (c • fderivWithin 𝕜 V s x) (W x) =
    c • (fderivWithin 𝕜 W s x) (V x) - c • (fderivWithin 𝕜 V s x) (W x)
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charpoly_coeff_eq_prod_coeff_of_le {k : ℕ} (h : Fintype.card n - 1 ≤ k) :
    M.charpoly.coeff k = (∏ i : n, (X - C (M i i))).coeff k

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k

Tactic:
apply h

Result:
no goals

Proof state:
case h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ M.charpoly.coeff k - (∏ i : n, (X - C (M i i))).coeff k = 0

Tactic:
rw [← coeff_sub]

Result:
case h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).coeff k = 0

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k

Tactic:
rw [Nat.cast_le]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ Fintype.card n - 1 ≤ k

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ M.charpoly.coeff k = (∏ i : n, (X - C (M i i))).coeff k

Tactic:
apply eq_of_sub_eq_zero

Result:
case h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ M.charpoly.coeff k - (∏ i : n, (X - C (M i i))).coeff k = 0

Proof state:
case h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).coeff k = 0

Tactic:
apply Polynomial.coeff_eq_zero_of_degree_lt

Result:
case h.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑k

Proof state:
case h.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑k

Tactic:
apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
h : Fintype.card n - 1 ≤ k
⊢ ↑(Fintype.card n - 1) ≤ ↑k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a)

Proof state:
case intro.h.inl
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
a₁✝ : α✝
h' : r a₁✝ x✝
⊢ Acc (Lex r s) (inl a₁✝)

Tactic:
exact IH _ h'

Result:
no goals

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : Acc r a
⊢ Acc (Lex r s) (inl a)

Tactic:
induction aca with
| intro _ _ IH =>
  constructor
  intro y h
  cases h with
  | inl h' => exact IH _ h'

Result:
no goals

Proof state:
case intro
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
⊢ Acc (Lex r s) (inl x✝)

Tactic:
constructor

Result:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
⊢ ∀ (y : α✝ ⊕ β✝), Lex r s y (inl x✝) → Acc (Lex r s) y

Proof state:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
⊢ ∀ (y : α✝ ⊕ β✝), Lex r s y (inl x✝) → Acc (Lex r s) y

Tactic:
intro y h

Result:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
y : α✝ ⊕ β✝
h : Lex r s y (inl x✝)
⊢ Acc (Lex r s) y

Proof state:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
a : α✝
β✝ : Type u_2
s : β✝ → β✝ → Prop
x✝ : α✝
h✝ : ∀ (y : α✝), r y x✝ → Acc r y
IH : ∀ (y : α✝), r y x✝ → Acc (Lex r s) (inl y)
y : α✝ ⊕ β✝
h : Lex r s y (inl x✝)
⊢ Acc (Lex r s) y

Tactic:
cases h with
| inl h' => exact IH _ h'

Result:
no goals
-- Mathlib/Combinatorics/Derangements/Finite.lean
theorem card_derangements_eq_numDerangements (α : Type*) [Fintype α] [DecidableEq α] :
    card (derangements α) = numDerangements (card α)

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)

Tactic:
rw [← card_derangements_invariant (card_fin _)]

Result:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)

Tactic:
exact card_derangements_fin_eq_numDerangements

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
Explicit bound for the decay rate of the Mahler coefficients of a continuous function on `ℤ_[p]`.
This will be used to prove Mahler's theorem.
-/
lemma fwdDiff_iter_le_of_forall_le {f : C(ℤ_[p], E)} {s t : ℕ}
    (hst : ∀ x y : ℤ_[p], ‖x - y‖ ≤ p ^ (-t : ℤ) → ‖f x - f y‖ ≤ ‖f‖ / p ^ s) (n : ℕ) :
    ‖Δ_[1]^[n + s * p ^ t] f 0‖ ≤ ‖f‖ / p ^ s

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + (k + 1) * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
rw [add_mul, one_mul, ← add_assoc]

Result:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + k * p ^ t + p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)

Proof state:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℚ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
j : ℕ
x✝ : j ∈ range (p ^ t - 1)
⊢ ‖Δ_[1]^[n + (j + 1) + k * p ^ t] (⇑f) 0‖₊ ≤ ‖f‖₊ / ↑p ^ k

Tactic:
exact_mod_cast IH (n + (j + 1)) (by omega)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem centroid_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n)
    (fs : Finset (Fin (n + 1))) :
    fs.centroid ℝ s.points =
      (univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
        (centroidWeightsWithCircumcenter fs)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ centroid ℝ fs s.points = (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)

Tactic:
simp_rw [centroid_def, affineCombination_apply, weightedVSubOfPoint_apply,
  sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter,
  pointsWithCircumcenter_point, zero_smul, add_zero, centroidWeights,
  ← sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (#fs : ℝ)⁻¹)
    (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun _ =>
    zero_smul ℝ _,
  Set.indicator_apply]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ ∑ x : Fin (n + 1),
        (if x ∈ ↑fs then Function.const (Fin (n + 1)) (↑(#fs))⁻¹ x else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ
      Classical.choice ⋯ =
    ∑ x : Fin (n + 1), (if x ∈ fs then (↑(#fs))⁻¹ else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ ∑ x : Fin (n + 1),
        (if x ∈ ↑fs then Function.const (Fin (n + 1)) (↑(#fs))⁻¹ x else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ
      Classical.choice ⋯ =
    ∑ x : Fin (n + 1), (if x ∈ fs then (↑(#fs))⁻¹ else 0) • (s.points x -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯

Tactic:
congr

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem posPart_map_norm (f : α →ₛ ℝ) : (posPart f).map norm = posPart f

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm f.posPart = f.posPart

Tactic:
ext

Result:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ (map norm f.posPart) a✝ = f.posPart a✝

Proof state:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ f.posPart a✝

Tactic:
exact le_max_right _ _

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ (map norm f.posPart) a✝ = f.posPart a✝

Tactic:
rw [map_apply, Real.norm_eq_abs, abs_of_nonneg]

Result:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ f.posPart a✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem succ_mod_two : succ x % 2 = 1 - x % 2

Proof state:
case succ.inr
x : Nat
hyp : x.succ % 2 = 1 - x % 2
p✝ : 2 ≤ x + 2
p : x % 2 = 1
⊢ x % 2 = 1 - (1 - x % 2)

Tactic:
simp [p]

Result:
no goals

Proof state:
case succ
x : Nat
hyp : x.succ % 2 = 1 - x % 2
⊢ (x + 1).succ % 2 = 1 - (x + 1) % 2

Tactic:
have p : 2 ≤ x + 2 := Nat.le_add_left _ _

Result:
case succ
x : Nat
hyp : x.succ % 2 = 1 - x % 2
p : 2 ≤ x + 2
⊢ (x + 1).succ % 2 = 1 - (x + 1) % 2

Proof state:
x : Nat
⊢ x.succ % 2 = 1 - x % 2

Tactic:
induction x with
| zero =>
  trivial
| succ x hyp =>
  have p : 2 ≤ x + 2 := Nat.le_add_left _ _
  simp [Nat.mod_eq (x+2) 2, p, hyp]
  cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]

Result:
no goals

Proof state:
case succ
x : Nat
hyp : x.succ % 2 = 1 - x % 2
p : 2 ≤ x + 2
⊢ x % 2 = 1 - (1 - x % 2)

Tactic:
cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]

Result:
no goals

Proof state:
case zero

⊢ succ 0 % 2 = 1 - 0 % 2

Tactic:
trivial

Result:
no goals

Proof state:
case succ
x : Nat
hyp : x.succ % 2 = 1 - x % 2
p : 2 ≤ x + 2
⊢ (x + 1).succ % 2 = 1 - (x + 1) % 2

Tactic:
simp [Nat.mod_eq (x+2) 2, p, hyp]

Result:
case succ
x : Nat
hyp : x.succ % 2 = 1 - x % 2
p : 2 ≤ x + 2
⊢ x % 2 = 1 - (1 - x % 2)
-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_subtypeDomain_index [CommMonoid N] {v : α →₀ M} {h : α → M → N}
    (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun a b ↦ h a b) = v.prod h

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
p : α → Prop
inst✝ : CommMonoid N
v : α →₀ M
h : α → M → N
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun a b => h (↑a) b) = v.prod h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.coprime_of_no_prime_ge {I J : Ideal R} (h : ∀ P, I ≤ P → J ≤ P → ¬IsPrime P) :
    IsCoprime I J

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ : ¬I ⊔ J = ⊤
⊢ False

Tactic:
obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ✝ : ¬I ⊔ J = ⊤
P : Ideal R
hP : P.IsMaximal
hIJ : I ⊔ J ≤ P
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ IsCoprime I J

Tactic:
rw [isCoprime_iff_sup_eq]

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ I ⊔ J = ⊤

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ✝ : ¬I ⊔ J = ⊤
P : Ideal R
hP : P.IsMaximal
hIJ : I ⊔ J ≤ P
⊢ False

Tactic:
exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ I ⊔ J = ⊤

Tactic:
by_contra hIJ

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ : ¬I ⊔ J = ⊤
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → Id β
⊢ mapM f l = map f l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra.lean
theorem le_of_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
    elemental R x ≤ s :=
  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem toFunLinear_mul_tmul_mul_aux_1 (p : R[X]) (k : ℕ) (h : Decidable ¬p.coeff k = 0) (a : A) :
    ite (¬coeff p k = 0) (a * (algebraMap R A) (coeff p k)) 0 =
    a * (algebraMap R A) (coeff p k)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
⊢ (if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
⊢ (if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)

Tactic:
classical split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem rightUnitor_naturality {X Y : Dial C} (f : X ⟶ Y) :
    (f ⊗ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ (f ⊗ 𝟙 (𝟙_ (Dial C))) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
ext <;> simp

Result:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt))

Proof state:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt))

Tactic:
ext

Result:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁ =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁

Proof state:
case hF.h₁.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) = prod.map π₁ (𝟙 Y.tgt)

Tactic:
ext <;> simp

Result:
no goals

Proof state:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π(π₁ ≫ π₁, π₂) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁ =
    π(prod.map π₁ (𝟙 Y.tgt) ≫ f.F, terminal.from ((X.src ⨯ ⊤_ C) ⨯ Y.tgt)) ≫ π₁

Tactic:
simp

Result:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ f.F = prod.map π₁ (𝟙 Y.tgt) ≫ f.F

Proof state:
case hF.h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) ≫ f.F = prod.map π₁ (𝟙 Y.tgt) ≫ f.F

Tactic:
congr 1

Result:
case hF.h₁.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
f : X ⟶ Y
⊢ π(π₁ ≫ π₁, π₂) = prod.map π₁ (𝟙 Y.tgt)
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normalize_coe_units (u : αˣ) : normalize (u : α) = 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
u : αˣ
⊢ normalize ↑u = 1

Tactic:
simp [normalize_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_injective_image [MeasurableSingletonClass α] [MeasurableSingletonClass β] {f : β → α}
    (hf : Function.Injective f) (s : Set β) : count (f '' s) = count s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
rw [count_apply_infinite hs]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ count (f '' s) = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
⊢ count (f '' s) = count s

Tactic:
by_cases hs : s.Finite

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ count (f '' s) = count s

case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ count (f '' s) = count s

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ count (f '' s) = ⊤

Tactic:
rw [← finite_image_iff hf.injOn] at hs

Result:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬(f '' s).Finite
⊢ count (f '' s) = ⊤

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ count (f '' s) = count s

Tactic:
exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬(f '' s).Finite
⊢ count (f '' s) = ⊤

Tactic:
rw [count_apply_infinite hs]

Result:
no goals