harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Pell.lean
theorem exists_pos_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃ a : Solution₁ d, 1 < a.x ∧ 0 < a.y

Proof state:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, 1 < a.x ∧ 0 < a.y

Tactic:
refine ⟨mk |x| |y| (by rwa [sq_abs, sq_abs]), ?_, abs_pos.mpr hy⟩

Result:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < (mk |x| |y| ⋯).x

Proof state:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < (mk |x| |y| ⋯).x

Tactic:
rw [x_mk, ← one_lt_sq_iff_one_lt_abs, eq_add_of_sub_eq h, lt_add_iff_pos_right]

Result:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2

Proof state:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2

Tactic:
exact mul_pos h₀ (sq_pos_of_ne_zero hy)

Result:
no goals

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ |x| ^ 2 - d * |y| ^ 2 = 1

Tactic:
rwa [sq_abs, sq_abs]

Result:
no goals

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, 1 < a.x ∧ 0 < a.y

Tactic:
obtain ⟨x, y, h, hy⟩ := exists_of_not_isSquare h₀ hd

Result:
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, 1 < a.x ∧ 0 < a.y
-- Mathlib/Data/Finsupp/Single.lean
theorem equivFunOnFinite_symm_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ equivFunOnFinite.symm (Pi.single x m) = single x m

Tactic:
rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem cofan_inj_epi_naturality {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : IndexSet Δ₁) (p : Δ₁ ⟶ Δ₂)
    [Epi p.unop] : (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.cofan Δ₁).inj A ≫ X.map p = (s.cofan Δ₂).inj (A.epiComp p)

Tactic:
dsimp [cofan]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.ι (unop A.fst).len ≫ X.map A.e.op) ≫ X.map p = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (s.ι (unop A.fst).len ≫ X.map A.e.op) ≫ X.map p = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op

Tactic:
rw [assoc, ← X.map_comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ s.ι (unop A.fst).len ≫ X.map (A.e.op ≫ p) = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ s.ι (unop A.fst).len ≫ X.map (A.e.op ≫ p) = s.ι (unop A.fst).len ≫ X.map (A.epiComp p).e.op

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem not_decide_mod_two_eq_one (x : Nat)
    : (!decide (x % 2 = 1)) = decide (x % 2 = 0)

Proof state:
case inr
x : Nat
p : x % 2 = 1
⊢ (!decide (x % 2 = 1)) = decide (x % 2 = 0)

Tactic:
simp [p]

Result:
no goals

Proof state:
x : Nat
⊢ (!decide (x % 2 = 1)) = decide (x % 2 = 0)

Tactic:
cases Nat.mod_two_eq_zero_or_one x <;> (rename_i p; simp [p])

Result:
no goals

Proof state:
case inr
x : Nat
h✝ : x % 2 = 1
⊢ (!decide (x % 2 = 1)) = decide (x % 2 = 0)

Tactic:
rename_i p

Result:
case inr
x : Nat
p : x % 2 = 1
⊢ (!decide (x % 2 = 1)) = decide (x % 2 = 0)
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_sSup : x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
𝒮 : Set ↥L
x : X
⊢ x ∈ sSup 𝒮 ↔ ∃ T ∈ 𝒮, x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
@[simp] lemma add_modEq_right : a + n ≡ a [MOD n]

Proof state:
n a : ℕ
⊢ a + n ≡ a [MOD n]

Tactic:
rw [ModEq, add_mod_right]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Ico {a b : ℝ} : volume (Ico a b) = ofReal (b - a)

Proof state:
a b : ℝ
⊢ volume (Ico a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
lemma homologyMap'_congr (h : Homotopy φ₁ φ₂) (h₁ : S₁.HomologyData)
    (h₂ : S₂.HomologyData) : homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivLeft_X_none : optionEquivLeft R S₁ (X none) = Polynomial.X

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivLeft R S₁) (X none) = Polynomial.X

Tactic:
simp [optionEquivLeft_apply, aeval_X]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem nnabs_coe (x : ℝ≥0) : nnabs x = x

Proof state:
x : ℝ≥0
⊢ nnabs ↑x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_right_of_pos (x y : V) {r : ℝ} (hr : 0 < r) :
    o.oangle x (r • y) = o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : 0 < r
⊢ o.oangle x (r • y) = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_mapIdx {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {g : Nat → α → β}
    (h : ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i]) :
    l.mapFinIdx f = l.mapIdx g

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : (i : Nat) → α → i < n → β
g : Nat → α → β
h : ∀ (i : Nat) (h : i < n), f i l[i] h = g i l[i]
⊢ l.mapFinIdx f = mapIdx g l

Tactic:
simp_all [mapFinIdx_eq_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem one_le_of_le_mul_left [MulRightReflectLE α] {a b : α}
    (h : b ≤ a * b) :
    1 ≤ a :=
  le_of_mul_le_mul_right' (a := b) <| by simpa only [one_mul]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
simpa only [one_mul]

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem measure_mem_eq (h : IdentDistrib f g μ ν) {s : Set γ} (hs : MeasurableSet s) :
    μ (f ⁻¹' s) = ν (g ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
h : IdentDistrib f g μ ν
s : Set γ
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) = ν (g ⁻¹' s)

Tactic:
rw [← Measure.map_apply_of_aemeasurable h.aemeasurable_fst hs, ←
  Measure.map_apply_of_aemeasurable h.aemeasurable_snd hs, h.map_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Localization.lean
lemma iff {X Y : C} (f : X ⟶ Y) (a : A) : W (f⟦a⟧') ↔ W f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W ((shiftFunctor C a).map f) ↔ W f

Tactic:
conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W ((shiftFunctor C a).map f) ↔ W.inverseImage (shiftFunctor C a) f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W ((shiftFunctor C a).map f) ↔ W.inverseImage (shiftFunctor C a) f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.periodicPts_add_left [NeZero n] (x : G) : periodicPts (x + ·) = .univ :=
  Set.eq_univ_of_forall fun y ↦ ⟨n, NeZero.pos n, by
    simpa [char_nsmul_eq_zero, IsPeriodicPt] using isFixedPt_id _⟩

Proof state:
n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : NeZero n
x y : G
⊢ IsPeriodicPt (fun x_1 => x + x_1) n y

Tactic:
simpa [char_nsmul_eq_zero, IsPeriodicPt] using isFixedPt_id _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Basic.lean
theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
  | 0 => rfl
  | k + 1 => by simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]

Proof state:
m n k : Nat
⊢ m >>> (n + (k + 1)) = m >>> n >>> (k + 1)

Tactic:
simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem continuous_insertIdx {n : ℕ} : Continuous fun p : α × List α => insertIdx n p.1 p.2 :=
  continuous_iff_continuousAt.mpr fun ⟨a, l⟩ => by
    rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx'

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p => insertIdx n p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx n (a, l).1 (a, l).2))

Tactic:
exact tendsto_insertIdx'

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ ContinuousAt (fun p => insertIdx n p.1 p.2) (a, l)

Tactic:
rw [ContinuousAt, nhds_prod_eq]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p => insertIdx n p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx n (a, l).1 (a, l).2))
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem min?_eq_some_iff'' {xs : List Nat} :
    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
  min?_eq_some_iff
    (le_refl := Nat.le_refl)
    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
    (le_min_iff := fun _ _ _ => Nat.le_min)

Proof state:
a : Nat
xs : List Nat
x✝¹ x✝ : Nat
⊢ (if x✝¹ ≤ x✝ then x✝¹ else x✝) = x✝¹ ∨ (if x✝¹ ≤ x✝ then x✝¹ else x✝) = x✝

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem decide_exists_mem {xs : Vector α n} {p : α → Prop} [DecidablePred p] :
    decide (∃ x, x ∈ xs ∧ p x) = xs.any p

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, x ∈ xs ∧ p x) = xs.any fun b => decide (p b)

Tactic:
simp [any_eq']

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS'_three : preNormEDS' b c d 3 = c

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS' b c d 3 = c

Tactic:
rw [preNormEDS']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₀₂_τ₃ : S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₀₂, zero_τ₃]

Result:
no goals
-- Mathlib/Data/Nat/Basic.lean
lemma dvd_sub' (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n

Proof state:
case inr
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n

Tactic:
rw [Nat.sub_eq_zero_iff_le.mpr H]

Result:
case inr
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0

Proof state:
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
⊢ k ∣ m - n

Tactic:
rcases le_total n m with H | H

Result:
case inl
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n

case inr
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ m - n

Proof state:
case inl
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : n ≤ m
⊢ k ∣ m - n

Tactic:
exact dvd_sub H h₁ h₂

Result:
no goals

Proof state:
case inr
m n k : ℕ
h₁ : k ∣ m
h₂ : k ∣ n
H : m ≤ n
⊢ k ∣ 0

Tactic:
exact Nat.dvd_zero k

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Real.logDeriv_cosh : logDeriv (Real.cosh) = Real.tanh

Proof state:
⊢ logDeriv cosh = tanh

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ logDeriv cosh x✝ = tanh x✝

Proof state:
case h
x✝ : ℝ
⊢ logDeriv cosh x✝ = tanh x✝

Tactic:
rw [logDeriv, Real.deriv_cosh, Pi.div_apply, Real.tanh_eq_sinh_div_cosh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    (h : m.WF) :
    (Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).getKey? k = if (f (get? m k)).isSome = true then some k else none

Tactic:
simp [getKey?_alter h]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem tails_eq_inits : ∀ l : List α, l.tails = (reverse <| map reverse <| inits <| reverse l)
  | [] => by simp
  | a :: l => by simp [tails_eq_inits l, append_left_inj]

Proof state:
α : Type u_1
⊢ [].tails = (map reverse [].reverse.inits).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).tails = (map reverse (a :: l).reverse.inits).reverse

Tactic:
simp [tails_eq_inits l, append_left_inj]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem tendsto_nhds_true {l : Filter α} {p : α → Prop} :
    Tendsto p l (𝓝 True) ↔ ∀ᶠ x in l, p x

Proof state:
α : Type u_1
l : Filter α
p : α → Prop
⊢ Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem tail_nil : tail (nil : WSeq α) = nil

Proof state:
α : Type u
⊢ nil.tail = nil

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_pow (x y : R) (p : R[X][Y]) (n : ℕ) : (p ^ n).evalEval x y = p.evalEval x y ^ n

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
n : ℕ
⊢ evalEval x y (p ^ n) = evalEval x y p ^ n

Tactic:
simp only [evalEval, eval_pow]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
@[reassoc, to_app]
lemma map₂_rightUnitor_hom {a b : B} (f : a ⟶ b) :
    (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom

Tactic:
rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_comp]

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b : B
f : a ⟶ b
⊢ (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)

Tactic:
simp only [Functor.mapIso_inv, PrelaxFunctor.mapFunctor_map, map₂_rightUnitor]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_zero : v ⬝ᵥ 0 = 0

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
⊢ v ⬝ᵥ 0 = 0

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean
theorem structuralIsoOfExpr_whiskerRight {f g : C} (h : C)
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η)  :
    (whiskerRightIso η' h).hom = η ▷ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (whiskerRightIso η' h).hom = η ▷ h

Tactic:
simp [ih_η]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mono_on (h : ∀ x ∈ Icc a b, f x ≤ g x) :
    (∫ u in a..b, f u ∂μ) ≤ ∫ u in a..b, g u ∂μ

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ x ∈ Icc a b, f x ≤ g x
H : ∀ x ∈ Ioc a b, f x ≤ g x := fun x hx => h x (Ioc_subset_Icc_self hx)
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_on hf.1 hg.1 measurableSet_Ioc H

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ x ∈ Icc a b, f x ≤ g x
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
let H x hx := h x <| Ioc_subset_Icc_self hx

Result:
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : ∀ x ∈ Icc a b, f x ≤ g x
H : ∀ x ∈ Ioc a b, f x ≤ g x := fun x hx => h x (Ioc_subset_Icc_self hx)
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem decay_neg_aux (k n : ℕ) (f : 𝓢(E, F)) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-f : E → F) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖

Tactic:
rw [iteratedFDeriv_neg_apply, norm_neg]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Finset.insert_eq_cons {α : Type*} [DecidableEq α] (a : α) (s : Finset α) (h : a ∉ s) :
    insert a s = Finset.cons a s h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ insert a s = Finset.cons a s h

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s ↔ a✝ ∈ Finset.cons a s h

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s ↔ a✝ ∈ Finset.cons a s h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Bimodule.lean
theorem smul_mem' (p : Submodule (A ⊗[R] B) M) (b : B) {m : M} (hm : m ∈ p) : b • m ∈ p

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
this : b • m = 1 ⊗ₜ[R] b • m
⊢ b • m ∈ p

Tactic:
exact this.symm ▸ p.smul_mem _ hm

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m = 1 ⊗ₜ[R] b • m

Tactic:
simp [TensorProduct.Algebra.smul_def]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m ∈ p

Tactic:
suffices b • m = (1 : A) ⊗ₜ[R] b • m by exact this.symm ▸ p.smul_mem _ hm

Result:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
p : Submodule (A ⊗[R] B) M
b : B
m : M
hm : m ∈ p
⊢ b • m = 1 ⊗ₜ[R] b • m
-- Mathlib/Logic/Basic.lean
theorem Decidable.and_forall_ne [DecidableEq α] (a : α) {p : α → Prop} :
    (p a ∧ ∀ b, b ≠ a → p b) ↔ ∀ b, p b

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

Tactic:
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]

Result:
no goals
-- Mathlib/RingTheory/Etale/Pi.lean
theorem pi_iff [Finite I] :
    FormallyEtale R (Π i, A i) ↔ ∀ i, FormallyEtale R (A i)

Proof state:
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyEtale R ((i : I) → A i) ↔ ∀ (i : I), FormallyEtale R (A i)

Tactic:
simp_rw [FormallyEtale.iff_unramified_and_smooth, forall_and]

Result:
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)

Proof state:
R : Type (max u v)
I : Type u
A : I → Type (max u v)
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)

Tactic:
rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem disjoint_principal_principal {s t : Set α} : Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Set α
⊢ Disjoint (𝓟 s) (𝓟 t) ↔ Disjoint s t

Tactic:
rw [← subset_compl_iff_disjoint_left, disjoint_principal_left, mem_principal]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_top : f =O[⊤] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =O[⊤] g ↔ ∃ C, ∀ (x : α), ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp_rw [isBigO_iff, eventually_top]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.size_eq_zero {t : Ordnode α} (ht : Sized t) : size t = 0 ↔ t = nil

Proof state:
α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil

Tactic:
cases t <;> [simp;simp [ht.1]]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂Aux_eq (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) :
    LinearMap.toMatrix₂Aux R b₁ b₂ B = LinearMap.toMatrix₂ b₁ b₂ B :=
  Matrix.ext fun i j => by rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module R N₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] N₂
i : n
j : m
⊢ (toMatrix₂Aux R ⇑b₁ ⇑b₂) B i j = (toMatrix₂ b₁ b₂) B i j

Tactic:
rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]

Result:
no goals