harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub' (a b : α) : toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_sub_zsmul' hp a b 1

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_restrict {f : α →. β} {s : Set α} (h : s ⊆ f.Dom) (a : α) (b : β) :
    b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
s : Set α
h : s ⊆ f.Dom
a : α
b : β
⊢ b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a

Tactic:
simp [restrict]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem inf_himp_le : a ⊓ (a ⇨ b) ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ (a ⇨ b) ≤ b

Tactic:
rw [inf_comm, ← le_himp_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ne_cons_self {a : α} {l : List α} : l ≠ a :: l

Proof state:
α : Type u_1
a : α
l : List α
⊢ l ≠ a :: l

Tactic:
rw [ne_eq, eq_comm]

Result:
α : Type u_1
a : α
l : List α
⊢ ¬a :: l = l

Proof state:
α : Type u_1
a : α
l : List α
⊢ ¬a :: l = l

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
lemma smul_ne_zero_iff_left (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
hx : x ≠ 0
⊢ c • x ≠ 0 ↔ c ≠ 0

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_map {f : α → Option β} {g : α → β → σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec fun a => (f a).map (g a) :=
  (option_bind hf (option_some.comp₂ hg)).of_eq fun x => by cases f x <;> rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → σ
hf : Primrec f
hg : Primrec₂ g
x : α
⊢ ((f x).bind fun b => some (g x b)) = Option.map (g x) (f x)

Tactic:
cases f x <;> rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem subgroupOf_eq_top {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H

Tactic:
rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Linear.lean
lemma coe_toLinear_ne_zero_iff : (χ : L →ₗ[R] R) ≠ 0 ↔ χ.IsNonZero

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : LinearWeights R L M
χ : Weight R L M
⊢ toLinear R L M χ ≠ 0 ↔ χ.IsNonZero

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma isOpen_iff_forall_specializes : IsOpen s ↔ ∀ x y, x ⤳ y → y ∈ s → x ∈ s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s

Tactic:
simp only [← exterior_subset_iff_isOpen, Set.subset_def, mem_exterior_iff_specializes, exists_imp,
  and_imp, @forall_swap (_ ⤳ _)]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem mul_moveRight_inl {x y : PGame} {i j} :
    (x * y).moveRight (toRightMovesMul (Sum.inl (i, j))) =
      x.moveLeft i * y + x * y.moveRight j - x.moveLeft i * y.moveRight j

Proof state:
x y : PGame
i : x.LeftMoves
j : y.RightMoves
⊢ (x * y).moveRight (toRightMovesMul (Sum.inl (i, j))) =
    x.moveLeft i * y + x * y.moveRight j - x.moveLeft i * y.moveRight j

Tactic:
cases x

Result:
case mk
y : PGame
j : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveRight (toRightMovesMul (Sum.inl (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveLeft i * y + mk α✝ β✝ a✝¹ a✝ * y.moveRight j - (mk α✝ β✝ a✝¹ a✝).moveLeft i * y.moveRight j

Proof state:
case mk
y : PGame
j : y.RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ * y).moveRight (toRightMovesMul (Sum.inl (i, j))) =
    (mk α✝ β✝ a✝¹ a✝).moveLeft i * y + mk α✝ β✝ a✝¹ a✝ * y.moveRight j - (mk α✝ β✝ a✝¹ a✝).moveLeft i * y.moveRight j

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesMul (Sum.inl (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveRight j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * (mk α✝ β✝ a✝¹ a✝).moveRight j

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
j : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesMul (Sum.inl (i, j))) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * mk α✝ β✝ a✝¹ a✝ + mk α✝¹ β✝¹ a✝³ a✝² * (mk α✝ β✝ a✝¹ a✝).moveRight j -
      (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i * (mk α✝ β✝ a✝¹ a✝).moveRight j

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem map_floor (f : F) (hf : StrictMono f) (a : α) : ⌊f a⌋₊ = ⌊a⌋₊ :=
  floor_congr fun n => by rw [← map_natCast f, hf.le_iff_le]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : LinearOrderedSemiring β
inst✝³ : FloorSemiring α
inst✝² : FloorSemiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
n : ℕ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
rw [← map_natCast f, hf.le_iff_le]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
@[simp] lemma toNat_beq_zero (b : Bool) : (b.toNat == 0) = !b

Proof state:
b : Bool
⊢ (b.toNat == 0) = !b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem dropSlice_zero₂ : ∀ n l, @dropSlice α n 0 l = l
  | 0, [] | 0, _::_ | _+1, [] => rfl
  | n+1, x::xs => by simp [dropSlice, dropSlice_zero₂]

Proof state:
α : Type u_1
n : Nat
x : α
xs : List α
⊢ dropSlice (n + 1) 0 (x :: xs) = x :: xs

Tactic:
simp [dropSlice, dropSlice_zero₂]

Result:
no goals
-- Mathlib/Algebra/Module/Lattice.lean
lemma of_le_of_isLattice_of_fg {M N : Submodule R V} (hle : M ≤ N) [IsLattice A M]
    (hfg : N.FG) : IsLattice A N :=
  ⟨hfg, eq_top_iff.mpr <|
    le_trans (by rw [IsLattice.span_eq_top]) (Submodule.span_mono hle)⟩

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M N : Submodule R V
hle : M ≤ N
inst✝ : IsLattice A M
hfg : N.FG
⊢ ⊤ ≤ span A ↑M

Tactic:
rw [IsLattice.span_eq_top]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_pow [IsReduced R] (f : MvPolynomial σ R) (n : ℕ) :
    m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
rw [leadingCoeff, degree_pow, coeff_pow_nsmul_degree]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem transfer_eq_map_of_le (hp) (GH : G ≤ H) :
    p.transfer H hp = p.map (SimpleGraph.Hom.mapSpanningSubgraphs GH)

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
H : SimpleGraph V
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
GH : G ≤ H
⊢ p.transfer H hp = Walk.map (Hom.mapSpanningSubgraphs GH) p

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
@[ext]
lemma hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y)
    (h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g :=
  NatTrans.ext (by ext; apply h)

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
⊢ f.app = g.app

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowingε₀_one : fastGrowingε₀ 1 = 2

Proof state:
⊢ fastGrowingε₀ 1 = 2

Tactic:
simp [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_zeta_mul_moebius : (ζ * μ : ArithmeticFunction ℤ) = 1

Proof state:
⊢ ↑ζ * μ = 1

Tactic:
rw [mul_comm, moebius_mul_coe_zeta]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp]
lemma essSup_smul_measure (hc : c ≠ 0) (f : α → β) : essSup f (c • μ) = essSup f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : ConditionallyCompleteLattice β
R : Type u_3
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → β
⊢ essSup f (c • μ) = essSup f μ

Tactic:
simp_rw [essSup, Measure.ae_smul_measure_eq hc]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
lemma coprime_add_iff_left (h : a ∣ c) : Coprime a (b + c) ↔ Coprime a b

Proof state:
case intro
a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℕ
h : a ∣ c
⊢ a.Coprime (b + c) ↔ a.Coprime b

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
a b n : ℕ
⊢ a.Coprime (b + a * n) ↔ a.Coprime b
-- Mathlib/Dynamics/BirkhoffSum/Basic.lean
theorem birkhoffSum_apply_sub_birkhoffSum (f : α → α) (g : α → G) (n : ℕ) (x : α) :
    birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x

Proof state:
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x

Tactic:
rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
  ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
  ← sub_add, ← sub_add, sub_add_comm]

Result:
no goals
-- Mathlib/Order/PropInstances.lean
theorem isCompl_iff [∀ i, BoundedOrder (α' i)] {f g : ∀ i, α' i} :
    IsCompl f g ↔ ∀ i, IsCompl (f i) (g i)

Proof state:
ι : Type u_1
α' : ι → Type u_2
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem trace_eq_neg_charpoly_coeff [Nonempty n] (M : Matrix n n R) :
    trace M = -M.charpoly.coeff (Fintype.card n - 1)

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i : n, M.diag i = ∑ i : n, M i i

Tactic:
simp_rw [diag_apply]

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = -M.charpoly.coeff (Fintype.card n - 1)

Tactic:
rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
  prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]

Result:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nonempty n
M : Matrix n n R
⊢ ∑ i : n, M.diag i = ∑ i : n, M i i
-- Mathlib/Order/Filter/Cofinite.lean
theorem coprodᵢ_cofinite {α : ι → Type*} [Finite ι] :
    (Filter.coprodᵢ fun i => (cofinite : Filter (α i))) = cofinite :=
  Filter.coext fun s => by
    simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

Proof state:
ι : Type u_1
α : ι → Type u_4
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i => cofinite) ↔ sᶜ ∈ cofinite

Tactic:
simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_dblY (P : Fin 3 → A) : (W'.baseChange B).toProjective.dblY (f ∘ P) =
    f ((W'.baseChange A).toProjective.dblY P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.dblY (⇑f ∘ P) = f ((baseChange W' A).toProjective.dblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem subset_pair_iff : s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b

Proof state:
α : Type u
s : Set α
a b : α
⊢ s ⊆ {a, b} ↔ ∀ x ∈ s, x = a ∨ x = b

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Filter.Tendsto.max_right {l : Filter β} {a : α} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun i => max a (f i)) l (𝓝 a)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝 a)

Tactic:
convert ((continuous_max.comp (@Continuous.Prod.mk α α _ _ a)).tendsto a).comp h

Result:
case h.e'_5.h.e'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ a = ((fun p => p.1 ⊔ p.2) ∘ fun y => (a, y)) a

Proof state:
case h.e'_5.h.e'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ a = ((fun p => p.1 ⊔ p.2) ∘ fun y => (a, y)) a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
  ⟨fun h => ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩,
   fun h => by simp [h]⟩

Proof state:
i j : Nat
h : i = 0 ∧ j = 0
⊢ i.gcd j = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem ite {c : α → Prop} [DecidablePred c] {f : α → σ} {g : α → σ} (hc : PrimrecPred c)
    (hf : Primrec f) (hg : Primrec g) : Primrec fun a => if c a then f a else g a

Proof state:
α : Type u_1
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable σ
c : α → Prop
inst✝ : DecidablePred c
f g : α → σ
hc : PrimrecPred c
hf : Primrec f
hg : Primrec g
⊢ Primrec fun a => if c a then f a else g a

Tactic:
simpa [Bool.cond_decide] using cond hc hf hg

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem map_le_iff (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
    x.map f ≤ y.map f ↔ x ≤ y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : WithTop α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f x ≤ map f y ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [mono_iff]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulReflectLT_iff_contravariant_pos :
    PosMulReflectLT α ↔ ContravariantClass α>0 α (fun x y => x * y) (· < ·) :=
  ⟨@PosMulReflectLT.to_contravariantClass_pos_mul_lt _ _ _ _, fun h =>
    { elim a b c h

Proof state:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : ↑a * b < ↑a * c
ha : 0 = ↑a
⊢ b < c

Tactic:
simp [← ha] at h

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : ↑a * b < ↑a * c
⊢ b < c

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Result:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : ↑a * b < ↑a * c
ha : 0 = ↑a
⊢ b < c

case inr
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
a : α≥0
b c : α
h : ↑a * b < ↑a * c
ha : 0 < ↑a
⊢ b < c
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_two : Prime 2

Proof state:
⊢ Prime 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem getElem_map {β : Type*} (v : Vector α n) (f : α → β) {i : ℕ} (hi : i < n) :
    (v.map f)[i] = f v[i]

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : ℕ
hi : i < n
⊢ (map f v)[i] = f v[i]

Tactic:
simp only [getElem_def, toList_map, List.getElem_map]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem eq_cuspFunction [NeZero n] [SlashInvariantFormClass F Γ(n) k] (τ : ℍ) :
    cuspFunction n f (𝕢 n τ) = f τ

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : SlashInvariantFormClass F Γ(n) k
τ : ℍ
⊢ cuspFunction n f (𝕢 ↑n ↑τ) = f τ

Tactic:
simpa only [comp_apply, ofComplex_apply]
  using (periodic_comp_ofComplex n f).eq_cuspFunction (NeZero.ne _) τ

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_injective2 : Function.Injective2 (@cons n α) := fun x₀ y₀ x y h ↦
  ⟨congr_fun h 0, funext fun i ↦ by simpa using congr_fun h (Fin.succ i)⟩

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
h : cons x₀ x = cons y₀ y
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (Fin.succ i)

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem mem_closed_set_iff (h : IsGenericPoint x S) (hZ : IsClosed Z) : x ∈ Z ↔ S ⊆ Z

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ S ⊆ Z

Tactic:
rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_swap_right_iff [NoZeroSMulDivisors R V] (x : P) {y z : P} :
    Wbtw R x y z ∧ Wbtw R x z y ↔ y = z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R x z y ↔ y = z

Tactic:
rw [wbtw_comm, wbtw_comm (z := y), eq_comm]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ z = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R z y x ∧ Wbtw R y z x ↔ z = y

Tactic:
exact wbtw_swap_left_iff R x

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem Iso.inv_hom (f : X ≅ Y) : inv f.hom = f.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ inv f.hom = f.inv

Tactic:
apply inv_eq_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.hom ≫ f.inv = 𝟙 X

Proof state:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.hom ≫ f.inv = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
/--
Given `sq' : SqStruct c p f g j`, this is the commutative square
```
               sq'.f'
F.obj j --------------------> X
   |                          |
   |                          |p
   v                      g   v
F.obj (succ j) ---> c.pt ---> Y
```

(Using the lifting property for this square is the key ingredient
in the proof that the left lifting property with respect to `p`
is stable under transfinite composition.) -/
lemma sq [SuccOrder J] :
    CommSq sq'.f' (F.map (homOfLE (Order.le_succ j))) p (c.ι.app _ ≫ g) where
  w

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
inst✝ : SuccOrder J
⊢ sq'.f' ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app (Order.succ j) ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem inv_eq_of_lf_zero {x : PGame} (h : x ⧏ 0) : x⁻¹ = -inv' (-x)

Proof state:
x : PGame
h : x ⧏ 0
⊢ x⁻¹ = -(-x).inv'

Tactic:
exact (if_neg h.not_equiv).trans (if_neg h.not_gt)

Result:
no goals

Proof state:
x : PGame
h : x ⧏ 0
⊢ x⁻¹ = -(-x).inv'

Tactic:
classical exact (if_neg h.not_equiv).trans (if_neg h.not_gt)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Derivation.lean
theorem derivation_C_mul (D : Derivation R (MvPolynomial σ R) A) (a : R) (f : MvPolynomial σ R) :
    C (σ := σ) a • D f = a • D f

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Tactic:
rw [this, C_mul', D.map_smul]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ C a • D f = a • D f

Tactic:
have : C (σ := σ) a • D f = D (C a * f) := by simp

Result:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f

Proof state:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ C a • D f = D (C a * f)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_isInfix : ∀ l : List α, Chain' (fun x y => [x, y] <:+: l) l
  | [] => chain'_nil
  | [_] => chain'_singleton _
  | a :: b :: l =>
    chain'_cons.2
      ⟨⟨[], l, by simp⟩, (chain'_isInfix (b :: l)).imp fun _ _ h => h.trans ⟨[a], [], by simp⟩⟩

Proof state:
α : Type u
a b : α
l : List α
⊢ [] ++ [a, b] ++ l = a :: b :: l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a b : α
l : List α
x✝¹ x✝ : α
h : [x✝¹, x✝] <:+: b :: l
⊢ [a] ++ b :: l ++ [] = a :: b :: l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w)

Proof state:
w : Nat
a : BitVec w
⊢ ~~~a + a = -1#w

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
a : BitVec w
⊢ a + ~~~a = -1#w

Proof state:
w : Nat
a : BitVec w
⊢ a + ~~~a = -1#w

Tactic:
rw [BitVec.add_not]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem dist_le_opNorm (x y : E) : dist (f x) (f y) ≤ ‖f‖ * dist x y

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x y : E
⊢ dist (f x) (f y) ≤ ‖f‖ * dist x y

Tactic:
simp_rw [dist_eq_norm, ← map_sub, f.le_opNorm]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_mul (x y : α) : sign (x * y) = sign x * sign y

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x y : α
⊢ sign (x * y) = sign x * sign y

Tactic:
rcases lt_trichotomy x 0 with (hx | hx | hx) <;> rcases lt_trichotomy y 0 with (hy | hy | hy) <;>
  simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Result:
no goals