harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
    m.isEmpty = true ↔ ∀ a, ¬a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
⊢ m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

Tactic:
simpa [mem_iff_contains] using isEmpty_iff_forall_contains

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_linePolynomial : linePolynomial (f x) (f y) (f ℓ) = (linePolynomial x y ℓ).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y ℓ : R
⊢ C (f ℓ) * (X - C (f x)) + C (f y) = Polynomial.map f (C ℓ * (X - C x) + C y)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y ℓ : R
⊢ linePolynomial (f x) (f y) (f ℓ) = Polynomial.map f (linePolynomial x y ℓ)

Tactic:
simp only [linePolynomial]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y ℓ : R
⊢ C (f ℓ) * (X - C (f x)) + C (f y) = Polynomial.map f (C ℓ * (X - C x) + C y)
-- Mathlib/Order/Filter/Basic.lean
theorem not_frequently {p : α → Prop} {f : Filter α} : (¬∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, ¬p x

Proof state:
α : Type u
p : α → Prop
f : Filter α
⊢ (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x

Tactic:
simp only [Filter.Frequently, not_not]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem edist_nndist (x y : α) : edist x y = nndist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ edist x y = ↑(nndist x y)

Tactic:
rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean
theorem treeHom_eq {a : G} (p : Path (root T) a) : treeHom T a = homOfPath T p

Proof state:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ treeHom T a = homOfPath T p

Tactic:
rw [treeHom, Unique.default_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem false_eq_decide_iff {p : Prop} [h : Decidable p] : false = decide p ↔ ¬p

Proof state:
case isTrue
p : Prop
q : p
⊢ false = decide p ↔ ¬p

Tactic:
simp [q]

Result:
no goals

Proof state:
p : Prop
h : Decidable p
⊢ false = decide p ↔ ¬p

Tactic:
cases h with | _ q => simp [q]

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
⊢ -x ≡ -y [SMOD U]

Tactic:
simpa only [SModEq.def, Quotient.mk_neg, neg_inj]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_iff_forall_eventually_exists_and {p : α → Prop} {f : Filter α} :
    (∃ᶠ x in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ x in f, q x) → ∃ x, p x ∧ q x :=
  ⟨fun hp _ hq => (hp.and_eventually hq).exists, fun H hp => by
    simpa only [and_not_self_iff, exists_false] using H hp⟩

Proof state:
α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x => p x) x
⊢ False

Tactic:
simpa only [and_not_self_iff, exists_false] using H hp

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem iUnion_Ioc_coe_nat : ⋃ n : ℕ, Ioc a n = Ioi a \ {∞}

Proof state:
a : ℝ≥0∞
⊢ ⋃ n, Ioc a ↑n = Ioi a \ {⊤}

Tactic:
simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioc_pred_pred_eq_Ico (a b : α) : Ioc (pred a) (pred b) = Ico a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioc (pred a) (pred b)) = ↑(Ico a b)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem mem_sInf : x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Proof state:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem card_empty : Language.empty.card = 0

Proof state:
⊢ Language.empty.card = 0

Tactic:
simp only [card, mk_sum, mk_sigma, mk_eq_zero,
sum_const, mk_eq_aleph0, lift_id', mul_zero, add_zero]

Result:
no goals
-- Mathlib/RingTheory/Flat/Equalizer.lean
@[simp]
private lemma LinearMap.lTensor_eqLocus_subtype_tensorEqLocusInv [Module.Flat R M]
    (x : eqLocus (AlgebraTensorModule.lTensor S M f) (AlgebraTensorModule.lTensor S M g)) :
    (lTensor M (eqLocus f g).subtype) (tensorEqLocusInv S M f g x) = x

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(eqLocus ((AlgebraTensorModule.lTensor S M) f) ((AlgebraTensorModule.lTensor S M) g))
⊢ (lTensor M (eqLocus f g).subtype) ((LinearMap.tensorEqLocusInv S M f g) x) = ↑x

Tactic:
rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(eqLocus ((AlgebraTensorModule.lTensor S M) f) ((AlgebraTensorModule.lTensor S M) g))
⊢ ((AlgebraTensorModule.lTensor S M) (eqLocus f g).subtype) ((LinearMap.tensorEqLocusInv S M f g) x) = ↑x

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥(eqLocus ((AlgebraTensorModule.lTensor S M) f) ((AlgebraTensorModule.lTensor S M) g))
⊢ ((AlgebraTensorModule.lTensor S M) (eqLocus f g).subtype) ((LinearMap.tensorEqLocusInv S M f g) x) = ↑x

Tactic:
simp [LinearMap.tensorEqLocusInv]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma one_le_coverMincard_iff (T : X → X) (F : Set X) (U : Set (X × X)) (n : ℕ) :
    1 ≤ coverMincard T F U n ↔ F.Nonempty

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ 1 ≤ coverMincard T F U n ↔ F.Nonempty

Tactic:
rw [ENat.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]

Result:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅

Proof state:
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
n : ℕ
⊢ coverMincard T F U n = 0 ↔ F = ∅

Tactic:
exact coverMincard_eq_zero_iff T F U n

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem end_hom_mk_of_mk {s} (sec : s ∈ G.end) {K L : (Finset V)ᵒᵖ} (h : L ⟶ K) {v : V}
    (vnL : v ∉ L.unop) (hs : s L = G.componentComplMk vnL) :
    s K = G.componentComplMk (Set.not_mem_subset (le_of_op_hom h : _ ⊆ _) vnL)

Proof state:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ G.componentComplFunctor.map h (G.componentComplMk vnL) = G.componentComplMk ⋯

Tactic:
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ s K = G.componentComplMk ⋯

Tactic:
rw [← sec h, hs]

Result:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk vnL
⊢ G.componentComplFunctor.map h (G.componentComplMk vnL) = G.componentComplMk ⋯
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma congr_var {solution' : relations.Solution M} (h : solution = solution') (g : relations.G) :
    solution.var g = solution'.var g

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution solution' : relations.Solution M
h : solution = solution'
g : relations.G
⊢ solution.var g = solution'.var g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_right_left {w x y z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) :
    Wbtw R w x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w

Tactic:
exact h₁.trans_left_right h₂

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w x y

Tactic:
rw [wbtw_comm] at *

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R y x w
-- Mathlib/Analysis/Seminorm.lean
theorem mem_closedBall_zero : y ∈ closedBall p 0 r ↔ p y ≤ r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
⊢ y ∈ p.closedBall 0 r ↔ p y ≤ r

Tactic:
rw [mem_closedBall, sub_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem monotone (hf : IsFundamentalSequence a o f) {i j : Ordinal} (hi : i < o)
    (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj

Proof state:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj

Tactic:
rcases lt_or_eq_of_le hij with (hij | rfl)

Result:
case inl
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

case inr
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj

Proof state:
case inl
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

Tactic:
exact (hf.2.1 hi hj hij).le

Result:
no goals

Proof state:
case inr
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_reflection (s : AffineSubspace ℝ P) [Nonempty s] [HasOrthogonalProjection s.direction]
    (p₁ p₂ : P) : dist p₁ (reflection s p₂) = dist (reflection s p₁) p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
⊢ dist ((reflection s) ((reflection s) p₁)) ((reflection s) p₂) = dist ((reflection s) p₁) p₂

Tactic:
exact (reflection s).dist_map _ _

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 : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist ((reflection s) p₁) p₂

Tactic:
conv_lhs => rw [← reflection_reflection s p₁]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ : P
⊢ dist ((reflection s) ((reflection s) p₁)) ((reflection s) p₂) = dist ((reflection s) p₁) p₂
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_mul_inv_iff_mul_eq {a b : α} : a = b * ↑c⁻¹ ↔ a * c = b :=
  ⟨fun h => by rw [h, inv_mul_cancel_right], fun h => by rw [← h, mul_inv_cancel_right]⟩

Proof state:
α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a * ↑c = b
⊢ a = b * ↑c⁻¹

Tactic:
rw [← h, mul_inv_cancel_right]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
c : αˣ
a b : α
h : a = b * ↑c⁻¹
⊢ a * ↑c = b

Tactic:
rw [h, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem mul_one_add_self : a * (1 + a) = 0

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a * (1 + a) = 0

Tactic:
rw [mul_add, mul_one, mul_self, add_self]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f

Tactic:
rw [f.comm, ← assoc, P.idem]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- In a C⋆-algebra, the spectral radius of a self-adjoint element is equal to its norm.
See `IsSelfAdjoint.toReal_spectralRadius_eq_norm` for a version involving
`spectralRadius ℝ a`. -/
lemma IsSelfAdjoint.toReal_spectralRadius_complex_eq_norm {a : A} (ha : IsSelfAdjoint a) :
    (spectralRadius ℂ a).toReal = ‖a‖

Proof state:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ (spectralRadius ℂ a).toReal = ‖a‖

Tactic:
simp [ha.spectralRadius_eq_nnnorm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/WithZero.lean
lemma map'_map'  (f : α →* β) (g : β →* γ) (x) : map' g (map' f x) = map' (g.comp f) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
⊢ (map' g) ((map' f) x) = (map' (g.comp f)) x

Tactic:
induction x <;> rfl

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem id : RightOrdContinuous (id : α → α) := fun s x h => by
  simpa only [image_id] using h

Proof state:
α : Type u
inst✝ : Preorder α
s : Set α
x : α
h : IsGLB s x
⊢ IsGLB (id '' s) (id x)

Tactic:
simpa only [image_id] using h

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
    ⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h =
      ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩

Proof state:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ ⋂ x, ⋂ y, ⋂ (h : p x ∧ q x y), s x y h = ⋂ x, ⋂ (hx : p x), ⋂ y, ⋂ (hy : q x y), s x y ⋯

Tactic:
simp only [iInter_and, @iInter_comm _ ι']

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zpow_eq_one_iff_dvd (h : IsPrimitiveRoot ζ k) (l : ℤ) : ζ ^ l = 1 ↔ (k : ℤ) ∣ l

Proof state:
case pos.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l

Tactic:
exact_mod_cast h.pow_eq_one_iff_dvd l

Result:
no goals

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
by_cases h0 : 0 ≤ l

Result:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Proof state:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'

Tactic:
norm_cast

Result:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'

Proof state:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
rw [← dvd_neg, ← hl']

Result:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ ↑l'

Proof state:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le

Result:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Proof state:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
lift -l to ℕ using this with l' hl'

Result:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Proof state:
case neg.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
l' : ℕ
hl' : ↑l' = -l
⊢ ζ ^ l = 1 ↔ k ∣ l'

Tactic:
rw [← h.pow_eq_one_iff_dvd, ← inv_inj, ← zpow_neg, ← hl', zpow_natCast, inv_one]

Result:
no goals

Proof state:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
lift l to ℕ using h0

Result:
case pos.intro
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ ζ ^ ↑l = 1 ↔ ↑k ∣ ↑l
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem integral_average_sub [IsFiniteMeasure μ] (hf : Integrable f μ) :
    ∫ x, ⨍ a, f a ∂μ - f x ∂μ = 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
μ : Measure α
f : α → E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
hf : Integrable f μ
⊢ ∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ = 0

Tactic:
rw [integral_sub (integrable_const _) hf, integral_average, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem find?_congr [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = .eq) :
    t.find? k₁ = t.find? k₂

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k₁ k₂ : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k₁ k₂ = Ordering.eq
⊢ t.find? k₁ = t.find? k₂

Tactic:
simp [find?, findEntry?_congr _ h]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp_fix (f k) :
    codeSupp (Code.fix f) k = trStmts₁ (trNormal (Code.fix f) k) ∪ codeSupp f (Cont'.fix f k)

Proof state:
f : Code
k : Cont'
⊢ codeSupp f.fix k = trStmts₁ (trNormal f.fix k) ∪ codeSupp f (Cont'.fix f k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc, Finset.union_left_comm,
  Finset.union_left_idem]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem IsConformalMap.smul (hf : IsConformalMap f) {c : R} (hc : c ≠ 0) :
    IsConformalMap (c • f)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
inst✝¹ : NormedSpace R M
inst✝ : NormedSpace R N
f : M →L[R] N
hf : IsConformalMap f
c : R
hc : c ≠ 0
⊢ IsConformalMap (c • f)

Tactic:
rcases hf with ⟨c', hc', li, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
inst✝¹ : NormedSpace R M
inst✝ : NormedSpace R N
c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • li.toContinuousLinearMap)

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
inst✝¹ : NormedSpace R M
inst✝ : NormedSpace R N
c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • li.toContinuousLinearMap)

Tactic:
exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mk_eq_bot_iff {N : Submodule R M} {h} :
    (⟨N, h⟩ : LieSubmodule R L M) = ⊥ ↔ N = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
⊢ { toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥

Tactic:
rw [← toSubmodule_inj, bot_toSubmodule]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem join [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) :
    IsLprojection X (P + Q - P * Q)

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ IsLprojection X (P + Q - P * Q)

Tactic:
convert (Lcomplement_iff _).mp (h₁.Lcomplement.mul h₂.Lcomplement) using 1

Result:
case h.e'_6
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)

Proof state:
case h.e'_6
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
⊢ P + Q - P * Q = 1 - (1 - P) * (1 - Q)

Tactic:
noncomm_ring

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_one : quadraticCharFun F 1 = 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
⊢ quadraticCharFun F 1 = 1

Tactic:
simp only [quadraticCharFun, one_ne_zero, IsSquare.one, if_true, if_false]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₗ[R] N) (k : κ) (n : N) :
    (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n)

Proof state:
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ (lcongr e₁ e₂) ((lcongr e₁ e₂).symm (single k n)) = (lcongr e₁ e₂) (single (e₁.symm k) (e₂.symm n))

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ (lcongr e₁ e₂).symm (single k n) = single (e₁.symm k) (e₂.symm n)

Tactic:
apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective

Result:
M : Type u_2
N : Type u_3
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
κ : Type u_8
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
k : κ
n : N
⊢ (lcongr e₁ e₂) ((lcongr e₁ e₂).symm (single k n)) = (lcongr e₁ e₂) (single (e₁.symm k) (e₂.symm n))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector_of_neg (h : ¬ p a) : find? p (mkVector n a) = none

Proof state:
α✝ : Type
p : α✝ → Bool
n : Nat
a : α✝
h : ¬p a = true
⊢ find? p (mkVector n a) = none

Tactic:
simp [find?_mkVector, h]

Result:
no goals