harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma Equation.baseChange (h : (W'.baseChange A).toAffine.Equation x y) :
    (W'.baseChange B).toAffine.Equation (f x) (f y)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (WeierstrassCurve.baseChange W' A).toAffine.Equation x y
⊢ (WeierstrassCurve.baseChange W' B).toAffine.Equation (f x) (f y)

Tactic:
convert Equation.map f.toRingHom h using 1

Result:
case h.e'_3
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (WeierstrassCurve.baseChange W' A).toAffine.Equation x y
⊢ (WeierstrassCurve.baseChange W' B).toAffine =
    (WeierstrassCurve.map (WeierstrassCurve.baseChange W' A).toAffine f.toRingHom).toAffine

Proof state:
case h.e'_3
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (WeierstrassCurve.baseChange W' A).toAffine.Equation x y
⊢ (WeierstrassCurve.baseChange W' B).toAffine =
    (WeierstrassCurve.map (WeierstrassCurve.baseChange W' A).toAffine f.toRingHom).toAffine

Tactic:
rw [AlgHom.toRingHom_eq_coe, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
    x + Fin.ofNat' n y = Fin.ofNat' n (x.val + y)

Proof state:
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ x + Fin.ofNat' n y = Fin.ofNat' n (↑x + y)

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ ↑(x + Fin.ofNat' n y) = ↑(Fin.ofNat' n (↑x + y))

Proof state:
case a
n : Nat
inst✝ : NeZero n
x : Fin n
y : Nat
⊢ ↑(x + Fin.ofNat' n y) = ↑(Fin.ofNat' n (↑x + y))

Tactic:
simp [Fin.ofNat', Fin.add_def]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardDistinctFactors_apply_prime_pow {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
    ω (p ^ k) = 1

Proof state:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ ω (p ^ k) = 1

Tactic:
rw [cardDistinctFactors_apply, hp.primeFactorsList_pow, List.replicate_dedup hk,
  List.length_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem isKernelCompMono_lift {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g]
    {h : X ⟶ Z} (hh : h = f ≫ g) (s : KernelFork h) :
    (isKernelCompMono i g hh).lift s = i.lift (Fork.ofι s.ι (by
      rw [← cancel_mono g, Category.assoc, ← hh]
      simp)) := rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ f = Fork.ι s ≫ 0

Tactic:
rw [← cancel_mono g, Category.assoc, ← hh]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem hasDerivWithinAt_Iio_iff_Iic [PartialOrder 𝕜] :
    HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x

Tactic:
rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma lt_div_mul_add (hb : 0 < b) : a < a / b * b + b

Proof state:
a b : ℕ
hb : 0 < b
⊢ a < a / b * b + b

Tactic:
rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]

Result:
a b : ℕ
hb : 0 < b
⊢ a / b < (a / b).succ

Proof state:
a b : ℕ
hb : 0 < b
⊢ a / b < (a / b).succ

Tactic:
exact Nat.lt_succ_self _

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_top_of_isLocalized'_span {N : Submodule R M}
    (h : ∀ r : s, N.localized' (Rₚ r) (.powers r.1) (f r) = ⊤) : N = ⊤ :=
  eq_of_isLocalized'_span s span_eq Rₚ Mₚ f fun _ ↦ by simp only [h, Submodule.localized'_top]

Proof state:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Rₚ : ↑s → Type u_4
inst✝⁷ : (r : ↑s) → CommSemiring (Rₚ r)
inst✝⁶ : (r : ↑s) → Algebra R (Rₚ r)
inst✝⁵ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)
Mₚ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝³ : (r : ↑s) → Module R (Mₚ r)
inst✝² : (r : ↑s) → Module (Rₚ r) (Mₚ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊤
x✝ : ↑s
⊢ localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) N = localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) ⊤

Tactic:
simp only [h, Submodule.localized'_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_append (a : Vector α n) (b : Vector α m) (i : Nat) (hi : i < n + m) :
    (a ++ b)[i] = if h : i < n then a[i] else b[i - n]

Proof state:
case mk
α : Type u_1
m : Nat
b : Vector α m
i : Nat
a : Array α
hi : i < a.size + m
⊢ ({ toArray := a, size_toArray := ⋯ } ++ b)[i] =
    if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else b[i - a.size]

Tactic:
rcases b with ⟨b, rfl⟩

Result:
case mk.mk
α : Type u_1
i : Nat
a b : Array α
hi : i < a.size + b.size
⊢ ({ toArray := a, size_toArray := ⋯ } ++ { toArray := b, size_toArray := ⋯ })[i] =
    if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else { toArray := b, size_toArray := ⋯ }[i - a.size]

Proof state:
α : Type u_1
n m : Nat
a : Vector α n
b : Vector α m
i : Nat
hi : i < n + m
⊢ (a ++ b)[i] = if h : i < n then a[i] else b[i - n]

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
b : Vector α m
i : Nat
a : Array α
hi : i < a.size + m
⊢ ({ toArray := a, size_toArray := ⋯ } ++ b)[i] =
    if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else b[i - a.size]

Proof state:
case mk.mk
α : Type u_1
i : Nat
a b : Array α
hi : i < a.size + b.size
⊢ ({ toArray := a, size_toArray := ⋯ } ++ { toArray := b, size_toArray := ⋯ })[i] =
    if h : i < a.size then { toArray := a, size_toArray := ⋯ }[i] else { toArray := b, size_toArray := ⋯ }[i - a.size]

Tactic:
simp [Array.getElem_append, hi]

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

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

Tactic:
simp [getKey!_alter h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem isLittleO_pow_log_id_atTop {n : ℕ} : (fun x => log x ^ n) =o[atTop] id

Proof state:
n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0

Tactic:
filter_upwards [eventually_ne_atTop (0 : ℝ)] with x h₁ h₂ using (h₁ h₂).elim

Result:
no goals

Proof state:
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)

Tactic:
simpa using tendsto_pow_log_div_mul_add_atTop 1 0 n one_ne_zero

Result:
no goals

Proof state:
n : ℕ
⊢ (fun x => log x ^ n) =o[atTop] id

Tactic:
rw [Asymptotics.isLittleO_iff_tendsto']

Result:
n : ℕ
⊢ Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)

n : ℕ
⊢ ∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem lineMap_lt_right_iff_lt (h : r < 1) : lineMap a b r < b ↔ a < b :=
  Iff.trans (by rw [lineMap_apply_one]) (lineMap_lt_lineMap_iff_of_lt h)

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r : k
h : r < 1
⊢ (lineMap a b) r < b ↔ (lineMap a b) r < (lineMap a b) 1

Tactic:
rw [lineMap_apply_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι]
    {h : finrank R M = 1} {v : M} {i : ι} :
    (basisUnique ι h).repr v i = 0 ↔ v = 0 :=
  ⟨fun hv =>
    (basisUnique ι h).repr.map_eq_zero_iff.mp (Finsupp.ext fun j => Subsingleton.elim i j ▸ hv),
    fun hv => by rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]⟩

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
ι : Type u_1
inst✝ : Unique ι
h : finrank R M = 1
v : M
i : ι
hv : v = 0
⊢ ((basisUnique ι h).repr v) i = 0

Tactic:
rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem constantCoeff_wittPolynomial [hp : Fact p.Prime] (n : ℕ) :
    constantCoeff (wittPolynomial p R n) = 0

Proof state:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0

Tactic:
rw [Finsupp.single_eq_zero]

Result:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (W_ R n) = 0

Tactic:
simp only [wittPolynomial, map_sum, constantCoeff_monomial]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0

Tactic:
rintro i _

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0

Proof state:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬p ^ (n - i) = 0

Tactic:
exact ne_of_gt (pow_pos hp.1.pos _)

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ (if single i (p ^ (n - i)) = 0 then ↑p ^ i else 0) = 0

Tactic:
rw [if_neg]

Result:
case hnc
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n i : ℕ
a✝ : i ∈ range (n + 1)
⊢ ¬single i (p ^ (n - i)) = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0

Tactic:
rw [sum_eq_zero]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1), (if single x (p ^ (n - x)) = 0 then ↑p ^ x else 0) = 0
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- A set is open in `deltaGenerated X` iff all its preimages under continuous functions ℝⁿ → X are
  open. -/
lemma isOpen_deltaGenerated_iff {u : Set X} :
    IsOpen[deltaGenerated X] u ↔ ∀ n (p : C(Fin n → ℝ, X)), IsOpen (p ⁻¹' u)

Proof state:
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ IsOpen u ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

Tactic:
simp_rw [deltaGenerated, isOpen_iSup_iff, isOpen_coinduced, Sigma.forall]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem closure_addSubmonoid_closure {s : Set R} :
    closure ↑(AddSubmonoid.closure s) = closure s

Proof state:
case h
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s

Tactic:
refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩

Result:
case h
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J

Tactic:
refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_

Result:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Proof state:
case h
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
⊢ x ∈ closure s

Tactic:
rintro - ⟨H, rfl⟩

Result:
case h.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Tactic:
refine (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_

Result:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid

Proof state:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid

Tactic:
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Result:
no goals

Proof state:
case h.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
⊢ x ∈ (fun t => ⋂ (_ : t ∈ {S | s ⊆ ↑S}), ↑t) H

Tactic:
rintro - ⟨J, rfl⟩

Result:
case h.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
⊢ x ∈ (fun h => ↑H) J

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ closure ↑(AddSubmonoid.closure s) = closure s

Tactic:
ext x

Result:
case h
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
⊢ x ∈ closure ↑(AddSubmonoid.closure s) ↔ x ∈ closure s
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_add_left_left (h : IsCoprime (y * z + x) y) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y * z + x) y
⊢ IsCoprime x y

Tactic:
rw [add_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_left

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vadd_right_cancel {g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g₁ g₂ : G
p : P
h : g₁ +ᵥ p = g₂ +ᵥ p
⊢ g₁ = g₂

Tactic:
rw [← vadd_vsub g₁ p, h, vadd_vsub]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem insert_prod : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
a : α
⊢ insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Tactic:
simp only [insert_eq, union_prod, singleton_prod]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
@[simp] lemma iInf_lt_top : ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨅ i, s i < ⊤ ↔ ∃ i, s i < ⊤

Tactic:
simp [lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
    match x.msb, y.msb with
    | false, false => (x.umod y).toNat
    | false, true =>
      let u := x.umod (- y)
      (if u = 0#w then u.toNat else (u + y).toNat)
    | true, false =>
      let u := (-x).umod y
      (if u = 0#w then u.toNat else (y - u).toNat)
    | true, true => (- ((- x).umod (- y))).toNat

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
      | false, false => x.umod y
      | false, true => if x.umod (-y) = 0#w then x.umod (-y) else x.umod (-y) + y
      | true, false => if (-x).umod y = 0#w then (-x).umod y else y - (-x).umod y
      | true, true => -(-x).umod (-y)).toNat =
    match x.msb, y.msb with
    | false, false => (x.umod y).toNat
    | false, true => if x.umod (-y) = 0#w then (x.umod (-y)).toNat else (x.umod (-y) + y).toNat
    | true, false => if (-x).umod y = 0#w then ((-x).umod y).toNat else (y - (-x).umod y).toNat
    | true, true => (-(-x).umod (-y)).toNat

Tactic:
by_cases h : x.msb <;> by_cases h' : y.msb
<;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
<;> simp only [h, h', h'', h''']
<;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp [h'', h''']

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ (x.smod y).toNat =
    match x.msb, y.msb with
    | false, false => (x.umod y).toNat
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u.toNat else (u + y).toNat
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u.toNat else (y - u).toNat
    | true, true => (-(-x).umod (-y)).toNat

Tactic:
simp only [smod_eq, toNat_umod]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
      | false, false => x.umod y
      | false, true => if x.umod (-y) = 0#w then x.umod (-y) else x.umod (-y) + y
      | true, false => if (-x).umod y = 0#w then (-x).umod y else y - (-x).umod y
      | true, true => -(-x).umod (-y)).toNat =
    match x.msb, y.msb with
    | false, false => (x.umod y).toNat
    | false, true => if x.umod (-y) = 0#w then (x.umod (-y)).toNat else (x.umod (-y) + y).toNat
    | true, false => if (-x).umod y = 0#w then ((-x).umod y).toNat else (y - (-x).umod y).toNat
    | true, true => (-(-x).umod (-y)).toNat
-- Mathlib/Data/Int/Order/Lemmas.lean
theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Proof state:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs

Tactic:
exact Int.ofNat_le.symm

Result:
no goals

Proof state:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]

Result:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ ↑a.natAbs ≤ ↑b.natAbs
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem SimpleFunc.integral_eq_integral (f : α →ₛ E) (hfi : Integrable f μ) :
    f.integral μ = ∫ x, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (Lp.simpleFunc.toLp f ⋯))

Tactic:
exact SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = ∫ (x : α), f x ∂μ

Tactic:
rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1,
  L1.SimpleFunc.integral_L1_eq_integral, L1.SimpleFunc.integral_eq_integral]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (Lp.simpleFunc.toLp f ⋯))
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem constantCoeff_invUnitsSub (u : Rˣ) : constantCoeff R (invUnitsSub u) = 1 /ₚ u

Proof state:
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (constantCoeff R) (invUnitsSub u) = 1 /ₚ u

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.inv {f : E → 𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ x, f x ≠ 0) :
    ContDiff 𝕜 n fun x => (f x)⁻¹

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff 𝕜 n fun x => (f x)⁻¹

Tactic:
rw [contDiff_iff_contDiffAt]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : WithTop ℕ∞
𝕜' : Type u_4
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ∀ (x : E), ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x

Tactic:
exact fun x => hf.contDiffAt.inv (h x)

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem row_eq_zero_of_commute_stdBasisMatrix {i j k : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) (hkj : k ≠ j) : M j k = 0

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hkj : k ≠ j
this : (stdBasisMatrix i j 1 * M) i k = (M * stdBasisMatrix i j 1) i k
⊢ M j k = 0

Tactic:
aesop

Result:
no goals

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hkj : k ≠ j
⊢ M j k = 0

Tactic:
have := ext_iff.mpr hM i k

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
hkj : k ≠ j
this : (stdBasisMatrix i j 1 * M) i k = (M * stdBasisMatrix i j 1) i k
⊢ M j k = 0
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_mul_right_left (m n k : ℕ) : gcd (m + k * n) n = gcd m n

Proof state:
m n k : ℕ
⊢ (m + k * n).gcd n = m.gcd n

Tactic:
rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem inv_id : inv (@Eq α) = @Eq α

Proof state:
α : Type u_1
⊢ inv Eq = Eq

Tactic:
ext x y

Result:
case a.h.a
α : Type u_1
x y : α
⊢ inv Eq x y ↔ x = y

Proof state:
case a.h.a
α : Type u_1
x y : α
⊢ inv Eq x y ↔ x = y

Tactic:
constructor <;> apply Eq.symm

Result:
no goals