mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
L L' : Submodule R M
s : S
hr : IsSMulRegular M s
h✝ : ∀ x ∈ L, s • x ∈ L'
x✝¹ x✝ : ↥L
h : (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝¹ = (LinearMap.restrict ((Algebra.lsmul S R M) s) h✝) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using hr (Subtype.ext_iff.mp h)

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

Tactic:
convert! h s f 0

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) ↔ ∑ i ∈ s, f i • v i = ∑ i ∈ s, 0 i • v i → ∀ i ∈ s, f i = 0 i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ s.encard = 2

Tactic:
rw [hs, encard_pair hne]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = s.ncard

Tactic:
ncard_eq_toFinset_card',

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = s.toFinset.card
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:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).encard = s.encard
hs : s.Finite
⊢ InjOn f s
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}

Tactic:
ncard_eq_toFinset_card',

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : s.toFinset.card = 1
⊢ ∃ a, s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
    Finite.toFinset_subset, Finset.coe_singleton]

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

Goal state before:
pp: case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
rw [f.injective (fa.trans fb.symm)]

Goal state after:
case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) b b
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).comap f ≤ ((ringConGen (r on ⇑f)).comap f.symm.toNonUnitalRingHom).comap f.toNonUnitalRingHom

Tactic:
apply comap_mono
    grw [← le_comap_ringConGen]
    gcongr
    simp [Function.onFun, RingEquiv.coe_toNonUnitalRingHom']

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ ∃ y_1, g y_1 = f y

Tactic:
use -z

Goal state after:
case h
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : f y + g z = 0
⊢ g (-z) = f y
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ≤ succFn i

Tactic:
le_isGLB_iff (succFn_spec i),

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ i ∈ lowerBounds (Set.Ioi i)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0

Tactic:
· by_contra h
    have h_eq := iterate_pred_toZ i hi
    rw [← h_eq, h] at hi
    simp only [neg_zero, Int.toNat_zero, Function.iterate_zero, id, lt_self_iff_false] at hi

Goal state after:
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 (c + x) = ∏ x ∈ Ico (a + c) (b + c), f x

Tactic:
convert! prod_Ico_add' f a b c using 2

Goal state after:
case a
α : 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✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
suffices IsMin (pred^[n.succ] i0) from absurd this hn
    exact isMin_iterate_pred_of_eq_of_ne h_eq.symm (Ne.symm hmn)

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

Goal state before:
pp: n : ℕ
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!

Tactic:
prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n,

Goal state after:
n : ℕ
⊢ (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1)!
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ 1 ∈ ⊤

Tactic:
trivial

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 : ℕ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * n.choose m

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)
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * ↑(n.choose m)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
rcases mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ span {a * x} = span {x}

Tactic:
span_singleton_mul_left_unit h2

Goal state after:
α : Type u
inst✝ : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ span {x} = span {x}
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
← span_pair_add_right_mul,

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - y * z + y * ?z, y} = span {x, y}

case z
α : Type u
inst✝ : CommRing α
x y z : α
⊢ α
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n m : ℕ
⊢ ∑ k ∈ range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)

Tactic:
induction m with

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

pp: case neg
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c < n + 1
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
· refine ⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) *
      ((Multiset.card s + 1) * n + 1).choose c, 0, Submodule.zero_mem _, ?_⟩
    rw [mul_comm _ (a ^ (n + 1))]
    simp_rw [← mul_assoc]
    rw [← pow_add, add_zero, add_tsub_cancel_of_le h]

Goal state after:
case neg
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c < n + 1
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤

Tactic:
trivial

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
⊢ f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K

Tactic:
induction m with

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
⊢ l.HasBasis p' s'

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩
  rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩
  rcases h i hi with ⟨i', hi', hs's⟩
  exact ⟨i', hi', hs's.trans ht⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
⊢ (mapRange.linearMap f) { support := x.support, toFun := y, mem_support_toFun := ⋯ } = x

Tactic:
by ext; simp_all

Goal state after:
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
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
s t : Set α
hqs : q s
hqt : q t
𝓕 : Filter α := { sets := {s | ∀ (t : Set α), q t → q (s ∩ t)}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
⊢ q (s ∩ t)

Tactic:
exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

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

Tactic:
by
  simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Tactic:
rw [Tendsto, Tendsto, map_congr hl]

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

Goal state before:
pp: α : Type u
s t x✝ : Set α
⊢ x✝ ∈ 𝓟 s \ 𝓟 t ↔ x✝ ∈ 𝓟 (s \ t)

Tactic:
by simp [← le_principal_iff, principal_mono]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter γ
m₁ : α → γ
m₂ : β → γ
s : Set (α ⊕ β)
⊢ (Sum.elim m₁ m₂ '' sᶜ)ᶜ ∈ l ↔ (m₁ '' (inl ⁻¹' s)ᶜ)ᶜ ∈ l ∧ (m₂ '' (inr ⁻¹' s)ᶜ)ᶜ ∈ l

Tactic:
simp [image_sumElim]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : Filter β
hα : Nonempty α
⊢ (comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot

Tactic:
· simp [comap_neBot_iff_frequently, hα]

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

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
H : ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
hp : ∀ᶠ (x : α) in f, ¬(fun x ↦ p x) x
⊢ False

Tactic:
simpa only [and_not_self_iff, exists_false] using H hp

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : ∅.Finite
⊢ ∃ a, ∀ b ∈ ∅, f a ≤ f b

pp: case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
· exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩

Goal state after:
case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : AddSubmonoid.closure ↑S = P.toAddSubmonoid
⊢ span ℕ ↑S = P

Tactic:
simpa [← span_nat_eq_addSubmonoidClosure] using hS

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]; exact le_sup_left

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsCofinal {t}
⊢ ∃ x, IsTop x

Tactic:
use t

Goal state after:
case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsCofinal {t}
⊢ IsTop t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ Nonempty α

Tactic:
use t

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
singleton : ∀ (x : M), motive (R ∙ x) ⋯
sup : ∀ (N₁ N₂ : Submodule R M) (hN₁ : N₁.FG) (hN₂ : N₂.FG), motive N₁ hN₁ → motive N₂ hN₂ → motive (N₁ ⊔ N₂) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯

Tactic:
induction s using Finset.induction with
  | empty => simpa using singleton 0
  | insert x s hxs ih =>
    simpa [span_insert, sup_comm] using
      sup (span R s) (R ∙ x) _ (fg_span_singleton _) ih (singleton x)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
rw [le_lift_cof_iff]
  exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R ↑t = S
⊢ (span A ↑S).FG

Tactic:
use t

Goal state after:
case h
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type u_3
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R ↑t = S
⊢ span A ↑t = span A ↑S
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : CompleteLattice α
⊢ DirSupClosedOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s

Tactic:
by
  simp [DirSupClosedOn, isLUB_iff_sSup_eq]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
s : Set Ordinal.{u_2}
hs : Cardinal.lift.{u_2 + 1, u_2 + 1} #↑s < Cardinal.univ.{u_2, u_2 + 1}
⊢ ¬IsCofinal s

Tactic:
← small_iff_lift_mk_lt_univ

Goal state after:
α : Type u_1
s : Set Ordinal.{u_2}
hs : Small.{u_2, u_2 + 1} ↑s
⊢ ¬IsCofinal s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c

Tactic:
rwa [sub_lt_of_le hba]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ a * b

Tactic:
by
  convert! mul_le_mul_right (one_le_iff_pos.2 hb) a
  rw [mul_one a]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ o.card < ℵ₀

Tactic:
← typein_enum _ ho

Goal state after:
o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ ((typein fun x1 x2 ↦ x1 < x2).toRelEmbedding ((enum fun x1 x2 ↦ x1 < x2) ⟨o, ho⟩)).card < ℵ₀
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = b / c

Tactic:
by
  convert! mul_add_div_mul (pos_iff_ne_zero.2 ha) b c using 1
  rw [add_zero]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
rw [opow_of_ne_zero h, opow_of_ne_zero h]

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ (limitRecOn (b + 1) 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) =
    (limitRecOn b 1 (fun x x_1 ↦ x_1 * a) fun o x f ↦ ⨆ x, f ↑x ⋯) * a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n

Tactic:
by
  rw [div_lt_iff_lt_mul (by lia), ← succ_le_iff, ← pred_eq_sub_one,
    succ_pred_eq_of_pos (by lia)]
  exact Nat.add_le_mul hn hb

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
← add_left_cancel_iff (a := ↑n),

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑n + ↑(m - n) = ↑n + (↑m - ↑n)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ (∀ a < o, op a a < o) → IsPrincipal op o

Tactic:
intro H a b ha hb

Goal state after:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
⊢ op a b < o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mp
a✝ b✝ : Ordinal.{u_1}
hb✝ : b✝ ≠ 0
a b : Ordinal.{u_1}
hb : b < b✝
m : ℕ
hm : a < ω ^ b * ↑m
n : ℕ
hn : a✝ < ω ^ a * ↑n
⊢ ∃ c < b✝, ∃ n, a✝ < ω ^ (ω ^ c * ↑n)

Tactic:
exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∃ o, derivFamily (fun x ↦ f) o = a

Tactic:
rw [← le_iff_derivFamily fun _ : Unit => H]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0

Tactic:
exact eq_comm

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

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
⊢ (typein s).toRelEmbedding p < typeLT α

Tactic:
obtain ⟨q, hq'⟩ := exists_gt (g p)

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ (typein s).toRelEmbedding p < typeLT α
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preBeth o = ℶ_ o

Tactic:
rw [beth, add_of_omega0_opow_le _ ho]

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
o : Ordinal.{u}
⊢ 1 ≤ (succ o).cof.ord

Tactic:
rw [cof_succ, ord_one]

Goal state after: