harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Perfection.lean
theorem coeff_pow_p (f : Ring.Perfection R p) (n : ℕ) :
    coeff R p (n + 1) (f ^ p) = coeff R p n f

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ (coeff R p (n + 1)) (f ^ p) = (coeff R p n) f

Tactic:
rw [RingHom.map_pow]

Result:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ (coeff R p (n + 1)) f ^ p = (coeff R p n) f

Proof state:
R : Type u₁
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
f : Ring.Perfection R p
n : ℕ
⊢ (coeff R p (n + 1)) f ^ p = (coeff R p n) f

Tactic:
exact f.2 n

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_union_of_symmetric (hr : Symmetric r) :
    (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b :=
  pairwise_union.trans <| by simp only [hr.iff, and_self_iff]

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
hr : Symmetric r
⊢ (s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a) ↔
    s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b

Tactic:
simp only [hr.iff, and_self_iff]

Result:
no goals
-- Mathlib/Algebra/Algebra/Equiv.lean
theorem algebraMap_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :
    algebraMap R A₂ y = e x ↔ algebraMap R A₁ y = x :=
  ⟨fun h => by simpa using e.symm.toAlgHom.algebraMap_eq_apply h, fun h =>
    e.toAlgHom.algebraMap_eq_apply h⟩

Proof state:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
y : R
x : A₁
h : (algebraMap R A₂) y = e x
⊢ (algebraMap R A₁) y = x

Tactic:
simpa using e.symm.toAlgHom.algebraMap_eq_apply h

Result:
no goals
-- Mathlib/NumberTheory/Wilson.lean
theorem prod_Ico_one_prime : ∏ x ∈ Ico 1 p, (x : ZMod p) = -1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - succ 0).succ, ↑x = -1

Tactic:
rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 p, ↑x = -1

Tactic:
conv =>
  congr
  congr
  rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - succ 0).succ, ↑x = -1
-- Mathlib/Order/BooleanAlgebra.lean
theorem disjoint_sdiff_iff_le (hz : z ≤ y) (hx : x ≤ y) : Disjoint z (y \ x) ↔ z ≤ x :=
  ⟨fun H =>
    le_of_inf_le_sup_le (le_trans H.le_bot bot_le)
      (by
        rw [sup_sdiff_cancel_right hx]
        refine le_trans (sup_le_sup_left sdiff_le z) ?_
        rw [sup_eq_right.2 hz]),
    fun H => disjoint_sdiff_self_right.mono_left H⟩

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y

Tactic:
rw [sup_eq_right.2 hz]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x

Tactic:
rw [sup_sdiff_cancel_right hx]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y

Tactic:
refine le_trans (sup_le_sup_left sdiff_le z) ?_

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y ≤ y
-- Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
@[simp]
lemma Functor.imageSieve_map {U V : C} (f : U ⟶ V) : G.imageSieve (G.map f) = ⊤

Proof state:
C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
⊢ G.imageSieve (G.map f) = ⊤

Tactic:
ext W g

Result:
case h
C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ ⊤.arrows g

Proof state:
case h
C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ ⊤.arrows g

Tactic:
simpa using ⟨g ≫ f, by simp⟩

Result:
no goals

Proof state:
C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ G.map (g ≫ f) = G.map g ≫ G.map f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_bmod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ bmod x m - x

Proof state:
case isFalse
x : Int
m : Nat
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - x - ↑m

Tactic:
exact Int.dvd_sub dvd_emod_sub_self (Int.dvd_refl _)

Result:
no goals

Proof state:
case isFalse
x : Int
m : Nat
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - ↑m - x

Tactic:
rw [Int.sub_sub, Int.add_comm, ← Int.sub_sub]

Result:
case isFalse
x : Int
m : Nat
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - x - ↑m

Proof state:
x : Int
m : Nat
⊢ ↑m ∣ x.bmod m - x

Tactic:
dsimp [bmod]

Result:
x : Int
m : Nat
⊢ ↑m ∣ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) - x

Proof state:
case isTrue
x : Int
m : Nat
h✝ : x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - x

Tactic:
exact dvd_emod_sub_self

Result:
no goals

Proof state:
x : Int
m : Nat
⊢ ↑m ∣ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) - x

Tactic:
split

Result:
case isTrue
x : Int
m : Nat
h✝ : x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - x

case isFalse
x : Int
m : Nat
h✝ : ¬x % ↑m < (↑m + 1) / 2
⊢ ↑m ∣ x % ↑m - ↑m - x
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[to_additive (attr := simp)]
lemma insertNth_div_same [∀ j, Group (α j)] (i : Fin (n + 1)) (x y : α i)
    (p : ∀ j, α (i.succAbove j)) : i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Tactic:
simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]

Result:
no goals
-- Mathlib/Algebra/Field/ZMod.lean
theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
obtain ⟨k, rfl⟩ := natCast_zmod_surjective a

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1

Proof state:
case intro.h
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ k.Coprime p

Tactic:
apply Nat.Coprime.symm

Result:
case intro.h.a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ p.Coprime k

Proof state:
case intro.h.a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ p.Coprime k

Tactic:
rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]

Result:
no goals

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1

Tactic:
apply coe_mul_inv_eq_one

Result:
case intro.h
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ k.Coprime p
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIoc_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ioc a (a + p)) :
    liftIoc p a f ↑x = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : (equivIoc p a) ↑x = ⟨x, hx⟩
⊢ (Ioc a (a + p)).restrict f ⟨x, hx⟩ = f x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ liftIoc p a f ↑x = f x

Tactic:
have : (equivIoc p a) x = ⟨x, hx⟩ := by
  rw [Equiv.apply_eq_iff_eq_symm_apply]
  rfl

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : (equivIoc p a) ↑x = ⟨x, hx⟩
⊢ liftIoc p a f ↑x = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ (equivIoc p a) ↑x = ⟨x, hx⟩

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply]

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑x = (equivIoc p a).symm ⟨x, hx⟩

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : (equivIoc p a) ↑x = ⟨x, hx⟩
⊢ liftIoc p a f ↑x = f x

Tactic:
rw [liftIoc, comp_apply, this]

Result:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
this : (equivIoc p a) ↑x = ⟨x, hx⟩
⊢ (Ioc a (a + p)).restrict f ⟨x, hx⟩ = f x

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑x = (equivIoc p a).symm ⟨x, hx⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem isInvariant_of_support_le {c : Perm α} {s : Finset α} (hcs : c.support ≤ s) (x : α) :
    x ∈ s ↔ c x ∈ s

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∉ c.support
⊢ x ∈ s ↔ c x ∈ s

Tactic:
rw [not_mem_support.mp hx']

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
⊢ x ∈ s ↔ c x ∈ s

Tactic:
by_cases hx' : x ∈ c.support

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∈ c.support
⊢ x ∈ s ↔ c x ∈ s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∉ c.support
⊢ x ∈ s ↔ c x ∈ s

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∈ c.support
⊢ x ∈ s ↔ c x ∈ s

Tactic:
simp only [hcs hx', true_iff, hcs (apply_mem_support.mpr hx')]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive norm_nsmul_le]
lemma norm_pow_le_mul_norm : ∀ {n : ℕ}, ‖a ^ n‖ ≤ n * ‖a‖
  | 0 => by simp
  | n + 1 => by simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a ^ 0‖ ≤ ↑0 * ‖a‖

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖

Tactic:
simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/MulOpposite.lean
theorem unop_closure (s : Set Rᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Proof state:
R : Type u_2
inst✝ : Ring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
s : Set Rᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]

Result:
R : Type u_2
inst✝ : Ring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem conj_iff {a x y b : G} :
    SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Proof state:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a

Tactic:
simp only [← mul_assoc, inv_mul_cancel_right]

Result:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a

Proof state:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a

Tactic:
repeat rw [mul_assoc]

Result:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Proof state:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y

Tactic:
unfold SemiconjBy

Result:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a

Proof state:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * y * (a * b⁻¹) ↔ a * x = y * a

Tactic:
rw [mul_assoc]

Result:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Proof state:
G : Type u_3
inst✝ : Group G
a x y b : G
⊢ b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a

Tactic:
rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Conjneg.lean
@[simp] lemma conjneg_nonpos : conjneg f ≤ 0 ↔ f ≤ 0

Proof state:
G : Type u_1
R : Type u_2
inst✝³ : AddGroup G
inst✝² : OrderedCommRing R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f ≤ 0 ↔ f ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← conjneg_neg, conjneg_nonneg]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean
lemma morphismProperty_eq_top
    (W : MorphismProperty SimplexCategory) [W.IsMultiplicative]
    (δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (SimplexCategory.δ i))
    (σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (SimplexCategory.σ i)) :
    W = ⊤

Proof state:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f

Tactic:
change W.inverseImage (Truncated.inclusion _)
  (f : ⟨a, Nat.le_max_left _ _⟩ ⟶ ⟨b, Nat.le_max_right _ _⟩)

Result:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W.inverseImage (Truncated.inclusion (a.len ⊔ b.len)) f

Proof state:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f ↔ ⊤ f

Tactic:
simp only [MorphismProperty.top_apply, iff_true]

Result:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f

Proof state:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W.inverseImage (Truncated.inclusion (a.len ⊔ b.len)) f

Tactic:
simp only [hW, MorphismProperty.top_apply]

Result:
no goals

Proof state:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤

Tactic:
have hW (d : ℕ) : W.inverseImage (Truncated.inclusion d) = ⊤ :=
  Truncated.morphismProperty_eq_top _ (fun _ _ i ↦ δ_mem i)
    (fun _ _ i ↦ σ_mem i)

Result:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
⊢ W = ⊤

Proof state:
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
⊢ W = ⊤

Tactic:
ext a b f

Result:
case h
W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ W f ↔ ⊤ f
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma nnnorm_zpow_le (x : S) (z : ℤ) :
    ‖x ^ z‖₊ ≤ ‖x‖₊

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
z : ℤ
⊢ ‖x ^ z‖₊ ≤ ‖x‖₊

Tactic:
cases z <;>
simpa using nnnorm_pow_le _ _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma one_eq_ofENat {m : ℕ∞} : 1 = (m : Cardinal) ↔ m = 1

Proof state:
m : ℕ∞
⊢ 1 = ↑m ↔ m = 1

Tactic:
norm_cast

Result:
m : ℕ∞
⊢ 1 = m ↔ m = 1

Proof state:
m : ℕ∞
⊢ 1 = m ↔ m = 1

Tactic:
apply eq_comm

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Hom.lean
theorem Commute.of_map [MulHomClass F M N] {f : F} (hf : Function.Injective f)
    (h : Commute (f x) (f y)) : Commute x y :=
  hf (by simpa only [map_mul] using h.eq)

Proof state:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f (x * y) = f (y * x)

Tactic:
simpa only [map_mul] using h.eq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem beqFalseOfEqFalse {a b : Nat} (p : (a = b) = False) : (a == b) = false

Proof state:
a b : Nat
p : (a = b) = False
⊢ (a == b) = false

Tactic:
simp [Bool.beq_eq_decide_eq, p]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem append_reverseAux {u v w x : V}
    (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk u x) :
    (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w x u✝ : V
q : G.Walk u✝ w
r : G.Walk u✝ x
⊢ (nil.append q).reverseAux r = q.reverseAux (nil.reverseAux r)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w x u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : ∀ (q : G.Walk w✝ w) (r : G.Walk v✝ x), (p✝.append q).reverseAux r = q.reverseAux (p✝.reverseAux r)
q : G.Walk w✝ w
r : G.Walk u✝ x
⊢ ((cons h p✝).append q).reverseAux r = q.reverseAux ((cons h p✝).reverseAux r)

Tactic:
exact ih q (cons (G.symm h) r)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk u x
⊢ (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

Tactic:
induction p with
| nil => rfl
| cons h _ ih => exact ih q (cons (G.symm h) r)

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_le_one_iff_subsingleton [Finite α] : Nat.card α ≤ 1 ↔ Subsingleton α

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_one_sub_lt_of_lt (h : a < b) : b - 1 - a < b

Proof state:
a b : Nat
h : a < b
⊢ b - (1 + a) < b

Tactic:
exact sub_lt (zero_lt_of_lt h) (Nat.lt_add_right a Nat.one_pos)

Result:
no goals

Proof state:
a b : Nat
h : a < b
⊢ b - 1 - a < b

Tactic:
rw [← Nat.sub_add_eq]

Result:
a b : Nat
h : a < b
⊢ b - (1 + a) < b
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderivWithin_comp_of_preimage_mem_nhdsWithin
    (hg : MDifferentiableWithinAt I' I'' g u (f x))
    (hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x)
    (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I'' (g ∘ f) s x =
      (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
B : mfderivWithin I I'' (g ∘ f) s x = mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x
C : mfderivWithin I I' f s x = mfderivWithin I I' f (s ∩ f ⁻¹' u) x
⊢ mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x)

Tactic:
rw [B, C]

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
u : Set M'
hg : MDifferentiableWithinAt I' I'' g u (f x)
hf : MDifferentiableWithinAt I I' f s x
h : f ⁻¹' u ∈ 𝓝[s] x
hxs : UniqueMDiffWithinAt I s x
A : s ∩ f ⁻¹' u ∈ 𝓝[s] x
B : mfderivWithin I I'' (g ∘ f) s x = mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x
C : mfderivWithin I I' f s x = mfderivWithin I I' f (s ∩ f ⁻¹' u) x
⊢ mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x =
    (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f (s ∩ f ⁻¹' u) x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_empty_list_le [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} :
    (insertMany empty l).1.1.size ≤ l.length

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (empty.insertMany l).val.val.size ≤ 0 + l.length

Tactic:
apply (size_insertMany_list_le _ Raw.WF.empty₀)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (empty.insertMany l).val.val.size ≤ l.length

Tactic:
rw [← Nat.zero_add l.length]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (empty.insertMany l).val.val.size ≤ 0 + l.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tmod_left (a b : Int) : (a * b).tmod b = 0 :=
  if h : b = 0 then by simp [h, Int.mul_zero] else by
    rw [Int.tmod_def, Int.mul_tdiv_cancel _ h, Int.mul_comm, Int.sub_self]

Proof state:
a b : Int
h : ¬b = 0
⊢ (a * b).tmod b = 0

Tactic:
rw [Int.tmod_def, Int.mul_tdiv_cancel _ h, Int.mul_comm, Int.sub_self]

Result:
no goals

Proof state:
a b : Int
h : b = 0
⊢ (a * b).tmod b = 0

Tactic:
simp [h, Int.mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_eq_toNat_of_lt {x : BitVec n} (h : 2 * x.toNat < 2^n) :
    x.toInt = x.toNat

Proof state:
n : Nat
x : BitVec n
h : 2 * x.toNat < 2 ^ n
⊢ x.toInt = ↑x.toNat

Tactic:
simp [toInt_eq_toNat_cond, h]

Result:
no goals