harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₀₂_iff' :
    (graph t).Adj (in₀ a) (in₂ c) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.1 = a ∧ x.2.2 = c where
  mp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (graph t).Adj (in₀ a) (in₂ c) → ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Tactic:
rintro ⟨⟩

Result:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?intro.mk.mk.intro.intro.b, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β

Tactic:
assumption

Result:
no goals

Proof state:
case in₀₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (∃ x ∈ t, x.1 = a ∧ x.2.2 = c) → (graph t).Adj (in₀ a) (in₂ c)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ (a, b✝, c).1 = a ∧ (a, b✝, c).2.2 = c

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ((a, b, c).1, ?intro.mk.mk.intro.intro.b, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.b
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ β
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma chainTop_neg : chainTop (-α) β = chainBot α β

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainTop (-α) β) x✝ = (chainBot α β) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainTop (-α) β = chainBot α β

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainTop (-α) β) x✝ = (chainBot α β) x✝
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y =
    bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1)

Proof state:
α : Type u_1
x : α
xs : List α
y : α
inst✝ : BEq α
⊢ indexesOf y (x :: xs) =
    bif x == y then 0 :: map (fun x => x + 1) (indexesOf y xs) else map (fun x => x + 1) (indexesOf y xs)

Tactic:
simp [indexesOf, findIdxs_cons]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem mem_of_promises {a} (p : s ~> a) : a ∈ s

Proof state:
case mk.intro
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s

Tactic:
rw [p h]

Result:
case mk.intro
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s

Proof state:
case mk.intro
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
⊢ a ∈ s

Tactic:
obtain ⟨h⟩ := h

Result:
case mk
α : Type u
s : Computation α
a : α
p : s ~> a
h : ∃ a, a ∈ s
⊢ a ∈ s

Proof state:
case mk
α : Type u
s : Computation α
a : α
p : s ~> a
h : ∃ a, a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨a', h⟩ := h

Result:
case mk.intro
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s
-- Mathlib/Data/Nat/ModEq.lean
theorem odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
  have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → m = 1 ∨ m = 3

Proof state:
n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 2 ∣ 4

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ 4 > 0

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_eq_empty_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = #[] ↔ l = #[]

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } H = #[] ↔ { toList := toList✝ } = #[]

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ pmap f { toList := toList✝ } H = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem map_equiv (b : Basis ι R M) (b' : Basis ι' R M') (e : ι ≃ ι') :
    b.map (b.equiv b' e) = b'.reindex e.symm

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ (b.map (b.equiv b' e)) i = (b'.reindex e.symm) i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ b.map (b.equiv b' e) = b'.reindex e.symm

Tactic:
ext i

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ (b.map (b.equiv b' e)) i = (b'.reindex e.symm) i
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem inj_right {w : σ → M} (hφ : φ ≠ 0) (hm : IsWeightedHomogeneous w φ m)
    (hn : IsWeightedHomogeneous w φ n) : m = n

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
⊢ m = n

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ

Result:
case intro
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_compl_self :
    ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
⊢ ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [compl_eq_univ_diff, contDiffWithinAt_diff_singleton, contDiffWithinAt_univ]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem mem_eval {σ} {f : σ → Option σ} {a b} : b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Proof state:
case refine_1
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases e : f a with - | a'

Result:
case refine_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

case refine_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma Even.pow_abs (hn : Even n) (a : α) : |a| ^ n = a ^ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
exact hn.pow_nonneg _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ |a| ^ n = a ^ n

Tactic:
rw [← abs_pow, abs_eq_self]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
hn : Even n
a : α
⊢ 0 ≤ a ^ n
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_neg {R : Type u} [Ring R] {a} : (⟨-a⟩ : R[X]) = -⟨a⟩ :=
  show _ = neg _ by rw [neg_def]

Proof state:
R : Type u
inst✝ : Ring R
a : R[ℕ]
⊢ { toFinsupp := -a } = Polynomial.neg { toFinsupp := a }

Tactic:
rw [neg_def]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [Ring R]
    [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
    minpoly K x ∣ (minpoly A x).map (algebraMap A K)

Proof state:
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ minpoly K x ∣ map (algebraMap A K) (minpoly A x)

Tactic:
refine minpoly.dvd K x ?_

Result:
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ (Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0

Proof state:
A : Type u_3
K : Type u_4
R : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : Field K
inst✝⁴ : Ring R
inst✝³ : Algebra A K
inst✝² : Algebra A R
inst✝¹ : Algebra K R
inst✝ : IsScalarTower A K R
x : R
⊢ (Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0

Tactic:
rw [aeval_map_algebraMap, minpoly.aeval]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_comp_const_mul {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiff 𝕜 n f) (c : 𝕜) :
    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
f : 𝕜 → 𝕜
h : ContDiff 𝕜 (↑n) f
c : 𝕜
⊢ (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)

Tactic:
simpa only [smul_eq_mul] using iteratedDeriv_comp_const_smul h c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as

Proof state:
α : Type u
as : List α
acc : Array α
⊢ (as.toArrayAux acc).toList = acc.toList ++ as

Tactic:
induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_mul_eq_zero_of_right (p : R[X]) (hq : q.eval₂ f x = 0) : (p * q).eval₂ f x = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x (p * q) = 0

Tactic:
rw [eval₂_mul f x]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0

Tactic:
exact mul_eq_zero_of_right (p.eval₂ f x) hq

Result:
no goals
-- Mathlib/Tactic/Simproc/ExistsAndEq.lean
theorem exists_of_imp_eq {α : Sort u} {p : α → Prop} (a : α) (h : ∀ b, p b → a = b) :
    (∃ b, p b) = p a

Proof state:
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ (∃ b, p b) = p a

Tactic:
apply propext

Result:
case a
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ (∃ b, p b) ↔ p a

Proof state:
case a
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ (∃ b, p b) ↔ p a

Tactic:
constructor

Result:
case a.mp
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ (∃ b, p b) → p a

case a.mpr
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ p a → ∃ b, p b

Proof state:
case a.mpr
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ p a → ∃ b, p b

Tactic:
intro h'

Result:
case a.mpr
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
h' : p a
⊢ ∃ b, p b

Proof state:
case a.mp
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
⊢ (∃ b, p b) → p a

Tactic:
intro h'

Result:
case a.mp
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
h' : ∃ b, p b
⊢ p a

Proof state:
case a.mp
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
h' : ∃ b, p b
⊢ p a

Tactic:
obtain ⟨b, hb⟩ := h'

Result:
case a.mp.intro
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
b : α
hb : p b
⊢ p a

Proof state:
case a.mpr
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
h' : p a
⊢ ∃ b, p b

Tactic:
exact ⟨a, h'⟩

Result:
no goals

Proof state:
case a.mp.intro
α : Sort u
p : α → Prop
a : α
h : ∀ (b : α), p b → a = b
b : α
hb : p b
⊢ p a

Tactic:
rwa [h b hb]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma tangentBundleCore.isContMDiff [h : IsManifold I (n + 1) M] :
    haveI : IsManifold I 1 M := .of_le (n := n + 1) le_add_self
    (tangentBundleCore I M).IsContMDiff I n

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContMDiffOn I 𝓘(𝕜, E →L[𝕜] E) n ((tangentBundleCore I M).coordChange i j)
    ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j)

Tactic:
rw [contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2),
  contMDiffOn_iff_contDiffOn]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ ContDiffOn 𝕜 n ((tangentBundleCore I M).coordChange i j ∘ ↑((↑i).extend I).symm)
    (↑((↑i).extend I) '' ((tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j))

𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_4
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
h : IsManifold I (n + 1) M
this : IsManifold I n M
i j : ↑(atlas H M)
⊢ (tangentBundleCore I M).baseSet i ∩ (tangentBundleCore I M).baseSet j ⊆ (↑i).source
-- Mathlib/Data/List/Rotate.lean
theorem Nodup.cyclicPermutations {l : List α} (hn : Nodup l) :
    Nodup (cyclicPermutations l)

Proof state:
α : Type u
l : List α
hn : l.Nodup
⊢ l.cyclicPermutations.Nodup

Tactic:
rcases eq_or_ne l [] with rfl | hl

Result:
case inl
α : Type u
hn : [].Nodup
⊢ [].cyclicPermutations.Nodup

case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup

Proof state:
case inr.mk.mk
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi⟩ = l.cyclicPermutations.get ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
simp only [length_cyclicPermutations_of_ne_nil l hl] at hi hj

Result:
case inr.mk.mk
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩

Proof state:
case inl
α : Type u
hn : [].Nodup
⊢ [].cyclicPermutations.Nodup

Tactic:
simp

Result:
no goals

Proof state:
case inr.mk.mk
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi✝ : i < l.cyclicPermutations.length
j : ℕ
hj✝ : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi✝⟩ = l.cyclicPermutations.get ⟨j, hj✝⟩
hi : i < l.length
hj : j < l.length
⊢ ⟨i, hi✝⟩ = ⟨j, hj✝⟩

Tactic:
simpa [hn.rotate_congr_iff, mod_eq_of_lt, *] using h

Result:
no goals

Proof state:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ Injective l.cyclicPermutations.get

Tactic:
rintro ⟨i, hi⟩ ⟨j, hj⟩ h

Result:
case inr.mk.mk
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
i : ℕ
hi : i < l.cyclicPermutations.length
j : ℕ
hj : j < l.cyclicPermutations.length
h : l.cyclicPermutations.get ⟨i, hi⟩ = l.cyclicPermutations.get ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Proof state:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ l.cyclicPermutations.Nodup

Tactic:
rw [nodup_iff_injective_get]

Result:
case inr
α : Type u
l : List α
hn : l.Nodup
hl : l ≠ []
⊢ Injective l.cyclicPermutations.get
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem iterate_injective (h : Injective f') : ∀ n : ℕ, Injective (f' ^ n)
  | 0 => injective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_injective h n).comp h

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑((f' ^ n) ∘ₗ f')

Tactic:
exact (iterate_injective h n).comp h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑((f' ^ n) ∘ₗ f')
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/ExceptCps.lean
theorem runCatch_lift {α : Type u} [Monad m] [LawfulMonad m] (x : m α) : runCatch (ExceptCpsT.lift x : ExceptCpsT α m α) = x

Proof state:
m : Type u → Type u_1
α : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ (lift x).runCatch = x

Tactic:
simp [runCatch, lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_lt_sub_right : ∀ {a b c : Nat}, c ≤ a → a < b → a - c < b - c
  | 0, _, _, hle, h => by
    rw [Nat.eq_zero_of_le_zero hle, Nat.sub_zero, Nat.sub_zero]
    exact h
  | _, _, 0, _, h => by
    rw [Nat.sub_zero, Nat.sub_zero]
    exact h
  | _+1, _+1, _+1, hle, h => by
    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
    exact Nat.sub_lt_sub_right (le_of_succ_le_succ hle) (lt_of_succ_lt_succ h)

Proof state:
x✝² x✝¹ : Nat
x✝ : 0 ≤ x✝²
h : x✝² < x✝¹
⊢ x✝² < x✝¹

Tactic:
exact h

Result:
no goals

Proof state:
x✝² x✝¹ : Nat
x✝ : 0 ≤ x✝²
h : x✝² < x✝¹
⊢ x✝² - 0 < x✝¹ - 0

Tactic:
rw [Nat.sub_zero, Nat.sub_zero]

Result:
x✝² x✝¹ : Nat
x✝ : 0 ≤ x✝²
h : x✝² < x✝¹
⊢ x✝² < x✝¹

Proof state:
x✝¹ x✝ : Nat
hle : x✝ ≤ 0
h : 0 < x✝¹
⊢ 0 - x✝ < x✝¹ - x✝

Tactic:
rw [Nat.eq_zero_of_le_zero hle, Nat.sub_zero, Nat.sub_zero]

Result:
x✝¹ x✝ : Nat
hle : x✝ ≤ 0
h : 0 < x✝¹
⊢ 0 < x✝¹

Proof state:
n✝² n✝¹ n✝ : Nat
hle : n✝ + 1 ≤ n✝² + 1
h : n✝² + 1 < n✝¹ + 1
⊢ n✝² - n✝ < n✝¹ - n✝

Tactic:
exact Nat.sub_lt_sub_right (le_of_succ_le_succ hle) (lt_of_succ_lt_succ h)

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
hle : x✝ ≤ 0
h : 0 < x✝¹
⊢ 0 < x✝¹

Tactic:
exact h

Result:
no goals

Proof state:
n✝² n✝¹ n✝ : Nat
hle : n✝ + 1 ≤ n✝² + 1
h : n✝² + 1 < n✝¹ + 1
⊢ n✝² + 1 - (n✝ + 1) < n✝¹ + 1 - (n✝ + 1)

Tactic:
rw [Nat.add_sub_add_right, Nat.add_sub_add_right]

Result:
n✝² n✝¹ n✝ : Nat
hle : n✝ + 1 ≤ n✝² + 1
h : n✝² + 1 < n✝¹ + 1
⊢ n✝² - n✝ < n✝¹ - n✝