harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_linearDisjoint_fg_right
    (H : ∀ N' : Submodule R S, N' ≤ N → N'.FG → M.LinearDisjoint N') :
    M.LinearDisjoint N := (linearDisjoint_iff _ _).2 fun x y hxy ↦ by
  obtain ⟨N', hN, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_right_of_finite' {x, y} (Set.toFinite _)
  rw [Module.Finite.iff_fg] at hFG
  obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
  obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
  rw [← hx', ← hy']; congr
  exact (H N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])

Proof state:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)

Result:
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M) (inclusion hN)))
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ x = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem finRange_succ_last (n) :
    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n]

Proof state:
case h.isTrue
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
h✝ : i✝ < n
⊢ ⟨i✝, ⋯⟩ = ⟨i✝, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
⊢ (finRange (n + 1))[i✝] = (map Fin.castSucc (finRange n) ++ [Fin.last n])[i✝]

Tactic:
simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
  getElem_map, Fin.castSucc_mk, getElem_singleton]

Result:
case h
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
⊢ ⟨i✝, ⋯⟩ = if h : i✝ < n then ⟨i✝, ⋯⟩ else Fin.last n

Proof state:
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
h : ¬i✝ < n
⊢ ⟨i✝, ⋯⟩ = Fin.last n

Tactic:
exact Fin.eq_last_of_not_lt h

Result:
no goals

Proof state:
case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length),
    (finRange (n + 1))[i] = (map Fin.castSucc (finRange n) ++ [Fin.last n])[i]

Tactic:
intros

Result:
case h
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
⊢ (finRange (n + 1))[i✝] = (map Fin.castSucc (finRange n) ++ [Fin.last n])[i✝]

Proof state:
case h
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
⊢ ⟨i✝, ⋯⟩ = if h : i✝ < n then ⟨i✝, ⋯⟩ else Fin.last n

Tactic:
split

Result:
case h.isTrue
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
h✝ : i✝ < n
⊢ ⟨i✝, ⋯⟩ = ⟨i✝, ⋯⟩

case h.isFalse
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
h✝ : ¬i✝ < n
⊢ ⟨i✝, ⋯⟩ = Fin.last n

Proof state:
case hl
n : Nat
⊢ (finRange (n + 1)).length = (map Fin.castSucc (finRange n) ++ [Fin.last n]).length

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ finRange (n + 1) = map Fin.castSucc (finRange n) ++ [Fin.last n]

Tactic:
apply List.ext_getElem

Result:
case hl
n : Nat
⊢ (finRange (n + 1)).length = (map Fin.castSucc (finRange n) ++ [Fin.last n]).length

case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length),
    (finRange (n + 1))[i] = (map Fin.castSucc (finRange n) ++ [Fin.last n])[i]

Proof state:
case h.isFalse
n i✝ : Nat
h₁✝ : i✝ < (finRange (n + 1)).length
h₂✝ : i✝ < (map Fin.castSucc (finRange n) ++ [Fin.last n]).length
h✝ : ¬i✝ < n
⊢ ⟨i✝, ⋯⟩ = Fin.last n

Tactic:
next h => exact Fin.eq_last_of_not_lt h

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive sub_zsmul] lemma zpow_sub (a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bitwise_or : bitwise or = lor

Proof state:
case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x || !y)) m n = m &&& n

Tactic:
congr

Result:
case h.h.negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and

Proof state:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || y)) = (x && !y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x || y)) = fun a b => a && !b

Tactic:
funext x y

Result:
case h.h.negSucc.ofNat.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || y)) = (x && !y)

Proof state:
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x => !(x || !y)) = fun a b => a && !b

Tactic:
funext x y

Result:
case h.h.ofNat.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(y || !x)) = (x && !y)

Proof state:
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)

Tactic:
cases x <;> cases y <;> rfl

Result:
no goals

Proof state:
case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x || y)) m n = Nat.bitwise (fun a b => a && !b) m n

Tactic:
congr

Result:
case h.h.negSucc.ofNat.e_f
m n : ℕ
⊢ (fun x y => !(!x || y)) = fun a b => a && !b

Proof state:
case h.h.negSucc.negSucc.e_f
m n : ℕ
⊢ (fun x y => !(!x || !y)) = and

Tactic:
funext x y

Result:
case h.h.negSucc.negSucc.e_f.h.h
m n : ℕ
x y : Bool
⊢ (!(!x || !y)) = (x && y)

Proof state:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(x || !y)) m n = Nat.bitwise (fun a b => a && !b) n m

Tactic:
rw [Nat.bitwise_swap, Function.swap]

Result:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun y x => !(x || !y)) n m = Nat.bitwise (fun a b => a && !b) n m

Proof state:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun y x => !(x || !y)) n m = Nat.bitwise (fun a b => a && !b) n m

Tactic:
congr

Result:
case h.h.ofNat.negSucc.e_f
m n : ℕ
⊢ (fun y x => !(x || !y)) = fun a b => a && !b

Proof state:
⊢ bitwise or = lor

Tactic:
funext m n

Result:
case h.h
m n : ℤ
⊢ bitwise or m n = m.lor n

Proof state:
case h.h
m n : ℤ
⊢ bitwise or m n = m.lor n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
  <;> simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
    negSucc.injEq, Bool.true_or, Nat.land]

Result:
case h.h.ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(x || !y)) m n = Nat.bitwise (fun a b => a && !b) n m

case h.h.negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x || y)) m n = Nat.bitwise (fun a b => a && !b) m n

case h.h.negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y => !(!x || !y)) m n = m &&& n
-- Mathlib/Algebra/CharP/Defs.lean
lemma «exists» : ∃ p, CharP R p :=
  letI := Classical.decEq R
  by_cases
    (fun H : ∀ p : ℕ, (p : R) = 0 → p = 0 =>
      ⟨0, ⟨fun x => by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩⟩⟩)
    fun H =>
    ⟨Nat.find (not_forall.1 H),
      ⟨fun x =>
        ⟨fun H1 =>
          Nat.dvd_of_mod_eq_zero
            (by_contradiction fun H2 =>
              Nat.find_min (not_forall.1 H)
                (Nat.mod_lt x <|
                  Nat.pos_of_ne_zero <| not_of_not_imp <| Nat.find_spec (not_forall.1 H))
                (not_imp_of_and_not
                  ⟨by
                    rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                      Nat.cast_mul,
                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
                      zero_mul, add_zero] at H1,
                    H2⟩)),
          fun H1 => by
          rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]⟩⟩⟩

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find ⋯ ∣ x
⊢ ↑x = 0

Tactic:
rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
  zero_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x

Tactic:
rw [zero_dvd_iff]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ x = 0 → ↑x = 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
⊢ ↑0 = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ x = 0

Tactic:
exact ⟨H x, by rintro rfl; simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : ↑x = 0
H2 : ¬x % Nat.find ⋯ = 0
⊢ ↑(x % Nat.find ⋯) = 0

Tactic:
rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
  Nat.cast_mul,
  of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
  zero_mul, add_zero] at H1

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive] lemma prod_sdiff_le_prod_sdiff :
    ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
  ← prod_union, inter_comm, sdiff_union_inter]

Result:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : OrderedCancelCommMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa only [inter_comm] using disjoint_sdiff_inter t s

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem map_toPoly : (map φ P).toPoly = Polynomial.map φ P.toPoly

Proof state:
R : Type u_1
S : Type u_2
P : Cubic R
inst✝¹ : Semiring R
inst✝ : Semiring S
φ : R →+* S
⊢ (map φ P).toPoly = Polynomial.map φ P.toPoly

Tactic:
simp only [map, toPoly, map_C, map_X, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_pow]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem linearCombination_coord [CommRing R] [AddCommGroup M] [Module R M] [Finite ι]
    (b : Basis ι R M) (f : ι →₀ R) (i : ι) : Finsupp.linearCombination R b.coord f (b i) = f i

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i

Tactic:
rw [← coe_dualBasis, linearCombination_dualBasis]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i

Tactic:
haveI := Classical.decEq ι

Result:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ ((Finsupp.linearCombination R b.coord) f) (b i) = f i
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (image₂ f s t).image g = image₂ f' (t.image g₁) (s.image g₂)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ (fun a b => f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
exact image_image₂_distrib fun _ _ => h_antidistrib _ _

Result:
no goals

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ f s t) = image₂ f' (image g₁ t) (image g₂ s)

Tactic:
rw [image₂_swap f]

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝³ : DecidableEq α'
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ image g (image₂ (fun a b => f b a) t s) = image₂ f' (image g₁ t) (image g₂ s)
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem single_zero_mul_eq_smul [Semiring R] {r : R} {x : HahnSeries Γ R} :
    single 0 r * x = r • x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
⊢ (single 0) r * x = r • x

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
x✝ : Γ
⊢ ((single 0) r * x).coeff x✝ = (r • x).coeff x✝

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
x✝ : Γ
⊢ ((single 0) r * x).coeff x✝ = (r • x).coeff x✝

Tactic:
exact coeff_single_zero_mul

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} :
    (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1

Proof state:
n : ℕ
u v : Fin (n + 2)
⊢ u - v = 1 ∨ v - u = 1 → ¬u = v

Tactic:
intro _ _

Result:
n : ℕ
u v : Fin (n + 2)
a✝¹ : u - v = 1 ∨ v - u = 1
a✝ : u = v
⊢ False

Proof state:
n : ℕ
u v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1

Tactic:
simp only [cycleGraph, circulantGraph_adj, Set.mem_singleton_iff, and_iff_right_iff_imp]

Result:
n : ℕ
u v : Fin (n + 2)
⊢ u - v = 1 ∨ v - u = 1 → ¬u = v

Proof state:
n : ℕ
u v : Fin (n + 2)
a✝¹ : u - v = 1 ∨ v - u = 1
a✝ : u = v
⊢ False

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem exists_norm_eq_of_isOfFinAddOrder {u : AddCircle p} (hu : IsOfFinAddOrder u) :
    ∃ k : ℕ, ‖u‖ = p * (k / addOrderOf u)

Proof state:
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(m % n ⊓ (n - m % n)) / ↑n)

Tactic:
rw [← hm, norm_div_natCast]

Result:
no goals

Proof state:
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)

Tactic:
refine ⟨min (m % n) (n - m % n), ?_⟩

Result:
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(m % n ⊓ (n - m % n)) / ↑n)

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Tactic:
let n := addOrderOf u

Result:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)

Tactic:
obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu

Result:
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)

Proof state:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))

Tactic:
change ∃ k : ℕ, ‖u‖ = p * (k / n)

Result:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_infty_iff_deriv_of_isOpen (hs : IsOpen s₂) :
    ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ ∞ = ∞ + 1

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂

Tactic:
rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_deriv_of_isOpen hs]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (∞ + 1) (deriv f₂) s₂

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : IsOpen s₂
⊢ DifferentiableOn 𝕜 f₂ s₂ ∧ (∞ = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂ ↔
    DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (∞ + 1) (deriv f₂) s₂

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem mkArray_count_eq_of_count_eq_size {l : Array α} (h : count a l = l.size) :
    mkArray (count a l) a = l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : count a l = l.size
⊢ mkArray (count a l) a = l

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : count a { toList := toList✝ } = { toList := toList✝ }.size
⊢ mkArray (count a { toList := toList✝ }) a = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : count a { toList := toList✝ } = { toList := toList✝ }.size
⊢ (mkArray (count a { toList := toList✝ }) a).toList = { toList := toList✝ }.toList

Tactic:
simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : count a { toList := toList✝ } = { toList := toList✝ }.size
⊢ List.count ?m.21442 ?m.21443 = List.length ?m.21443

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : count a { toList := toList✝ } = { toList := toList✝ }.size
⊢ mkArray (count a { toList := toList✝ }) a = { toList := toList✝ }

Tactic:
rw [← toList_inj]

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
h : count a { toList := toList✝ } = { toList := toList✝ }.size
⊢ (mkArray (count a { toList := toList✝ }) a).toList = { toList := toList✝ }.toList
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Icc : (some : α → WithBot α) ⁻¹' Icc a b = Icc a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_add_single_eq_single_add_single [AddCommMonoid M] {k l m n : α} {u v : M}
    (hu : u ≠ 0) (hv : v ≠ 0) :
    single k u + single l v = single m u + single n v ↔
      (k = m ∧ l = n) ∨ (u = v ∧ k = n ∧ l = m) ∨ (u + v = 0 ∧ k = l ∧ m = n)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]

Result:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ single k u + single l v = single m u + single n v ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
classical
  simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
  exact Pi.single_add_single_eq_single_add_single hu hv

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
k l m n : α
u v : M
hu : u ≠ 0
hv : v ≠ 0
⊢ Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
exact Pi.single_add_single_eq_single_add_single hu hv

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_subgraphOfAdj {v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}

Tactic:
ext e

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ e ∈ {s(v, w)}

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ e ∈ (G.subgraphOfAdj hvw).edgeSet ↔ e ∈ {s(v, w)}

Tactic:
refine e.ind ?_

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ s(x, y) ∈ {s(v, w)}

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
e : Sym2 V
⊢ ∀ (x y : V), s(x, y) ∈ (G.subgraphOfAdj hvw).edgeSet ↔ s(x, y) ∈ {s(v, w)}

Tactic:
simp only [eq_comm, Set.mem_singleton_iff, Subgraph.mem_edgeSet, subgraphOfAdj_adj,
  forall₂_true_iff]

Result:
no goals