harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_id : nfp id = id

Proof state:
case h
x✝ : Ordinal.{u_1}
⊢ ⨆ n, id x✝ = id x✝

Tactic:
exact ciSup_const

Result:
no goals

Proof state:
⊢ nfp id = id

Tactic:
ext

Result:
case h
x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝

Proof state:
case h
x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝

Tactic:
simp_rw [← iSup_iterate_eq_nfp, iterate_id]

Result:
case h
x✝ : Ordinal.{u_1}
⊢ ⨆ n, id x✝ = id x✝
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute (h : Commute x y) :
    (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_left_inj {a : R} (ha : a ≠ 0) {i j : ℕ} :
    monomial i a = monomial j a ↔ i = j

Proof state:
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
i j : ℕ
⊢ (monomial i) a = (monomial j) a ↔ i = j

Tactic:
simp only [← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem univ_pi_piecewise {ι : Type*} {α : ι → Type*} (s : Set ι) (t t' : ∀ i, Set (α i))
    [∀ x, Decidable (x ∈ s)] : pi univ (s.piecewise t t') = pi s t ∩ pi sᶜ t'

Proof state:
ι : Type u_8
α : ι → Type u_9
s : Set ι
t t' : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t t') = s.pi t ∩ sᶜ.pi t'

Tactic:
simp [compl_eq_univ_diff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_lt_right_of_lt_add {a b c : Int} (h : a < b + c) : -c + a < b

Proof state:
a b c : Int
h : a < b + c
⊢ -c + a < b

Tactic:
rw [Int.add_comm] at h

Result:
a b c : Int
h : a < c + b
⊢ -c + a < b

Proof state:
a b c : Int
h : a < c + b
⊢ -c + a < b

Tactic:
exact Int.neg_add_lt_left_of_lt_add h

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem sub_eq_add (x y : R) : x - y = x + y

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x - y = x + y

Tactic:
rw [sub_eq_add_neg, neg_eq]

Result:
no goals
-- Mathlib/Logic/Function/DependsOn.lean
/-- A function which depends on the empty set is constant. -/
lemma DependsOn.empty (hf : DependsOn f ∅) (x y : Π i, α i) : f x = f y := hf (by simp)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
hf : DependsOn f ∅
x y : (i : ι) → α i
⊢ ∀ i ∈ ∅, x i = y i

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.strictConvexOn (hf : UniformConvexOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) :
    StrictConvexOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
⊢ StrictConvexOn ℝ s f

Tactic:
refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt <|
  sub_lt_self _ ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : 0 < φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
have := hφ _ hxy.ne'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this : 0 < φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_add_pi_div_two (x : ℝ) : sin (x + π / 2) = cos x

Proof state:
x : ℝ
⊢ sin (x + π / 2) = cos x

Tactic:
simp [sin_add]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc]
lemma cyclesMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData) :
    cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
let γ₂ := leftHomologyMapData φ₂ h₂ h₃

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.cyclesMap'_eq, γ₂.cyclesMap'_eq, (γ₁.comp γ₂).cyclesMap'_eq,
  LeftHomologyMapData.comp_φK]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃

Tactic:
let γ₁ := leftHomologyMapData φ₁ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ cyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = cyclesMap' φ₁ h₁ h₂ ≫ cyclesMap' φ₂ h₂ h₃
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_bot [Nonempty V] : (⊥ : SimpleGraph V).chromaticNumber = 1

Proof state:
V : Type u
inst✝ : Nonempty V
⊢ ⊥.chromaticNumber = 1

Tactic:
have : (⊥ : SimpleGraph V).Colorable 1 := ⟨.mk 0 <| by simp⟩

Result:
V : Type u
inst✝ : Nonempty V
this : ⊥.Colorable 1
⊢ ⊥.chromaticNumber = 1

Proof state:
V : Type u
inst✝ : Nonempty V
this : ⊥.Colorable 1
⊢ ⊥.chromaticNumber = 1

Tactic:
exact this.chromaticNumber_le.antisymm <| Order.one_le_iff_pos.2 <| chromaticNumber_pos this

Result:
no goals

Proof state:
V : Type u
inst✝ : Nonempty V
⊢ ∀ {v w : V}, ⊥.Adj v w → 0 v ≠ 0 w

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_sub_int (x : α) (y : ℤ) : round (x - y) = round x - y

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y

Tactic:
norm_cast

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x - ↑y) = round x - y

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + -↑y) = round x - y

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑(-y)) = round x - y

Tactic:
rw [round_add_int, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (init : β) (l : Vector α n) :
    forIn l init f = ForInStep.value <$>
      l.foldlM (fun b a => match b with
        | .yield b => f a b
        | .done b => pure (.done b)) (ForInStep.yield init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Vector α n
⊢ forIn l init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Array α
⊢ forIn { toArray := l, size_toArray := ⋯ } init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Array α
⊢ forIn { toArray := l, size_toArray := ⋯ } init f =
    ForInStep.value <$>
      foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.forIn_eq_foldlM]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Array α
⊢ ForInStep.value <$>
      Array.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    ForInStep.value <$>
      Array.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
init : β
l : Array α
⊢ ForInStep.value <$>
      Array.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    ForInStep.value <$>
      Array.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => f a b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem singleton_mul_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : {a} * s ∈ 𝓝 a

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ {a} * s ∈ 𝓝 a

Tactic:
simpa only [mul_one] using singleton_mul_mem_nhds a h

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem inl_injective : Function.Injective (inl R M M₂) := fun _ => by simp

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M
⊢ ∀ ⦃a₂ : M⦄, (inl R M M₂) x✝ = (inl R M M₂) a₂ → x✝ = a₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_ne_of_natTrailingDegree_ne {n : ℕ} :
    p.natTrailingDegree ≠ n → trailingDegree p ≠ n :=
  mt fun h => by rw [natTrailingDegree, h, ENat.toNat_coe]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = ↑n
⊢ p.natTrailingDegree = n

Tactic:
rw [natTrailingDegree, h, ENat.toNat_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn_yield_eq_elim [Monad m] [LawfulMonad m] (o : Option α)
    (f : (a : α) → β → m γ) (g : (a : α) → β → γ → β) (b : β) :
    forIn o b (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
      o.elim (pure b) (fun a => g a b <$> f a b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : α → β → m γ
g : α → β → γ → β
b : β
⊢ (forIn o b fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = o.elim (pure b) fun a => g a b <$> f a b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_max_distrib_left : ∀ (a b c : Nat), min a (max b c) = max (min a b) (min a c)
  | 0, _, _ => by simp only [Nat.zero_min, Nat.max_self]
  | _, 0, _ => by simp only [Nat.min_zero, Nat.zero_max]
  | _, _, 0 => by simp only [Nat.min_zero, Nat.max_zero]
  | _+1, _+1, _+1 => by
    simp only [Nat.succ_max_succ, Nat.succ_min_succ]
    exact congrArg succ <| Nat.min_max_distrib_left ..

Proof state:
x✝¹ x✝ : Nat
⊢ min x✝¹ (max x✝ 0) = max (min x✝¹ x✝) (min x✝¹ 0)

Tactic:
simp only [Nat.min_zero, Nat.max_zero]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ min 0 (max x✝¹ x✝) = max (min 0 x✝¹) (min 0 x✝)

Tactic:
simp only [Nat.zero_min, Nat.max_self]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ min x✝¹ (max 0 x✝) = max (min x✝¹ 0) (min x✝¹ x✝)

Tactic:
simp only [Nat.min_zero, Nat.zero_max]

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ min (n✝² + 1) (max (n✝¹ + 1) (n✝ + 1)) = max (min (n✝² + 1) (n✝¹ + 1)) (min (n✝² + 1) (n✝ + 1))

Tactic:
simp only [Nat.succ_max_succ, Nat.succ_min_succ]

Result:
n✝² n✝¹ n✝ : Nat
⊢ (min n✝² (max n✝¹ n✝)).succ = (max (min n✝² n✝¹) (min n✝² n✝)).succ

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ (min n✝² (max n✝¹ n✝)).succ = (max (min n✝² n✝¹) (min n✝² n✝)).succ

Tactic:
exact congrArg succ <| Nat.min_max_distrib_left ..

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

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

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
n : Nat
inst✝ : LawfulBEq α
a b : α
h : (!b == a) = true
⊢ (mkArray n a).erase b = mkArray 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 ∈ mkArray n a
-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean
theorem isDiag_conjTranspose_iff [Semiring α] [StarRing α] {A : Matrix n n α} :
    Aᴴ.IsDiag ↔ A.IsDiag :=
  ⟨fun ha => by
    convert ha.conjTranspose
    simp, IsDiag.conjTranspose⟩

Proof state:
α : Type u_1
n : Type u_4
inst✝¹ : Semiring α
inst✝ : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A.IsDiag

Tactic:
convert ha.conjTranspose

Result:
case h.e'_4
α : Type u_1
n : Type u_4
inst✝¹ : Semiring α
inst✝ : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A = Aᴴᴴ

Proof state:
case h.e'_4
α : Type u_1
n : Type u_4
inst✝¹ : Semiring α
inst✝ : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A = Aᴴᴴ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
@[simp]
lemma image_preimage (e : α ≃ᵐ β) (s : Set β) : e '' (e ⁻¹' s) = s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ ⇑e '' (⇑e ⁻¹' s) = s

Tactic:
rw [← coe_toEquiv, Equiv.image_preimage]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
    (x ^^^ y) >>> n = (x >>> n) ^^^ (y >>> n)

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ^^^ y) >>> n = x >>> n ^^^ y >>> n

Tactic:
ext

Result:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x ^^^ y) >>> n).getLsbD i✝ = (x >>> n ^^^ y >>> n).getLsbD i✝

Proof state:
case pred
w : Nat
x y : BitVec w
n i✝ : Nat
a✝ : i✝ < w
⊢ ((x ^^^ y) >>> n).getLsbD i✝ = (x >>> n ^^^ y >>> n).getLsbD i✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div (a b c : G) : a * (b / c) = a * b / c

Proof state:
G : Type u_3
inst✝ : DivInvMonoid G
a b c : G
⊢ a * (b / c) = a * b / c

Tactic:
simp only [mul_assoc, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_max {x y p : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hp : 0 ≤ p) :
    (max x y) ^ p = max (x ^ p) (y ^ p)

Proof state:
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
⊢ (x ⊔ y) ^ p = x ^ p ⊔ y ^ p

Tactic:
rcases le_total x y with hxy | hxy

Result:
case inl
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
⊢ (x ⊔ y) ^ p = x ^ p ⊔ y ^ p

case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ (x ⊔ y) ^ p = x ^ p ⊔ y ^ p

Proof state:
case inl
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : x ≤ y
⊢ (x ⊔ y) ^ p = x ^ p ⊔ y ^ p

Tactic:
rw [max_eq_right hxy, max_eq_right (rpow_le_rpow hx hxy hp)]

Result:
no goals

Proof state:
case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ (x ⊔ y) ^ p = x ^ p ⊔ y ^ p

Tactic:
rw [max_eq_left hxy, max_eq_left (rpow_le_rpow hy hxy hp)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_reverse (L : Vector (Vector α m) n) :
    L.reverse.flatten = (L.map reverse).flatten.reverse

Proof state:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.reverse.flatten =
    (map reverse
          {
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }).flatten.reverse

Tactic:
simp [Array.flatten_reverse]

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
⊢ L.reverse.flatten = (map reverse L).flatten.reverse

Tactic:
cases L using vector₂_induction

Result:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.reverse.flatten =
    (map reverse
          {
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }).flatten.reverse
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_pow_two_sub_one_eq_mod (x n : Nat) : x &&& 2^n - 1 = x % 2^n

Proof state:
case pred
x n i : Nat
⊢ (x &&& 2 ^ n - 1).testBit i = (x % 2 ^ n).testBit i

Tactic:
simp only [testBit_and, testBit_mod_two_pow]

Result:
case pred
x n i : Nat
⊢ (x.testBit i && (2 ^ n - 1).testBit i) = (decide (i < n) && x.testBit i)

Proof state:
case pred
x n : Nat
⊢ ∀ (i : Nat), (x &&& 2 ^ n - 1).testBit i = (x % 2 ^ n).testBit i

Tactic:
intro i

Result:
case pred
x n i : Nat
⊢ (x &&& 2 ^ n - 1).testBit i = (x % 2 ^ n).testBit i

Proof state:
case pred
x n i : Nat
⊢ (x.testBit i && (2 ^ n - 1).testBit i) = (decide (i < n) && x.testBit i)

Tactic:
cases testBit x i <;> simp

Result:
no goals

Proof state:
x n : Nat
⊢ x &&& 2 ^ n - 1 = x % 2 ^ n

Tactic:
apply eq_of_testBit_eq

Result:
case pred
x n : Nat
⊢ ∀ (i : Nat), (x &&& 2 ^ n - 1).testBit i = (x % 2 ^ n).testBit i
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.stieltjesFunctionAux_def' (f : α → ℚ → ℝ) (a : α) :
    IsMeasurableRatCDF.stieltjesFunctionAux f a
      = fun (t : ℝ) ↦ ⨅ r : { r' : ℚ // t < r' }, f a r

Proof state:
case h
α : Type u_1
f : α → ℚ → ℝ
a : α
t : ℝ
⊢ stieltjesFunctionAux f a t = ⨅ r, f a ↑r

Tactic:
exact IsMeasurableRatCDF.stieltjesFunctionAux_def f a t

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ stieltjesFunctionAux f a = fun t => ⨅ r, f a ↑r

Tactic:
ext t

Result:
case h
α : Type u_1
f : α → ℚ → ℝ
a : α
t : ℝ
⊢ stieltjesFunctionAux f a t = ⨅ r, f a ↑r
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasStrictFDerivAt.abs_of_pos (hf : HasStrictFDerivAt f f' x)
    (h₀ : 0 < f x) : HasStrictFDerivAt (fun x ↦ |f x|) f' x

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
y : E
⊢ f' y = ((ContinuousLinearMap.smulRight 1 1).comp f') y

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
⊢ f' = (ContinuousLinearMap.smulRight 1 1).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
y : E
⊢ f' y = ((ContinuousLinearMap.smulRight 1 1).comp f') y

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
⊢ HasStrictFDerivAt (fun x => |f x|) f' x

Tactic:
convert (hasStrictDerivAt_abs_pos h₀).hasStrictFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : 0 < f x
⊢ f' = (ContinuousLinearMap.smulRight 1 1).comp f'