mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then ⟨a, ⋯⟩
      else
        if hm : m = 0 then ⟨b, ⋯⟩
        else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) <
    n.lcm m

Tactic:
dif_neg hn,

Goal state after:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hm : m = 0 then ⟨b, ⋯⟩
      else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) <
    n.lcm m
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case pos
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Sum.inl ⟨iv, him⟩, j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
simpa using! ih _

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * n - m + m - 1

Tactic:
Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)

Goal state after:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * n - 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Fintype.card (ZMod (n✝ + 1)) = n✝ + 1

Tactic:
ZMod.card

Goal state after:
case succ
n✝ : ℕ
⊢ n✝ + 1 = n✝ + 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α → β) = card β ^ card α

Tactic:
by
  classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · let := Fintype.ofFinite α
      let := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      rw [top_epow]
      rwa [card_ne_zero_iff_nonempty]
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [Order.lt_one_iff, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · let := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · let := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
· refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩
    simp [heq]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t).encard + t.encard + (s ∩ t).encard = s.encard + t.encard

Tactic:
add_right_comm,

Goal state after:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + (s ∩ t).encard + t.encard = s.encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ ({x} ∩ s).encard ≤ 1

Tactic:
by
  grw [← encard_singleton x, inter_subset_left]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
h : ∀ (i : ι) (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0
⊢ g i = 0

Tactic:
apply h _ _ hit

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0

pp: case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0

Tactic:
· have := card_eq_zero_iff.mp h
    have := Function.isEmpty f
    exact Nat.card_of_isEmpty

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
    cases h
    rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
    exact Cardinal.mk_union_le s t

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ⋯.toFinset.card = s.card

Tactic:
Finset.finite_toSet_toFinset

Goal state after:
α : Type u_1
s : Finset α
⊢ s.card = s.card
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = i.removeNth (Pi.mulSingle i x)

Tactic:
by unfold removeNth; simp [succAbove_ne, Pi.one_def]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)

Tactic:
by ext i; refine i.cases ?_ ?_ <;> simp

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_and_left]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
φ : ((i : ι) → A i) →* (i : ι) → A i ⧸ (powMonoidHom n).range :=
  { toFun := fun x x_1 ↦ ↑(x x_1), map_one' := ⋯, map_mul' := ⋯ }
⊢ (powMonoidHom n).range = φ.ker

Tactic:
by
    ext x : 1
    simpa [φ, funext_iff] using (Classical.skolem (p := fun i a ↦ a ^ n = x i)).symm

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
e₂ : I →* H
he₂ : mrange (MulEquiv.prodComm.toMonoidHom.comp f) = e₂.mgraph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
rw [he₁₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
⊢ ∀ (m : R) (x : M ⧸ p),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (m • x) = (RingHom.id R) m • (Quotient.congr (Equiv.refl M) ⋯).toFun x

Tactic:
by
      rintro x ⟨y⟩
      rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s ∪ ⇑(inr R M M₂) '' t) = (span R s).prod (span R t)

Tactic:
by
  rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa [pred_eq_sub_one] using insert_Ioc_left_eq_Ioc_pred h

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ p (x ⊔ y) = max (p x) (p y)

Tactic:
rw [hp]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ (p x ∧ p y) = max (p x) (p y)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
rw [he₁₂]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: S : Type u_4
H : Type u_6
I : Type u_7
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
G : Submodule S (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = (↑e).graph

Tactic:
simpa only [range_subtype] using LinearMap.exists_linearEquiv_eq_graph
    hG₁.surjective hG₂.surjective fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
rw [pred_succ_iterate_of_not_isMax]

Goal state after:
case succ.hin
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ ¬IsMax (succ^[n + 1 - 1] i)
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d ≤ a + d + c
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a

Tactic:
add_right_comm,

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d ≤ a + c + d
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ici a
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d < a + d + c
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ioi a

Tactic:
add_right_comm,

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d < a + c + d
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ioi a
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
⊢ toZ i0 (succ^[n] i0) = ↑n

Tactic:
let m := (toZ i0 (succ^[n] i0)).toNat

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
⊢ toZ i0 (succ^[n] i0) = ↑n
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ disjointed ⇑(partialSups f) = disjointed f

Tactic:
by
  classical
  ext i
  have step1 : f i \ (Iio i).sup f = partialSups f i \ (Iio i).sup f := by
    rw [sdiff_eq_symm (sdiff_le.trans (le_partialSups f i))]
    simp only [funext (partialSups_apply f), sup'_eq_sup]
    rw [sdiff_sdiff_eq_sdiff_sup (sup_mono Iio_subset_Iic_self), sup_eq_right]
    simp only [Iic_eq_cons_Iio, sup_cons, sup_sdiff_left_self, sdiff_le_iff, le_sup_right]
  simp only [disjointed_apply, step1, funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion]
  congr 2 with r
  simpa only [mem_biUnion, mem_Iio, mem_Iic] using
    ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ {x ∈ antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅

Tactic:
rw [← map_swap_antidiagonal, filter_map]

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ map { toFun := Prod.swap, inj' := ⋯ }
      (filter ((fun x ↦ x.2 = m) ∘ ⇑{ toFun := Prod.swap, inj' := ⋯ }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some (if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) = n

Tactic:
if_neg (not_le.mpr hn)

Goal state after:
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some (pred^[(-n).toNat] hι.some) = n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
i : ι
⊢ (fun n ↦ succ^[n] ⊥) ((fun i ↦ (toZ ⊥ i).toNat) i) = i

Tactic:
by
    dsimp only
    exact iterate_succ_toZ i bot_le

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + k + j = n

Tactic:
add_right_comm,

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = n - k
⊢ l + j + k = n
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-1) ^ (n - m) = (-1) ^ (n + m)

Tactic:
rw [mem_range] at hm

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ (-1) ^ (n - m) = (-1) ^ (n + m)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, x - y} = span {x, y}

Tactic:
rw [← span_pair_sub_left, sub_sub_cancel_left, span_pair_neg]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m

Tactic:
rw [pow_succ, pow_mul, mul_comm]; rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
I J : (i : ι) → Ideal (R i)
le : pi I ≤ pi J
i : ι
r : R i
hr : r ∈ I i
⊢ r ∈ J i

Tactic:
by classical simpa using le (single_mem_pi hr) i

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico k (n + 1 + k)

Tactic:
add_right_comm,

Goal state after:
case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico k (n + k + 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b x y : R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
dif_neg ha

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b x y : R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ a * Classical.choose ⋯ = 1
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
x : (j : ι) → R j
⊢ x ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
induction x using Pi.single_induction with
  | zero => simp
  | add f g hf hg => exact Ideal.add_mem _ hf hg
  | single i r =>
      rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g : Filter α
s t : Set α
f : Filter (Filter α)
⊢ univ ∈ {s | {t | s ∈ t} ∈ f}

Tactic:
by simp only [mem_ofPred_eq, univ_mem, ofPred_true]

Goal state after:
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ ⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f

Tactic:
← sInter_range,

Goal state after:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ q (s ∩ t)

Tactic:
use inter_mem (mem_iInf_of_mem _ hs) ht.1

Goal state after:
case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := ⋯
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ ∀ (t' : Set α), s ∩ t ⊆ t' → p t'
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
⊢ ∀ {x y : Set β}, x ∈ kernImage m '' f.sets → x ⊆ y → y ∈ kernImage m '' f.sets

Tactic:
rintro _ t ⟨s, hs, rfl⟩ hst

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ t ∈ kernImage m '' f.sets
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_6
s : Set α
t : Set ↑s
⊢ 𝓟 t = 𝓟 (Subtype.val ⁻¹' Subtype.val '' t)

Tactic:
preimage_image_eq _ Subtype.coe_injective

Goal state after:
α : Type u_6
s : Set α
t : Set ↑s
⊢ 𝓟 t = 𝓟 t
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t

Tactic:
simp only [eventuallyLE_antisymm_iff, le_antisymm_iff, set_eventuallyLE_iff_inf_principal_le]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ (pure g).seq f

Tactic:
rw [← singleton_seq]
    apply seq_mem_seq _ hs
    exact singleton_mem_pure

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
⊢ (fun g ↦ g a) '' s ⊆ s.seq t

Tactic:
rintro b ⟨g, hg, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : Filter (α → β)
a : α
s : Set (α → β)
hs : s ∈ f
t : Set α
ht : t ∈ pure a
g : α → β
hg : g ∈ s
⊢ (fun g ↦ g a) g ∈ s.seq t
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : Semiring R
A : Type ?u.8
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
inst✝ : Module A β
e : α ≃+ β
⊢ ∀ (r s : A) (x : α), (r + s) • x = r • x + s • x

Tactic:
simp [Equiv.smul_def, add_smul]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : t'.Finite
⊢ (span R t').FG

Tactic:
have := h.exists_finset_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : t'.Finite
this : ∃ s', ↑s' = t'
⊢ (span R t').FG
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.FG
S : Finset G
hS : span ℤ ↑S = P
⊢ AddSubgroup.closure ↑S = P.toAddSubgroup

Tactic:
by simpa [← span_int_eq_addSubgroupClosure]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ WellFoundedGT (Submodule R M) ↔ WellFounded fun x1 x2 ↦ x1 > x2

Tactic:
← isWellFounded_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ WellFoundedGT (Submodule R M) ↔ IsWellFounded (Submodule R M) fun x1 x2 ↦ x1 > x2
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT { N // N.FG }

Tactic:
by
  let α := { N : Submodule R M // N.FG }
  constructor
  · intro H
    let f : α ↪o Submodule R M := OrderEmbedding.subtype _
    exact OrderEmbedding.wellFoundedLT f.dual
  · intro H
    constructor
    intro N
    obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ :=
      WellFounded.has_min H.wf { N' : α | N'.1 ≤ N } ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩
    convert! h₁
    refine (e.antisymm ?_).symm
    by_contra h₃
    obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
    apply hx₂
    rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]
    exact (le_sup_left : R ∙ x ≤ _) (Submodule.mem_span_singleton_self _)

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
by
  simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
by
  simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Goal state after: