harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

Proof state:
case mp
s n s' n' : Nat
⊢ range' s n = range' s' n' → n = n' ∧ (n = 0 ∨ s = s')

Tactic:
intro h

Result:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
⊢ n = n' ∧ (n = 0 ∨ s = s')

Proof state:
case mp.succ
s s' n : Nat
h : range' s (n + 1) = range' s' (n + 1)
⊢ n + 1 = n + 1 ∧ (n + 1 = 0 ∨ s = s')

Tactic:
simp only [range'_succ] at h

Result:
case mp.succ
s s' n : Nat
h : s :: range' (s + 1) n = s' :: range' (s' + 1) n
⊢ n + 1 = n + 1 ∧ (n + 1 = 0 ∨ s = s')

Proof state:
s n s' n' : Nat
⊢ range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
constructor

Result:
case mp
s n s' n' : Nat
⊢ range' s n = range' s' n' → n = n' ∧ (n = 0 ∨ s = s')

case mpr
s n s' n' : Nat
⊢ n = n' ∧ (n = 0 ∨ s = s') → range' s n = range' s' n'

Proof state:
case mpr
s n s' n' : Nat
⊢ n = n' ∧ (n = 0 ∨ s = s') → range' s n = range' s' n'

Tactic:
rintro ⟨rfl, rfl | rfl⟩ <;> simp

Result:
no goals

Proof state:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
⊢ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
have h' := congrArg List.length h

Result:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
h' : (range' s n).length = (range' s' n').length
⊢ n = n' ∧ (n = 0 ∨ s = s')

Proof state:
case mp
s n s' : Nat
h : range' s n = range' s' n
⊢ n = n ∧ (n = 0 ∨ s = s')

Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [range'_succ] at h
  simp_all

Result:
no goals

Proof state:
case mp.succ
s s' n : Nat
h : s :: range' (s + 1) n = s' :: range' (s' + 1) n
⊢ n + 1 = n + 1 ∧ (n + 1 = 0 ∨ s = s')

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
h' : (range' s n).length = (range' s' n').length
⊢ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
simp at h'

Result:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
h' : n = n'
⊢ n = n' ∧ (n = 0 ∨ s = s')

Proof state:
case mp
s n s' n' : Nat
h : range' s n = range' s' n'
h' : n = n'
⊢ n = n' ∧ (n = 0 ∨ s = s')

Tactic:
subst h'

Result:
case mp
s n s' : Nat
h : range' s n = range' s' n
⊢ n = n ∧ (n = 0 ∨ s = s')

Proof state:
case mp.zero
s s' : Nat
h : range' s 0 = range' s' 0
⊢ 0 = 0 ∧ (0 = 0 ∨ s = s')

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.ofComponents_snd :
    Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fst ≫ f₁₂ + biprod.snd ≫ f₂₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fst ≫ f₁₂ + biprod.snd ≫ f₂₂

Tactic:
simp [Biprod.ofComponents]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_ne_moveLeft {G : PGame} (i : G.LeftMoves) :
    grundyValue (G.moveLeft i) ≠ grundyValue G

Proof state:
G : PGame
i : G.LeftMoves
this : sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ ∈ (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Tactic:
rw [Set.mem_compl_iff, Set.mem_range, not_exists] at this

Result:
G : PGame
i : G.LeftMoves
this : ∀ (x : G.LeftMoves), ¬(G.moveLeft x).grundyValue = sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Proof state:
G : PGame
i : G.LeftMoves
⊢ (G.moveLeft i).grundyValue ≠ G.grundyValue

Tactic:
conv_rhs => rw [grundyValue_eq_sInf_moveLeft]

Result:
G : PGame
i : G.LeftMoves
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Proof state:
G : PGame
i : G.LeftMoves
this : ∀ (x : G.LeftMoves), ¬(G.moveLeft x).grundyValue = sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Tactic:
exact this _

Result:
no goals

Proof state:
G : PGame
i : G.LeftMoves
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ

Tactic:
have := csInf_mem (nonempty_of_not_bddAbove <|
  Nimber.not_bddAbove_compl_of_small (Set.range fun i => grundyValue (G.moveLeft i)))

Result:
G : PGame
i : G.LeftMoves
this : sInf (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ ∈ (Set.range fun i => (G.moveLeft i).grundyValue)ᶜ
⊢ (G.moveLeft i).grundyValue ≠ sInf (Set.range (grundyValue ∘ G.moveLeft))ᶜ
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma not_differentiableWithinAt_klFun_Ioi_zero : ¬ DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Proof state:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
rw [deriv_klFun]

Result:
⊢ Tendsto log (nhdsWithin 0 (Ioi 0)) atBot

Proof state:
⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_

Result:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot

Proof state:
⊢ Tendsto log (nhdsWithin 0 (Ioi 0)) atBot

Tactic:
exact tendsto_log_nhdsWithin_zero_right

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sdiv_self {x : BitVec w} :
    x.sdiv x = if x == 0#w then 0#w else 1#w

Proof state:
case pos
w : Nat
x : BitVec w
h : w = 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#w then 0#w else 1#w
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#w then 0#w else 1#w) =
    if x = 0#w then 0#w else 1#w

Tactic:
subst h

Result:
case pos
x : BitVec 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#1 then 0#1 else 1#1
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#1 then 0#1 else 1#1) =
    if x = 0#1 then 0#1 else 1#1

Proof state:
case pos
x : BitVec 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#1 then 0#1 else 1#1
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#1 then 0#1 else 1#1) =
    if x = 0#1 then 0#1 else 1#1

Tactic:
rcases x.msb with msb | msb <;> simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.sdiv x = if (x == 0#w) = true then 0#w else 1#w

Tactic:
simp [sdiv_eq]

Result:
w : Nat
x : BitVec w
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#w then 0#w else 1#w
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#w then 0#w else 1#w) =
    if x = 0#w then 0#w else 1#w

Proof state:
case neg
w : Nat
x : BitVec w
h : ¬w = 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#w then 0#w else 1#w
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#w then 0#w else 1#w) =
    if x = 0#w then 0#w else 1#w

Tactic:
rcases x.msb with msb | msb <;> simp [h]

Result:
no goals

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

Tactic:
by_cases h : w = 1

Result:
case pos
w : Nat
x : BitVec w
h : w = 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#w then 0#w else 1#w
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#w then 0#w else 1#w) =
    if x = 0#w then 0#w else 1#w

case neg
w : Nat
x : BitVec w
h : ¬w = 1
⊢ (match x.msb, x.msb with
    | false, false => if x = 0#w then 0#w else 1#w
    | false, true => -(x / -x)
    | true, false => -(-x / x)
    | true, true => if x = 0#w then 0#w else 1#w) =
    if x = 0#w then 0#w else 1#w
-- Mathlib/Algebra/Module/Equiv/Opposite.lean
theorem LinearMap.ext_ring_op
    {σ : Rᵐᵒᵖ →+* S} {f g : R →ₛₗ[σ] M} (h : f (1 : R) = g (1 : R)) :
    f = g :=
  ext fun x ↦ by
    rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem sup_eq_closure (N N' : Submonoid M) : N ⊔ N' = closure ((N : Set M) ∪ (N' : Set M))

Proof state:
M : Type u_1
inst✝ : MulOneClass M
N N' : Submonoid M
⊢ N ⊔ N' = closure (↑N ∪ ↑N')

Tactic:
simp_rw [closure_union, closure_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_three : W.Ψ 3 = C W.Ψ₃

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
decide

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ 3 = C W.Ψ₃

Tactic:
rw [← Nat.cast_three, Ψ_ofNat, preΨ'_three, if_neg <| by decide, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.isoProduct_inv {f : J → C} [HasBiproduct f] :
    (biproduct.isoProduct f).inv = biproduct.lift (Pi.π f) :=
  biproduct.hom_ext _ _ fun j => by simp [Iso.inv_comp_eq]

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ (isoProduct f).inv ≫ π f j = lift (Pi.π f) ≫ π f j

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem pi_le_borel_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, MeasurableSpace (π i)] [∀ i, BorelSpace (π i)] :
      MeasurableSpace.pi ≤ borel (∀ i, π i)

Proof state:
ι : Type u_6
π : ι → Type u_7
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)

Tactic:
have : ‹∀ i, MeasurableSpace (π i)› = fun i => borel (π i) :=
  funext fun i => BorelSpace.measurable_eq

Result:
ι : Type u_6
π : ι → Type u_7
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)

Proof state:
ι : Type u_6
π : ι → Type u_7
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : (i : ι) → MeasurableSpace (π i)
inst✝ : ∀ (i : ι), BorelSpace (π i)
this : inst✝¹ = fun i => borel (π i)
⊢ MeasurableSpace.pi ≤ borel ((i : ι) → π i)

Tactic:
exact iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem Path.ext : ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂

Proof state:
case mk.mk.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
x✝ y : X
x : ↑I → X
h11 : Continuous x
h12 : { toFun := x, continuous_toFun := h11 }.toFun 0 = x✝
h13 : { toFun := x, continuous_toFun := h11 }.toFun 1 = y
h21 : Continuous ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }
h22 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      0 =
    x✝
h23 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      1 =
    y
⊢ { toFun := x, continuous_toFun := h11, source' := h12, target' := h13 } =
    { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21,
      source' := h22, target' := h23 }

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ∀ {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

Tactic:
rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl

Result:
case mk.mk.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
x✝ y : X
x : ↑I → X
h11 : Continuous x
h12 : { toFun := x, continuous_toFun := h11 }.toFun 0 = x✝
h13 : { toFun := x, continuous_toFun := h11 }.toFun 1 = y
h21 : Continuous ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }
h22 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      0 =
    x✝
h23 :
  { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21 }.toFun
      1 =
    y
⊢ { toFun := x, continuous_toFun := h11, source' := h12, target' := h13 } =
    { toFun := ⇑{ toFun := x, continuous_toFun := h11, source' := h12, target' := h13 }, continuous_toFun := h21,
      source' := h22, target' := h23 }
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@[to_additive]
lemma image_inclusion (s : SubMulAction M α) :
    Set.range s.inclusion = s.carrier

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : SubMulAction M α
⊢ Set.range ⇑s.inclusion = s.carrier

Tactic:
rw [inclusion.coe_eq]

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : SubMulAction M α
⊢ Set.range Subtype.val = s.carrier

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : SubMulAction M α
⊢ Set.range Subtype.val = s.carrier

Tactic:
exact Subtype.range_coe

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).source`. -/
lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm' {x : M}
    {y : M} (hy : y ∈ (extChartAt I x).source) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) y) ∘L
      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) (extChartAt I x y))
    = ContinuousLinearMap.id _ _

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))

Tactic:
convert mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm ((extChartAt I x).map_source hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))

Tactic:
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) y).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))
-- Mathlib/RingTheory/Coprime/Basic.lean
/-- `IsCoprime` is not a useful definition if an inverse is available. -/
@[simp]
lemma Semifield.isCoprime_iff {R : Type*} [Semifield R] {m n : R} :
    IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Proof state:
case inl
R : Type u_1
inst✝ : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ 0 ≠ 0

Tactic:
simp [isCoprime_zero_right]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
this : IsCoprime m n
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
simpa [hn]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
suffices IsCoprime m n by simpa [hn]

Result:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n

Proof state:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n

Tactic:
refine ⟨0, n⁻¹, ?_⟩

Result:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ 0 * m + n⁻¹ * n = 1

Proof state:
R : Type u_1
inst✝ : Semifield R
m n : R
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
R : Type u_1
inst✝ : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ 0 ≠ 0

case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Proof state:
case inr
R : Type u_1
inst✝ : Semifield R
m n : R
hn : n ≠ 0
⊢ 0 * m + n⁻¹ * n = 1

Tactic:
simp [inv_mul_cancel₀ hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
    a / b = c ↔ a = c * b

Proof state:
a b c : Nat
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = c * b

Tactic:
rw [Nat.mul_comm]

Result:
a b c : Nat
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c

Proof state:
a b c : Nat
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c

Tactic:
exact Nat.div_eq_iff_eq_mul_right H H'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
    {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a)

Proof state:
α : Type u_1
inst✝² : Max α
inst✝¹ : Std.IdempotentOp max
inst✝ : Std.Associative max
l : List α
a : α
⊢ foldl max a l = max a (l.max?.getD a)

Tactic:
cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x = true

Tactic:
simp [all_eq]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma IsLocallyClosed.inter (hs : IsLocallyClosed s) (ht : IsLocallyClosed t) :
    IsLocallyClosed (s ∩ t)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsLocallyClosed t
U₁ Z₁ : Set X
hU₁ : IsOpen U₁
hZ₁ : IsClosed Z₁
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)

Tactic:
obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U₁ Z₁ : Set X
hU₁ : IsOpen U₁
hZ₁ : IsClosed Z₁
U₂ Z₂ : Set X
hU₂ : IsOpen U₂
hZ₂ : IsClosed Z₂
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U₁ Z₁ : Set X
hU₁ : IsOpen U₁
hZ₁ : IsClosed Z₁
U₂ Z₂ : Set X
hU₂ : IsOpen U₂
hZ₂ : IsClosed Z₂
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))

Tactic:
refine ⟨_, _, hU₁.inter hU₂, hZ₁.inter hZ₂, inter_inter_inter_comm U₁ Z₁ U₂ Z₂⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyClosed s
ht : IsLocallyClosed t
⊢ IsLocallyClosed (s ∩ t)

Tactic:
obtain ⟨U₁, Z₁, hU₁, hZ₁, rfl⟩ := hs

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsLocallyClosed t
U₁ Z₁ : Set X
hU₁ : IsOpen U₁
hZ₁ : IsClosed Z₁
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_zero (s : S) : mk' f 0 s = 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
s : ↥S
⊢ mk' f 0 s = 0

Tactic:
rw [← zero_smul R (0 : M), mk'_smul, zero_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR

Proof state:
case h.h.h.h
α : Type u_1
f : Nat
n : α
l : List α
⊢ insertIdx f n l = insertIdxTR f n l

Tactic:
simp [insertIdxTR, insertIdxTR_go_eq]

Result:
no goals

Proof state:
⊢ @insertIdx = @insertIdxTR

Tactic:
funext α f n l

Result:
case h.h.h.h
α : Type u_1
f : Nat
n : α
l : List α
⊢ insertIdx f n l = insertIdxTR f n l
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem X_pow_sub_C_ne_zero {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n - C a ≠ 0

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - C a ≠ 0

Tactic:
rw [sub_eq_add_neg, ← map_neg C a]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + C (-a) ≠ 0

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + C (-a) ≠ 0

Tactic:
exact X_pow_add_C_ne_zero hn _

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_prod_list_of_pairwise_disjoint {l : List (Perm α)} (h : l.Pairwise Disjoint) :
    #l.prod.support = (l.map (card ∘ support)).sum

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ #l.prod.support = (List.map (card ∘ support) l).sum

Tactic:
induction' l with a t ih

Result:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ # [].prod.support = (List.map (card ∘ support) []).sum

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a * t.prod).support = (card ∘ support) a + #t.prod.support

Tactic:
exact (disjoint_prod_right _ ha).card_support_mul

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum

Tactic:
obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h

Result:
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum

Proof state:
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a :: t).prod.support = (List.map (card ∘ support) (a :: t)).sum

Tactic:
rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]

Result:
case cons.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a : Perm α
t : List (Perm α)
ih : List.Pairwise Disjoint t → #t.prod.support = (List.map (card ∘ support) t).sum
h : List.Pairwise Disjoint (a :: t)
ha : ∀ a' ∈ t, a.Disjoint a'
ht : List.Pairwise Disjoint t
⊢ #(a * t.prod).support = (card ∘ support) a + #t.prod.support

Proof state:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ # [].prod.support = (List.map (card ∘ support) []).sum

Tactic:
exact card_support_eq_zero.mpr rfl

Result:
no goals