mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ InjOn g' sᶜ

Tactic:
intro x

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
⊢ x ∈ sᶜ → ∀ ⦃x₂ : α⦄, x₂ ∈ sᶜ → g' x = g' x₂ → x = x₂
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
⊢ Monotone fun x ↦ (f x) (g x)

Tactic:
intro x

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
x : α
⊢ ∀ ⦃b : α⦄, x ≤ b → (fun x ↦ (f x) (g x)) x ≤ (fun x ↦ (f x) (g x)) b
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
⊢ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y

Tactic:
intro x

Goal state after:
case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
⊢ x ∈ s → ∀ y ∉ s, f x ≠ g' y
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux = ↑n ↔ x = ↑n

Tactic:
simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g

Tactic:
intro x

Goal state after:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x : R
⊢ ∀ ⦃a₂ : R⦄, (fun x ↦ g • x) x = (fun x ↦ g • x) a₂ → x = a₂
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀

Tactic:
succ_natCast,

Goal state after:
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑n + 1 < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑s

Tactic:
by
  convert! mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1 <;> rw [lift_id]

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

Goal state before:
pp: α : Type u
⊢ 2 ≤ #α ↔ ∃ x y, x ≠ y

Tactic:
by
  rw [two_le_iff_one_lt, one_lt_iff_nontrivial, nontrivial_iff]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module S M₃
σ✝ : R →+* S
σ : R →+* R
inst✝ : RingHomId σ
r : R
x : M
⊢ r • x = σ r • x

Tactic:
by
    have := (RingHomId.eq_id : σ = _)
    subst this
    rfl

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M
inst✝ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
f : M →ₛₗ[σ₁₂] M₂
⊢ ⇑f = 0 ↔ f = 0

Tactic:
by
  aesop

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M✝ : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝³ : Semiring R
inst✝² : Semiring S
ι : Type u_14
M : ι → Type u_15
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i j : ι
h : i = j
x✝¹ : R
x✝ : M i
⊢ (AddEquiv.cast h).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (AddEquiv.cast h).toFun x✝

Tactic:
by cases h; rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
⊢ Function.RightInverse
    (fun _insts ↦
      have this := ⋯;
      prodOfSMulCommClass M N α)
    fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩

Tactic:
rintro ⟨_, x, _⟩

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ (fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
      ((fun _insts ↦
          have this := ⋯;
          prodOfSMulCommClass M N α)
        ⟨fst✝, ⟨x, snd✝⟩⟩) =
    ⟨fst✝, ⟨x, snd✝⟩⟩
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m

Tactic:
rw [← val_image_orbit, Subtype.val_injective.preimage_image]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ (N.subtype ∘ₗ g ^ k) m = 0

Tactic:
← Module.End.commute_pow_left_of_commute h,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ ((G ^ k) ∘ₗ N.subtype) m = 0
Module: Mathlib.Algebra.Module.Submodule.RestrictScalars

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s t : Submodule R M
⊢ restrictScalars S (s ⊔ t) = restrictScalars S s ⊔ restrictScalars S t

Tactic:
by
  simpa [Set.image_insert_eq] using restrictScalars_sSup S (s := {s, t})

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective ⇑f
⊢ f.ker ≤ ⊥

Tactic:
intro x

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective ⇑f
x : M
⊢ x ∈ f.ker → x ∈ ⊥
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
⊢ C x₁ hx₁

Tactic:
refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
  refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
  · exact ⟨_, mem _ _ hx₂⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
Set.insert_eq,

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
n : ℕ
s : Set R
⊢ closure ({↑n} ∪ s) = closure s
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure (insert (↑n) s) = closure s

Tactic:
Set.insert_eq,

Goal state after:
R : Type u
inst✝ : NonAssocRing R
n : ℤ
s : Set R
⊢ closure ({↑n} ∪ s) = closure s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a * (c * d) = a * 1

Tactic:
rw [← mul_assoc, ← a_eq, mul_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c * (d * c) = a * c * 1

Tactic:
rw [← mul_assoc, ← a_eq, mul_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀

Tactic:
intro x

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
⊢ x * a = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ b ∈ nonZeroDivisorsRight M₀

Tactic:
intro x

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
⊢ x * b = 0 → x = 0
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
intro x

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
⊢ x ∈ comap f (map f s) → x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y

Tactic:
exact h _ _ <| .refl _

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Set.range ⇑f = Set.univ ↔ Surjective ⇑f

Tactic:
Set.range_eq_univ

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective ⇑f ↔ Surjective ⇑f
Module: Mathlib.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A₁
inst✝¹² : Semiring A₂
inst✝¹¹ : Semiring A₃
inst✝¹⁰ : Semiring A₁'
inst✝⁹ : Semiring A₂'
inst✝⁸ : Semiring A₃'
inst✝⁷ : Algebra R A₁
inst✝⁶ : Algebra R A₂
inst✝⁵ : Algebra R A₃
inst✝⁴ : Algebra R A₁'
inst✝³ : Algebra R A₂'
inst✝² : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
ι : Type u_1
A : ι → Type u_2
inst✝¹ : (i : ι) → Semiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
i j : ι
h : i = j
x✝ : R
⊢ (RingEquiv.cast h).toFun ((algebraMap R (A i)) x✝) = (algebraMap R (A j)) x✝

Tactic:
by cases h; rfl

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
x : A₁ ≃ₐ[R] A₁
y z : A₁ˣ
⊢ x • (y * z) = x • y * x • z

Tactic:
ext; exact map_mul x _ _

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p' : Submodule R ↥p
⊢ Injective ⇑p.subtype

Tactic:
exact Subtype.val_injective

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Codisjoint ⟨a ⊓ b, ⋯⟩ ⟨a ⊓ c, ⋯⟩

Tactic:
simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]

Goal state after:
case codisjoint
α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ (b ⊓ a ⊔ c) ⊓ a = a
Module: Mathlib.Order.SupClosed

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
⊢ SupClosed (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊔ f b ∈ ⇑f '' s
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ⊔ p') ↔ ∀ (m : M), ∃ u ∈ p, ∃ v ∈ p', m = u + v

Tactic:
refine forall_congr' fun m ↦ ?_

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
m : M
⊢ m ∈ p ⊔ p' ↔ ∃ u ∈ p, ∃ v ∈ p', m = u + v
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
⊢ x ≤ y

Tactic:
have : x ⊓ yᶜ = ⊥ := of_not_not fun hbot =>
    have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
    have ⟨hx, hy'⟩ := le_inf_iff.1 hle
    have hy := h a ha hx
    have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
    ha.1 (by simpa using this)

Goal state after:
α : Type u_4
inst✝¹ : BooleanAlgebra α
inst✝ : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
this : x ⊓ yᶜ = ⊥
⊢ x ≤ y
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤

Tactic:
obtain ⟨a, b, h⟩ := exists_pair_ne α

Goal state after:
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥

Tactic:
by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
hs'

Goal state after:
case mp
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ k ≤ sSup s → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x

Tactic:
hs'

Goal state after:
case mpr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ IsLUB s u → k ≤ u → ∃ x ∈ s, k ≤ x
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f ↔ (s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')) ∧ t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')

Tactic:
classical
  refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
  · suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]
  · suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
⊢ s ⊆ S

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : α
⊢ x ∈ s → x ∈ S
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : Disjoint (t j) (t j)
⊢ t j = ⊥

Tactic:
disjoint_self

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
i : ι
a✝ : i ∈ {i | t i ≠ ⊥}
j : ι
hj : t j ≠ ⊥
h : t i = t j
contra : i ≠ j
this : t j ≤ ⨆ k, ⨆ (_ : k ≠ i), t k
ht : t j = ⊥
⊢ t j = ⊥
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t

Tactic:
exact Subset.trans h1 h2

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
x : α
⊢ x ∈ mulSupport (s.mulIndicator f) ↔ x ∈ s ∩ mulSupport f

Tactic:
simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∀ b ∈ t, b ≤ sSup s

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
x : α
⊢ x ∈ t → x ≤ sSup s
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: R : Type u
A : Type w
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hsur : Function.Surjective ⇑(algebraMap R A)
X : Set M
⊢ restrictScalars R (span A X) = span R X

Tactic:
by
  refine ((span_le_restrictScalars R A X).antisymm fun m hm => ?_).symm
  refine span_induction subset_span (zero_mem _) (fun _ _ _ _ => add_mem) (fun a m _ hm => ?_) hm
  obtain ⟨r, rfl⟩ := hsur a
  simpa [algebraMap_smul] using smul_mem _ r hm

Goal state after: