mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₁ : J.fst b = J.snd b
f : (left (J.snd b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = ?m.571 (J.snd b) ⋯ h₁

Tactic:
simp only [eqToHom_refl, Category.id_comp, f]

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₁ : J.fst b = J.snd b
f : (left (J.snd b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False = ?m.571 (J.snd b) ⋯ h₁
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).left = x✝.left

Tactic:
by simp [Shrink.equivalence]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).right = x✝.right

Tactic:
by simp [Shrink.equivalence]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow C
⊢ ((Shrink.equivalence C).inverse.mapArrow.obj ((Shrink.equivalence C).functor.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
by simp [Shrink.equivalence]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
this : ∀ (R : CommRingCat), Q R → ∀ (φ : R ⟶ S), (Hom.hom φ).FiniteType → Q' R → (ObjectProperty.ofObj f).isoClosure S
hR' : ¬Q' R
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR
    exact this R' (hQ'Q _ hR') (e.inv ≫ φ)
      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ((piRight R S N M).symm fun i ↦ x ⊗ₜ[R] m i) = x ⊗ₜ[R] m

Tactic:
by
  simp [piRight]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
⊢ (piRight R S N M).symm (Pi.single i (x ⊗ₜ[R] m)) = x ⊗ₜ[R] Pi.single i m

Tactic:
by
  simp [piRight]

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
y : K₂
⊢ g₁ 0 = i₂ (ι₂ y)

Tactic:
rw [map_zero, hι₂.apply_apply_eq_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ ∀ (j : WalkingCospan),
    Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app j =
      (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app j

Tactic:
rintro (_ | _ | _) <;> simp [← Over.comp_left_assoc, ← Over.comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                  map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                  map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
            X).pt.hom ≫
      (Iso.refl
          (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                      map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                    { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                      map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                X).pt.right).hom =
    ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).pt.hom

Tactic:
by dsimp; simpa using X.inl.w

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
r : S
x : M
⊢ { toFun := fun a ↦ ⟨(r • x) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) r • { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext y; simp [smul_tmul']

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case intro.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
p : ℕ
hp : CharP (R ⧸ I) (p + 1)
h_mixed : MixedCharZero R p.succ
⊢ CharP (R ⧸ I) 0

Tactic:
exact absurd h_mixed (h p.succ p.succ_pos)

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
h : (some a :: ↑s) 0 = none
⊢ (some a :: ↑s) (0 + 1) = none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : (fun a' ↦ (a', s.tail)) <$> some val✝ = none
⊢ s = nil

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = some (a, s')
⊢ s = cons a s'

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
a : α
b' : β
h₁ : f b = some (a, b')
h :
  (match some (a, b') with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some (a, b') with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h : Stream'.cons none c.val 0 = some a
⊢ Stream'.cons none c.val (0 + 1) = some a

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Stream' α
n : ℕ
h : map some s n = none
⊢ map some s (n + 1) = none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
a✝ : Option.map f (some e✝) = none
⊢ Option.map f (s (n + 1)) = none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
s : Computation α
a : α
h : some a = s.think.val.get 0
⊢ a ∈ s

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
x✝ : a ∈ empty α
n : ℕ
h : (fun b ↦ some a = b) ((empty α).val.get n)
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)

Tactic:
apply List.ext_getElem <;> simp

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length

Tactic:
have : (Option.isSome ((think s).val (length (think s))) : Prop) :=
      Nat.find_spec ((terminates_def _).1 s.think_terminates)
    revert this; rcases length (think s) with - | n <;> intro this
    · simp [think, Stream'.cons] at this
    · apply Nat.succ_le_succ
      apply Nat.find_min'
      apply this

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
⊢ take n (drop m a) = List.drop m (take (m + n) a)

Tactic:
apply List.ext_getElem <;> simp

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.think.intro
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
n : ℕ
left✝ : s.Results a n
right✝ : 0 = n + 1
⊢ s.think = (pure a).thinkN 0

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.pure
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
a' : α
h : (pure a').Results a (n + 1)
this : n + 1 = 0
⊢ pure a' = (pure a).thinkN (n + 1)

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
e : s n = none
h : Option.rec none (fun val ↦ some (f val)) none = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : m ≤ k
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
· obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk
    have hm' : m = (x.drop n).length := by simp [hm]
    simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
this : (s'.think.bind f).head = ((pure b).thinkN 0).head
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
contradiction

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
this : Ideal.span ?m.44 ≤ Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    Ideal.span
      {a |
        (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
          (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
            (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
              ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x = 0

Tactic:
exact (mem_bot P).1 (this hx)

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

pp: case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
· rw [hnone] at ih
      rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
        succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]

Goal state after:
case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) (IntFractPair.of v).fr

Tactic:
suffices v = ⌊v⌋ by
        simpa [compExactValue, IntFractPair.of, fract_eq_zero]

Goal state after:
case zero.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = ↑⌊v⌋
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: f : ℕ → ℕ
hf : IsStrongDvdSequence f
⊢ IsDvdSequence f

Tactic:
by
  intro a b hab
  simpa [gcd_eq_left hab, gcd_eq_left_iff_dvd] using hf a b

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: ⊢ StrictMono fun n ↦ fib (n + 2)

Tactic:
refine strictMono_nat_of_lt_succ fun n => ?_
  rw [add_right_comm]
  exact fib_lt_fib_succ (self_le_add_left _ _)

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd tl_hd : α
tl_tl : Seq α
h : Pairwise R (cons hd (cons tl_hd tl_tl))
⊢ R hd tl_hd

Tactic:
by
  simp only [Pairwise] at h
  simpa using h 0 1 Nat.one_pos

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ 1

Tactic:
change (0 : Ring.DirectLimit G (f' · · ·)) ≠ 1
        rw [← (Ring.DirectLimit.of _ _ _).map_one]
        · intro H; rcases Ring.DirectLimit.of.zero_exact H.symm with ⟨j, hij, hf⟩
          rw [(f' i j hij).map_one] at hf
          exact one_ne_zero hf

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
nth_stream_eq_none : IntFractPair.stream v 0 = none
⊢ v = (of v).convs (0 - 1)

Tactic:
contradiction

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ.inl.zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
IH : IntFractPair.stream v 0 = none → v = (of v).convs (0 - 1)
nth_stream_eq_none✝ : IntFractPair.stream v (0 + 1) = none
nth_stream_eq_none : IntFractPair.stream v 0 = none
⊢ v = g.convs 0

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
hb' : b.TerminatedAt (a.length ha)
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos.nil
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
this : motive (a.drop (a.length ha)) nil
hb_cons : nil ≠ nil
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.c = Q.c

Tactic:
by rw [← coeff_eq_c, h, coeff_eq_c]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)

Tactic:
DFinsupp.sumAddHom_apply

Goal state after:
ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h h' : (i : ι) → β i →+ M
f g : Π₀ (i : ι), β i
H : ∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))
⊢ c (f.sum fun x ↦ ⇑(h x)) (g.sum fun x ↦ ⇑(h' x))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k = ⨆ l, (f.genEigenspace μ) ↑↑l

Tactic:
genEigenspace_nat,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
⊢ (f.genEigenspace μ) k = ⨆ l, ((f - μ • 1) ^ ↑l).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) ↑1 = (f - μ • 1).ker

Tactic:
genEigenspace_nat,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ ((f - μ • 1) ^ 1).ker = (f - μ • 1).ker
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : ∏ i, e i = 0
⊢ ∏ i, (1 - (1 - e i)) = 0

Tactic:
simpa using he₂

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
le : matrix n I ≤ matrix n J
x : R
xI : x ∈ I
⊢ x ∈ J

Tactic:
specialize @le (of fun _ _ => x) (by simp [xI])

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
x : R
le : (of fun x_1 x_2 ↦ x) ∈ matrix n J
xI : x ∈ I
⊢ x ∈ J
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ (f.genEigenspace μ) ↑n ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
genEigenspace_nat,

Goal state after:
case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f - μ • 1) ^ n).ker ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ (((f - μ • 1) ^ k).restrict ⋯) ⟨x, hx✝⟩ = 0

Tactic:
LinearMap.restrict_apply

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
⊢ ∀ {a b : R},
    a ∈ (Subsemigroup.corner e).carrier → b ∈ (Subsemigroup.corner e).carrier → a + b ∈ (Subsemigroup.corner e).carrier

Tactic:
by rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by simp_rw [mul_add, add_mul]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : μ₁ = μ₂
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False

Tactic:
contradiction

Goal state after: