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

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (n + m * k) ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (n + m * k) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.gcd (n + m * k) = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (n + m * k) = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (k * m + n) ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (k * m + n) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.gcd (k * m + n) = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (k * m + n) = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.Coprime (m * k + n) ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (m * k + n) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ m.gcd (m * k + n) = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ m.gcd (m * k + n) = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + k * n).Coprime n ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (m + k * n).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + k * n).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (m + k * n).gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + n * k).Coprime n ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (m + n * k).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + n * k).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (m + n * k).gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (k * n + m).Coprime n ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (k * n + m).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (k * n + m).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (k * n + m).gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (n * k + m).Coprime n ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (n * k + m).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (n * k + m).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n k : ℕ
⊢ (n * k + m).gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime m ↔ n.Coprime m

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd m = 1 ↔ n.Coprime m
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).gcd m = 1 ↔ n.Coprime m

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd m = 1 ↔ n.gcd m = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m.Coprime (n - m) ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ m.gcd (n - m) = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m.gcd (n - m) = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ m.gcd (n - m) = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).Coprime n ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd n = 1 ↔ m.Coprime n
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).gcd n = 1 ↔ m.Coprime n

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ n.Coprime (n - m) ↔ n.Coprime m

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ n.gcd (n - m) = 1 ↔ n.Coprime m
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ n.gcd (n - m) = 1 ↔ n.Coprime m

Tactic:
Coprime,

Goal state after:
m n : ℕ
h : m ≤ n
⊢ n.gcd (n - m) = 1 ↔ n.gcd m = 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inl
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n = 0
⊢ k / m * (m / n) = k / n

pp: case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k / m * (m / n) = k / n

Tactic:
· simp [hn]

Goal state after:
case inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ m
hn : n > 0
⊢ k / m * (m / n) = k / n
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m : ℕ
n : Fin m → ℕ
k : (i : Fin m) × Fin (n i)
⊢ ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd

Tactic:
by
  induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
  rcases k with ⟨⟨iv, hi⟩, j⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using! ih _
  · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
⊢ s.encard = k + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])
    refine ⟨a, s \ {a}, fun h ↦ h.2 rfl, by rwa [insert_sdiff_singleton, insert_eq_of_mem], ?_⟩
    rw [encard_sdiff_singleton_of_mem ha, h,
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).add_tsub_cancel_right]
  rintro ⟨a, t, h, rfl, rfl⟩
  rw [encard_insert_of_notMem h]

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

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr rfl)).2 rfl

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : t.encard = s.encard + 1
⊢ ∃ a, t = insert a s

Tactic:
← encard_sdiff_add_encard_of_subset h,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : (t \ s).encard + s.encard = s.encard + 1
⊢ ∃ a, t = insert a s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard = 0 ↔ s = ∅

Tactic:
← Nat.cast_inj (R := ℕ∞),

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ↑s.ncard = ↑0 ↔ s = ∅
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_3
inst✝ : Group H
K : Subgroup G
f : G →* H
hf : Function.Injective ⇑f
⊢ Nat.card ↥(map f K) = Nat.card ↥K

Tactic:
apply Nat.card_image_of_injective hf

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).ncard = s.ncard + 1

Tactic:
← Nat.cast_inj (R := ℕ∞),

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ ↑(insert a s).ncard = ↑(s.ncard + 1)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : b ∈ {a}
⊢ a ∈ s

Tactic:
← mem_singleton_iff.mp h

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : b ∈ {a}
⊢ b ∈ s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : s.Finite
⊢ InjOn f s

Tactic:
← Nat.cast_inj (R := ℕ∞),

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : ↑(f '' s).ncard = ↑s.ncard
hs : s.Finite
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact iff_of_true (by simp) (Or.inl rfl)
  rw [ncard_le_one_iff hs]
  refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩
  grind

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
⊢ ∀ (g₁ g₂ : G),
    ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).1 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).1 →
      ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).2 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).2

Tactic:
simp [hf]

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

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom ≤ ringConGen (r on ⇑f)

Tactic:
← comap_nonUnitalRingHomComp

Goal state after:
R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen (r on ⇑f)).comap (f.symm.toNonUnitalRingHom.comp f.toNonUnitalRingHom) ≤ ringConGen (r on ⇑f)
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ factor H ∘ₗ p.mkQ = p'.mkQ

Tactic:
by
  ext x
  rw [LinearMap.comp_apply, factor_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
R : Type u
M₂ : Type w
ι : Type x
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ (update f i b j) c = update (fun i ↦ (f i) c) i (b c) j

Tactic:
rw [update_of_ne h, update_of_ne h]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂✝ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommMonoid M✝
inst✝¹¹ : AddCommMonoid M₂✝
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ M₂✝
inst✝⁶ : Module R✝ M₃
inst✝⁵ : Module R✝ M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
x : M
⊢ ∃ a, (codRestrict f.range f ⋯ ∘ₗ C.subtype) a = ⟨f x, ⋯⟩

Tactic:
obtain ⟨y, z, hy, hz, rfl⟩ := codisjoint_iff_exists_add_eq.mp h.codisjoint x

Goal state after:
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂✝ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommMonoid M✝
inst✝¹¹ : AddCommMonoid M₂✝
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Module R✝ M₂✝
inst✝⁶ : Module R✝ M₃
inst✝⁵ : Module R✝ M₄
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M →ₗ[R] M₂
C : Submodule R M
h : IsCompl C f.ker
y z : M
hy : y ∈ C
hz : z ∈ f.ker
⊢ ∃ a, (codRestrict f.range f ⋯ ∘ₗ C.subtype) a = ⟨f (y + z), ⋯⟩
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x✝ y✝ : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x y : ↥(p.compatibleMaps q)
⊢ p.mapQ q ↑(x + y) ⋯ = p.mapQ q ↑x ⋯ + p.mapQ q ↑y ⋯

Tactic:
ext
    rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
r : R
x y : M
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
c : R
f : ↥(p.compatibleMaps q)
⊢ p.mapQ q ↑(c • f) ⋯ = (RingHom.id R) c • p.mapQ q ↑f ⋯

Tactic:
ext
    rfl

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝¹ : IsTrans α r
γ : Type u_3
inst✝ : Nonempty γ
f : γ → α
D : Directed r f
s : Set γ
hs : s.Finite
⊢ ∃ z, ∀ i ∈ s, r (f i) (f z)

Tactic:
by
  convert! D.finset_le hs.toFinset using 3; rw [Set.Finite.mem_toFinset]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by_cases h : BddAbove (Set.range f)

Goal state after:
case pos
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
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
⊢ ∀ (g₁ g₂ : G),
    ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₁).1 = ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₂).1 →
      ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₁).2 = ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₂).2

Tactic:
simp [hf]

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

Goal state before:
pp: ι : 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] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] j = i

Tactic:
rw [← hn_eq]

Goal state after:
ι : 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] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] (succ^[n] i) = i
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
by
  rw [← map_add_right_Ico, prod_map]
  rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
by
  rw [antidiagonal_succ, prod_cons, prod_map]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.succ.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
rw [choose_succ_succ, cast_add, mul_add]

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y ^ (n + 1)

Tactic:
_root_.pow_succ'

Goal state after:
case succ.e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * y ^ n
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ↑(Submonoid.powers a) → a_1 ∉ ↑I

Tactic:
rw [ha.coe_powers]
    rintro _ (rfl | rfl)
    exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]

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

Goal state before:
pp: α : Type u_1
B : FilterBasis α
⊢ B.filter = ⨅ s, 𝓟 ↑s

Tactic:
have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) := by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub
  ext U
  simp [mem_filter_iff, mem_iInf_of_directed this]

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

Goal state before:
pp: α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
hf : is.Subsingleton
⊢ ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f

Tactic:
by
  apply Subsingleton.induction_on hf <;> simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
simp only [Filter.Frequently, hl.eventually_iff]; push Not; rfl

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

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ atTop = generate (Ici '' s)

Tactic:
refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_

Goal state after:
α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
x : α
⊢ ∃ y ∈ s, x ≤ y
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico

Goal state after:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (toDual a₂) (toDual a₁)) (Ico (toDual b₂) (toDual b₁)) ↔
    min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ

Tactic:
rw [kernImage_compl, compl_eq_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
⊢ (p x → x ∈ f ⁻¹' s) → (¬p x → x ∈ g ⁻¹' s) → x ∈ (fun x ↦ if p x then f x else g x) ⁻¹' s

Tactic:
hp₀

Goal state after:
α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : ∀ s ∈ l₂, {x | x ∈ {x | p x} → x ∈ f ⁻¹' s} ∈ l₁
h₁ : ∀ s ∈ l₂, {x | x ∈ {x | ¬p x} → x ∈ g ⁻¹' s} ∈ l₁
s : Set β
hs : s ∈ l₂
x : α
hp₀ : p x → x ∈ f ⁻¹' s
⊢ (¬p x → x ∈ g ⁻¹' s) → x ∈ (fun x ↦ if p x then f x else g x) ⁻¹' s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ ((fun b a ↦ (a, b)) '' u).seq t ∈ (map Prod.mk f).seq g

Tactic:
← Set.prod_image_seq_comm

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ (Prod.mk '' t).seq u ∈ (map Prod.mk f).seq g
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
⊢ CommSemigroup α

Tactic:
let mul := e.mul
  apply e.injective.commSemigroup _; intros; exact e.apply_symm_apply _

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Div α
x y : Shrink.{v, u_2} α
⊢ (equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y

Tactic:
simp [Equiv.div_def]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Div α
x y : α
⊢ (equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y

Tactic:
simp [Equiv.div_def]

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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ atTop ≤ map f atTop

Tactic:
rw [(atTop_basis.map f).ge_iff]

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
⊢ ∀ (i' : α), True → f '' Ici i' ∈ atTop
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ C S

Tactic:
have : Finite S := Finite.to_subtype h

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this : Finite ↑S
⊢ C S
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

Tactic:
← f.apply_covBy_apply_iff

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : f b ⋖ f a
⊢ False
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case refine_1
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
this : ↑s ⊆ ↑(restrictScalars R S)
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S

Tactic:
rwa [restrictScalars_le, span_le]

Goal state after: