harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Monic.lean
lemma comp_X_add_C (hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False

Tactic:
exact one_ne_zero ha

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (X + C r)).Monic

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
⊢ (p.comp (X + C r)).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : (X + C r).natDegree = 0
⊢ False

Tactic:
rw [natDegree_X_add_C] at ha

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
⊢ (p.comp (X + C r)).Monic

Tactic:
refine hp.comp (monic_X_add_C _) fun ha ↦ ?_

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : (X + C r).natDegree = 0
⊢ False
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem removeZero_of_pos (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (h : 0 < n) :
    p.removeZero n = p n

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n = p n

Tactic:
rw [← Nat.succ_pred_eq_of_pos h]

Result:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n.pred.succ = p n.pred.succ

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : 0 < n
⊢ p.removeZero n.pred.succ = p n.pred.succ

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma transpose_swap (i j : n) : (swap R i j).transpose = swap R i j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Zero R
inst✝¹ : One R
inst✝ : DecidableEq n
i j : n
⊢ (swap R i j)ᵀ = swap R i j

Tactic:
simp [swap]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_symm_zero {n : ℕ} [NeZero n] (i : Fin n) : i.cycleRange.symm 0 = i :=
  i.cycleRange.injective (by simp)

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.cycleRange ((Equiv.symm i.cycleRange) 0) = i.cycleRange i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Time/Date/Unit/Month.lean
theorem days_gt_27 (leap : Bool) (i : Month.Ordinal) : days leap i > 27

Proof state:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ 27 < [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 11)]

Tactic:
decide +revert

Result:
no goals

Proof state:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 2 ∧ 2 ≤ 12
⊢ 27 < if leap = true then 29 else 28

Tactic:
split <;> decide

Result:
no goals

Proof state:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 2 ∧ 2 ≤ 12
⊢ days leap ⟨2, property✝⟩ > 27

Tactic:
simp [days]

Result:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 2 ∧ 2 ≤ 12
⊢ 27 < if leap = true then 29 else 28

Proof state:
leap : Bool
i : Ordinal
⊢ days leap i > 27

Tactic:
match i with
| ⟨2, _⟩ =>
  simp [days]
  split <;> decide
| ⟨1, _⟩ | ⟨3, _⟩ | ⟨4, _⟩ | ⟨5, _⟩ | ⟨6, _⟩ | ⟨7, _⟩
| ⟨8, _⟩ | ⟨9, _⟩ | ⟨10, _⟩ | ⟨11, _⟩ | ⟨12, _⟩ =>
  simp [days, monthSizesNonLeap]
  decide +revert

Result:
no goals

Proof state:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ days leap ⟨12, property✝⟩ > 27

Tactic:
simp [days, monthSizesNonLeap]

Result:
leap : Bool
i : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ 27 < [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 11)]
-- Mathlib/Topology/Connected/PathConnected.lean
theorem JoinedIn.mem (h : JoinedIn F x y) : x ∈ F ∧ y ∈ F

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ x ∈ F ∧ y ∈ F

Tactic:
have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
this : γ 0 ∈ F ∧ γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F

Proof state:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
this : γ 0 ∈ F ∧ γ 1 ∈ F
⊢ x ∈ F ∧ y ∈ F

Tactic:
simpa using this

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F

Tactic:
rcases h with ⟨γ, γ_in⟩

Result:
case intro
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ x ∈ F ∧ y ∈ F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : ↑I), γ t ∈ F
⊢ γ 0 ∈ F ∧ γ 1 ∈ F

Tactic:
constructor <;> apply γ_in

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem connectedComponents_preimage_image (U : Set α) :
    (↑) ⁻¹' ((↑) '' U : Set (ConnectedComponents α)) = ⋃ x ∈ U, connectedComponent x

Proof state:
α : Type u
inst✝ : TopologicalSpace α
U : Set α
⊢ ConnectedComponents.mk ⁻¹' (ConnectedComponents.mk '' U) = ⋃ x ∈ U, connectedComponent x

Tactic:
simp only [connectedComponents_preimage_singleton, preimage_iUnion₂, image_eq_iUnion]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_toReal_eq {f : α → ℝ≥0∞} (hf : ∀ a, f a ≠ ∞) :
    (∑' a, f a).toReal = ∑' a, (f a).toReal

Proof state:
α : Type u_1
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≠ ⊤
⊢ (∑' (a : α), f a).toReal = ∑' (a : α), (f a).toReal

Tactic:
simp only [ENNReal.toReal, tsum_toNNReal_eq hf, NNReal.coe_tsum]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_zero_eq_range : Ico 0 = range

Proof state:
⊢ Ico 0 = range

Tactic:
rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_add_zero (a : A) :
    shiftFunctorAdd' C a 0 a (add_zero a) = (Functor.rightUnitor _).symm ≪≫
    isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ shiftFunctorAdd' C a 0 a ⋯ =
    (shiftFunctor C a).rightUnitor.symm ≪≫ isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm

Tactic:
ext

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).hom.app x✝ =
    ((shiftFunctor C a).rightUnitor.symm ≪≫ isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm).hom.app x✝

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    eqToHom ⋯ ≫ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a } (𝟙_ (Discrete A))).app x✝

Tactic:
rfl

Result:
no goals

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (eqToHom ⋯).app x✝ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝) ≫
      (Functor.LaxMonoidal.ε (shiftMonoidalFunctor C A)).app (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝)

Tactic:
simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv,
  eqToHom_map, Category.id_comp]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ eqToHom ⋯ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    eqToHom ⋯ ≫ (Functor.OplaxMonoidal.δ (shiftMonoidalFunctor C A) { as := a } (𝟙_ (Discrete A))).app x✝

Proof state:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (shiftFunctorAdd' C a 0 a ⋯).hom.app x✝ =
    ((shiftFunctor C a).rightUnitor.symm ≪≫ isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm).hom.app x✝

Tactic:
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]

Result:
case w.w.h
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
x✝ : C
⊢ (eqToHom ⋯).app x✝ ≫ (shiftFunctorAdd C a 0).hom.app x✝ =
    𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝) ≫
      (Functor.LaxMonoidal.ε (shiftMonoidalFunctor C A)).app (((shiftMonoidalFunctor C A).obj { as := a }).obj x✝)
-- Mathlib/NumberTheory/Multiplicity.lean
theorem dvd_geom_sum₂_iff_of_dvd_sub' {x y p : R} (h : p ∣ x - y) :
    (p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) ↔ p ∣ n * x ^ (n - 1)

Proof state:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * x ^ (n - 1)

Tactic:
rw [geom_sum₂_comm, dvd_geom_sum₂_iff_of_dvd_sub]

Result:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x

Proof state:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : p ∣ x - y
⊢ p ∣ y - x

Tactic:
simpa using h.neg_right

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
@[norm_cast]
lemma ofNat_isUnit {n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n

Proof state:
n : ℕ
⊢ IsUnit ↑n ↔ IsUnit n

Tactic:
simp [isUnit_iff_natAbs_eq]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem length_nontrivial {s : Cycle α} (h : Nontrivial s) : 2 ≤ length s

Proof state:
case intro.intro.intro.intro.h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)

Result:
case intro.intro.intro.intro.h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])

case intro.intro.intro.intro.h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

case intro.intro.intro.intro.h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Proof state:
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

Tactic:
simp only [mem_coe_iff, mk_eq_coe, mem_singleton] at hx hy

Result:
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length

Tactic:
induction' s using Quot.inductionOn with l

Result:
case intro.intro.intro.intro.h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)

Proof state:
case intro.intro.intro.intro.h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x = hd
hy : y = hd
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

Tactic:
simp [hx, hy] at hxy

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
h : s.Nontrivial
⊢ 2 ≤ s.length

Tactic:
obtain ⟨x, y, hxy, hx, hy⟩ := h

Result:
case intro.intro.intro.intro
α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length

Proof state:
case intro.intro.intro.intro.h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])

Tactic:
simp at hx

Result:
no goals

Proof state:
case intro.intro.intro.intro.h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
simp [Nat.succ_le_succ_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem map_comp {f : T ⟶ T'} {f' : T' ⟶ T''} {h : CostructuredArrow S T} :
    (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj h = (map f').obj ((map f).obj h)

Tactic:
rw [eq_mk h]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
S : C ⥤ D
f : T ⟶ T'
f' : T' ⟶ T''
h : CostructuredArrow S T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f').obj ((map f).obj (mk h.hom))
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_span_singleton_iff (x y : R) :
    IsCoprime (span <| singleton x) (span <| singleton y) ↔ IsCoprime x y

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
rintro ⟨a, b, e⟩

Result:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) → IsCoprime x y

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

Result:
case mp.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ a b, y ∣ b ∧ a * x + b = 1

Tactic:
exact ⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y

Tactic:
exact ⟨a, b, mul_comm b y ▸ e⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) → IsCoprime x y

case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime (span {x}) (span {y}) ↔ IsCoprime x y

Tactic:
simp_rw [isCoprime_iff_codisjoint, codisjoint_iff, eq_top_iff_one, mem_span_singleton_sup,
  mem_span_singleton]

Result:
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
-- Mathlib/RingTheory/Unramified/Locus.lean
lemma unramifiedLocus_eq_univ_iff :
    unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A

Proof state:
R A : Type u
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

Tactic:
rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
  Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_trans {a b c : Int} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
  let ⟨n, hn⟩ := le.dest h₁; let ⟨m, hm⟩ := le.dest h₂
  le.intro (n + m) <| by rw [← hm, ← hn, Int.add_assoc, ofNat_add]

Proof state:
a b c : Int
h₁ : a ≤ b
h₂ : b ≤ c
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = c
⊢ a + ↑(n + m) = c

Tactic:
rw [← hm, ← hn, Int.add_assoc, ofNat_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_erase_self (a : α) (l : List α) :
    count a (List.erase l a) = count a l - 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (a == a) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a (l.erase a) = count a l - 1

Tactic:
rw [count_erase, if_pos (by simp)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.add_measure {f : α → β} (hμ : HasFiniteIntegral f μ)
    (hν : HasFiniteIntegral f ν) : HasFiniteIntegral f (μ + ν)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : HasFiniteIntegral f μ
hν : HasFiniteIntegral f ν
⊢ HasFiniteIntegral f (μ + ν)

Tactic:
simp only [HasFiniteIntegral, lintegral_add_measure] at *

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
hν : ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hμ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
hν : ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ⊤

Tactic:
exact add_lt_top.2 ⟨hμ, hν⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean
theorem hasFDerivAt_integral_of_dominated_loc_of_lip
    {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H}
    (ε_pos : 0 < ε) (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b)))
    (hF_int : IntervalIntegrable (F x₀) μ a b)
    (hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b)))
    (h_lip : ∀ᵐ t ∂μ, t ∈ Ι a b →
      LipschitzOnWith (Real.nnabs <| bound t) (fun x => F x t) (ball x₀ ε))
    (bound_integrable : IntervalIntegrable bound μ a b)
    (h_diff : ∀ᵐ t ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀) :
    IntervalIntegrable F' μ a b ∧
      HasFDerivAt (fun x => ∫ t in a..b, F x t ∂μ) (∫ t in a..b, F' t ∂μ) x₀

Proof state:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
rw [← ae_restrict_iff' measurableSet_uIoc] at h_lip h_diff

Result:
𝕜 : Type u_1
inst✝⁵ : RCLike 𝕜
μ : Measure ℝ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
a b ε : ℝ
bound : ℝ → ℝ
F : H → ℝ → E
F' : ℝ → H →L[𝕜] E
x₀ : H
ε_pos : 0 < ε
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
-- Mathlib/Data/Matroid/Dual.lean
theorem IsBase.ssubset_ground [h : RankPos M✶] (hB : M.IsBase B) : B ⊂ M.E :=
  hB.subset_ground.ssubset_of_ne (by rintro rfl; exact M.ground_not_isBase hB)

Proof state:
α : Type u_1
M : Matroid α
B : Set α
h : M✶.RankPos
hB : M.IsBase B
⊢ B ≠ M.E

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False

Proof state:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False

Tactic:
exact M.ground_not_isBase hB

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_add_equiv_zero_iff (o₁ o₂ : Ordinal) : (nim o₁ + nim o₂ ≈ 0) ↔ o₁ = o₂

Proof state:
case mp
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
⊢ nim o₁ + nim o₂ ‖ 0

Tactic:
wlog h : o₁ < o₂

Result:
case mp.inr
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
this : ∀ (o₁ o₂ : Ordinal.{u_1}), o₁ ≠ o₂ → o₁ < o₂ → nim o₁ + nim o₂ ‖ 0
h : ¬o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0

o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0

Proof state:
case mpr
o₁ o₂ : Ordinal.{u_1}
⊢ o₁ = o₂ → nim o₁ + nim o₂ ≈ 0

Tactic:
rintro rfl

Result:
case mpr
o₁ : Ordinal.{u_1}
⊢ nim o₁ + nim o₁ ≈ 0

Proof state:
case h
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ 0 ≤ (nim o₁ + nim o₂).moveLeft (toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨o₁, h⟩)))

Tactic:
simpa using (Impartial.add_self (nim o₁)).2

Result:
no goals

Proof state:
case mp.inr
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
this : ∀ (o₁ o₂ : Ordinal.{u_1}), o₁ ≠ o₂ → o₁ < o₂ → nim o₁ + nim o₂ ‖ 0
h : ¬o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0

Tactic:
exact (fuzzy_congr_left add_comm_equiv).1 (this _ _ hne.symm (hne.lt_or_lt.resolve_left h))

Result:
no goals

Proof state:
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ≈ 0 ↔ o₁ = o₂

Tactic:
constructor

Result:
case mp
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ≈ 0 → o₁ = o₂

case mpr
o₁ o₂ : Ordinal.{u_1}
⊢ o₁ = o₂ → nim o₁ + nim o₂ ≈ 0

Proof state:
case mpr
o₁ : Ordinal.{u_1}
⊢ nim o₁ + nim o₁ ≈ 0

Tactic:
exact Impartial.add_self (nim o₁)

Result:
no goals

Proof state:
case mp
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ≈ 0 → o₁ = o₂

Tactic:
refine not_imp_not.1 fun hne : _ ≠ _ => (Impartial.not_equiv_zero_iff (nim o₁ + nim o₂)).2 ?_

Result:
case mp
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
⊢ nim o₁ + nim o₂ ‖ 0

Proof state:
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ ∃ i, 0 ≤ (nim o₁ + nim o₂).moveLeft i

Tactic:
use toLeftMovesAdd (Sum.inr <| toLeftMovesNim ⟨_, h⟩)

Result:
case h
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ 0 ≤ (nim o₁ + nim o₂).moveLeft (toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨o₁, h⟩)))

Proof state:
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0

Tactic:
rw [Impartial.fuzzy_zero_iff_gf, zero_lf_le]

Result:
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ ∃ i, 0 ≤ (nim o₁ + nim o₂).moveLeft i
-- Mathlib/Data/Set/Card.lean
theorem encard_le_one_iff_eq : s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Proof state:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
rw [le_iff_lt_or_eq, lt_iff_not_le, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
  encard_eq_one]

Result:
no goals