harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Tower.lean
@[simp]
lemma eval_map_algebraMap (P : R[X]) (b : B) :
    (map (algebraMap R B) P).eval b = aeval b P

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring B
inst✝ : Algebra R B
P : R[X]
b : B
⊢ eval b (map (algebraMap R B) P) = (aeval b) P

Tactic:
rw [aeval_def, eval_map]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem inv_mem_center (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ g✝ * a⁻¹ = a⁻¹ * g✝

Tactic:
rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ ∀ (g : M), g * a⁻¹ = a⁻¹ * g

Tactic:
intro _

Result:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ g✝ * a⁻¹ = a⁻¹ * g✝

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ a⁻¹ ∈ center M

Tactic:
rw [_root_.Semigroup.mem_center_iff]

Result:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
⊢ ∀ (g : M), g * a⁻¹ = a⁻¹ * g
-- Mathlib/Topology/QuasiSeparated.lean
theorem isQuasiSeparated_iff_quasiSeparatedSpace (s : Set α) (hs : IsOpen s) :
    IsQuasiSeparated s ↔ QuasiSeparatedSpace s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated univ

Tactic:
convert (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm

Result:
case h.e'_1.h.e'_3
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ s = Subtype.val '' univ

Proof state:
case h.e'_1.h.e'_3
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ s = Subtype.val '' univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s

Tactic:
rw [← isQuasiSeparated_univ_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated univ
-- Mathlib/Order/Disjoint.lean
theorem Disjoint.ne (ha : a ≠ ⊥) (hab : Disjoint a b) : a ≠ b :=
  fun h ↦ ha <| disjoint_self.1 <| by rwa [← h] at hab

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a

Tactic:
rwa [← h] at hab

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem range_inl_sup_range_inr :
    MonoidHom.range (inl : G →* G ∗ H) ⊔ MonoidHom.range inr = ⊤

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = ⊤

Tactic:
rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
  ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_ball (hr : 0 ≤ r) (x : E) : gauge (ball (0 : E) r) x = ‖x‖ / r

Proof state:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (ball 0 0) x = ‖x‖ / 0

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
rcases hr.eq_or_lt with rfl | hr

Result:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (ball 0 0) x = ‖x‖ / 0

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r

Proof state:
case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1

Tactic:
exact fun _ => id

Result:
no goals

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ gauge (ball 0 r) x = ‖x‖ / r

Tactic:
rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul,
abs_of_nonneg hr.le, div_eq_inv_mul]

Result:
case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ x ∈ ball 0 1, -x ∈ ball 0 1

Proof state:
case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ x ∈ ball 0 1, -x ∈ ball 0 1

Tactic:
simp_rw [mem_ball_zero_iff, norm_neg]

Result:
case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_isNone {xs : Array α} {p : α → Bool} :
    (xs.findIdx? p).isNone = xs.all (¬p ·)

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ (findIdx? p { toList := xs }).isNone = { toList := xs }.all fun x => decide ¬p x = true

Tactic:
simp [List.findIdx?_isNone]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ (findIdx? p xs).isNone = xs.all fun x => decide ¬p x = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ (findIdx? p { toList := xs }).isNone = { toList := xs }.all fun x => decide ¬p x = true
-- Mathlib/Data/Finset/Basic.lean
theorem erase_inter (a : α) (s t : Finset α) : s.erase a ∩ t = (s ∩ t).erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s.erase a ∩ t = (s ∩ t).erase a

Tactic:
simpa only [inter_comm t] using inter_erase a t s

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
theorem disjoint_map_inl_map_inr : Disjoint (s.map Embedding.inl) (t.map Embedding.inr)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
simp_rw [disjoint_left, mem_map]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1 ∈ s, Embedding.inl a_1 = a) → ¬∃ a_2 ∈ t, Embedding.inr a_2 = a

Tactic:
rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem comul_comp_inr :
    comul ∘ₗ inr R A B = TensorProduct.map (.inr R A B) (.inr R A B) ∘ₗ comul

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ inr R A B = TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (comul ∘ₗ inr R A B) x✝ = (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) x✝

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (comul ∘ₗ inr R A B) x✝ = (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whisker_exchange {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) :
    W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ W ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g

Tactic:
simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem inv_appTop {X Y : Scheme} (f : X ⟶ Y) [IsIso f] :
    (inv f).appTop = inv (f.appTop)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.appTop (inv f) = inv (Hom.appTop f)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive add_abs_eq_two_nsmul_posPart]
lemma mul_mabs_eq_oneLePart_sq (a : α) : a * |a|ₘ = a⁺ᵐ ^ 2

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a * mabs a = a⁺ᵐ ^ 2

Tactic:
rw [mul_comm, mabs_mul_eq_oneLePart_sq]

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
lemma isLocallyInjective_iff_nhds {f : X → Y} :
    IsLocallyInjective f ↔ ∀ x : X, ∃ U ∈ 𝓝 x, U.InjOn f

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
exact ⟨interior U, isOpen_interior, mem_interior_iff_mem_nhds.mpr hn, hi.mono interior_subset⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
exact ⟨U, ho.mem_nhds hm, hi⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
constructor <;> intro h x

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Tactic:
obtain ⟨U, ho, hm, hi⟩ := h x

Result:
case mp.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : IsLocallyInjective f
x : X
U : Set X
ho : IsOpen U
hm : x ∈ U
hi : Set.InjOn f U
⊢ ∃ U ∈ 𝓝 x, Set.InjOn f U

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U

Tactic:
obtain ⟨U, hn, hi⟩ := h x

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn f U
x : X
U : Set X
hn : U ∈ 𝓝 x
hi : Set.InjOn f U
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U
-- Mathlib/Topology/QuasiSeparated.lean
theorem Topology.IsOpenEmbedding.isQuasiSeparated_iff (h : IsOpenEmbedding f) {s : Set α} :
    IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s

Tactic:
intro H U V hU hU' hU'' hV hV' hV''

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)

Tactic:
refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
⊢ IsQuasiSeparated (f '' s) → IsQuasiSeparated s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
rw [h.isEmbedding.isCompact_iff, Set.image_inter h.injective]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
h : IsOpenEmbedding f
s : Set α
H : IsQuasiSeparated (f '' s)
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' U ∩ f '' V)

Tactic:
exact
  H (f '' U) (f '' V) (Set.image_subset _ hU) (h.isOpenMap _ hU') (hU''.image h.continuous)
    (Set.image_subset _ hV) (h.isOpenMap _ hV') (hV''.image h.continuous)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
lemma FiniteField.primitiveChar_to_Complex_isPrimitive :
    (primitiveChar_to_Complex F).IsPrimitive

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
nn : ℕ+ := (primitiveChar F ℂ ⋯).n
⊢ Function.Injective
    ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)

Tactic:
exact (IsCyclotomicExtension.algEquiv nn ℂ (CyclotomicField nn ℂ) ℂ).injective

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ Function.Injective
    ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)

Tactic:
let nn := (primitiveChar F ℂ <| ringChar_ne F).n

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
nn : ℕ+ := (primitiveChar F ℂ ⋯).n
⊢ Function.Injective
    ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ (primitiveChar_to_Complex F).IsPrimitive

Tactic:
refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ Function.Injective
    ⇑↑(IsCyclotomicExtension.algEquiv (primitiveChar F ℂ ⋯).n ℂ (CyclotomicField (primitiveChar F ℂ ⋯).n ℂ) ℂ)
-- Mathlib/Data/Set/NAry.lean
lemma image_prod : (fun x : α × β ↦ f x.1 x.2) '' s ×ˢ t = image2 f s t :=
  ext fun _ ↦ by simp [and_assoc]

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ (fun x => f x.1 x.2) '' s ×ˢ t ↔ x✝ ∈ image2 f s t

Tactic:
simp [and_assoc]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem eq_one_or_neg_one_iff_y_eq_zero {a : Solution₁ d} : a = 1 ∨ a = -1 ↔ a.y = 0

Proof state:
d : ℤ
a : Solution₁ d
H : a.y = 0
⊢ a = 1 ∨ a = -1

Tactic:
have prop := a.prop

Result:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a = 1 ∨ a = -1

Proof state:
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = -1
⊢ a.y = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1

Tactic:
exact prop.imp (fun h => ext h H) fun h => ext h H

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
⊢ a = 1 ∨ a = -1 ↔ a.y = 0

Tactic:
refine ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => ?_⟩

Result:
d : ℤ
a : Solution₁ d
H : a.y = 0
⊢ a = 1 ∨ a = -1

Proof state:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a = 1 ∨ a = -1

Tactic:
rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop

Result:
d : ℤ
a : Solution₁ d
H : a.y = 0
prop : a.x = 1 ∨ a.x = -1
⊢ a = 1 ∨ a = -1

Proof state:
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = 1
⊢ a.y = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/Support.lean
theorem mulSupport_comp_inv_smul [One γ] (c : α) (f : β → γ) :
    (mulSupport fun x ↦ f (c⁻¹ • x)) = c • mulSupport f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem nonempty_inter_of_measure_lt_add {m : MeasurableSpace α} (μ : Measure α) {s t u : Set α}
    (ht : MeasurableSet t) (h's : s ⊆ u) (h't : t ⊆ u) (h : μ u < μ s + μ t) :
    (s ∩ t).Nonempty

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ ¬Disjoint s t

Tactic:
contrapose! h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ μ s + μ t ≤ μ u

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ μ s + μ t ≤ μ u

Tactic:
calc
  μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
  _ ≤ μ u := measure_mono (union_subset h's h't)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ (s ∩ t).Nonempty

Tactic:
rw [← Set.not_disjoint_iff_nonempty_inter]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ u < μ s + μ t
⊢ ¬Disjoint s t
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of a Dirichlet character mod `N > 0` converges absolutely at `s` if and only if
`re s > 1`. -/
lemma LSeriesSummable_iff {N : ℕ} (hN : N ≠ 0) (χ : DirichletCharacter ℂ N) {s : ℂ} :
    LSeriesSummable ↗χ s ↔ 1 < s.re

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
⊢ LSeriesSummable (fun n => χ ↑n) s ↔ 1 < s.re

Tactic:
refine ⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩

Result:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n => χ ↑n) s
⊢ 1 < s.re

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n => χ ↑n) s
⊢ 1 < s.re

Tactic:
by_contra! h

Result:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n => χ ↑n) s
h : s.re ≤ 1
⊢ False

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n => χ ↑n) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simp [h]

Result:
no goals

Proof state:
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n => χ ↑n) s
h : s.re ≤ 1
⊢ False

Tactic:
exact not_LSeriesSummable_at_one hN χ <| LSeriesSummable.of_re_le_re (by simp [h]) H

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldl_eq (f : α → Char → α) (s a) : foldl f a s = s.1.foldl f a

Proof state:
α : Type u_1
f : α → Char → α
s : String
a : α
⊢ foldl f a s = List.foldl f a s.data

Tactic:
simpa using foldlAux_of_valid f [] s.1 [] a

Result:
no goals
-- Mathlib/Analysis/Complex/Circle.lean
theorem exp_add (x y : ℝ) : exp (x + y) = exp x * exp y :=
  Subtype.ext <| by
    simp only [coe_exp, Submonoid.coe_mul, ofReal_add, add_mul, Complex.exp_add, coe_mul]

Proof state:
x y : ℝ
⊢ ↑(exp (x + y)) = ↑(exp x * exp y)

Tactic:
simp only [coe_exp, Submonoid.coe_mul, ofReal_add, add_mul, Complex.exp_add, coe_mul]

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem eq_of_le_of_inf_le_of_le_sup (hxy : x ≤ y) (hinf : y ⊓ z ≤ x) (hsup : y ≤ x ⊔ z) :
    x = y

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ y ≤ x

Tactic:
rw [← inf_eq_right, sup_inf_assoc_of_le _ hxy] at hsup

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ y ≤ x

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ y ≤ x

Tactic:
rwa [← hsup, sup_le_iff, and_iff_right rfl.le, inf_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ x = y

Tactic:
refine hxy.antisymm ?_

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : y ≤ x ⊔ z
⊢ y ≤ x
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem exists_pow_or_neg_mul_pow_of_isOfFinOrder [IsCyclotomicExtension {n} ℚ K]
    (hno : Odd (n : ℕ)) {ζ x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) :
    ∃ r : ℕ, r < n ∧ (x = ζ ^ r ∨ x = -ζ ^ r) :=  by
  obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx
  refine ⟨r % n, Nat.mod_lt _ n.2, ?_⟩
  rw [show ζ ^ (r % ↑n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]
  rcases Nat.even_or_odd r with (h | h) <;> simp [neg_pow, h.neg_one_pow]

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
⊢ ∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx

Result:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r

Proof state:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ x = ζ ^ (r % ↑n) ∨ x = -ζ ^ (r % ↑n)

Tactic:
rw [show ζ ^ (r % ↑n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]

Result:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r

Proof state:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ ∃ r < ↑n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
refine ⟨r % n, Nat.mod_lt _ n.2, ?_⟩

Result:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ x = ζ ^ (r % ↑n) ∨ x = -ζ ^ (r % ↑n)

Proof state:
case intro
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd ↑n
ζ x : K
hζ : IsPrimitiveRoot ζ ↑n
hx : IsOfFinOrder x
r : ℕ
hr : x = (-ζ) ^ r
⊢ (-ζ) ^ r = ζ ^ r ∨ (-ζ) ^ r = -ζ ^ r

Tactic:
rcases Nat.even_or_odd r with (h | h) <;> simp [neg_pow, h.neg_one_pow]

Result:
no goals