harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem inner_nonneg_of_dist_le_radius {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : dist p₂ s.center ≤ s.radius) : 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Proof state:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
⊢ 0 ≤ inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
exact h.le

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 ≤ inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

Tactic:
rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)

Result:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : 0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)
⊢ 0 ≤ inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₁ s.center ≤ s.radius
⊢ 0 ≤ inner (p₁ -ᵥ p₁) (p₁ -ᵥ s.center)

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₁ s.center ≤ s.radius
⊢ 0 ≤ inner (p₁ -ᵥ p₁) (p₁ -ᵥ s.center)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem isoExt_inv_m : (isoExt hF hF').inv ≫ F.m = F'.m

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').inv ≫ F.m = F'.m

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_diff_eq_self (h : Y ⊆ M.closure (X \ Y)) : M.closure (X \ Y) = M.closure X

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
⊢ M.closure (X \ Y) = M.closure X

Tactic:
rw [← diff_union_inter X Y, ← closure_union_closure_left_eq,
  union_eq_self_of_subset_right (inter_subset_right.trans h), closure_closure, diff_union_inter]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Cauchy.prod [UniformSpace β] {f : Filter α} {g : Filter β} (hf : Cauchy f) (hg : Cauchy g) :
    Cauchy (f ×ˢ g)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
have := hg.1

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this✝ : f.NeBot
this : g.NeBot
⊢ Cauchy (f ×ˢ g)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
⊢ Cauchy (f ×ˢ g)

Tactic:
have := hf.1

Result:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this : f.NeBot
⊢ Cauchy (f ×ˢ g)

Proof state:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this✝ : f.NeBot
this : g.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
simpa [cauchy_prod_iff, hf.1] using ⟨hf, hg⟩

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp] lemma iSup_eq_zero (hf : BddAbove (range f)) : ⨆ i, f i = 0 ↔ ∀ i, f i = 0

Proof state:
case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_of_singleton (s : Set α) : ⋃ x ∈ s, {x} = s :=
  ext <| by simp

Proof state:
α : Type u_1
s : Set α
⊢ ∀ (x : α), x ∈ ⋃ x ∈ s, {x} ↔ x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma isSemisimple_iff :
    f.IsSemisimple ↔ ∀ p ∈ invtSubmodule f, ∃ q ∈ invtSubmodule f, IsCompl p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ f.IsSemisimple ↔ ∀ p ∈ f.invtSubmodule, ∃ q ∈ f.invtSubmodule, IsCompl p q

Tactic:
simp [isSemisimple_iff']

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem not_covBy_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b

Proof state:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b

Tactic:
simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0

Proof state:
m n : ℕ
⊢ min m n = 0 ↔ m = 0 ∨ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Faces.lean
theorem of_succ {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish (q + 1) φ) :
    HigherFacesVanish q φ := fun j hj => v j (by simpa only [← add_assoc] using le_add_right hj)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish (q + 1) φ
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ n + 1 ≤ ↑j + (q + 1)

Tactic:
simpa only [← add_assoc] using le_add_right hj

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfc_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ IsStarNormal
inst✝ : T2Space A
a : A
f : ℝ → ℝ
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ cfc f a = cfc (fun x => ↑(f x.re)) a

Tactic:
replace ha : IsSelfAdjoint a := ha

Result:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ IsStarNormal
inst✝ : T2Space A
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfc f a = cfc (fun x => ↑(f x.re)) a

Proof state:
A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : ContinuousFunctionalCalculus ℂ IsStarNormal
inst✝ : T2Space A
a : A
f : ℝ → ℝ
ha : IsSelfAdjoint a
⊢ cfc f a = cfc (fun x => ↑(f x.re)) a

Tactic:
exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM)
  Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
@[simp] lemma posFittingComp_eq_bot_of_isNilpotent
    [IsNilpotent L M] :
    posFittingComp R L M = ⊥

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✝ : IsNilpotent L M
⊢ posFittingComp R L M = ⊥

Tactic:
simp [posFittingComp]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem finSepDegree_mul_finInsepDegree : finSepDegree F E * finInsepDegree F E = finrank F E

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
this : Cardinal.toNat (sepDegree F E * insepDegree F E) = Cardinal.toNat (Module.rank F E)
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this

Result:
no goals

Proof state:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
rw [finInsepDegree, finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
    halg (Algebra.IsAlgebraic.of_finite F E),
  finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
    halg (.trans _ (separableClosure F E) _),
  mul_zero]

Result:
no goals

Proof state:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
have := congr_arg Cardinal.toNat (sepDegree_mul_insepDegree F E)

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
this : Cardinal.toNat (sepDegree F E * insepDegree F E) = Cardinal.toNat (Module.rank F E)
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
by_cases halg : Algebra.IsAlgebraic F E

Result:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊

Proof state:
l : Type u_2
m : Type u_3
α : Type u_5
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊

Tactic:
rw [← linfty_opNNNorm_col (ι := Fin 1) (A *ᵥ v), ← linfty_opNNNorm_col v (ι := Fin 1)]

Result:
l : Type u_2
m : Type u_3
α : Type u_5
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖col (Fin 1) (A *ᵥ v)‖₊ ≤ ‖A‖₊ * ‖col (Fin 1) v‖₊

Proof state:
l : Type u_2
m : Type u_3
α : Type u_5
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
v : m → α
⊢ ‖col (Fin 1) (A *ᵥ v)‖₊ ≤ ‖A‖₊ * ‖col (Fin 1) v‖₊

Tactic:
exact linfty_opNNNorm_mul A (col (Fin 1) v)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_add_const (c : F) : fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ fderiv 𝕜 (fun y => f y + c) x = fderiv 𝕜 f x

Tactic:
simp only [← fderivWithin_univ, fderivWithin_add_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_beq : ∀b, (false == b) = !b

Proof state:
⊢ ∀ (b : Bool), (false == b) = !b

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_erase (p : R[X]) (n : ℕ) : toFinsupp (p.erase n) = p.toFinsupp.erase n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = Finsupp.erase n p.toFinsupp

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).toFinsupp = Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).toFinsupp = Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
simp only [erase_def]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem sq_eq_one {m n : ℕ} (hm : Odd m) (hn : Odd n) : qrSign m n ^ 2 = 1

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n ^ 2 = 1

Tactic:
rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

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

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

Tactic:
ext

Result:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (-1#w &&& a).getLsbD i✝ = a.getLsbD i✝

Proof state:
case pred
w : Nat
a : BitVec w
i✝ : Nat
a✝ : i✝ < w
⊢ (-1#w &&& a).getLsbD i✝ = a.getLsbD i✝

Tactic:
simp [BitVec.negOne_eq_allOnes]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
/-- **Goursat's lemma** for module isomorphisms.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some module isomorphism `f : H ≃ I`. -/
lemma Submodule.exists_equiv_eq_graph {G : Submodule S (H × I)}
    (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
    ∃ e : H ≃ₗ[S] I, G = e.toLinearMap.graph

Proof state:
S : Type u_4
H : Type u_6
I : Type u_7
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
G : Submodule S (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = (↑e).graph

Tactic:
simpa only [range_subtype] using LinearMap.exists_linearEquiv_eq_graph
  hG₁.surjective hG₂.surjective fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `succ` commutes with `predAbove`. -/
@[simp] lemma succ_predAbove_succ (a : Fin n) (b : Fin (n + 1)) :
    a.succ.predAbove b.succ = (a.predAbove b).succ

Proof state:
case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]

Result:
no goals

Proof state:
n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
obtain h | h := Fin.le_or_lt (succ a) b

Result:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Proof state:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem choose_le_centralBinom (r n : ℕ) : choose (2 * n) r ≤ centralBinom n :=
  calc
    (2 * n).choose r ≤ (2 * n).choose (2 * n / 2) := choose_le_middle r (2 * n)
    _ = (2 * n).choose n

Proof state:
r n : ℕ
⊢ (2 * n).choose (2 * n / 2) = (2 * n).choose n

Tactic:
rw [Nat.mul_div_cancel_left n zero_lt_two]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem prod_bind [CommMonoid β] (s : Multiset α) (t : α → Multiset β) :
    (s.bind t).prod = (s.map fun a => (t a).prod).prod

Proof state:
α : Type u_1
β : Type v
inst✝ : CommMonoid β
s : Multiset α
t : α → Multiset β
⊢ (s.bind t).prod = (map (fun a => (t a).prod) s).prod

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_left_square (f : X' ⟶ X) (g : F.obj X ⟶ Y')
    (h : F.obj X' ⟶ Y) (k : Y ⟶ Y') (w : F.map f ≫ g = h ≫ k) :
    f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : F.map f ≫ g = h ≫ k
⊢ f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k

Tactic:
rw [← homEquiv_naturality_left, ← homEquiv_naturality_right, w]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem map_cyclotomic_int (n : ℕ) (R : Type*) [Ring R] :
    map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Proof state:
case pos
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Tactic:
simp only [hzero, cyclotomic, dif_pos, Polynomial.map_one]

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Tactic:
by_cases hzero : n = 0

Result:
case pos
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

case neg
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : ¬n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Proof state:
case neg
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : ¬n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Tactic:
simp [cyclotomic, hzero]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsRefl.nondegenerate_iff_separatingRight {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) :
    B.Nondegenerate ↔ B.SeparatingRight

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingLeft

Tactic:
rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ ker B.flip = ⊥

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ ker B.flip = ⊥

Tactic:
rwa [← separatingRight_iff_flip_ker_eq_bot]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingRight

Tactic:
refine ⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingLeft
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem dz_val : ↑(d a1) = az a * az a - 1 :=
  have : 1 ≤ a * a := asq_pos a1
  by rw [Pell.d, Int.ofNat_sub this]; rfl

Proof state:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(Pell.d a1) = az a * az a - 1

Tactic:
rw [Pell.d, Int.ofNat_sub this]

Result:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(a * a) - ↑1 = az a * az a - 1

Proof state:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(a * a) - ↑1 = az a * az a - 1

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_some (X Y : R) : W'.Equation ![X, Y, 1] ↔ W'.toAffine.Equation X Y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
X Y : R
⊢ W'.Equation ![X, Y, 1] ↔ (toAffine W').Equation X Y

Tactic:
simp only [equation_iff, Affine.equation_iff', fin3_def_ext, one_pow, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem pentagon (W X Y Z : Dial C) :
    (tensorHom (associator W X Y).hom (𝟙 Z)) ≫ (associator W (tensorObj X Y) Z).hom ≫
      (tensorHom (𝟙 W) (associator X Y Z).hom) =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W X Y Z : Dial C
⊢ tensorHom (W.associator X Y).hom (𝟙 Z) ≫
      (W.associator (X.tensorObj Y) Z).hom ≫ tensorHom (𝟙 W) (X.associator Y Z).hom =
    ((W.tensorObj X).associator Y Z).hom ≫ (W.associator X (Y.tensorObj Z)).hom

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_add_intCast' (hx : 0 ≤ x) {n : ℤ} (h : y + n ≠ 0) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y + ↑n ≠ 0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
rw [rpow_add' hx h, rpow_intCast]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_inj [LinearOrderedSemiring α] {m n : Num} : (m : α) = n ↔ m = n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : Num
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem totalDegree_eq_zero_iff (p : MvPolynomial σ R) :
    p.totalDegree = 0 ↔ ∀ (m : σ →₀ ℕ) (_ : m ∈ p.support) (x : σ), m x = 0

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight 1

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight 1

Tactic:
exact nonTorsionWeight_of (Function.const σ one_ne_zero)

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma _root_.CovBy.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⋖ t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
simpa using h.exists_finset_cons

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_image_eq_span_vsub_set_right_ne (p : ι → P) {s : Set ι} {i : ι} (hi : i ∈ s) :
    vectorSpan k (p '' s) = Submodule.span k ((· -ᵥ p i) '' (p '' (s \ {i})))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert (p i -ᵥ p i) ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))

Tactic:
simp [Submodule.span_insert_eq_span]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))

Tactic:
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi), ← Set.insert_eq_of_mem hi,
    ← Set.insert_diff_singleton, Set.image_insert_eq, Set.image_insert_eq]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
⊢ Submodule.span k (insert (p i -ᵥ p i) ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))) =
    Submodule.span k ((fun x => x -ᵥ p i) '' (p '' (s \ {i})))
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_sUnion {S : Set (Set E)} (hS : S.Finite) :
    IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : Zero E
inst✝ : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Tactic:
rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_translate (x : ℝ) : τ (translate <| Multiplicative.ofAdd x) = x :=
  translationNumber_eq_of_tendsto₀' _ <| by
    simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
      mul_div_cancel_left₀ (M₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]

Proof state:
x : ℝ
⊢ Tendsto (fun n => (⇑↑(translate (Multiplicative.ofAdd x)))^[n + 1] 0 / (↑n + 1)) atTop (𝓝 x)

Tactic:
simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
  mul_div_cancel_left₀ (M₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]

Result:
no goals