harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc]
lemma mappingConeCompHomotopyEquiv_comm₂ :
    (mappingConeCompHomotopyEquiv f g).hom ≫
      (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
      (mappingConeCompTriangle f g).mor₃

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
    (mappingConeCompTriangle f g).mor₃

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ ((mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
    (mappingConeCompTriangle f g).mor₃.f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ ((mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃).f n =
    (mappingConeCompTriangle f g).mor₃.f n

Tactic:
simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.hom,
  lift_f _ _ _ _ _ (n+1) rfl, ext_from_iff _ (n+1) _ rfl]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem expand_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    expand p (bind₁ f φ) = bind₁ (fun i ↦ expand p (f i)) φ

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (expand p) ((bind₁ f) φ) = (bind₁ fun i => (expand p) (f i)) φ

Tactic:
rw [← AlgHom.comp_apply, expand_comp_bind₁]

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem pow_le_kstar : ∀ {n : ℕ}, a ^ n ≤ a∗
  | 0 => (pow_zero _).trans_le one_le_kstar
  | n + 1 => by
    rw [pow_succ']
    exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
n : ℕ
⊢ a ^ (n + 1) ≤ a∗

Tactic:
rw [pow_succ']

Result:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
n : ℕ
⊢ a * a ^ n ≤ a∗

Proof state:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
n : ℕ
⊢ a * a ^ n ≤ a∗

Tactic:
exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem nonempty_mk {m : Multiset α} {hm} : (⟨m, hm⟩ : Finset α).Nonempty ↔ m ≠ 0

Proof state:
α : Type u_1
m : Multiset α
hm : m.Nodup
⊢ { val := m, nodup := hm }.Nonempty ↔ m ≠ 0

Tactic:
induction m using Multiset.induction_on <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem Group.covariant_iff_contravariant [Group N] :
    Covariant N N (· * ·) r ↔ Contravariant N N (· * ·) r

Proof state:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Tactic:
exact h a⁻¹ bc

Result:
no goals

Proof state:
N : Type u_2
r : N → N → Prop
inst✝ : Group N
⊢ Covariant N N (fun x1 x2 => x1 * x2) r ↔ Contravariant N N (fun x1 x2 => x1 * x2) r

Tactic:
refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩

Result:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)
⊢ r b c

case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)

Proof state:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r b c
⊢ r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc

Result:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)

Proof state:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)
⊢ r b c

Tactic:
rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]

Result:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)
⊢ r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))

Proof state:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (fun x1 x2 => x1 * x2) r
a b c : N
bc : r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
⊢ r ((fun x1 x2 => x1 * x2) a b) ((fun x1 x2 => x1 * x2) a c)

Tactic:
exact h a⁻¹ bc

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma π_comp_colimitLeftOpIsoUnopLimit_inv (F : J ⥤ Cᵒᵖ) [HasLimit F] (j : J) :
    (limit.π F j).unop ≫ (colimitLeftOpIsoUnopLimit F).inv = colimit.ι F.leftOp (op j)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : J
⊢ (limit.π F j).unop ≫ (colimitLeftOpIsoUnopLimit F).inv = colimit.ι F.leftOp (op j)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem mul_polyOfInterest_aux5 (n : ℕ) :
    (p : 𝕄) ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
ring

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
rw [mul_polyOfInterest_aux4 p n]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Tactic:
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPushout.inr_iso_inv :
    G.map (pushout.inr _ _) ≫ (PreservesPushout.iso G f g).inv = pushout.inr _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map (pushout.inr f g) ≫ (iso G f g).inv = pushout.inr (G.map f) (G.map g)

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem of_nsmul : a ≡ b [PMOD n • p] → a ≡ b [PMOD p] := fun ⟨m, hm⟩ =>
  ⟨m * n, by rwa [mul_smul, natCast_zsmul]⟩

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
n : ℕ
x✝ : a ≡ b [PMOD n • p]
m : ℤ
hm : b - a = m • n • p
⊢ b - a = (m * ↑n) • p

Tactic:
rwa [mul_smul, natCast_zsmul]

Result:
no goals
-- Mathlib/CategoryTheory/EpiMono.lean
theorem IsIso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : SplitEpi f) [Epi <| hf.section_] :
    IsIso f :=
  ⟨⟨hf.section_, ⟨(cancel_epi_id <| hf.section_).mp (by simp), by simp⟩⟩⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive] lemma prod_eq_one_iff : m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
  Quotient.inductionOn m fun l ↦ by simpa using List.prod_eq_one_iff

Proof state:
α : Type u_2
inst✝¹ : OrderedCommMonoid α
inst✝ : CanonicallyOrderedMul α
m : Multiset α
l : List α
⊢ prod ⟦l⟧ = 1 ↔ ∀ x ∈ ⟦l⟧, x = 1

Tactic:
simpa using List.prod_eq_one_iff

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem mem_adjoin_support (f : R[M]) : f ∈ adjoin R (of' R M '' f.support)

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
⊢ of' R M '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))

Tactic:
exact subset_adjoin

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
this : span R (of' R M '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
⊢ f ∈ adjoin R (of' R M '' ↑f.support)

Tactic:
exact this (mem_span_support f)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
⊢ span R (of' R M '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))

Tactic:
rw [Submodule.span_le]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
⊢ of' R M '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
⊢ f ∈ adjoin R (of' R M '' ↑f.support)

Tactic:
suffices span R (of' R M '' f.support) ≤
    Subalgebra.toSubmodule (adjoin R (of' R M '' f.support)) by
  exact this (mem_span_support f)

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
f : R[M]
⊢ span R (of' R M '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_eq_map {f : α → σ → σ × β} {s₀ : σ} (S : Set σ) (h₀ : s₀ ∈ S)
    (closure : ∀ a s, s ∈ S → (f a s).1 ∈ S)
    (out : ∀ a s s', s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) :
    (mapAccumr f xs s₀).snd = map (f · s₀ |>.snd) xs

Proof state:
case h
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∃ R, R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2

Tactic:
use fun s _ => s ∈ S, h₀

Result:
case right
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2

Proof state:
case right
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2

Tactic:
exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = (mapAccumr (fun x x_1 => ((), (f x s₀).2)) xs ()).2

Tactic:
apply mapAccumr_bisim_tail

Result:
case h
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ ∃ R, R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = map (fun x => (f x s₀).2) xs

Tactic:
rw [Vector.map_eq_mapAccumr]

Result:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s₀ : σ
S : Set σ
h₀ : s₀ ∈ S
closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S
out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2
⊢ (mapAccumr f xs s₀).2 = (mapAccumr (fun x x_1 => ((), (f x s₀).2)) xs ()).2
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_nodup_of_support_nodup {u v : V} {p : G.Walk u v} (h : p.support.Nodup) :
    p.darts.Nodup

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : u✝ ∉ p'.support ∧ p'.support.Nodup
⊢ { toProd := (u✝, v✝), adj := h✝ } ∉ p'.darts ∧ p'.darts.Nodup

Tactic:
exact ⟨fun h' => h.1 (dart_fst_mem_support_of_mem_darts p' h'), ih h.2⟩

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : (cons h✝ p').support.Nodup
⊢ (cons h✝ p').darts.Nodup

Tactic:
simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢

Result:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : p'.support.Nodup → p'.darts.Nodup
h : u✝ ∉ p'.support ∧ p'.support.Nodup
⊢ { toProd := (u✝, v✝), adj := h✝ } ∉ p'.darts ∧ p'.darts.Nodup

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
h : nil.support.Nodup
⊢ nil.darts.Nodup

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.darts.Nodup

Tactic:
induction p with
| nil => simp
| cons _ p' ih =>
  simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
  exact ⟨fun h' => h.1 (dart_fst_mem_support_of_mem_darts p' h'), ih h.2⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi {θ ψ : Angle}
    (h : (2 : ℕ) • θ + (2 : ℕ) • ψ = π) : tan ψ = (tan θ)⁻¹

Proof state:
case h
ψ : Angle
x✝ : ℝ
h : 2 • ↑x✝ + 2 • ψ = ↑π
⊢ ψ.tan = (↑x✝).tan⁻¹

Tactic:
induction ψ using Real.Angle.induction_on

Result:
case h.h
x✝¹ x✝ : ℝ
h : 2 • ↑x✝¹ + 2 • ↑x✝ = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Proof state:
θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
ψ : Angle
x✝ : ℝ
h : 2 • ↑x✝ + 2 • ψ = ↑π
⊢ ψ.tan = (↑x✝).tan⁻¹

Proof state:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)

Tactic:
exact Real.tan_periodic.int_mul _ _

Result:
no goals

Proof state:
case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
rcases h with ⟨k, h⟩

Result:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Proof state:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
rw [tan_coe, tan_coe, ← tan_pi_div_two_sub, h, add_sub_assoc, add_comm]

Result:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ Real.tan (π / 2 - x✝¹ + ↑k * π) = Real.tan (π / 2 - x✝¹)

Proof state:
case h.h
x✝¹ x✝ : ℝ
h : 2 • ↑x✝¹ + 2 • ↑x✝ = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h

Result:
case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Proof state:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add,
  mul_right_inj' (two_ne_zero' ℝ), ← eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π,
  inv_mul_eq_div, mul_comm] at h

Result:
case h.h.intro
x✝¹ x✝ : ℝ
k : ℤ
h : x✝ = ↑k * π + π / 2 - x✝¹
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
-- Mathlib/ModelTheory/Complexity.lean
lemma Theory.IsUniversal.insert
    {T : L.Theory} [hT : T.IsUniversal] {φ : L.Sentence} (hφ : φ.IsUniversal) :
    (insert φ T).IsUniversal := ⟨by
  simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]
  exact hT.isUniversal_of_mem⟩

Proof state:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ a ∈ T, BoundedFormula.IsUniversal a

Tactic:
exact hT.isUniversal_of_mem

Result:
no goals

Proof state:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ ⦃φ_1 : L.Sentence⦄, φ_1 ∈ Insert.insert φ T → BoundedFormula.IsUniversal φ_1

Tactic:
simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]

Result:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ a ∈ T, BoundedFormula.IsUniversal a
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_mul (m : ℕ) : ∀ n, f^[m * n] = f^[m]^[n]
  | 0 => by simp only [Nat.mul_zero, iterate_zero]
  | n + 1 => by simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]

Proof state:
α : Type u
f : α → α
m : ℕ
⊢ f^[m * 0] = f^[m]^[0]

Tactic:
simp only [Nat.mul_zero, iterate_zero]

Result:
no goals

Proof state:
α : Type u
f : α → α
m n : ℕ
⊢ f^[m * (n + 1)] = f^[m]^[n + 1]

Tactic:
simp only [Nat.mul_succ, Nat.mul_one, iterate_one, iterate_add, iterate_mul m n]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem comap_eq {f : γ → β} :
    𝒰(α, γ, ‹UniformSpace β›.comap f) = 𝒰(α, β, _).comap (f ∘ ·)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
⊢ uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)

Tactic:
exact (UniformFun.postcomp_isUniformInducing (f := f) ⟨rfl⟩).comap_uniformSpace.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → β
⊢ uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)

Tactic:
letI : UniformSpace γ := .comap f ‹_›

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
⊢ uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l

Proof state:
α : Type u_1
a : α
l : List α
⊢ (a :: l).Nodup ↔ ¬a ∈ l ∧ l.Nodup

Tactic:
simp only [Nodup, pairwise_cons, forall_mem_ne]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Defs.lean
theorem eq_comp_toLinearMap_iff (f g : M₂ →ₛₗ[σ₂₃] M₃) :
    f.comp e₁₂.toLinearMap = g.comp e₁₂.toLinearMap ↔ f = g

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ₂₁ : R₂ →+* R₁
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f.comp ↑e₁₂ = g.comp ↑e₁₂
⊢ f = g

Tactic:
rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]

Result:
no goals

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ₂₁ : R₂ →+* R₁
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
⊢ f.comp ↑e₁₂ = g.comp ↑e₁₂ ↔ f = g

Tactic:
refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩

Result:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_7
M₂ : Type u_8
M₃ : Type u_9
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ₂₁ : R₂ →+* R₁
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f g : M₂ →ₛₗ[σ₂₃] M₃
h : f.comp ↑e₁₂ = g.comp ↑e₁₂
⊢ f = g
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem factorial_mul_ascPochhammer (S : Type*) [Semiring S] (r n : ℕ) :
    (r ! : S) * (ascPochhammer S n).eval (r + 1 : S) = (r + n)!

Proof state:
S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (ascPochhammer S n) = ↑(r + n)!

Tactic:
rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem length_le : c.length ≤ n

Proof state:
n : ℕ
c : Composition n
⊢ c.length ≤ n

Tactic:
conv_rhs => rw [← c.blocks_sum]

Result:
n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum

Proof state:
n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum

Tactic:
exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : range (a • f) = range f

Proof state:
K : Type u_4
V : Type u_8
V₂ : Type u_9
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
a : K
h : a ≠ 0
⊢ range (a • f) = range f

Tactic:
simpa only [range_eq_map] using Submodule.map_smul f _ a h

Result:
no goals