mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = (RingHom.id R) r • ∑ i, f i • v i

Tactic:
simp_rw [Finset.smul_sum, smul_smul]

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁶ : Fintype α
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
v : α → M
r : R
f : α → R
⊢ ∑ i, (r • f) i • v i = ∑ x, ((RingHom.id R) r * f x) • v x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ (b.reindex e).sumCoords x = b.sumCoords x

Tactic:
simp only [coe_sumCoords, repr_reindex]

Goal state after:
ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ ((mapDomain (⇑e) (b.repr x)).sum fun x ↦ id) = (b.repr x).sum fun x ↦ id
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R

Tactic:
refine .ofLinearMap (linearCombination _ fun j ↦ single j 1 + single i (c j))
    (linearCombination _ fun j ↦ single j 1 - single i (c j)) ?_ ?_

Goal state after:
case refine_1
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
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 + single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 - single i (c j)) =
    LinearMap.id

case refine_2
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
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ ((linearCombination R fun j ↦ single j 1 - single i (c j)) ∘ₗ
      linearCombination R fun j ↦ single j 1 + single i (c j)) =
    LinearMap.id
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j

Tactic:
lift s to Finset α using hs; lift t to Finset β using ht
  simp only [finprod_mem_coe_finset]
  exact Finset.prod_comm

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a ⟨n, h⟩ = cons a v ((finRotate (n + 1)) ⟨n, h⟩)

Tactic:
finRotate_last',

Goal state after:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a ⟨n, h⟩ = cons a v ⟨0, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (Equiv.symm (finRotate n)) i = i - 1

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero i.pos.ne'
  apply (finRotate n.succ).symm_apply_eq.mpr
  rw [finRotate_apply, sub_add_cancel]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.lapply i) (Finsupp.single i (f i))

Tactic:
rw [Finsupp.lapply_apply, Finsupp.single_eq_same]

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

Tactic:
apply_fun i at h

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i (i' x✝¹) = i (i' x✝)
⊢ x✝¹ = x✝
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ (k / m).lcm (k / n) = k / m.gcd n

Tactic:
Nat.lcm_eq_iff

Goal state after:
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
⊢ k / m ∣ k / m.gcd n ∧ k / n ∣ k / m.gcd n ∧ ∀ (c : ℕ), k / m ∣ c → k / n ∣ c → k / m.gcd n ∣ c
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ i, f i • v i - ∑ i, g i • v i = 0
i : ι
⊢ f i = g i

Tactic:
← sum_sub_distrib

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ x, (f x • v x - g x • v x) = 0
i : ι
⊢ f i = g i
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

Tactic:
apply_fun i at h

Goal state after:
case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i (i' x✝¹) = i (i' x✝)
⊢ x✝¹ = x✝
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ (insert x s).encard ≤ s.encard + 1

Tactic:
rw [← union_singleton, ← encard_singleton x]

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ (s ∪ {x}).encard ≤ s.encard + {x}.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (s \ {a}).encard + 1 = s.encard

Tactic:
← encard_insert_of_notMem (fun h ↦ h.2 rfl),

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a (s \ {a})).encard = s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Tactic:
← add_zero (encard _)

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Tactic:
nth_rw 1 [← add_zero (encard _)]

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ (rightRel (s.prod s')) x y ↔ (rightRel s) x.1 y.1 ∧ (rightRel s') x.2 y.2

Tactic:
rightRel_apply

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
β : Type u_2
inst✝ : Group β
s' : Subgroup β
x y : α × β
⊢ y * x⁻¹ ∈ s.prod s' ↔ y.1 * x.1⁻¹ ∈ s ∧ y.2 * x.2⁻¹ ∈ s'
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ a₁ = a₂

Tactic:
exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
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₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)

Tactic:
rw [← prodMap_comap_prod, Submodule.prod_bot]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Tactic:
by
  rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

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.1 = m} = if m ≤ n then {(m, n - m)} else ∅

Tactic:
by
  ext ⟨a, b⟩
  suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
    rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
  rintro rfl
  constructor
  · rintro rfl
    exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
  · rintro ⟨h, rfl⟩
    exact add_tsub_cancel_of_le h

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ (toZ ⊥ i).toNat, invFun := fun n ↦ succ^[n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by
    intro i j
    simp only [Equiv.coe_fn_mk, Int.toNat_le]
    rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * (x * y) + y * b ∈ I

Tactic:
refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ b ∈ I
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
rw [mul_comm, span_pair_add_left_mul]

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

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

Tactic:
span_pair_left_mul_add

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ x - y ∈ I

Tactic:
← eq_zero_iff_mem,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ (mk I) (x - y) = 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
ha : IsUnit a
⊢ span {a} = ⊤

Tactic:
rw [span_singleton_eq_top.2 ha]

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

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = span {p}

Tactic:
by
  rw [or_iff_not_imp_left, ← forall_congr' isPrime_iff_of_isPrincipalIdealRing,
    ← or_iff_not_imp_left, or_iff_right_of_imp]
  rintro rfl; exact isPrime_bot

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
⊢ (mapRange.linearMap f).range = submodule fun x ↦ f.range

Tactic:
by
  ext x
  constructor
  · rintro ⟨y, hy⟩
    simp [← hy]
  · intro hx
    choose y hy using hx
    refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
    constructor
    <;> contrapose
    <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

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

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

Tactic:
comap_principal,

Goal state after:
α : Type u_6
s : Set α
t : Set ↑s
⊢ 𝓟 t = 𝓟 (Subtype.val ⁻¹' Subtype.val '' t)
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
y : α
hys : y ∈ s
left✝ : a ≤ y
hyx : y < x
⊢ x ∈ ⋃ i ∈ s, Ici i
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g

Tactic:
by
  refine le_antisymm hφ (le_trans ?_ (map_mono hψ))
  rw [map_map, eq, map_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g = ⊥

Tactic:
apply le_bot_iff.mp
  trans map inl ⊤ ⊓ map inr ⊤
  · apply inf_le_inf <;> simp
  · simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
a : α
⊢ f ≤ 𝓟 {a} ↔ {a} ∈ f

Tactic:
le_principal_iff

Goal state after:
α : Type u_1
f : Filter α
a : α
⊢ {a} ∈ f ↔ {a} ∈ f
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ atTop ≤ comap f (𝓟 s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s

Tactic:
comap_principal,

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
f : α → β
s : Set β
⊢ atTop ≤ 𝓟 (f ⁻¹' s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
⊢ map Subtype.val atTop = atTop

Tactic:
by
  choose f hl hr using exists_ge_ge (α := α)
  have : DirectedOn (· ≤ ·) s := fun x _ y _ ↦
    ⟨f a (f x y), h <| hl _ _, (hl x y).trans (hr _ _), (hr x y).trans (hr _ _)⟩
  have : IsDirectedOrder s := by
    rw [directedOn_iff_directed] at this
    rwa [IsDirectedOrder, ← directed_id_iff]
  refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_
  exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]

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
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
N : Submodule R M
hs : N.FG
t : Set M
ht : t.Finite
span_t : span R t = N
⊢ span S (⇑f '' t) = Submodule.map f N

Tactic:
rw [span_image, span_t]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Tactic:
· simp [← hb]

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
s : { s // IsCofinal s }
hs : (fun s ↦ #↑↑s) s = ⨅ s, #↑↑s
⊢ ∃ s, IsCofinal s ∧ #↑s = cof α

Tactic:
exact ⟨s.1, s.2, 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
s : Submodule R M
⊢ s.FG ↔ IsCompactElement s

Tactic:
by
  -- Introduce shorthand for span of an element
  let sp : M → Submodule R M := fun a => span R {a}
  -- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
  have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
  constructor
  · rintro ⟨t, rfl⟩
    rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← t.sup_eq_iSup sp]
    apply CompleteLattice.isCompactElement_finsetSup
    exact fun n _ => singleton_span_isCompactElement n
  · intro h
    rw [CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup] at h
    -- s is the Sup of the spans of its elements.
    have sSup' : s = sSup (sp '' ↑s) := by
      rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
    -- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
    obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
    have ssup : s = u.sup id := by
      suffices u.sup id ≤ s from le_antisymm husup this
      rw [sSup', Finset.sup_id_eq_sSup]
      exact sSup_le_sSup huspan
    obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
    rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw,
      ← span_eq_iSup_of_singleton_spans, eq_comm] at ssup
    exact ⟨t, ssup⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ familyOfBFamily' r ho f ((enum r) ⟨i, ⋯⟩) = f i hi

Tactic:
by
  simp only [familyOfBFamily', typein_enum]

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
by
  induction a, b using inductionOn₂ with | _ α _ β _
  simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]

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

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

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

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
rw [not_bddAbove_iff] at hs
  obtain ⟨a, ha⟩ := bddAbove_of_small (s := enumOrd s '' Iio o)
  obtain ⟨b, hb, hba⟩ := hs a
  exact ⟨b, hb, fun c hc ↦ (ha (mem_image_of_mem _ hc)).trans_lt hba⟩

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

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h✝ : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a

Tactic:
grind [asymm_of s]

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
by
    have := type_ne_zero_iff_nonempty.1 h
    rw [← iSup'_eq_bsup r, Order.IsNormal.map_iSup H bddAbove_of_small, ← iSup'_eq_bsup r] <;>
      rfl

Goal state after: